# Metamath Proof Explorer

## Theorem faclbnd4lem1

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

Ref Expression
Hypotheses faclbnd4lem1.1 ${⊢}{N}\in ℕ$
faclbnd4lem1.2 ${⊢}{K}\in {ℕ}_{0}$
faclbnd4lem1.3 ${⊢}{M}\in {ℕ}_{0}$
Assertion faclbnd4lem1 ${⊢}{\left({N}-1\right)}^{{K}}{{M}}^{{N}-1}\le {2}^{{{K}}^{2}}{{M}}^{{M}+{K}}\left({N}-1\right)!\to {{N}}^{{K}+1}{{M}}^{{N}}\le {2}^{{\left({K}+1\right)}^{2}}{{M}}^{{M}+{K}+1}{N}!$

### Proof

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