faclbnd4lem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > faclbnd4lem1		Structured version Visualization version GIF version

Theorem faclbnd4lem1 14240

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

**Hypotheses**
Ref	Expression
faclbnd4lem1.1	⊢ 𝑁 ∈ ℕ
faclbnd4lem1.2	⊢ 𝐾 ∈ ℕ₀
faclbnd4lem1.3	⊢ 𝑀 ∈ ℕ₀

**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 12208	. . 3 ⊢ 𝑁 ∈ ℝ
3		1re 11201	. . 3 ⊢ 1 ∈ ℝ
4		lelttric 11308	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 ≤ 1 ∨ 1 < 𝑁))
5	2, 3, 4	mp2an 691	. 2 ⊢ (𝑁 ≤ 1 ∨ 1 < 𝑁)
6		nnge1 12227	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
7	1, 6	ax-mp 5	. . . . . 6 ⊢ 1 ≤ 𝑁
8	2, 3	letri3i 11317	. . . . . 6 ⊢ (𝑁 = 1 ↔ (𝑁 ≤ 1 ∧ 1 ≤ 𝑁))
9	7, 8	mpbiran2 709	. . . . 5 ⊢ (𝑁 = 1 ↔ 𝑁 ≤ 1)
10		0le1 11724	. . . . . . . . . 10 ⊢ 0 ≤ 1
11	3, 10	pm3.2i 472	. . . . . . . . 9 ⊢ (1 ∈ ℝ ∧ 0 ≤ 1)
12		2re 12273	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
13		faclbnd4lem1.2	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℕ₀
14		1nn 12210	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
15		nn0nnaddcl 12490	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 1 ∈ ℕ) → (𝐾 + 1) ∈ ℕ)
16	13, 14, 15	mp2an 691	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℕ
17	16	nnnn0i 12467	. . . . . . . . . . 11 ⊢ (𝐾 + 1) ∈ ℕ₀
18		2nn0 12476	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
19	17, 18	nn0expcli 14041	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℕ₀
20		reexpcl 14031	. . . . . . . . . 10 ⊢ ((2 ∈ ℝ ∧ ((𝐾 + 1)↑2) ∈ ℕ₀) → (2↑((𝐾 + 1)↑2)) ∈ ℝ)
21	12, 19, 20	mp2an 691	. . . . . . . . 9 ⊢ (2↑((𝐾 + 1)↑2)) ∈ ℝ
22	11, 21	pm3.2i 472	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ)
23		faclbnd4lem1.3	. . . . . . . . . . 11 ⊢ 𝑀 ∈ ℕ₀
24	23	nn0rei 12470	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℝ
25	23	nn0ge0i 12486	. . . . . . . . . 10 ⊢ 0 ≤ 𝑀
26	24, 25	pm3.2i 472	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀)
27		nn0nnaddcl 12490	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ₀ ∧ (𝐾 + 1) ∈ ℕ) → (𝑀 + (𝐾 + 1)) ∈ ℕ)
28	23, 16, 27	mp2an 691	. . . . . . . . . . . 12 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ
29	28	nnnn0i 12467	. . . . . . . . . . 11 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ₀
30	23, 29	nn0expcli 14041	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℕ₀
31	30	nn0rei 12470	. . . . . . . . 9 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ
32	26, 31	pm3.2i 472	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ)
33	22, 32	pm3.2i 472	. . . . . . 7 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ) ∧ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ))
34		2cn 12274	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
35		exp0 14018	. . . . . . . . . 10 ⊢ (2 ∈ ℂ → (2↑0) = 1)
36	34, 35	ax-mp 5	. . . . . . . . 9 ⊢ (2↑0) = 1
37		1le2 12408	. . . . . . . . . 10 ⊢ 1 ≤ 2
38		nn0uz 12851	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
39	19, 38	eleqtri 2832	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘0)
40		leexp2a 14124	. . . . . . . . . 10 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘0)) → (2↑0) ≤ (2↑((𝐾 + 1)↑2)))
41	12, 37, 39, 40	mp3an 1462	. . . . . . . . 9 ⊢ (2↑0) ≤ (2↑((𝐾 + 1)↑2))
42	36, 41	eqbrtrri 5167	. . . . . . . 8 ⊢ 1 ≤ (2↑((𝐾 + 1)↑2))
43		elnn0 12461	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ₀ ↔ (𝑀 ∈ ℕ ∨ 𝑀 = 0))
44		nncn 12207	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
45	44	exp1d 14093	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑀↑1) = 𝑀)
46		nnge1 12227	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
47		nnuz 12852	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
48	28, 47	eleqtri 2832	. . . . . . . . . . . . . 14 ⊢ (𝑀 + (𝐾 + 1)) ∈ (ℤ_≥‘1)
49		leexp2a 14124	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℝ ∧ 1 ≤ 𝑀 ∧ (𝑀 + (𝐾 + 1)) ∈ (ℤ_≥‘1)) → (𝑀↑1) ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
50	24, 48, 49	mp3an13 1453	. . . . . . . . . . . . 13 ⊢ (1 ≤ 𝑀 → (𝑀↑1) ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
51	46, 50	syl 17	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑀↑1) ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
52	45, 51	eqbrtrrd 5168	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
53	30	nn0ge0i 12486	. . . . . . . . . . . 12 ⊢ 0 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))
54		breq1 5147	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))) ↔ 0 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))))
55	53, 54	mpbiri 258	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
56	52, 55	jaoi 856	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
57	43, 56	sylbi 216	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
58	23, 57	ax-mp 5	. . . . . . . 8 ⊢ 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))
59	42, 58	pm3.2i 472	. . . . . . 7 ⊢ (1 ≤ (2↑((𝐾 + 1)↑2)) ∧ 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
60		lemul12a 12059	. . . . . . 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 7403	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑁↑(𝐾 + 1)) = (1↑(𝐾 + 1)))
63	16	nnzi 12573	. . . . . . . . . 10 ⊢ (𝐾 + 1) ∈ ℤ
64		1exp 14044	. . . . . . . . . 10 ⊢ ((𝐾 + 1) ∈ ℤ → (1↑(𝐾 + 1)) = 1)
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (1↑(𝐾 + 1)) = 1
66	62, 65	eqtrdi 2789	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝑁↑(𝐾 + 1)) = 1)
67		oveq2 7404	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = (𝑀↑1))
68	23	nn0cni 12471	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℂ
69		exp1 14020	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℂ → (𝑀↑1) = 𝑀)
70	68, 69	ax-mp 5	. . . . . . . . 9 ⊢ (𝑀↑1) = 𝑀
71	67, 70	eqtrdi 2789	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = 𝑀)
72	66, 71	oveq12d 7414	. . . . . . 7 ⊢ (𝑁 = 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (1 · 𝑀))
73		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (!‘𝑁) = (!‘1))
74		fac1 14224	. . . . . . . . . 10 ⊢ (!‘1) = 1
75	73, 74	eqtrdi 2789	. . . . . . . . 9 ⊢ (𝑁 = 1 → (!‘𝑁) = 1)
76	75	oveq2d 7412	. . . . . . . 8 ⊢ (𝑁 = 1 → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · 1))
77	21	recni 11215	. . . . . . . . . 10 ⊢ (2↑((𝐾 + 1)↑2)) ∈ ℂ
78	30	nn0cni 12471	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℂ
79	77, 78	mulcli 11208	. . . . . . . . 9 ⊢ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) ∈ ℂ
80	79	mulridi 11205	. . . . . . . 8 ⊢ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · 1) = ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1))))
81	76, 80	eqtrdi 2789	. . . . . . 7 ⊢ (𝑁 = 1 → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))))
82	72, 81	breq12d 5157	. . . . . 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 482	. . 3 ⊢ ((𝑁 ≤ 1 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
86		reexpcl 14031	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ (𝐾 + 1) ∈ ℕ₀) → (𝑁↑(𝐾 + 1)) ∈ ℝ)
87	2, 17, 86	mp2an 691	. . . . . . 7 ⊢ (𝑁↑(𝐾 + 1)) ∈ ℝ
88	1	nnnn0i 12467	. . . . . . . 8 ⊢ 𝑁 ∈ ℕ₀
89		reexpcl 14031	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ₀) → (𝑀↑𝑁) ∈ ℝ)
90	24, 88, 89	mp2an 691	. . . . . . 7 ⊢ (𝑀↑𝑁) ∈ ℝ
91	87, 90	remulcli 11217	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ
92	91	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ)
93	13, 18	nn0expcli 14041	. . . . . . . . 9 ⊢ (𝐾↑2) ∈ ℕ₀
94		reexpcl 14031	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (𝐾↑2) ∈ ℕ₀) → (2↑(𝐾↑2)) ∈ ℝ)
95	12, 93, 94	mp2an 691	. . . . . . . 8 ⊢ (2↑(𝐾↑2)) ∈ ℝ
96	18, 13	nn0expcli 14041	. . . . . . . . 9 ⊢ (2↑𝐾) ∈ ℕ₀
97	96	nn0rei 12470	. . . . . . . 8 ⊢ (2↑𝐾) ∈ ℝ
98	95, 97	remulcli 11217	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℝ
99		faccl 14230	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (!‘𝑁) ∈ ℕ)
100	88, 99	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) ∈ ℕ
101	100	nnnn0i 12467	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℕ₀
102	30, 101	nn0mulcli 12497	. . . . . . . 8 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℕ₀
103	102	nn0rei 12470	. . . . . . 7 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ
104	98, 103	remulcli 11217	. . . . . 6 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
105	104	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
106	21, 103	remulcli 11217	. . . . . 6 ⊢ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
107	106	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
108	1	nncni 12209	. . . . . . . . 9 ⊢ 𝑁 ∈ ℂ
109		expp1 14021	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 𝐾 ∈ ℕ₀) → (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁))
110	108, 13, 109	mp2an 691	. . . . . . . 8 ⊢ (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁)
111		expm1t 14043	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀))
112	68, 1, 111	mp2an 691	. . . . . . . 8 ⊢ (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀)
113	110, 112	oveq12i 7408	. . . . . . 7 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀))
114		reexpcl 14031	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ₀) → (𝑁↑𝐾) ∈ ℝ)
115	2, 13, 114	mp2an 691	. . . . . . . . 9 ⊢ (𝑁↑𝐾) ∈ ℝ
116	115	recni 11215	. . . . . . . 8 ⊢ (𝑁↑𝐾) ∈ ℂ
117		elnnnn0 12502	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ₀))
118	1, 117	mpbi 229	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ₀)
119	118	simpri 487	. . . . . . . . . . 11 ⊢ (𝑁 − 1) ∈ ℕ₀
120	23, 119	nn0expcli 14041	. . . . . . . . . 10 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℕ₀
121	120, 23	nn0mulcli 12497	. . . . . . . . 9 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℕ₀
122	121	nn0cni 12471	. . . . . . . 8 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℂ
123	116, 108, 122	mulassi 11212	. . . . . . 7 ⊢ (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
124	113, 123	eqtri 2761	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
125	88, 121	nn0mulcli 12497	. . . . . . . . . . 11 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℕ₀
126	125	nn0rei 12470	. . . . . . . . . 10 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ
127	115, 126	remulcli 11217	. . . . . . . . 9 ⊢ ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ)
129	119	nn0rei 12470	. . . . . . . . . . . 12 ⊢ (𝑁 − 1) ∈ ℝ
130		reexpcl 14031	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝐾 ∈ ℕ₀) → ((𝑁 − 1)↑𝐾) ∈ ℝ)
131	129, 13, 130	mp2an 691	. . . . . . . . . . 11 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℝ
132	120	nn0rei 12470	. . . . . . . . . . 11 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℝ
133	131, 132	remulcli 11217	. . . . . . . . . 10 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ
134	96, 88	nn0mulcli 12497	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℕ₀
135	134, 23	nn0mulcli 12497	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℕ₀
136	135	nn0rei 12470	. . . . . . . . . 10 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ
137	133, 136	remulcli 11217	. . . . . . . . 9 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
138	137	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
139	23, 13	nn0addcli 12496	. . . . . . . . . . . . 13 ⊢ (𝑀 + 𝐾) ∈ ℕ₀
140		reexpcl 14031	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ (𝑀 + 𝐾) ∈ ℕ₀) → (𝑀↑(𝑀 + 𝐾)) ∈ ℝ)
141	24, 139, 140	mp2an 691	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℝ
142	95, 141	remulcli 11217	. . . . . . . . . . 11 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℝ
143		faccl 14230	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℕ₀ → (!‘(𝑁 − 1)) ∈ ℕ)
144	119, 143	ax-mp 5	. . . . . . . . . . . 12 ⊢ (!‘(𝑁 − 1)) ∈ ℕ
145	144	nnrei 12208	. . . . . . . . . . 11 ⊢ (!‘(𝑁 − 1)) ∈ ℝ
146	142, 145	remulcli 11217	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ
147	146, 136	remulcli 11217	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
148	147	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
149	97, 131	remulcli 11217	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ
150	125	nn0ge0i 12486	. . . . . . . . . . . . 13 ⊢ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))
151	126, 150	pm3.2i 472	. . . . . . . . . . . 12 ⊢ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
152	115, 149, 151	3pm3.2i 1340	. . . . . . . . . . 11 ⊢ ((𝑁↑𝐾) ∈ ℝ ∧ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ ∧ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
153		nnltp1le 12605	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁))
154	14, 1, 153	mp2an 691	. . . . . . . . . . . . 13 ⊢ (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁)
155		df-2 12262	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
156	155	breq1i 5151	. . . . . . . . . . . . 13 ⊢ (2 ≤ 𝑁 ↔ (1 + 1) ≤ 𝑁)
157	154, 156	bitr4i 278	. . . . . . . . . . . 12 ⊢ (1 < 𝑁 ↔ 2 ≤ 𝑁)
158		expubnd 14129	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ₀ ∧ 2 ≤ 𝑁) → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
159	2, 13, 158	mp3an12 1452	. . . . . . . . . . . 12 ⊢ (2 ≤ 𝑁 → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
160	157, 159	sylbi 216	. . . . . . . . . . 11 ⊢ (1 < 𝑁 → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
161		lemul1a 12055	. . . . . . . . . . 11 ⊢ ((((𝑁↑𝐾) ∈ ℝ ∧ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ ∧ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))) ∧ (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
162	152, 160, 161	sylancr 588	. . . . . . . . . 10 ⊢ (1 < 𝑁 → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
163	96	nn0cni 12471	. . . . . . . . . . . 12 ⊢ (2↑𝐾) ∈ ℂ
164	131	recni 11215	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℂ
165	163, 164, 108, 122	mul4i 11398	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
166	120	nn0cni 12471	. . . . . . . . . . . . 13 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℂ
167	164, 166, 68	mulassi 11212	. . . . . . . . . . . 12 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀) = (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀))
168	167	oveq2i 7407	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
169	134	nn0cni 12471	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℂ
170	133	recni 11215	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℂ
171	169, 170, 68	mul12i 11396	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
172	165, 168, 171	3eqtr2i 2767	. . . . . . . . . 10 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
173	162, 172	breqtrdi 5185	. . . . . . . . 9 ⊢ (1 < 𝑁 → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
174	173	adantr 482	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
175	135	nn0ge0i 12486	. . . . . . . . . . . 12 ⊢ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀)
176	136, 175	pm3.2i 472	. . . . . . . . . . 11 ⊢ ((((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ ∧ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀))
177	133, 146, 176	3pm3.2i 1340	. . . . . . . . . 10 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ ∧ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ ∧ ((((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ ∧ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀)))
178		lemul1a 12055	. . . . . . . . . 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 689	. . . . . . . . 9 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
180	179	adantl 483	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
181	128, 138, 148, 174, 180	letrd 11358	. . . . . . 7 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
182	163, 108, 68	mul32i 11397	. . . . . . . . 9 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) = (((2↑𝐾) · 𝑀) · 𝑁)
183	182	oveq2i 7407	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁))
184		expp1 14021	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ (𝑀 + 𝐾) ∈ ℕ₀) → (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀))
185	68, 139, 184	mp2an 691	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀)
186	13	nn0cni 12471	. . . . . . . . . . . . . . 15 ⊢ 𝐾 ∈ ℂ
187		ax-1cn 11155	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
188	68, 186, 187	addassi 11211	. . . . . . . . . . . . . 14 ⊢ ((𝑀 + 𝐾) + 1) = (𝑀 + (𝐾 + 1))
189	188	oveq2i 7407	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = (𝑀↑(𝑀 + (𝐾 + 1)))
190	185, 189	eqtr3i 2763	. . . . . . . . . . . 12 ⊢ ((𝑀↑(𝑀 + 𝐾)) · 𝑀) = (𝑀↑(𝑀 + (𝐾 + 1)))
191	190	oveq2i 7407	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1))))
192	95	recni 11215	. . . . . . . . . . . 12 ⊢ (2↑(𝐾↑2)) ∈ ℂ
193	141	recni 11215	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℂ
194	192, 163, 193, 68	mul4i 11398	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
195	191, 194	eqtr3i 2763	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
196		facnn2 14229	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
197	1, 196	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)
198	195, 197	oveq12i 7408	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀)) · ((!‘(𝑁 − 1)) · 𝑁))
199	142	recni 11215	. . . . . . . . . 10 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℂ
200	144	nncni 12209	. . . . . . . . . 10 ⊢ (!‘(𝑁 − 1)) ∈ ℂ
201	163, 68	mulcli 11208	. . . . . . . . . 10 ⊢ ((2↑𝐾) · 𝑀) ∈ ℂ
202	199, 200, 201, 108	mul4i 11398	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀)) · ((!‘(𝑁 − 1)) · 𝑁))
203	198, 202	eqtr4i 2764	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁))
204	98	recni 11215	. . . . . . . . 9 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℂ
205	100	nncni 12209	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℂ
206	204, 78, 205	mulassi 11212	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
207	183, 203, 206	3eqtr2i 2767	. . . . . . 7 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
208	181, 207	breqtrdi 5185	. . . . . 6 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
209	124, 208	eqbrtrid 5179	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
210	102	nn0ge0i 12486	. . . . . . . . 9 ⊢ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))
211	103, 210	pm3.2i 472	. . . . . . . 8 ⊢ (((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ ∧ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
212	98, 21, 211	3pm3.2i 1340	. . . . . . 7 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℝ ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ ∧ (((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ ∧ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
213		expadd 14057	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (𝐾↑2) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ₀) → (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾)))
214	34, 93, 13, 213	mp3an 1462	. . . . . . . 8 ⊢ (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾))
215	19	nn0zi 12574	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℤ
216	13	nn0rei 12470	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℝ
217	16	nnrei 12208	. . . . . . . . . . . . 13 ⊢ (𝐾 + 1) ∈ ℝ
218	17	nn0ge0i 12486	. . . . . . . . . . . . . 14 ⊢ 0 ≤ (𝐾 + 1)
219	217, 218	pm3.2i 472	. . . . . . . . . . . . 13 ⊢ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1))
220	216, 217, 219	3pm3.2i 1340	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℝ ∧ (𝐾 + 1) ∈ ℝ ∧ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1)))
221	216	ltp1i 12105	. . . . . . . . . . . . 13 ⊢ 𝐾 < (𝐾 + 1)
222	216, 217, 221	ltleii 11324	. . . . . . . . . . . 12 ⊢ 𝐾 ≤ (𝐾 + 1)
223		lemul1a 12055	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ ℝ ∧ (𝐾 + 1) ∈ ℝ ∧ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1))) ∧ 𝐾 ≤ (𝐾 + 1)) → (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1)))
224	220, 222, 223	mp2an 691	. . . . . . . . . . 11 ⊢ (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1))
225	186	sqvali 14131	. . . . . . . . . . . . 13 ⊢ (𝐾↑2) = (𝐾 · 𝐾)
226	186	mulridi 11205	. . . . . . . . . . . . . 14 ⊢ (𝐾 · 1) = 𝐾
227	226	eqcomi 2742	. . . . . . . . . . . . 13 ⊢ 𝐾 = (𝐾 · 1)
228	225, 227	oveq12i 7408	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) = ((𝐾 · 𝐾) + (𝐾 · 1))
229	186, 186, 187	adddii 11213	. . . . . . . . . . . 12 ⊢ (𝐾 · (𝐾 + 1)) = ((𝐾 · 𝐾) + (𝐾 · 1))
230	228, 229	eqtr4i 2764	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) = (𝐾 · (𝐾 + 1))
231	16	nncni 12209	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℂ
232	231	sqvali 14131	. . . . . . . . . . 11 ⊢ ((𝐾 + 1)↑2) = ((𝐾 + 1) · (𝐾 + 1))
233	224, 230, 232	3brtr4i 5174	. . . . . . . . . 10 ⊢ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)
234	93, 13	nn0addcli 12496	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) ∈ ℕ₀
235	234	nn0zi 12574	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) ∈ ℤ
236	235	eluz1i 12817	. . . . . . . . . 10 ⊢ (((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾)) ↔ (((𝐾 + 1)↑2) ∈ ℤ ∧ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)))
237	215, 233, 236	mpbir2an 710	. . . . . . . . 9 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾))
238		leexp2a 14124	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾))) → (2↑((𝐾↑2) + 𝐾)) ≤ (2↑((𝐾 + 1)↑2)))
239	12, 37, 237, 238	mp3an 1462	. . . . . . . 8 ⊢ (2↑((𝐾↑2) + 𝐾)) ≤ (2↑((𝐾 + 1)↑2))
240	214, 239	eqbrtrri 5167	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ≤ (2↑((𝐾 + 1)↑2))
241		lemul1a 12055	. . . . . . 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 691	. . . . . 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 11358	. . . 4 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
245	77, 78, 205	mulassi 11212	. . . 4 ⊢ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
246	244, 245	breqtrrdi 5186	. . 3 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
247	85, 246	jaoian 956	. 2 ⊢ (((𝑁 ≤ 1 ∨ 1 < 𝑁) ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
248	5, 247	mpan 689	1 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 class class class wbr 5144 ‘cfv 6535 (class class class)co 7396 ℂcc 11095 ℝcr 11096 0cc0 11097 1c1 11098 + caddc 11100 · cmul 11102 < clt 11235 ≤ cle 11236 − cmin 11431 ℕcn 12199 2c2 12254 ℕ₀cn0 12459 ℤcz 12545 ℤ_≥cuz 12809 ↑cexp 14014 !cfa 14220

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5295 ax-nul 5302 ax-pow 5359 ax-pr 5423 ax-un 7712 ax-cnex 11153 ax-resscn 11154 ax-1cn 11155 ax-icn 11156 ax-addcl 11157 ax-addrcl 11158 ax-mulcl 11159 ax-mulrcl 11160 ax-mulcom 11161 ax-addass 11162 ax-mulass 11163 ax-distr 11164 ax-i2m1 11165 ax-1ne0 11166 ax-1rid 11167 ax-rnegex 11168 ax-rrecex 11169 ax-cnre 11170 ax-pre-lttri 11171 ax-pre-lttrn 11172 ax-pre-ltadd 11173 ax-pre-mulgt0 11174

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3965 df-nul 4321 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4905 df-iun 4995 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6292 df-ord 6359 df-on 6360 df-lim 6361 df-suc 6362 df-iota 6487 df-fun 6537 df-fn 6538 df-f 6539 df-f1 6540 df-fo 6541 df-f1o 6542 df-fv 6543 df-riota 7352 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7843 df-2nd 7963 df-frecs 8253 df-wrecs 8284 df-recs 8358 df-rdg 8397 df-er 8691 df-en 8928 df-dom 8929 df-sdom 8930 df-pnf 11237 df-mnf 11238 df-xr 11239 df-ltxr 11240 df-le 11241 df-sub 11433 df-neg 11434 df-div 11859 df-nn 12200 df-2 12262 df-n0 12460 df-z 12546 df-uz 12810 df-rp 12962 df-seq 13954 df-exp 14015 df-fac 14221

This theorem is referenced by: faclbnd4lem2 14241

W3C validator