Metamath Proof Explorer

Theorem faclbnd4lem1

Description: Lemma for faclbnd4 . Prepare the induction step. (Contributed by NM, 20-Dec-2005)

Ref Expression
Hypotheses faclbnd4lem1.1 ⊢ 𝑁 ∈ ℕ
faclbnd4lem1.2 ⊢ 𝐾 ∈ ℕ0
faclbnd4lem1.3 ⊢ 𝑀 ∈ ℕ0
Assertion faclbnd4lem1 ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 faclbnd4lem1.1 ⊢ 𝑁 ∈ ℕ
2 faclbnd4lem1.2 ⊢ 𝐾 ∈ ℕ0
3 faclbnd4lem1.3 ⊢ 𝑀 ∈ ℕ0
4 1 nnrei ⊢ 𝑁 ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 lelttric ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑁 ≤ 1 ∨ 1 < 𝑁 ) )
7 4 5 6 mp2an ⊢ ( 𝑁 ≤ 1 ∨ 1 < 𝑁 )
8 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
9 1 8 ax-mp ⊢ 1 ≤ 𝑁
10 4 5 letri3i ⊢ ( 𝑁 = 1 ↔ ( 𝑁 ≤ 1 ∧ 1 ≤ 𝑁 ) )
11 9 10 mpbiran2 ⊢ ( 𝑁 = 1 ↔ 𝑁 ≤ 1 )
12 0le1 ⊢ 0 ≤ 1
13 5 12 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 0 ≤ 1 )
14 2re ⊢ 2 ∈ ℝ
15 1nn ⊢ 1 ∈ ℕ
16 nn0nnaddcl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 1 ∈ ℕ ) → ( 𝐾 + 1 ) ∈ ℕ )
17 2 15 16 mp2an ⊢ ( 𝐾 + 1 ) ∈ ℕ
18 17 nnnn0i ⊢ ( 𝐾 + 1 ) ∈ ℕ0
19 2nn0 ⊢ 2 ∈ ℕ0
20 18 19 nn0expcli ⊢ ( ( 𝐾 + 1 ) ↑ 2 ) ∈ ℕ0
21 reexpcl ⊢ ( ( 2 ∈ ℝ ∧ ( ( 𝐾 + 1 ) ↑ 2 ) ∈ ℕ0 ) → ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∈ ℝ )
22 14 20 21 mp2an ⊢ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∈ ℝ
23 13 22 pm3.2i ⊢ ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∈ ℝ )
24 3 nn0rei ⊢ 𝑀 ∈ ℝ
25 3 nn0ge0i ⊢ 0 ≤ 𝑀
26 24 25 pm3.2i ⊢ ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 )
27 nn0nnaddcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ∈ ℕ ) → ( 𝑀 + ( 𝐾 + 1 ) ) ∈ ℕ )
28 3 17 27 mp2an ⊢ ( 𝑀 + ( 𝐾 + 1 ) ) ∈ ℕ
29 28 nnnn0i ⊢ ( 𝑀 + ( 𝐾 + 1 ) ) ∈ ℕ0
30 3 29 nn0expcli ⊢ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ∈ ℕ0
31 30 nn0rei ⊢ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ∈ ℝ
32 26 31 pm3.2i ⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ∈ ℝ )
33 23 32 pm3.2i ⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∈ ℝ ) ∧ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ∈ ℝ ) )
34 2cn ⊢ 2 ∈ ℂ
35 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
36 34 35 ax-mp ⊢ ( 2 ↑ 0 ) = 1
37 1le2 ⊢ 1 ≤ 2
38 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
39 20 38 eleqtri ⊢ ( ( 𝐾 + 1 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 0 )
40 leexp2a ⊢ ( ( 2 ∈ ℝ ∧ 1 ≤ 2 ∧ ( ( 𝐾 + 1 ) ↑ 2 ) ∈ ( ℤ≥ ‘ 0 ) ) → ( 2 ↑ 0 ) ≤ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) )
41 14 37 39 40 mp3an ⊢ ( 2 ↑ 0 ) ≤ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) )
42 36 41 eqbrtrri ⊢ 1 ≤ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) )
43 elnn0 ⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
44 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
45 44 exp1d ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ 1 ) = 𝑀 )
46 nnge1 ⊢ ( 𝑀 ∈ ℕ → 1 ≤ 𝑀 )
47 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
48 28 47 eleqtri ⊢ ( 𝑀 + ( 𝐾 + 1 ) ) ∈ ( ℤ≥ ‘ 1 )
49 leexp2a ⊢ ( ( 𝑀 ∈ ℝ ∧ 1 ≤ 𝑀 ∧ ( 𝑀 + ( 𝐾 + 1 ) ) ∈ ( ℤ≥ ‘ 1 ) ) → ( 𝑀 ↑ 1 ) ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
50 24 48 49 mp3an13 ⊢ ( 1 ≤ 𝑀 → ( 𝑀 ↑ 1 ) ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
51 46 50 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ↑ 1 ) ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
52 45 51 eqbrtrrd ⊢ ( 𝑀 ∈ ℕ → 𝑀 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
53 30 nn0ge0i ⊢ 0 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) )
54 breq1 ⊢ ( 𝑀 = 0 → ( 𝑀 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ↔ 0 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) )
55 53 54 mpbiri ⊢ ( 𝑀 = 0 → 𝑀 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
56 52 55 jaoi ⊢ ( ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) → 𝑀 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
57 43 56 sylbi ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
58 3 57 ax-mp ⊢ 𝑀 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) )
59 42 58 pm3.2i ⊢ ( 1 ≤ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∧ 𝑀 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
60 lemul12a ⊢ ( ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∈ ℝ ) ∧ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ∧ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ∈ ℝ ) ) → ( ( 1 ≤ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∧ 𝑀 ≤ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) → ( 1 · 𝑀 ) ≤ ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) ) )
61 33 59 60 mp2 ⊢ ( 1 · 𝑀 ) ≤ ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
62 oveq1 ⊢ ( 𝑁 = 1 → ( 𝑁 ↑ ( 𝐾 + 1 ) ) = ( 1 ↑ ( 𝐾 + 1 ) ) )
63 17 nnzi ⊢ ( 𝐾 + 1 ) ∈ ℤ
64 1exp ⊢ ( ( 𝐾 + 1 ) ∈ ℤ → ( 1 ↑ ( 𝐾 + 1 ) ) = 1 )
65 63 64 ax-mp ⊢ ( 1 ↑ ( 𝐾 + 1 ) ) = 1
66 62 65 eqtrdi ⊢ ( 𝑁 = 1 → ( 𝑁 ↑ ( 𝐾 + 1 ) ) = 1 )
67 oveq2 ⊢ ( 𝑁 = 1 → ( 𝑀 ↑ 𝑁 ) = ( 𝑀 ↑ 1 ) )
68 3 nn0cni ⊢ 𝑀 ∈ ℂ
69 exp1 ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ 1 ) = 𝑀 )
70 68 69 ax-mp ⊢ ( 𝑀 ↑ 1 ) = 𝑀
71 67 70 eqtrdi ⊢ ( 𝑁 = 1 → ( 𝑀 ↑ 𝑁 ) = 𝑀 )
72 66 71 oveq12d ⊢ ( 𝑁 = 1 → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) = ( 1 · 𝑀 ) )
73 fveq2 ⊢ ( 𝑁 = 1 → ( ! ‘ 𝑁 ) = ( ! ‘ 1 ) )
74 fac1 ⊢ ( ! ‘ 1 ) = 1
75 73 74 eqtrdi ⊢ ( 𝑁 = 1 → ( ! ‘ 𝑁 ) = 1 )
76 75 oveq2d ⊢ ( 𝑁 = 1 → ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · 1 ) )
77 22 recni ⊢ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∈ ℂ
78 30 nn0cni ⊢ ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ∈ ℂ
79 77 78 mulcli ⊢ ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) ∈ ℂ
80 79 mulridi ⊢ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · 1 ) = ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
81 76 80 eqtrdi ⊢ ( 𝑁 = 1 → ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) )
82 72 81 breq12d ⊢ ( 𝑁 = 1 → ( ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) ↔ ( 1 · 𝑀 ) ≤ ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) ) )
83 61 82 mpbiri ⊢ ( 𝑁 = 1 → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) )
84 11 83 sylbir ⊢ ( 𝑁 ≤ 1 → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) )
85 84 adantr ⊢ ( ( 𝑁 ≤ 1 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) )
86 reexpcl ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝐾 + 1 ) ∈ ℕ0 ) → ( 𝑁 ↑ ( 𝐾 + 1 ) ) ∈ ℝ )
87 4 18 86 mp2an ⊢ ( 𝑁 ↑ ( 𝐾 + 1 ) ) ∈ ℝ
88 1 nnnn0i ⊢ 𝑁 ∈ ℕ0
89 reexpcl ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑁 ) ∈ ℝ )
90 24 88 89 mp2an ⊢ ( 𝑀 ↑ 𝑁 ) ∈ ℝ
91 87 90 remulcli ⊢ ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ∈ ℝ
92 91 a1i ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ∈ ℝ )
93 2 19 nn0expcli ⊢ ( 𝐾 ↑ 2 ) ∈ ℕ0
94 reexpcl ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐾 ↑ 2 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝐾 ↑ 2 ) ) ∈ ℝ )
95 14 93 94 mp2an ⊢ ( 2 ↑ ( 𝐾 ↑ 2 ) ) ∈ ℝ
96 19 2 nn0expcli ⊢ ( 2 ↑ 𝐾 ) ∈ ℕ0
97 96 nn0rei ⊢ ( 2 ↑ 𝐾 ) ∈ ℝ
98 95 97 remulcli ⊢ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) ∈ ℝ
99 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
100 88 99 ax-mp ⊢ ( ! ‘ 𝑁 ) ∈ ℕ
101 100 nnnn0i ⊢ ( ! ‘ 𝑁 ) ∈ ℕ0
102 30 101 nn0mulcli ⊢ ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℕ0
103 102 nn0rei ⊢ ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℝ
104 98 103 remulcli ⊢ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) ∈ ℝ
105 104 a1i ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) ∈ ℝ )
106 22 103 remulcli ⊢ ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) ∈ ℝ
107 106 a1i ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) ∈ ℝ )
108 1 nncni ⊢ 𝑁 ∈ ℂ
109 expp1 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ↑ ( 𝐾 + 1 ) ) = ( ( 𝑁 ↑ 𝐾 ) · 𝑁 ) )
110 108 2 109 mp2an ⊢ ( 𝑁 ↑ ( 𝐾 + 1 ) ) = ( ( 𝑁 ↑ 𝐾 ) · 𝑁 )
111 expm1t ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ↑ 𝑁 ) = ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) )
112 68 1 111 mp2an ⊢ ( 𝑀 ↑ 𝑁 ) = ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 )
113 110 112 oveq12i ⊢ ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) = ( ( ( 𝑁 ↑ 𝐾 ) · 𝑁 ) · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) )
114 reexpcl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 ↑ 𝐾 ) ∈ ℝ )
115 4 2 114 mp2an ⊢ ( 𝑁 ↑ 𝐾 ) ∈ ℝ
116 115 recni ⊢ ( 𝑁 ↑ 𝐾 ) ∈ ℂ
117 elnnnn0 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) )
118 1 117 mpbi ⊢ ( 𝑁 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 )
119 118 simpri ⊢ ( 𝑁 − 1 ) ∈ ℕ0
120 3 119 nn0expcli ⊢ ( 𝑀 ↑ ( 𝑁 − 1 ) ) ∈ ℕ0
121 120 3 nn0mulcli ⊢ ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ∈ ℕ0
122 121 nn0cni ⊢ ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ∈ ℂ
123 116 108 122 mulassi ⊢ ( ( ( 𝑁 ↑ 𝐾 ) · 𝑁 ) · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) = ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) )
124 113 123 eqtri ⊢ ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) = ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) )
125 88 121 nn0mulcli ⊢ ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ∈ ℕ0
126 125 nn0rei ⊢ ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ∈ ℝ
127 115 126 remulcli ⊢ ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) ∈ ℝ
128 127 a1i ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) ∈ ℝ )
129 119 nn0rei ⊢ ( 𝑁 − 1 ) ∈ ℝ
130 reexpcl ⊢ ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑁 − 1 ) ↑ 𝐾 ) ∈ ℝ )
131 129 2 130 mp2an ⊢ ( ( 𝑁 − 1 ) ↑ 𝐾 ) ∈ ℝ
132 120 nn0rei ⊢ ( 𝑀 ↑ ( 𝑁 − 1 ) ) ∈ ℝ
133 131 132 remulcli ⊢ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ
134 96 88 nn0mulcli ⊢ ( ( 2 ↑ 𝐾 ) · 𝑁 ) ∈ ℕ0
135 134 3 nn0mulcli ⊢ ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ∈ ℕ0
136 135 nn0rei ⊢ ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ∈ ℝ
137 133 136 remulcli ⊢ ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) ∈ ℝ
138 137 a1i ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) ∈ ℝ )
139 3 2 nn0addcli ⊢ ( 𝑀 + 𝐾 ) ∈ ℕ0
140 reexpcl ⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑀 + 𝐾 ) ∈ ℕ0 ) → ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ∈ ℝ )
141 24 139 140 mp2an ⊢ ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ∈ ℝ
142 95 141 remulcli ⊢ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℝ
143 faccl ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ )
144 119 143 ax-mp ⊢ ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ
145 144 nnrei ⊢ ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℝ
146 142 145 remulcli ⊢ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ∈ ℝ
147 146 136 remulcli ⊢ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) ∈ ℝ
148 147 a1i ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) ∈ ℝ )
149 97 131 remulcli ⊢ ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) ∈ ℝ
150 125 nn0ge0i ⊢ 0 ≤ ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) )
151 126 150 pm3.2i ⊢ ( ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) )
152 115 149 151 3pm3.2i ⊢ ( ( 𝑁 ↑ 𝐾 ) ∈ ℝ ∧ ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) ∈ ℝ ∧ ( ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) )
153 nnltp1le ⊢ ( ( 1 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 1 < 𝑁 ↔ ( 1 + 1 ) ≤ 𝑁 ) )
154 15 1 153 mp2an ⊢ ( 1 < 𝑁 ↔ ( 1 + 1 ) ≤ 𝑁 )
155 df-2 ⊢ 2 = ( 1 + 1 )
156 155 breq1i ⊢ ( 2 ≤ 𝑁 ↔ ( 1 + 1 ) ≤ 𝑁 )
157 154 156 bitr4i ⊢ ( 1 < 𝑁 ↔ 2 ≤ 𝑁 )
158 expubnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 ↑ 𝐾 ) ≤ ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) )
159 4 2 158 mp3an12 ⊢ ( 2 ≤ 𝑁 → ( 𝑁 ↑ 𝐾 ) ≤ ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) )
160 157 159 sylbi ⊢ ( 1 < 𝑁 → ( 𝑁 ↑ 𝐾 ) ≤ ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) )
161 lemul1a ⊢ ( ( ( ( 𝑁 ↑ 𝐾 ) ∈ ℝ ∧ ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) ∈ ℝ ∧ ( ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) ) ∧ ( 𝑁 ↑ 𝐾 ) ≤ ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) ≤ ( ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) )
162 152 160 161 sylancr ⊢ ( 1 < 𝑁 → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) ≤ ( ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) )
163 96 nn0cni ⊢ ( 2 ↑ 𝐾 ) ∈ ℂ
164 131 recni ⊢ ( ( 𝑁 − 1 ) ↑ 𝐾 ) ∈ ℂ
165 163 164 108 122 mul4i ⊢ ( ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) = ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) )
166 120 nn0cni ⊢ ( 𝑀 ↑ ( 𝑁 − 1 ) ) ∈ ℂ
167 164 166 68 mulassi ⊢ ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · 𝑀 ) = ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) )
168 167 oveq2i ⊢ ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · 𝑀 ) ) = ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) )
169 134 nn0cni ⊢ ( ( 2 ↑ 𝐾 ) · 𝑁 ) ∈ ℂ
170 133 recni ⊢ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ
171 169 170 68 mul12i ⊢ ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · 𝑀 ) ) = ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) )
172 165 168 171 3eqtr2i ⊢ ( ( ( 2 ↑ 𝐾 ) · ( ( 𝑁 − 1 ) ↑ 𝐾 ) ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) = ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) )
173 162 172 breqtrdi ⊢ ( 1 < 𝑁 → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) ≤ ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) )
174 173 adantr ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) ≤ ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) )
175 135 nn0ge0i ⊢ 0 ≤ ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 )
176 136 175 pm3.2i ⊢ ( ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ∈ ℝ ∧ 0 ≤ ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) )
177 133 146 176 3pm3.2i ⊢ ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ ∧ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ∈ ℝ ∧ ( ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ∈ ℝ ∧ 0 ≤ ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) )
178 lemul1a ⊢ ( ( ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ∈ ℝ ∧ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ∈ ℝ ∧ ( ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ∈ ℝ ∧ 0 ≤ ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) ) ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) ≤ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) )
179 177 178 mpan ⊢ ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) ≤ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) )
180 179 adantl ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) ≤ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) )
181 128 138 148 174 180 letrd ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) ≤ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) )
182 163 108 68 mul32i ⊢ ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) = ( ( ( 2 ↑ 𝐾 ) · 𝑀 ) · 𝑁 )
183 182 oveq2i ⊢ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) = ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑀 ) · 𝑁 ) )
184 expp1 ⊢ ( ( 𝑀 ∈ ℂ ∧ ( 𝑀 + 𝐾 ) ∈ ℕ0 ) → ( 𝑀 ↑ ( ( 𝑀 + 𝐾 ) + 1 ) ) = ( ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) · 𝑀 ) )
185 68 139 184 mp2an ⊢ ( 𝑀 ↑ ( ( 𝑀 + 𝐾 ) + 1 ) ) = ( ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) · 𝑀 )
186 2 nn0cni ⊢ 𝐾 ∈ ℂ
187 ax-1cn ⊢ 1 ∈ ℂ
188 68 186 187 addassi ⊢ ( ( 𝑀 + 𝐾 ) + 1 ) = ( 𝑀 + ( 𝐾 + 1 ) )
189 188 oveq2i ⊢ ( 𝑀 ↑ ( ( 𝑀 + 𝐾 ) + 1 ) ) = ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) )
190 185 189 eqtr3i ⊢ ( ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) · 𝑀 ) = ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) )
191 190 oveq2i ⊢ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) · 𝑀 ) ) = ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) )
192 95 recni ⊢ ( 2 ↑ ( 𝐾 ↑ 2 ) ) ∈ ℂ
193 141 recni ⊢ ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ∈ ℂ
194 192 163 193 68 mul4i ⊢ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) · 𝑀 ) ) = ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ( 2 ↑ 𝐾 ) · 𝑀 ) )
195 191 194 eqtr3i ⊢ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) = ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ( 2 ↑ 𝐾 ) · 𝑀 ) )
196 facnn2 ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
197 1 196 ax-mp ⊢ ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 )
198 195 197 oveq12i ⊢ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ( 2 ↑ 𝐾 ) · 𝑀 ) ) · ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
199 142 recni ⊢ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) ∈ ℂ
200 144 nncni ⊢ ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℂ
201 163 68 mulcli ⊢ ( ( 2 ↑ 𝐾 ) · 𝑀 ) ∈ ℂ
202 199 200 201 108 mul4i ⊢ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑀 ) · 𝑁 ) ) = ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ( 2 ↑ 𝐾 ) · 𝑀 ) ) · ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
203 198 202 eqtr4i ⊢ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑀 ) · 𝑁 ) )
204 98 recni ⊢ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) ∈ ℂ
205 100 nncni ⊢ ( ! ‘ 𝑁 ) ∈ ℂ
206 204 78 205 mulassi ⊢ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) )
207 183 203 206 3eqtr2i ⊢ ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) · ( ( ( 2 ↑ 𝐾 ) · 𝑁 ) · 𝑀 ) ) = ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) )
208 181 207 breqtrdi ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ 𝐾 ) · ( 𝑁 · ( ( 𝑀 ↑ ( 𝑁 − 1 ) ) · 𝑀 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
209 124 208 eqbrtrid ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
210 102 nn0ge0i ⊢ 0 ≤ ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) )
211 103 210 pm3.2i ⊢ ( ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) )
212 98 22 211 3pm3.2i ⊢ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) ∈ ℝ ∧ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∈ ℝ ∧ ( ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
213 expadd ⊢ ( ( 2 ∈ ℂ ∧ ( 𝐾 ↑ 2 ) ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 2 ↑ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ) = ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) )
214 34 93 2 213 mp3an ⊢ ( 2 ↑ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ) = ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) )
215 20 nn0zi ⊢ ( ( 𝐾 + 1 ) ↑ 2 ) ∈ ℤ
216 2 nn0rei ⊢ 𝐾 ∈ ℝ
217 17 nnrei ⊢ ( 𝐾 + 1 ) ∈ ℝ
218 18 nn0ge0i ⊢ 0 ≤ ( 𝐾 + 1 )
219 217 218 pm3.2i ⊢ ( ( 𝐾 + 1 ) ∈ ℝ ∧ 0 ≤ ( 𝐾 + 1 ) )
220 216 217 219 3pm3.2i ⊢ ( 𝐾 ∈ ℝ ∧ ( 𝐾 + 1 ) ∈ ℝ ∧ ( ( 𝐾 + 1 ) ∈ ℝ ∧ 0 ≤ ( 𝐾 + 1 ) ) )
221 216 ltp1i ⊢ 𝐾 < ( 𝐾 + 1 )
222 216 217 221 ltleii ⊢ 𝐾 ≤ ( 𝐾 + 1 )
223 lemul1a ⊢ ( ( ( 𝐾 ∈ ℝ ∧ ( 𝐾 + 1 ) ∈ ℝ ∧ ( ( 𝐾 + 1 ) ∈ ℝ ∧ 0 ≤ ( 𝐾 + 1 ) ) ) ∧ 𝐾 ≤ ( 𝐾 + 1 ) ) → ( 𝐾 · ( 𝐾 + 1 ) ) ≤ ( ( 𝐾 + 1 ) · ( 𝐾 + 1 ) ) )
224 220 222 223 mp2an ⊢ ( 𝐾 · ( 𝐾 + 1 ) ) ≤ ( ( 𝐾 + 1 ) · ( 𝐾 + 1 ) )
225 186 sqvali ⊢ ( 𝐾 ↑ 2 ) = ( 𝐾 · 𝐾 )
226 186 mulridi ⊢ ( 𝐾 · 1 ) = 𝐾
227 226 eqcomi ⊢ 𝐾 = ( 𝐾 · 1 )
228 225 227 oveq12i ⊢ ( ( 𝐾 ↑ 2 ) + 𝐾 ) = ( ( 𝐾 · 𝐾 ) + ( 𝐾 · 1 ) )
229 186 186 187 adddii ⊢ ( 𝐾 · ( 𝐾 + 1 ) ) = ( ( 𝐾 · 𝐾 ) + ( 𝐾 · 1 ) )
230 228 229 eqtr4i ⊢ ( ( 𝐾 ↑ 2 ) + 𝐾 ) = ( 𝐾 · ( 𝐾 + 1 ) )
231 17 nncni ⊢ ( 𝐾 + 1 ) ∈ ℂ
232 231 sqvali ⊢ ( ( 𝐾 + 1 ) ↑ 2 ) = ( ( 𝐾 + 1 ) · ( 𝐾 + 1 ) )
233 224 230 232 3brtr4i ⊢ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ≤ ( ( 𝐾 + 1 ) ↑ 2 )
234 93 2 nn0addcli ⊢ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ∈ ℕ0
235 234 nn0zi ⊢ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ∈ ℤ
236 235 eluz1i ⊢ ( ( ( 𝐾 + 1 ) ↑ 2 ) ∈ ( ℤ≥ ‘ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ) ↔ ( ( ( 𝐾 + 1 ) ↑ 2 ) ∈ ℤ ∧ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ≤ ( ( 𝐾 + 1 ) ↑ 2 ) ) )
237 215 233 236 mpbir2an ⊢ ( ( 𝐾 + 1 ) ↑ 2 ) ∈ ( ℤ≥ ‘ ( ( 𝐾 ↑ 2 ) + 𝐾 ) )
238 leexp2a ⊢ ( ( 2 ∈ ℝ ∧ 1 ≤ 2 ∧ ( ( 𝐾 + 1 ) ↑ 2 ) ∈ ( ℤ≥ ‘ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ) ) → ( 2 ↑ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ) ≤ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) )
239 14 37 237 238 mp3an ⊢ ( 2 ↑ ( ( 𝐾 ↑ 2 ) + 𝐾 ) ) ≤ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) )
240 214 239 eqbrtrri ⊢ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) ≤ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) )
241 lemul1a ⊢ ( ( ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) ∈ ℝ ∧ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ∈ ℝ ∧ ( ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) ) ∧ ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) ≤ ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) ≤ ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
242 212 240 241 mp2an ⊢ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) ≤ ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) )
243 242 a1i ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 2 ↑ 𝐾 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) ≤ ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
244 92 105 107 209 243 letrd ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) ) )
245 77 78 205 mulassi ⊢ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) = ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) · ( ! ‘ 𝑁 ) ) )
246 244 245 breqtrrdi ⊢ ( ( 1 < 𝑁 ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) )
247 85 246 jaoian ⊢ ( ( ( 𝑁 ≤ 1 ∨ 1 < 𝑁 ) ∧ ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) )
248 7 247 mpan ⊢ ( ( ( ( 𝑁 − 1 ) ↑ 𝐾 ) · ( 𝑀 ↑ ( 𝑁 − 1 ) ) ) ≤ ( ( ( 2 ↑ ( 𝐾 ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + 𝐾 ) ) ) · ( ! ‘ ( 𝑁 − 1 ) ) ) → ( ( 𝑁 ↑ ( 𝐾 + 1 ) ) · ( 𝑀 ↑ 𝑁 ) ) ≤ ( ( ( 2 ↑ ( ( 𝐾 + 1 ) ↑ 2 ) ) · ( 𝑀 ↑ ( 𝑀 + ( 𝐾 + 1 ) ) ) ) · ( ! ‘ 𝑁 ) ) )