Theorem faclbnd4lem1 14250

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

Hypotheses

Ref	Expression
faclbnd4lem1.1	⊢ 𝑁 ∈ ℕ
faclbnd4lem1.2	⊢ 𝐾 ∈ ℕ0
faclbnd4lem1.3	⊢ 𝑀 ∈ ℕ0

Assertion

Ref	Expression
faclbnd4lem1	⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))

Proof of Theorem faclbnd4lem1

Step	Hyp	Ref	Expression
1		faclbnd4lem1.1	. . . 4 ⊢ 𝑁 ∈ ℕ
2	1	nnrei 12218	. . 3 ⊢ 𝑁 ∈ ℝ
3		1re 11211	. . 3 ⊢ 1 ∈ ℝ
4		lelttric 11318	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 ≤ 1 ∨ 1 < 𝑁))
5	2, 3, 4	mp2an 689	. 2 ⊢ (𝑁 ≤ 1 ∨ 1 < 𝑁)
6		nnge1 12237	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
7	1, 6	ax-mp 5	. . . . . 6 ⊢ 1 ≤ 𝑁
8	2, 3	letri3i 11327	. . . . . 6 ⊢ (𝑁 = 1 ↔ (𝑁 ≤ 1 ∧ 1 ≤ 𝑁))
9	7, 8	mpbiran2 707	. . . . 5 ⊢ (𝑁 = 1 ↔ 𝑁 ≤ 1)
10		0le1 11734	. . . . . . . . . 10 ⊢ 0 ≤ 1
11	3, 10	pm3.2i 470	. . . . . . . . 9 ⊢ (1 ∈ ℝ ∧ 0 ≤ 1)
12		2re 12283	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
13		faclbnd4lem1.2	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℕ0
14		1nn 12220	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
15		nn0nnaddcl 12500	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ0 ∧ 1 ∈ ℕ) → (𝐾 + 1) ∈ ℕ)
16	13, 14, 15	mp2an 689	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℕ
17	16	nnnn0i 12477	. . . . . . . . . . 11 ⊢ (𝐾 + 1) ∈ ℕ0
18		2nn0 12486	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
19	17, 18	nn0expcli 14051	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℕ0
20		reexpcl 14041	. . . . . . . . . 10 ⊢ ((2 ∈ ℝ ∧ ((𝐾 + 1)↑2) ∈ ℕ0) → (2↑((𝐾 + 1)↑2)) ∈ ℝ)
21	12, 19, 20	mp2an 689	. . . . . . . . 9 ⊢ (2↑((𝐾 + 1)↑2)) ∈ ℝ
22	11, 21	pm3.2i 470	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ)
23		faclbnd4lem1.3	. . . . . . . . . . 11 ⊢ 𝑀 ∈ ℕ0
24	23	nn0rei 12480	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℝ
25	23	nn0ge0i 12496	. . . . . . . . . 10 ⊢ 0 ≤ 𝑀
26	24, 25	pm3.2i 470	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀)
27		nn0nnaddcl 12500	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ0 ∧ (𝐾 + 1) ∈ ℕ) → (𝑀 + (𝐾 + 1)) ∈ ℕ)
28	23, 16, 27	mp2an 689	. . . . . . . . . . . 12 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ
29	28	nnnn0i 12477	. . . . . . . . . . 11 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ0
30	23, 29	nn0expcli 14051	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℕ0
31	30	nn0rei 12480	. . . . . . . . 9 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ
32	26, 31	pm3.2i 470	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ)
33	22, 32	pm3.2i 470	. . . . . . 7 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ) ∧ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ))
34		2cn 12284	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
35		exp0 14028	. . . . . . . . . 10 ⊢ (2 ∈ ℂ → (2↑0) = 1)
36	34, 35	ax-mp 5	. . . . . . . . 9 ⊢ (2↑0) = 1
37		1le2 12418	. . . . . . . . . 10 ⊢ 1 ≤ 2
38		nn0uz 12861	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
39	19, 38	eleqtri 2823	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ≥‘0)
40		leexp2a 14134	. . . . . . . . . 10 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝐾 + 1)↑2) ∈ (ℤ≥‘0)) → (2↑0) ≤ (2↑((𝐾 + 1)↑2)))
41	12, 37, 39, 40	mp3an 1457	. . . . . . . . 9 ⊢ (2↑0) ≤ (2↑((𝐾 + 1)↑2))
42	36, 41	eqbrtrri 5161	. . . . . . . 8 ⊢ 1 ≤ (2↑((𝐾 + 1)↑2))
43		elnn0 12471	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 ↔ (𝑀 ∈ ℕ ∨ 𝑀 = 0))
44		nncn 12217	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
45	44	exp1d 14103	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑀↑1) = 𝑀)
46		nnge1 12237	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
47		nnuz 12862	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ≥‘1)
48	28, 47	eleqtri 2823	. . . . . . . . . . . . . 14 ⊢ (𝑀 + (𝐾 + 1)) ∈ (ℤ≥‘1)
49		leexp2a 14134	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℝ ∧ 1 ≤ 𝑀 ∧ (𝑀 + (𝐾 + 1)) ∈ (ℤ≥‘1)) → (𝑀↑1) ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
50	24, 48, 49	mp3an13 1448	. . . . . . . . . . . . 13 ⊢ (1 ≤ 𝑀 → (𝑀↑1) ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
51	46, 50	syl 17	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑀↑1) ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
52	45, 51	eqbrtrrd 5162	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
53	30	nn0ge0i 12496	. . . . . . . . . . . 12 ⊢ 0 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))
54		breq1 5141	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))) ↔ 0 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))))
55	53, 54	mpbiri 258	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
56	52, 55	jaoi 854	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
57	43, 56	sylbi 216	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
58	23, 57	ax-mp 5	. . . . . . . 8 ⊢ 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))
59	42, 58	pm3.2i 470	. . . . . . 7 ⊢ (1 ≤ (2↑((𝐾 + 1)↑2)) ∧ 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
60		lemul12a 12069	. . . . . . 7 ⊢ ((((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ) ∧ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ)) → ((1 ≤ (2↑((𝐾 + 1)↑2)) ∧ 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))) → (1 · 𝑀) ≤ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1))))))
61	33, 59, 60	mp2 9	. . . . . 6 ⊢ (1 · 𝑀) ≤ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1))))
62		oveq1 7408	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑁↑(𝐾 + 1)) = (1↑(𝐾 + 1)))
63	16	nnzi 12583	. . . . . . . . . 10 ⊢ (𝐾 + 1) ∈ ℤ
64		1exp 14054	. . . . . . . . . 10 ⊢ ((𝐾 + 1) ∈ ℤ → (1↑(𝐾 + 1)) = 1)
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (1↑(𝐾 + 1)) = 1
66	62, 65	eqtrdi 2780	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝑁↑(𝐾 + 1)) = 1)
67		oveq2 7409	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = (𝑀↑1))
68	23	nn0cni 12481	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℂ
69		exp1 14030	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℂ → (𝑀↑1) = 𝑀)
70	68, 69	ax-mp 5	. . . . . . . . 9 ⊢ (𝑀↑1) = 𝑀
71	67, 70	eqtrdi 2780	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = 𝑀)
72	66, 71	oveq12d 7419	. . . . . . 7 ⊢ (𝑁 = 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (1 · 𝑀))
73		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (!‘𝑁) = (!‘1))
74		fac1 14234	. . . . . . . . . 10 ⊢ (!‘1) = 1
75	73, 74	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑁 = 1 → (!‘𝑁) = 1)
76	75	oveq2d 7417	. . . . . . . 8 ⊢ (𝑁 = 1 → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · 1))
77	21	recni 11225	. . . . . . . . . 10 ⊢ (2↑((𝐾 + 1)↑2)) ∈ ℂ
78	30	nn0cni 12481	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℂ
79	77, 78	mulcli 11218	. . . . . . . . 9 ⊢ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) ∈ ℂ
80	79	mulridi 11215	. . . . . . . 8 ⊢ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · 1) = ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1))))
81	76, 80	eqtrdi 2780	. . . . . . 7 ⊢ (𝑁 = 1 → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))))
82	72, 81	breq12d 5151	. . . . . 6 ⊢ (𝑁 = 1 → (((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) ↔ (1 · 𝑀) ≤ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1))))))
83	61, 82	mpbiri 258	. . . . 5 ⊢ (𝑁 = 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
84	9, 83	sylbir 234	. . . 4 ⊢ (𝑁 ≤ 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
85	84	adantr 480	. . 3 ⊢ ((𝑁 ≤ 1 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
86		reexpcl 14041	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ (𝐾 + 1) ∈ ℕ0) → (𝑁↑(𝐾 + 1)) ∈ ℝ)
87	2, 17, 86	mp2an 689	. . . . . . 7 ⊢ (𝑁↑(𝐾 + 1)) ∈ ℝ
88	1	nnnn0i 12477	. . . . . . . 8 ⊢ 𝑁 ∈ ℕ0
89		reexpcl 14041	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ∈ ℝ)
90	24, 88, 89	mp2an 689	. . . . . . 7 ⊢ (𝑀↑𝑁) ∈ ℝ
91	87, 90	remulcli 11227	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ
92	91	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ)
93	13, 18	nn0expcli 14051	. . . . . . . . 9 ⊢ (𝐾↑2) ∈ ℕ0
94		reexpcl 14041	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (𝐾↑2) ∈ ℕ0) → (2↑(𝐾↑2)) ∈ ℝ)
95	12, 93, 94	mp2an 689	. . . . . . . 8 ⊢ (2↑(𝐾↑2)) ∈ ℝ
96	18, 13	nn0expcli 14051	. . . . . . . . 9 ⊢ (2↑𝐾) ∈ ℕ0
97	96	nn0rei 12480	. . . . . . . 8 ⊢ (2↑𝐾) ∈ ℝ
98	95, 97	remulcli 11227	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℝ
99		faccl 14240	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
100	88, 99	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) ∈ ℕ
101	100	nnnn0i 12477	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℕ0
102	30, 101	nn0mulcli 12507	. . . . . . . 8 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℕ0
103	102	nn0rei 12480	. . . . . . 7 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ
104	98, 103	remulcli 11227	. . . . . 6 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
105	104	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
106	21, 103	remulcli 11227	. . . . . 6 ⊢ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
107	106	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
108	1	nncni 12219	. . . . . . . . 9 ⊢ 𝑁 ∈ ℂ
109		expp1 14031	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁))
110	108, 13, 109	mp2an 689	. . . . . . . 8 ⊢ (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁)
111		expm1t 14053	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀))
112	68, 1, 111	mp2an 689	. . . . . . . 8 ⊢ (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀)
113	110, 112	oveq12i 7413	. . . . . . 7 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀))
114		reexpcl 14041	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ0) → (𝑁↑𝐾) ∈ ℝ)
115	2, 13, 114	mp2an 689	. . . . . . . . 9 ⊢ (𝑁↑𝐾) ∈ ℝ
116	115	recni 11225	. . . . . . . 8 ⊢ (𝑁↑𝐾) ∈ ℂ
117		elnnnn0 12512	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ0))
118	1, 117	mpbi 229	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ0)
119	118	simpri 485	. . . . . . . . . . 11 ⊢ (𝑁 − 1) ∈ ℕ0
120	23, 119	nn0expcli 14051	. . . . . . . . . 10 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℕ0
121	120, 23	nn0mulcli 12507	. . . . . . . . 9 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℕ0
122	121	nn0cni 12481	. . . . . . . 8 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℂ
123	116, 108, 122	mulassi 11222	. . . . . . 7 ⊢ (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
124	113, 123	eqtri 2752	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
125	88, 121	nn0mulcli 12507	. . . . . . . . . . 11 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℕ0
126	125	nn0rei 12480	. . . . . . . . . 10 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ
127	115, 126	remulcli 11227	. . . . . . . . 9 ⊢ ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ)
129	119	nn0rei 12480	. . . . . . . . . . . 12 ⊢ (𝑁 − 1) ∈ ℝ
130		reexpcl 14041	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝐾 ∈ ℕ0) → ((𝑁 − 1)↑𝐾) ∈ ℝ)
131	129, 13, 130	mp2an 689	. . . . . . . . . . 11 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℝ
132	120	nn0rei 12480	. . . . . . . . . . 11 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℝ
133	131, 132	remulcli 11227	. . . . . . . . . 10 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ
134	96, 88	nn0mulcli 12507	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℕ0
135	134, 23	nn0mulcli 12507	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℕ0
136	135	nn0rei 12480	. . . . . . . . . 10 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ
137	133, 136	remulcli 11227	. . . . . . . . 9 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
138	137	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
139	23, 13	nn0addcli 12506	. . . . . . . . . . . . 13 ⊢ (𝑀 + 𝐾) ∈ ℕ0
140		reexpcl 14041	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ (𝑀 + 𝐾) ∈ ℕ0) → (𝑀↑(𝑀 + 𝐾)) ∈ ℝ)
141	24, 139, 140	mp2an 689	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℝ
142	95, 141	remulcli 11227	. . . . . . . . . . 11 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℝ
143		faccl 14240	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℕ0 → (!‘(𝑁 − 1)) ∈ ℕ)
144	119, 143	ax-mp 5	. . . . . . . . . . . 12 ⊢ (!‘(𝑁 − 1)) ∈ ℕ
145	144	nnrei 12218	. . . . . . . . . . 11 ⊢ (!‘(𝑁 − 1)) ∈ ℝ
146	142, 145	remulcli 11227	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ
147	146, 136	remulcli 11227	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
148	147	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
149	97, 131	remulcli 11227	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ
150	125	nn0ge0i 12496	. . . . . . . . . . . . 13 ⊢ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))
151	126, 150	pm3.2i 470	. . . . . . . . . . . 12 ⊢ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
152	115, 149, 151	3pm3.2i 1336	. . . . . . . . . . 11 ⊢ ((𝑁↑𝐾) ∈ ℝ ∧ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ ∧ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
153		nnltp1le 12615	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁))
154	14, 1, 153	mp2an 689	. . . . . . . . . . . . 13 ⊢ (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁)
155		df-2 12272	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
156	155	breq1i 5145	. . . . . . . . . . . . 13 ⊢ (2 ≤ 𝑁 ↔ (1 + 1) ≤ 𝑁)
157	154, 156	bitr4i 278	. . . . . . . . . . . 12 ⊢ (1 < 𝑁 ↔ 2 ≤ 𝑁)
158		expubnd 14139	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
159	2, 13, 158	mp3an12 1447	. . . . . . . . . . . 12 ⊢ (2 ≤ 𝑁 → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
160	157, 159	sylbi 216	. . . . . . . . . . 11 ⊢ (1 < 𝑁 → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
161		lemul1a 12065	. . . . . . . . . . 11 ⊢ ((((𝑁↑𝐾) ∈ ℝ ∧ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ ∧ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))) ∧ (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
162	152, 160, 161	sylancr 586	. . . . . . . . . 10 ⊢ (1 < 𝑁 → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
163	96	nn0cni 12481	. . . . . . . . . . . 12 ⊢ (2↑𝐾) ∈ ℂ
164	131	recni 11225	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℂ
165	163, 164, 108, 122	mul4i 11408	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
166	120	nn0cni 12481	. . . . . . . . . . . . 13 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℂ
167	164, 166, 68	mulassi 11222	. . . . . . . . . . . 12 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀) = (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀))
168	167	oveq2i 7412	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
169	134	nn0cni 12481	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℂ
170	133	recni 11225	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℂ
171	169, 170, 68	mul12i 11406	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
172	165, 168, 171	3eqtr2i 2758	. . . . . . . . . 10 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
173	162, 172	breqtrdi 5179	. . . . . . . . 9 ⊢ (1 < 𝑁 → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
174	173	adantr 480	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
175	135	nn0ge0i 12496	. . . . . . . . . . . 12 ⊢ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀)
176	136, 175	pm3.2i 470	. . . . . . . . . . 11 ⊢ ((((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ ∧ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀))
177	133, 146, 176	3pm3.2i 1336	. . . . . . . . . 10 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ ∧ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ ∧ ((((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ ∧ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀)))
178		lemul1a 12065	. . . . . . . . . 10 ⊢ ((((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ ∧ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ ∧ ((((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ ∧ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀))) ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
179	177, 178	mpan 687	. . . . . . . . 9 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
180	179	adantl 481	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
181	128, 138, 148, 174, 180	letrd 11368	. . . . . . 7 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
182	163, 108, 68	mul32i 11407	. . . . . . . . 9 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) = (((2↑𝐾) · 𝑀) · 𝑁)
183	182	oveq2i 7412	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁))
184		expp1 14031	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ (𝑀 + 𝐾) ∈ ℕ0) → (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀))
185	68, 139, 184	mp2an 689	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀)
186	13	nn0cni 12481	. . . . . . . . . . . . . . 15 ⊢ 𝐾 ∈ ℂ
187		ax-1cn 11164	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
188	68, 186, 187	addassi 11221	. . . . . . . . . . . . . 14 ⊢ ((𝑀 + 𝐾) + 1) = (𝑀 + (𝐾 + 1))
189	188	oveq2i 7412	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = (𝑀↑(𝑀 + (𝐾 + 1)))
190	185, 189	eqtr3i 2754	. . . . . . . . . . . 12 ⊢ ((𝑀↑(𝑀 + 𝐾)) · 𝑀) = (𝑀↑(𝑀 + (𝐾 + 1)))
191	190	oveq2i 7412	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1))))
192	95	recni 11225	. . . . . . . . . . . 12 ⊢ (2↑(𝐾↑2)) ∈ ℂ
193	141	recni 11225	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℂ
194	192, 163, 193, 68	mul4i 11408	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
195	191, 194	eqtr3i 2754	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
196		facnn2 14239	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
197	1, 196	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)
198	195, 197	oveq12i 7413	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀)) · ((!‘(𝑁 − 1)) · 𝑁))
199	142	recni 11225	. . . . . . . . . 10 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℂ
200	144	nncni 12219	. . . . . . . . . 10 ⊢ (!‘(𝑁 − 1)) ∈ ℂ
201	163, 68	mulcli 11218	. . . . . . . . . 10 ⊢ ((2↑𝐾) · 𝑀) ∈ ℂ
202	199, 200, 201, 108	mul4i 11408	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀)) · ((!‘(𝑁 − 1)) · 𝑁))
203	198, 202	eqtr4i 2755	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁))
204	98	recni 11225	. . . . . . . . 9 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℂ
205	100	nncni 12219	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℂ
206	204, 78, 205	mulassi 11222	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
207	183, 203, 206	3eqtr2i 2758	. . . . . . 7 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
208	181, 207	breqtrdi 5179	. . . . . 6 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
209	124, 208	eqbrtrid 5173	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
210	102	nn0ge0i 12496	. . . . . . . . 9 ⊢ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))
211	103, 210	pm3.2i 470	. . . . . . . 8 ⊢ (((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ ∧ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
212	98, 21, 211	3pm3.2i 1336	. . . . . . 7 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℝ ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ ∧ (((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ ∧ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
213		expadd 14067	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (𝐾↑2) ∈ ℕ0 ∧ 𝐾 ∈ ℕ0) → (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾)))
214	34, 93, 13, 213	mp3an 1457	. . . . . . . 8 ⊢ (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾))
215	19	nn0zi 12584	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℤ
216	13	nn0rei 12480	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℝ
217	16	nnrei 12218	. . . . . . . . . . . . 13 ⊢ (𝐾 + 1) ∈ ℝ
218	17	nn0ge0i 12496	. . . . . . . . . . . . . 14 ⊢ 0 ≤ (𝐾 + 1)
219	217, 218	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1))
220	216, 217, 219	3pm3.2i 1336	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℝ ∧ (𝐾 + 1) ∈ ℝ ∧ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1)))
221	216	ltp1i 12115	. . . . . . . . . . . . 13 ⊢ 𝐾 < (𝐾 + 1)
222	216, 217, 221	ltleii 11334	. . . . . . . . . . . 12 ⊢ 𝐾 ≤ (𝐾 + 1)
223		lemul1a 12065	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ ℝ ∧ (𝐾 + 1) ∈ ℝ ∧ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1))) ∧ 𝐾 ≤ (𝐾 + 1)) → (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1)))
224	220, 222, 223	mp2an 689	. . . . . . . . . . 11 ⊢ (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1))
225	186	sqvali 14141	. . . . . . . . . . . . 13 ⊢ (𝐾↑2) = (𝐾 · 𝐾)
226	186	mulridi 11215	. . . . . . . . . . . . . 14 ⊢ (𝐾 · 1) = 𝐾
227	226	eqcomi 2733	. . . . . . . . . . . . 13 ⊢ 𝐾 = (𝐾 · 1)
228	225, 227	oveq12i 7413	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) = ((𝐾 · 𝐾) + (𝐾 · 1))
229	186, 186, 187	adddii 11223	. . . . . . . . . . . 12 ⊢ (𝐾 · (𝐾 + 1)) = ((𝐾 · 𝐾) + (𝐾 · 1))
230	228, 229	eqtr4i 2755	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) = (𝐾 · (𝐾 + 1))
231	16	nncni 12219	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℂ
232	231	sqvali 14141	. . . . . . . . . . 11 ⊢ ((𝐾 + 1)↑2) = ((𝐾 + 1) · (𝐾 + 1))
233	224, 230, 232	3brtr4i 5168	. . . . . . . . . 10 ⊢ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)
234	93, 13	nn0addcli 12506	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) ∈ ℕ0
235	234	nn0zi 12584	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) ∈ ℤ
236	235	eluz1i 12827	. . . . . . . . . 10 ⊢ (((𝐾 + 1)↑2) ∈ (ℤ≥‘((𝐾↑2) + 𝐾)) ↔ (((𝐾 + 1)↑2) ∈ ℤ ∧ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)))
237	215, 233, 236	mpbir2an 708	. . . . . . . . 9 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ≥‘((𝐾↑2) + 𝐾))
238		leexp2a 14134	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝐾 + 1)↑2) ∈ (ℤ≥‘((𝐾↑2) + 𝐾))) → (2↑((𝐾↑2) + 𝐾)) ≤ (2↑((𝐾 + 1)↑2)))
239	12, 37, 237, 238	mp3an 1457	. . . . . . . 8 ⊢ (2↑((𝐾↑2) + 𝐾)) ≤ (2↑((𝐾 + 1)↑2))
240	214, 239	eqbrtrri 5161	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ≤ (2↑((𝐾 + 1)↑2))
241		lemul1a 12065	. . . . . . 7 ⊢ (((((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 689	. . . . . 6 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ≤ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
243	242	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ≤ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
244	92, 105, 107, 209, 243	letrd 11368	. . . 4 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
245	77, 78, 205	mulassi 11222	. . . 4 ⊢ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
246	244, 245	breqtrrdi 5180	. . 3 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
247	85, 246	jaoian 953	. 2 ⊢ (((𝑁 ≤ 1 ∨ 1 < 𝑁) ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
248	5, 247	mpan 687	1 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   class class class wbr 5138  ‘cfv 6533  (class class class)co 7401  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11245   ≤ cle 11246   − cmin 11441  ℕcn 12209  2c2 12264  ℕ₀cn0 12469  ℤcz 12555  ℤ_≥cuz 12819  ↑cexp 14024  !cfa 14230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-n0 12470  df-z 12556  df-uz 12820  df-rp 12972  df-seq 13964  df-exp 14025  df-fac 14231

This theorem is referenced by:  faclbnd4lem2  14251