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 ) ) ) ) · ( ! ‘ 𝑁 ) ) )