Proof help

Stream: maths

[duck]

Hi everybody, I have this statement

example {n : ℕ} (h: 2 < n): n ! < n^n - n := by sorry

that seems easy to prove on paper but formalizing it seems tricky and I’m not sure I can do it with induction

[Daniel Weber]

What is your paper proof?

[Daniel Weber]

You can say n ^ n - n = n (n-1) n^(n-2) and n! = n (n - 1) (n - 2)!, and then you can get the result from (n-2)! ≤ (n-2)^(n-2) ≤ n^(n-2)

[duck]

Ah but n^n - n is not n (n - 1) n^(n-2)

[duck]

But I think I’ve got it thanks so much

[duck]

Actually on second thought maybe not

[Daniel Weber]

duck said:

Ah but n^n - n is not n (n - 1) n^(n-2)

Of course, apologies. You can do $n^n - n \ge n^n - n^{n-1} = n (n-1) n^{n-2}$ though

[duck]

That does the trick. Thank you so much