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 13647

Description: Lemma for faclbnd4 13651. 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 11641	. . 3 ⊢ 𝑁 ∈ ℝ
3		1re 10635	. . 3 ⊢ 1 ∈ ℝ
4		lelttric 10741	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 ≤ 1 ∨ 1 < 𝑁))
5	2, 3, 4	mp2an 690	. 2 ⊢ (𝑁 ≤ 1 ∨ 1 < 𝑁)
6		nnge1 11659	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
7	1, 6	ax-mp 5	. . . . . 6 ⊢ 1 ≤ 𝑁
8	2, 3	letri3i 10750	. . . . . 6 ⊢ (𝑁 = 1 ↔ (𝑁 ≤ 1 ∧ 1 ≤ 𝑁))
9	7, 8	mpbiran2 708	. . . . 5 ⊢ (𝑁 = 1 ↔ 𝑁 ≤ 1)
10		0le1 11157	. . . . . . . . . 10 ⊢ 0 ≤ 1
11	3, 10	pm3.2i 473	. . . . . . . . 9 ⊢ (1 ∈ ℝ ∧ 0 ≤ 1)
12		2re 11705	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
13		faclbnd4lem1.2	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℕ₀
14		1nn 11643	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
15		nn0nnaddcl 11922	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 1 ∈ ℕ) → (𝐾 + 1) ∈ ℕ)
16	13, 14, 15	mp2an 690	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℕ
17	16	nnnn0i 11899	. . . . . . . . . . 11 ⊢ (𝐾 + 1) ∈ ℕ₀
18		2nn0 11908	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
19	17, 18	nn0expcli 13449	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℕ₀
20		reexpcl 13440	. . . . . . . . . 10 ⊢ ((2 ∈ ℝ ∧ ((𝐾 + 1)↑2) ∈ ℕ₀) → (2↑((𝐾 + 1)↑2)) ∈ ℝ)
21	12, 19, 20	mp2an 690	. . . . . . . . 9 ⊢ (2↑((𝐾 + 1)↑2)) ∈ ℝ
22	11, 21	pm3.2i 473	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ)
23		faclbnd4lem1.3	. . . . . . . . . . 11 ⊢ 𝑀 ∈ ℕ₀
24	23	nn0rei 11902	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℝ
25	23	nn0ge0i 11918	. . . . . . . . . 10 ⊢ 0 ≤ 𝑀
26	24, 25	pm3.2i 473	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀)
27		nn0nnaddcl 11922	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ₀ ∧ (𝐾 + 1) ∈ ℕ) → (𝑀 + (𝐾 + 1)) ∈ ℕ)
28	23, 16, 27	mp2an 690	. . . . . . . . . . . 12 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ
29	28	nnnn0i 11899	. . . . . . . . . . 11 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ₀
30	23, 29	nn0expcli 13449	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℕ₀
31	30	nn0rei 11902	. . . . . . . . 9 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ
32	26, 31	pm3.2i 473	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ)
33	22, 32	pm3.2i 473	. . . . . . 7 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ) ∧ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ))
34		2cn 11706	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
35		exp0 13427	. . . . . . . . . 10 ⊢ (2 ∈ ℂ → (2↑0) = 1)
36	34, 35	ax-mp 5	. . . . . . . . 9 ⊢ (2↑0) = 1
37		1le2 11840	. . . . . . . . . 10 ⊢ 1 ≤ 2
38		nn0uz 12274	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
39	19, 38	eleqtri 2911	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘0)
40		leexp2a 13530	. . . . . . . . . 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 5081	. . . . . . . 8 ⊢ 1 ≤ (2↑((𝐾 + 1)↑2))
43		elnn0 11893	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ₀ ↔ (𝑀 ∈ ℕ ∨ 𝑀 = 0))
44		nncn 11640	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
45	44	exp1d 13499	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑀↑1) = 𝑀)
46		nnge1 11659	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
47		nnuz 12275	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
48	28, 47	eleqtri 2911	. . . . . . . . . . . . . 14 ⊢ (𝑀 + (𝐾 + 1)) ∈ (ℤ_≥‘1)
49		leexp2a 13530	. . . . . . . . . . . . . 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 5082	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
53	30	nn0ge0i 11918	. . . . . . . . . . . 12 ⊢ 0 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))
54		breq1 5061	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))) ↔ 0 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))))
55	53, 54	mpbiri 260	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
56	52, 55	jaoi 853	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
57	43, 56	sylbi 219	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
58	23, 57	ax-mp 5	. . . . . . . 8 ⊢ 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))
59	42, 58	pm3.2i 473	. . . . . . 7 ⊢ (1 ≤ (2↑((𝐾 + 1)↑2)) ∧ 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
60		lemul12a 11492	. . . . . . 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 7157	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑁↑(𝐾 + 1)) = (1↑(𝐾 + 1)))
63	16	nnzi 12000	. . . . . . . . . 10 ⊢ (𝐾 + 1) ∈ ℤ
64		1exp 13452	. . . . . . . . . 10 ⊢ ((𝐾 + 1) ∈ ℤ → (1↑(𝐾 + 1)) = 1)
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (1↑(𝐾 + 1)) = 1
66	62, 65	syl6eq 2872	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝑁↑(𝐾 + 1)) = 1)
67		oveq2 7158	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = (𝑀↑1))
68	23	nn0cni 11903	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℂ
69		exp1 13429	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℂ → (𝑀↑1) = 𝑀)
70	68, 69	ax-mp 5	. . . . . . . . 9 ⊢ (𝑀↑1) = 𝑀
71	67, 70	syl6eq 2872	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = 𝑀)
72	66, 71	oveq12d 7168	. . . . . . 7 ⊢ (𝑁 = 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (1 · 𝑀))
73		fveq2 6664	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (!‘𝑁) = (!‘1))
74		fac1 13631	. . . . . . . . . 10 ⊢ (!‘1) = 1
75	73, 74	syl6eq 2872	. . . . . . . . 9 ⊢ (𝑁 = 1 → (!‘𝑁) = 1)
76	75	oveq2d 7166	. . . . . . . 8 ⊢ (𝑁 = 1 → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · 1))
77	21	recni 10649	. . . . . . . . . 10 ⊢ (2↑((𝐾 + 1)↑2)) ∈ ℂ
78	30	nn0cni 11903	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℂ
79	77, 78	mulcli 10642	. . . . . . . . 9 ⊢ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) ∈ ℂ
80	79	mulid1i 10639	. . . . . . . 8 ⊢ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · 1) = ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1))))
81	76, 80	syl6eq 2872	. . . . . . 7 ⊢ (𝑁 = 1 → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))))
82	72, 81	breq12d 5071	. . . . . 6 ⊢ (𝑁 = 1 → (((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) ↔ (1 · 𝑀) ≤ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1))))))
83	61, 82	mpbiri 260	. . . . 5 ⊢ (𝑁 = 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
84	9, 83	sylbir 237	. . . 4 ⊢ (𝑁 ≤ 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
85	84	adantr 483	. . 3 ⊢ ((𝑁 ≤ 1 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
86		reexpcl 13440	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ (𝐾 + 1) ∈ ℕ₀) → (𝑁↑(𝐾 + 1)) ∈ ℝ)
87	2, 17, 86	mp2an 690	. . . . . . 7 ⊢ (𝑁↑(𝐾 + 1)) ∈ ℝ
88	1	nnnn0i 11899	. . . . . . . 8 ⊢ 𝑁 ∈ ℕ₀
89		reexpcl 13440	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ₀) → (𝑀↑𝑁) ∈ ℝ)
90	24, 88, 89	mp2an 690	. . . . . . 7 ⊢ (𝑀↑𝑁) ∈ ℝ
91	87, 90	remulcli 10651	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ
92	91	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ)
93	13, 18	nn0expcli 13449	. . . . . . . . 9 ⊢ (𝐾↑2) ∈ ℕ₀
94		reexpcl 13440	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (𝐾↑2) ∈ ℕ₀) → (2↑(𝐾↑2)) ∈ ℝ)
95	12, 93, 94	mp2an 690	. . . . . . . 8 ⊢ (2↑(𝐾↑2)) ∈ ℝ
96	18, 13	nn0expcli 13449	. . . . . . . . 9 ⊢ (2↑𝐾) ∈ ℕ₀
97	96	nn0rei 11902	. . . . . . . 8 ⊢ (2↑𝐾) ∈ ℝ
98	95, 97	remulcli 10651	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℝ
99		faccl 13637	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (!‘𝑁) ∈ ℕ)
100	88, 99	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) ∈ ℕ
101	100	nnnn0i 11899	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℕ₀
102	30, 101	nn0mulcli 11929	. . . . . . . 8 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℕ₀
103	102	nn0rei 11902	. . . . . . 7 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ
104	98, 103	remulcli 10651	. . . . . 6 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
105	104	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
106	21, 103	remulcli 10651	. . . . . 6 ⊢ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
107	106	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
108	1	nncni 11642	. . . . . . . . 9 ⊢ 𝑁 ∈ ℂ
109		expp1 13430	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 𝐾 ∈ ℕ₀) → (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁))
110	108, 13, 109	mp2an 690	. . . . . . . 8 ⊢ (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁)
111		expm1t 13451	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀))
112	68, 1, 111	mp2an 690	. . . . . . . 8 ⊢ (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀)
113	110, 112	oveq12i 7162	. . . . . . 7 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀))
114		reexpcl 13440	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ₀) → (𝑁↑𝐾) ∈ ℝ)
115	2, 13, 114	mp2an 690	. . . . . . . . 9 ⊢ (𝑁↑𝐾) ∈ ℝ
116	115	recni 10649	. . . . . . . 8 ⊢ (𝑁↑𝐾) ∈ ℂ
117		elnnnn0 11934	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ₀))
118	1, 117	mpbi 232	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ₀)
119	118	simpri 488	. . . . . . . . . . 11 ⊢ (𝑁 − 1) ∈ ℕ₀
120	23, 119	nn0expcli 13449	. . . . . . . . . 10 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℕ₀
121	120, 23	nn0mulcli 11929	. . . . . . . . 9 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℕ₀
122	121	nn0cni 11903	. . . . . . . 8 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℂ
123	116, 108, 122	mulassi 10646	. . . . . . 7 ⊢ (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
124	113, 123	eqtri 2844	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
125	88, 121	nn0mulcli 11929	. . . . . . . . . . 11 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℕ₀
126	125	nn0rei 11902	. . . . . . . . . 10 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ
127	115, 126	remulcli 10651	. . . . . . . . 9 ⊢ ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ)
129	119	nn0rei 11902	. . . . . . . . . . . 12 ⊢ (𝑁 − 1) ∈ ℝ
130		reexpcl 13440	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝐾 ∈ ℕ₀) → ((𝑁 − 1)↑𝐾) ∈ ℝ)
131	129, 13, 130	mp2an 690	. . . . . . . . . . 11 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℝ
132	120	nn0rei 11902	. . . . . . . . . . 11 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℝ
133	131, 132	remulcli 10651	. . . . . . . . . 10 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ
134	96, 88	nn0mulcli 11929	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℕ₀
135	134, 23	nn0mulcli 11929	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℕ₀
136	135	nn0rei 11902	. . . . . . . . . 10 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ
137	133, 136	remulcli 10651	. . . . . . . . 9 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
138	137	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
139	23, 13	nn0addcli 11928	. . . . . . . . . . . . 13 ⊢ (𝑀 + 𝐾) ∈ ℕ₀
140		reexpcl 13440	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ (𝑀 + 𝐾) ∈ ℕ₀) → (𝑀↑(𝑀 + 𝐾)) ∈ ℝ)
141	24, 139, 140	mp2an 690	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℝ
142	95, 141	remulcli 10651	. . . . . . . . . . 11 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℝ
143		faccl 13637	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℕ₀ → (!‘(𝑁 − 1)) ∈ ℕ)
144	119, 143	ax-mp 5	. . . . . . . . . . . 12 ⊢ (!‘(𝑁 − 1)) ∈ ℕ
145	144	nnrei 11641	. . . . . . . . . . 11 ⊢ (!‘(𝑁 − 1)) ∈ ℝ
146	142, 145	remulcli 10651	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ
147	146, 136	remulcli 10651	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
148	147	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
149	97, 131	remulcli 10651	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ
150	125	nn0ge0i 11918	. . . . . . . . . . . . 13 ⊢ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))
151	126, 150	pm3.2i 473	. . . . . . . . . . . 12 ⊢ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
152	115, 149, 151	3pm3.2i 1335	. . . . . . . . . . 11 ⊢ ((𝑁↑𝐾) ∈ ℝ ∧ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ ∧ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
153		nnltp1le 12032	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁))
154	14, 1, 153	mp2an 690	. . . . . . . . . . . . 13 ⊢ (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁)
155		df-2 11694	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
156	155	breq1i 5065	. . . . . . . . . . . . 13 ⊢ (2 ≤ 𝑁 ↔ (1 + 1) ≤ 𝑁)
157	154, 156	bitr4i 280	. . . . . . . . . . . 12 ⊢ (1 < 𝑁 ↔ 2 ≤ 𝑁)
158		expubnd 13535	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ₀ ∧ 2 ≤ 𝑁) → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
159	2, 13, 158	mp3an12 1447	. . . . . . . . . . . 12 ⊢ (2 ≤ 𝑁 → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
160	157, 159	sylbi 219	. . . . . . . . . . 11 ⊢ (1 < 𝑁 → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
161		lemul1a 11488	. . . . . . . . . . 11 ⊢ ((((𝑁↑𝐾) ∈ ℝ ∧ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ ∧ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))) ∧ (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
162	152, 160, 161	sylancr 589	. . . . . . . . . 10 ⊢ (1 < 𝑁 → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
163	96	nn0cni 11903	. . . . . . . . . . . 12 ⊢ (2↑𝐾) ∈ ℂ
164	131	recni 10649	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℂ
165	163, 164, 108, 122	mul4i 10831	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
166	120	nn0cni 11903	. . . . . . . . . . . . 13 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℂ
167	164, 166, 68	mulassi 10646	. . . . . . . . . . . 12 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀) = (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀))
168	167	oveq2i 7161	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
169	134	nn0cni 11903	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℂ
170	133	recni 10649	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℂ
171	169, 170, 68	mul12i 10829	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
172	165, 168, 171	3eqtr2i 2850	. . . . . . . . . 10 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
173	162, 172	breqtrdi 5099	. . . . . . . . 9 ⊢ (1 < 𝑁 → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
174	173	adantr 483	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
175	135	nn0ge0i 11918	. . . . . . . . . . . 12 ⊢ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀)
176	136, 175	pm3.2i 473	. . . . . . . . . . 11 ⊢ ((((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ ∧ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀))
177	133, 146, 176	3pm3.2i 1335	. . . . . . . . . 10 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ ∧ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ ∧ ((((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ ∧ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀)))
178		lemul1a 11488	. . . . . . . . . 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 688	. . . . . . . . 9 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
180	179	adantl 484	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
181	128, 138, 148, 174, 180	letrd 10791	. . . . . . 7 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
182	163, 108, 68	mul32i 10830	. . . . . . . . 9 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) = (((2↑𝐾) · 𝑀) · 𝑁)
183	182	oveq2i 7161	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁))
184		expp1 13430	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ (𝑀 + 𝐾) ∈ ℕ₀) → (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀))
185	68, 139, 184	mp2an 690	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀)
186	13	nn0cni 11903	. . . . . . . . . . . . . . 15 ⊢ 𝐾 ∈ ℂ
187		ax-1cn 10589	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
188	68, 186, 187	addassi 10645	. . . . . . . . . . . . . 14 ⊢ ((𝑀 + 𝐾) + 1) = (𝑀 + (𝐾 + 1))
189	188	oveq2i 7161	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = (𝑀↑(𝑀 + (𝐾 + 1)))
190	185, 189	eqtr3i 2846	. . . . . . . . . . . 12 ⊢ ((𝑀↑(𝑀 + 𝐾)) · 𝑀) = (𝑀↑(𝑀 + (𝐾 + 1)))
191	190	oveq2i 7161	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1))))
192	95	recni 10649	. . . . . . . . . . . 12 ⊢ (2↑(𝐾↑2)) ∈ ℂ
193	141	recni 10649	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℂ
194	192, 163, 193, 68	mul4i 10831	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
195	191, 194	eqtr3i 2846	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
196		facnn2 13636	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
197	1, 196	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)
198	195, 197	oveq12i 7162	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀)) · ((!‘(𝑁 − 1)) · 𝑁))
199	142	recni 10649	. . . . . . . . . 10 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℂ
200	144	nncni 11642	. . . . . . . . . 10 ⊢ (!‘(𝑁 − 1)) ∈ ℂ
201	163, 68	mulcli 10642	. . . . . . . . . 10 ⊢ ((2↑𝐾) · 𝑀) ∈ ℂ
202	199, 200, 201, 108	mul4i 10831	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀)) · ((!‘(𝑁 − 1)) · 𝑁))
203	198, 202	eqtr4i 2847	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁))
204	98	recni 10649	. . . . . . . . 9 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℂ
205	100	nncni 11642	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℂ
206	204, 78, 205	mulassi 10646	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
207	183, 203, 206	3eqtr2i 2850	. . . . . . 7 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
208	181, 207	breqtrdi 5099	. . . . . 6 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
209	124, 208	eqbrtrid 5093	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
210	102	nn0ge0i 11918	. . . . . . . . 9 ⊢ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))
211	103, 210	pm3.2i 473	. . . . . . . 8 ⊢ (((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ ∧ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
212	98, 21, 211	3pm3.2i 1335	. . . . . . 7 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℝ ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ ∧ (((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ ∧ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
213		expadd 13465	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (𝐾↑2) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ₀) → (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾)))
214	34, 93, 13, 213	mp3an 1457	. . . . . . . 8 ⊢ (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾))
215	19	nn0zi 12001	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℤ
216	13	nn0rei 11902	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℝ
217	16	nnrei 11641	. . . . . . . . . . . . 13 ⊢ (𝐾 + 1) ∈ ℝ
218	17	nn0ge0i 11918	. . . . . . . . . . . . . 14 ⊢ 0 ≤ (𝐾 + 1)
219	217, 218	pm3.2i 473	. . . . . . . . . . . . 13 ⊢ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1))
220	216, 217, 219	3pm3.2i 1335	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℝ ∧ (𝐾 + 1) ∈ ℝ ∧ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1)))
221	216	ltp1i 11538	. . . . . . . . . . . . 13 ⊢ 𝐾 < (𝐾 + 1)
222	216, 217, 221	ltleii 10757	. . . . . . . . . . . 12 ⊢ 𝐾 ≤ (𝐾 + 1)
223		lemul1a 11488	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ ℝ ∧ (𝐾 + 1) ∈ ℝ ∧ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1))) ∧ 𝐾 ≤ (𝐾 + 1)) → (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1)))
224	220, 222, 223	mp2an 690	. . . . . . . . . . 11 ⊢ (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1))
225	186	sqvali 13537	. . . . . . . . . . . . 13 ⊢ (𝐾↑2) = (𝐾 · 𝐾)
226	186	mulid1i 10639	. . . . . . . . . . . . . 14 ⊢ (𝐾 · 1) = 𝐾
227	226	eqcomi 2830	. . . . . . . . . . . . 13 ⊢ 𝐾 = (𝐾 · 1)
228	225, 227	oveq12i 7162	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) = ((𝐾 · 𝐾) + (𝐾 · 1))
229	186, 186, 187	adddii 10647	. . . . . . . . . . . 12 ⊢ (𝐾 · (𝐾 + 1)) = ((𝐾 · 𝐾) + (𝐾 · 1))
230	228, 229	eqtr4i 2847	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) = (𝐾 · (𝐾 + 1))
231	16	nncni 11642	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℂ
232	231	sqvali 13537	. . . . . . . . . . 11 ⊢ ((𝐾 + 1)↑2) = ((𝐾 + 1) · (𝐾 + 1))
233	224, 230, 232	3brtr4i 5088	. . . . . . . . . 10 ⊢ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)
234	93, 13	nn0addcli 11928	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) ∈ ℕ₀
235	234	nn0zi 12001	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) ∈ ℤ
236	235	eluz1i 12245	. . . . . . . . . 10 ⊢ (((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾)) ↔ (((𝐾 + 1)↑2) ∈ ℤ ∧ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)))
237	215, 233, 236	mpbir2an 709	. . . . . . . . 9 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾))
238		leexp2a 13530	. . . . . . . . 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 5081	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ≤ (2↑((𝐾 + 1)↑2))
241		lemul1a 11488	. . . . . . 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 690	. . . . . 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 10791	. . . 4 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
245	77, 78, 205	mulassi 10646	. . . 4 ⊢ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
246	244, 245	breqtrrdi 5100	. . 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 688	1 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 class class class wbr 5058 ‘cfv 6349 (class class class)co 7150 ℂcc 10529 ℝcr 10530 0cc0 10531 1c1 10532 + caddc 10534 · cmul 10536 < clt 10669 ≤ cle 10670 − cmin 10864 ℕcn 11632 2c2 11686 ℕ₀cn0 11891 ℤcz 11975 ℤ_≥cuz 12237 ↑cexp 13423 !cfa 13627

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-er 8283 df-en 8504 df-dom 8505 df-sdom 8506 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-n0 11892 df-z 11976 df-uz 12238 df-rp 12384 df-seq 13364 df-exp 13424 df-fac 13628

This theorem is referenced by: faclbnd4lem2 13648

W3C validator