Metamath Proof Explorer

Theorem faclbnd

Description: A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005)

Ref Expression
Assertion faclbnd ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
2 oveq1 ⊢ ( 𝑗 = 0 → ( 𝑗 + 1 ) = ( 0 + 1 ) )
3 2 oveq2d ⊢ ( 𝑗 = 0 → ( 𝑀 ↑ ( 𝑗 + 1 ) ) = ( 𝑀 ↑ ( 0 + 1 ) ) )
4 fveq2 ⊢ ( 𝑗 = 0 → ( ! ‘ 𝑗 ) = ( ! ‘ 0 ) )
5 4 oveq2d ⊢ ( 𝑗 = 0 → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) = ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 0 ) ) )
6 3 5 breq12d ⊢ ( 𝑗 = 0 → ( ( 𝑀 ↑ ( 𝑗 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) ↔ ( 𝑀 ↑ ( 0 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 0 ) ) ) )
7 6 imbi2d ⊢ ( 𝑗 = 0 → ( ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 𝑗 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) ) ↔ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 0 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 0 ) ) ) ) )
8 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 + 1 ) = ( 𝑘 + 1 ) )
9 8 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑀 ↑ ( 𝑗 + 1 ) ) = ( 𝑀 ↑ ( 𝑘 + 1 ) ) )
10 fveq2 ⊢ ( 𝑗 = 𝑘 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑘 ) )
11 10 oveq2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) = ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) )
12 9 11 breq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑀 ↑ ( 𝑗 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) ↔ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) )
13 12 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 𝑗 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) ) ↔ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ) )
14 oveq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑘 + 1 ) + 1 ) )
15 14 oveq2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑀 ↑ ( 𝑗 + 1 ) ) = ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) )
16 fveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ! ‘ 𝑗 ) = ( ! ‘ ( 𝑘 + 1 ) ) )
17 16 oveq2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) = ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) )
18 15 17 breq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑀 ↑ ( 𝑗 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) ↔ ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) )
19 18 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 𝑗 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) ) ↔ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) )
20 oveq1 ⊢ ( 𝑗 = 𝑁 → ( 𝑗 + 1 ) = ( 𝑁 + 1 ) )
21 20 oveq2d ⊢ ( 𝑗 = 𝑁 → ( 𝑀 ↑ ( 𝑗 + 1 ) ) = ( 𝑀 ↑ ( 𝑁 + 1 ) ) )
22 fveq2 ⊢ ( 𝑗 = 𝑁 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑁 ) )
23 22 oveq2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) = ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )
24 21 23 breq12d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑀 ↑ ( 𝑗 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) ↔ ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) )
25 24 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 𝑗 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑗 ) ) ) ↔ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) ) )
26 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
27 nnge1 ⊢ ( 𝑀 ∈ ℕ → 1 ≤ 𝑀 )
28 elnnuz ⊢ ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
29 28 biimpi ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
30 26 27 29 leexp2ad ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ 1 ) ≤ ( 𝑀 ↑ 𝑀 ) )
31 0p1e1 ⊢ ( 0 + 1 ) = 1
32 31 oveq2i ⊢ ( 𝑀 ↑ ( 0 + 1 ) ) = ( 𝑀 ↑ 1 )
33 32 a1i ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 0 + 1 ) ) = ( 𝑀 ↑ 1 ) )
34 fac0 ⊢ ( ! ‘ 0 ) = 1
35 34 oveq2i ⊢ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 0 ) ) = ( ( 𝑀 ↑ 𝑀 ) · 1 )
36 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
37 26 36 reexpcld ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ 𝑀 ) ∈ ℝ )
38 37 recnd ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ 𝑀 ) ∈ ℂ )
39 38 mulid1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑀 ↑ 𝑀 ) · 1 ) = ( 𝑀 ↑ 𝑀 ) )
40 35 39 eqtrid ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 0 ) ) = ( 𝑀 ↑ 𝑀 ) )
41 30 33 40 3brtr4d ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 0 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 0 ) ) )
42 26 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → 𝑀 ∈ ℝ )
43 simpllr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
44 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
45 43 44 syl ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
46 42 45 reexpcld ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( 𝑀 ↑ ( 𝑘 + 1 ) ) ∈ ℝ )
47 36 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → 𝑀 ∈ ℕ0 )
48 42 47 reexpcld ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( 𝑀 ↑ 𝑀 ) ∈ ℝ )
49 43 faccld ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
50 49 nnred ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( ! ‘ 𝑘 ) ∈ ℝ )
51 48 50 remulcld ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ∈ ℝ )
52 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
53 peano2re ⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ )
54 43 52 53 3syl ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℝ )
55 nngt0 ⊢ ( 𝑀 ∈ ℕ → 0 < 𝑀 )
56 55 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → 0 < 𝑀 )
57 0re ⊢ 0 ∈ ℝ
58 ltle ⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 0 < 𝑀 → 0 ≤ 𝑀 ) )
59 57 58 mpan ⊢ ( 𝑀 ∈ ℝ → ( 0 < 𝑀 → 0 ≤ 𝑀 ) )
60 42 56 59 sylc ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → 0 ≤ 𝑀 )
61 42 45 60 expge0d ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → 0 ≤ ( 𝑀 ↑ ( 𝑘 + 1 ) ) )
62 simplr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) )
63 simprr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → 𝑀 ≤ ( 𝑘 + 1 ) )
64 46 51 42 54 61 60 62 63 lemul12ad ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) ∧ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) · 𝑀 ) ≤ ( ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) )
65 64 anandis ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) · 𝑀 ) ≤ ( ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) )
66 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
67 expp1 ⊢ ( ( 𝑀 ∈ ℂ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) = ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) · 𝑀 ) )
68 66 44 67 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) = ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) · 𝑀 ) )
69 68 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) = ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) · 𝑀 ) )
70 facp1 ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
71 70 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
72 71 oveq2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑀 ↑ 𝑀 ) · ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ) )
73 38 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑀 ) ∈ ℂ )
74 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
75 74 nncnd ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℂ )
76 75 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℂ )
77 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
78 peano2cn ⊢ ( 𝑘 ∈ ℂ → ( 𝑘 + 1 ) ∈ ℂ )
79 77 78 syl ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℂ )
80 79 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℂ )
81 73 76 80 mulassd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) = ( ( 𝑀 ↑ 𝑀 ) · ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ) )
82 72 81 eqtr4d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) )
83 82 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) · ( 𝑘 + 1 ) ) )
84 65 69 83 3brtr4d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) )
85 84 exp32 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) → ( 𝑀 ≤ ( 𝑘 + 1 ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) )
86 85 com23 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ≤ ( 𝑘 + 1 ) → ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) )
87 nn0ltp1le ⊢ ( ( ( 𝑘 + 1 ) ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) < 𝑀 ↔ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) )
88 44 36 87 syl2anr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) < 𝑀 ↔ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) )
89 peano2nn0 ⊢ ( ( 𝑘 + 1 ) ∈ ℕ0 → ( ( 𝑘 + 1 ) + 1 ) ∈ ℕ0 )
90 44 89 syl ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑘 + 1 ) + 1 ) ∈ ℕ0 )
91 reexpcl ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( 𝑘 + 1 ) + 1 ) ∈ ℕ0 ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ∈ ℝ )
92 26 90 91 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ∈ ℝ )
93 92 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ∈ ℝ )
94 37 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( 𝑀 ↑ 𝑀 ) ∈ ℝ )
95 44 faccld ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
96 95 nnred ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
97 remulcl ⊢ ( ( ( 𝑀 ↑ 𝑀 ) ∈ ℝ ∧ ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
98 37 96 97 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
99 98 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
100 26 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → 𝑀 ∈ ℝ )
101 27 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → 1 ≤ 𝑀 )
102 simpr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 )
103 90 ad2antlr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( ( 𝑘 + 1 ) + 1 ) ∈ ℕ0 )
104 103 nn0zd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( ( 𝑘 + 1 ) + 1 ) ∈ ℤ )
105 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
106 105 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → 𝑀 ∈ ℤ )
107 eluz ⊢ ( ( ( ( 𝑘 + 1 ) + 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ∈ ( ℤ≥ ‘ ( ( 𝑘 + 1 ) + 1 ) ) ↔ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) )
108 104 106 107 syl2anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( 𝑀 ∈ ( ℤ≥ ‘ ( ( 𝑘 + 1 ) + 1 ) ) ↔ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) )
109 102 108 mpbird ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ ( ( 𝑘 + 1 ) + 1 ) ) )
110 100 101 109 leexp2ad ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( 𝑀 ↑ 𝑀 ) )
111 37 96 anim12i ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 ↑ 𝑀 ) ∈ ℝ ∧ ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) )
112 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
113 id ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℕ0 )
114 nn0ge0 ⊢ ( 𝑀 ∈ ℕ0 → 0 ≤ 𝑀 )
115 112 113 114 expge0d ⊢ ( 𝑀 ∈ ℕ0 → 0 ≤ ( 𝑀 ↑ 𝑀 ) )
116 36 115 syl ⊢ ( 𝑀 ∈ ℕ → 0 ≤ ( 𝑀 ↑ 𝑀 ) )
117 95 nnge1d ⊢ ( 𝑘 ∈ ℕ0 → 1 ≤ ( ! ‘ ( 𝑘 + 1 ) ) )
118 116 117 anim12i ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 0 ≤ ( 𝑀 ↑ 𝑀 ) ∧ 1 ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) )
119 lemulge11 ⊢ ( ( ( ( 𝑀 ↑ 𝑀 ) ∈ ℝ ∧ ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) ∧ ( 0 ≤ ( 𝑀 ↑ 𝑀 ) ∧ 1 ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) → ( 𝑀 ↑ 𝑀 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) )
120 111 118 119 syl2anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑀 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) )
121 120 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( 𝑀 ↑ 𝑀 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) )
122 93 94 99 110 121 letrd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) )
123 122 ex ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) + 1 ) ≤ 𝑀 → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) )
124 88 123 sylbid ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) < 𝑀 → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) )
125 124 a1dd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) < 𝑀 → ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) )
126 52 53 syl ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℝ )
127 lelttric ⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( 𝑀 ≤ ( 𝑘 + 1 ) ∨ ( 𝑘 + 1 ) < 𝑀 ) )
128 26 126 127 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ≤ ( 𝑘 + 1 ) ∨ ( 𝑘 + 1 ) < 𝑀 ) )
129 86 125 128 mpjaod ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) )
130 129 expcom ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑀 ∈ ℕ → ( ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) )
131 130 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 𝑘 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑘 ) ) ) → ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( ( 𝑘 + 1 ) + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) )
132 7 13 19 25 41 131 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 ∈ ℕ → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) )
133 132 impcom ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )
134 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
135 134 nnnn0d ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ0 )
136 135 nn0ge0d ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ ( ! ‘ 𝑁 ) )
137 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
138 137 0expd ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ↑ ( 𝑁 + 1 ) ) = 0 )
139 0exp0e1 ⊢ ( 0 ↑ 0 ) = 1
140 139 oveq1i ⊢ ( ( 0 ↑ 0 ) · ( ! ‘ 𝑁 ) ) = ( 1 · ( ! ‘ 𝑁 ) )
141 134 nncnd ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℂ )
142 141 mulid2d ⊢ ( 𝑁 ∈ ℕ0 → ( 1 · ( ! ‘ 𝑁 ) ) = ( ! ‘ 𝑁 ) )
143 140 142 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( 0 ↑ 0 ) · ( ! ‘ 𝑁 ) ) = ( ! ‘ 𝑁 ) )
144 136 138 143 3brtr4d ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 0 ↑ 0 ) · ( ! ‘ 𝑁 ) ) )
145 oveq1 ⊢ ( 𝑀 = 0 → ( 𝑀 ↑ ( 𝑁 + 1 ) ) = ( 0 ↑ ( 𝑁 + 1 ) ) )
146 oveq12 ⊢ ( ( 𝑀 = 0 ∧ 𝑀 = 0 ) → ( 𝑀 ↑ 𝑀 ) = ( 0 ↑ 0 ) )
147 146 anidms ⊢ ( 𝑀 = 0 → ( 𝑀 ↑ 𝑀 ) = ( 0 ↑ 0 ) )
148 147 oveq1d ⊢ ( 𝑀 = 0 → ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) = ( ( 0 ↑ 0 ) · ( ! ‘ 𝑁 ) ) )
149 145 148 breq12d ⊢ ( 𝑀 = 0 → ( ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ↔ ( 0 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 0 ↑ 0 ) · ( ! ‘ 𝑁 ) ) ) )
150 144 149 syl5ibr ⊢ ( 𝑀 = 0 → ( 𝑁 ∈ ℕ0 → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) ) )
151 150 imp ⊢ ( ( 𝑀 = 0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )
152 133 151 jaoian ⊢ ( ( ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )
153 1 152 sylanb ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑁 ) ) )