This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem faclbnd4lem4

Description: Lemma for faclbnd4 . Prove the 0 < N case by induction on K . (Contributed by NM, 19-Dec-2005)

Ref Expression
Assertion faclbnd4lem4 ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ↑ 𝑗 ) = ( 𝑚 ↑ 𝑗 ) )
2 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑀 ↑ 𝑛 ) = ( 𝑀 ↑ 𝑚 ) )
3 1 2 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) )
4 fveq2 ⊢ ( 𝑛 = 𝑚 → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑚 ) )
5 4 oveq2d ⊢ ( 𝑛 = 𝑚 → ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) = ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) )
6 3 5 breq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) ) )
7 6 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) )
8 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
9 1re ⊢ 1 ∈ ℝ
10 lelttric ⊢ ( ( 𝑛 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑛 ≤ 1 ∨ 1 < 𝑛 ) )
11 8 9 10 sylancl ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ≤ 1 ∨ 1 < 𝑛 ) )
12 11 ancli ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ∈ ℕ ∧ ( 𝑛 ≤ 1 ∨ 1 < 𝑛 ) ) )
13 andi ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 ≤ 1 ∨ 1 < 𝑛 ) ) ↔ ( ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 1 ) ∨ ( 𝑛 ∈ ℕ ∧ 1 < 𝑛 ) ) )
14 12 13 sylib ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 1 ) ∨ ( 𝑛 ∈ ℕ ∧ 1 < 𝑛 ) ) )
15 nnge1 ⊢ ( 𝑛 ∈ ℕ → 1 ≤ 𝑛 )
16 letri3 ⊢ ( ( 𝑛 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑛 = 1 ↔ ( 𝑛 ≤ 1 ∧ 1 ≤ 𝑛 ) ) )
17 8 9 16 sylancl ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 = 1 ↔ ( 𝑛 ≤ 1 ∧ 1 ≤ 𝑛 ) ) )
18 17 biimpar ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 ≤ 1 ∧ 1 ≤ 𝑛 ) ) → 𝑛 = 1 )
19 18 anassrs ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 1 ) ∧ 1 ≤ 𝑛 ) → 𝑛 = 1 )
20 15 19 mpidan ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 1 ) → 𝑛 = 1 )
21 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 − 1 ) = ( 1 − 1 ) )
22 1m1e0 ⊢ ( 1 − 1 ) = 0
23 21 22 eqtrdi ⊢ ( 𝑛 = 1 → ( 𝑛 − 1 ) = 0 )
24 20 23 syl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 1 ) → ( 𝑛 − 1 ) = 0 )
25 faclbnd4lem3 ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑛 − 1 ) = 0 ) → ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) )
26 24 25 sylan2 ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 1 ) ) → ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) )
27 26 a1d ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 1 ) ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) → ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) ) )
28 1nn ⊢ 1 ∈ ℕ
29 nnsub ⊢ ( ( 1 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 1 < 𝑛 ↔ ( 𝑛 − 1 ) ∈ ℕ ) )
30 28 29 mpan ⊢ ( 𝑛 ∈ ℕ → ( 1 < 𝑛 ↔ ( 𝑛 − 1 ) ∈ ℕ ) )
31 30 biimpa ⊢ ( ( 𝑛 ∈ ℕ ∧ 1 < 𝑛 ) → ( 𝑛 − 1 ) ∈ ℕ )
32 oveq1 ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( 𝑚 ↑ 𝑗 ) = ( ( 𝑛 − 1 ) ↑ 𝑗 ) )
33 oveq2 ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( 𝑀 ↑ 𝑚 ) = ( 𝑀 ↑ ( 𝑛 − 1 ) ) )
34 32 33 oveq12d ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) = ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) )
35 fveq2 ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ! ‘ 𝑚 ) = ( ! ‘ ( 𝑛 − 1 ) ) )
36 35 oveq2d ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) = ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) )
37 34 36 breq12d ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) ↔ ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) ) )
38 37 rspcv ⊢ ( ( 𝑛 − 1 ) ∈ ℕ → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) → ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) ) )
39 31 38 syl ⊢ ( ( 𝑛 ∈ ℕ ∧ 1 < 𝑛 ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) → ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) ) )
40 39 adantl ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ ∧ 1 < 𝑛 ) ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) → ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) ) )
41 27 40 jaodan ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 1 ) ∨ ( 𝑛 ∈ ℕ ∧ 1 < 𝑛 ) ) ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) → ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) ) )
42 14 41 sylan2 ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) → ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) ) )
43 faclbnd4lem2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) → ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) )
44 43 3expa ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( ( ( ( 𝑛 − 1 ) ↑ 𝑗 ) · ( 𝑀 ↑ ( 𝑛 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ ( 𝑛 − 1 ) ) ) → ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) )
45 42 44 syld ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) → ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) )
46 45 ralrimdva ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) → ( ∀ 𝑚 ∈ ℕ ( ( 𝑚 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑚 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑚 ) ) → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) )
47 7 46 biimtrid ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) → ( ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) )
48 47 expcom ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) ) )
49 48 a2d ⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) ) → ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) ) )
50 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
51 faclbnd3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑛 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑛 ) ) )
52 50 51 sylan2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ↑ 𝑛 ) ≤ ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑛 ) ) )
53 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
54 53 exp0d ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 0 ) = 1 )
55 54 oveq1d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 ↑ 0 ) · ( 𝑀 ↑ 𝑛 ) ) = ( 1 · ( 𝑀 ↑ 𝑛 ) ) )
56 55 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ↑ 0 ) · ( 𝑀 ↑ 𝑛 ) ) = ( 1 · ( 𝑀 ↑ 𝑛 ) ) )
57 nn0cn ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
58 expcl ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑛 ) ∈ ℂ )
59 57 50 58 syl2an ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ↑ 𝑛 ) ∈ ℂ )
60 59 mullidd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( 1 · ( 𝑀 ↑ 𝑛 ) ) = ( 𝑀 ↑ 𝑛 ) )
61 56 60 eqtrd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ↑ 0 ) · ( 𝑀 ↑ 𝑛 ) ) = ( 𝑀 ↑ 𝑛 ) )
62 sq0 ⊢ ( 0 ↑ 2 ) = 0
63 62 oveq2i ⊢ ( 2 ↑ ( 0 ↑ 2 ) ) = ( 2 ↑ 0 )
64 2cn ⊢ 2 ∈ ℂ
65 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
66 64 65 ax-mp ⊢ ( 2 ↑ 0 ) = 1
67 63 66 eqtri ⊢ ( 2 ↑ ( 0 ↑ 2 ) ) = 1
68 67 a1i ⊢ ( 𝑀 ∈ ℕ0 → ( 2 ↑ ( 0 ↑ 2 ) ) = 1 )
69 57 addridd ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 0 ) = 𝑀 )
70 69 oveq2d ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ↑ ( 𝑀 + 0 ) ) = ( 𝑀 ↑ 𝑀 ) )
71 68 70 oveq12d ⊢ ( 𝑀 ∈ ℕ0 → ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) = ( 1 · ( 𝑀 ↑ 𝑀 ) ) )
72 expcl ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑀 ) ∈ ℂ )
73 57 72 mpancom ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ↑ 𝑀 ) ∈ ℂ )
74 73 mullidd ⊢ ( 𝑀 ∈ ℕ0 → ( 1 · ( 𝑀 ↑ 𝑀 ) ) = ( 𝑀 ↑ 𝑀 ) )
75 71 74 eqtrd ⊢ ( 𝑀 ∈ ℕ0 → ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) = ( 𝑀 ↑ 𝑀 ) )
76 75 oveq1d ⊢ ( 𝑀 ∈ ℕ0 → ( ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) · ( ! ‘ 𝑛 ) ) = ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑛 ) ) )
77 76 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) · ( ! ‘ 𝑛 ) ) = ( ( 𝑀 ↑ 𝑀 ) · ( ! ‘ 𝑛 ) ) )
78 52 61 77 3brtr4d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ↑ 0 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) · ( ! ‘ 𝑛 ) ) )
79 78 ralrimiva ⊢ ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 0 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) · ( ! ‘ 𝑛 ) ) )
80 oveq2 ⊢ ( 𝑚 = 0 → ( 𝑛 ↑ 𝑚 ) = ( 𝑛 ↑ 0 ) )
81 80 oveq1d ⊢ ( 𝑚 = 0 → ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝑛 ↑ 0 ) · ( 𝑀 ↑ 𝑛 ) ) )
82 oveq1 ⊢ ( 𝑚 = 0 → ( 𝑚 ↑ 2 ) = ( 0 ↑ 2 ) )
83 82 oveq2d ⊢ ( 𝑚 = 0 → ( 2 ↑ ( 𝑚 ↑ 2 ) ) = ( 2 ↑ ( 0 ↑ 2 ) ) )
84 oveq2 ⊢ ( 𝑚 = 0 → ( 𝑀 + 𝑚 ) = ( 𝑀 + 0 ) )
85 84 oveq2d ⊢ ( 𝑚 = 0 → ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) = ( 𝑀 ↑ ( 𝑀 + 0 ) ) )
86 83 85 oveq12d ⊢ ( 𝑚 = 0 → ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) = ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) )
87 86 oveq1d ⊢ ( 𝑚 = 0 → ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) = ( ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) · ( ! ‘ 𝑛 ) ) )
88 81 87 breq12d ⊢ ( 𝑚 = 0 → ( ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ( ( 𝑛 ↑ 0 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) · ( ! ‘ 𝑛 ) ) ) )
89 88 ralbidv ⊢ ( 𝑚 = 0 → ( ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 0 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) · ( ! ‘ 𝑛 ) ) ) )
90 89 imbi2d ⊢ ( 𝑚 = 0 → ( ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ) ↔ ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 0 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 0 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 0 ) ) ) · ( ! ‘ 𝑛 ) ) ) ) )
91 oveq2 ⊢ ( 𝑚 = 𝑗 → ( 𝑛 ↑ 𝑚 ) = ( 𝑛 ↑ 𝑗 ) )
92 91 oveq1d ⊢ ( 𝑚 = 𝑗 → ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) )
93 oveq1 ⊢ ( 𝑚 = 𝑗 → ( 𝑚 ↑ 2 ) = ( 𝑗 ↑ 2 ) )
94 93 oveq2d ⊢ ( 𝑚 = 𝑗 → ( 2 ↑ ( 𝑚 ↑ 2 ) ) = ( 2 ↑ ( 𝑗 ↑ 2 ) ) )
95 oveq2 ⊢ ( 𝑚 = 𝑗 → ( 𝑀 + 𝑚 ) = ( 𝑀 + 𝑗 ) )
96 95 oveq2d ⊢ ( 𝑚 = 𝑗 → ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) = ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) )
97 94 96 oveq12d ⊢ ( 𝑚 = 𝑗 → ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) = ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) )
98 97 oveq1d ⊢ ( 𝑚 = 𝑗 → ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) = ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) )
99 92 98 breq12d ⊢ ( 𝑚 = 𝑗 → ( ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) ) )
100 99 ralbidv ⊢ ( 𝑚 = 𝑗 → ( ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) ) )
101 100 imbi2d ⊢ ( 𝑚 = 𝑗 → ( ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ) ↔ ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑗 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑗 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑗 ) ) ) · ( ! ‘ 𝑛 ) ) ) ) )
102 oveq2 ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( 𝑛 ↑ 𝑚 ) = ( 𝑛 ↑ ( 𝑗 + 1 ) ) )
103 102 oveq1d ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) )
104 oveq1 ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( 𝑚 ↑ 2 ) = ( ( 𝑗 + 1 ) ↑ 2 ) )
105 104 oveq2d ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( 2 ↑ ( 𝑚 ↑ 2 ) ) = ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) )
106 oveq2 ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( 𝑀 + 𝑚 ) = ( 𝑀 + ( 𝑗 + 1 ) ) )
107 106 oveq2d ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) = ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) )
108 105 107 oveq12d ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) = ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) )
109 108 oveq1d ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) = ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) )
110 103 109 breq12d ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) )
111 110 ralbidv ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) )
112 111 imbi2d ⊢ ( 𝑚 = ( 𝑗 + 1 ) → ( ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ) ↔ ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ ( 𝑗 + 1 ) ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( ( 𝑗 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝑗 + 1 ) ) ) ) · ( ! ‘ 𝑛 ) ) ) ) )
113 oveq2 ⊢ ( 𝑚 = 𝐾 → ( 𝑛 ↑ 𝑚 ) = ( 𝑛 ↑ 𝐾 ) )
114 113 oveq1d ⊢ ( 𝑚 = 𝐾 → ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝑛 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑛 ) ) )
115 oveq1 ⊢ ( 𝑚 = 𝐾 → ( 𝑚 ↑ 2 ) = ( 𝐾 ↑ 2 ) )
116 115 oveq2d ⊢ ( 𝑚 = 𝐾 → ( 2 ↑ ( 𝑚 ↑ 2 ) ) = ( 2 ↑ ( 𝐾 ↑ 2 ) ) )
117 oveq2 ⊢ ( 𝑚 = 𝐾 → ( 𝑀 + 𝑚 ) = ( 𝑀 + 𝐾 ) )
118 117 oveq2d ⊢ ( 𝑚 = 𝐾 → ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) = ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) )
119 116 118 oveq12d ⊢ ( 𝑚 = 𝐾 → ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) = ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) )
120 119 oveq1d ⊢ ( 𝑚 = 𝐾 → ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) = ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑛 ) ) )
121 114 120 breq12d ⊢ ( 𝑚 = 𝐾 → ( ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ( ( 𝑛 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑛 ) ) ) )
122 121 ralbidv ⊢ ( 𝑚 = 𝐾 → ( ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑛 ) ) ) )
123 122 imbi2d ⊢ ( 𝑚 = 𝐾 → ( ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝑚 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝑚 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝑚 ) ) ) · ( ! ‘ 𝑛 ) ) ) ↔ ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑛 ) ) ) ) )
124 49 79 90 101 112 123 nn0indALT ⊢ ( 𝐾 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑛 ) ) ) )
125 124 imp ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑛 ) ) )
126 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ↑ 𝐾 ) = ( 𝑁 ↑ 𝐾 ) )
127 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑀 ↑ 𝑛 ) = ( 𝑀 ↑ 𝑁 ) )
128 126 127 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑛 ) ) = ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) )
129 fveq2 ⊢ ( 𝑛 = 𝑁 → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑁 ) )
130 129 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑛 ) ) = ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
131 128 130 breq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑛 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑛 ) ) ↔ ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
132 131 rspcva ⊢ ( ( 𝑁 ∈ ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑛 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑛 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑛 ) ) ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
133 125 132 sylan2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )
134 133 3impb ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )