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 syl5bi ( ( 𝑀 ∈ ℕ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 mulid2d ( ( 𝑀 ∈ ℕ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 addid1d ( 𝑀 ∈ ℕ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 mulid2d ( 𝑀 ∈ ℕ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 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ 𝑁 ) ) )