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 13649

Description: Lemma for faclbnd4 13653. 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 11634	. . 3 ⊢ 𝑁 ∈ ℝ
3		1re 10630	. . 3 ⊢ 1 ∈ ℝ
4		lelttric 10736	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 ≤ 1 ∨ 1 < 𝑁))
5	2, 3, 4	mp2an 691	. 2 ⊢ (𝑁 ≤ 1 ∨ 1 < 𝑁)
6		nnge1 11653	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
7	1, 6	ax-mp 5	. . . . . 6 ⊢ 1 ≤ 𝑁
8	2, 3	letri3i 10745	. . . . . 6 ⊢ (𝑁 = 1 ↔ (𝑁 ≤ 1 ∧ 1 ≤ 𝑁))
9	7, 8	mpbiran2 709	. . . . 5 ⊢ (𝑁 = 1 ↔ 𝑁 ≤ 1)
10		0le1 11152	. . . . . . . . . 10 ⊢ 0 ≤ 1
11	3, 10	pm3.2i 474	. . . . . . . . 9 ⊢ (1 ∈ ℝ ∧ 0 ≤ 1)
12		2re 11699	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
13		faclbnd4lem1.2	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℕ₀
14		1nn 11636	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
15		nn0nnaddcl 11916	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 1 ∈ ℕ) → (𝐾 + 1) ∈ ℕ)
16	13, 14, 15	mp2an 691	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℕ
17	16	nnnn0i 11893	. . . . . . . . . . 11 ⊢ (𝐾 + 1) ∈ ℕ₀
18		2nn0 11902	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
19	17, 18	nn0expcli 13451	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℕ₀
20		reexpcl 13442	. . . . . . . . . 10 ⊢ ((2 ∈ ℝ ∧ ((𝐾 + 1)↑2) ∈ ℕ₀) → (2↑((𝐾 + 1)↑2)) ∈ ℝ)
21	12, 19, 20	mp2an 691	. . . . . . . . 9 ⊢ (2↑((𝐾 + 1)↑2)) ∈ ℝ
22	11, 21	pm3.2i 474	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ)
23		faclbnd4lem1.3	. . . . . . . . . . 11 ⊢ 𝑀 ∈ ℕ₀
24	23	nn0rei 11896	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℝ
25	23	nn0ge0i 11912	. . . . . . . . . 10 ⊢ 0 ≤ 𝑀
26	24, 25	pm3.2i 474	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀)
27		nn0nnaddcl 11916	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ₀ ∧ (𝐾 + 1) ∈ ℕ) → (𝑀 + (𝐾 + 1)) ∈ ℕ)
28	23, 16, 27	mp2an 691	. . . . . . . . . . . 12 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ
29	28	nnnn0i 11893	. . . . . . . . . . 11 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ₀
30	23, 29	nn0expcli 13451	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℕ₀
31	30	nn0rei 11896	. . . . . . . . 9 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ
32	26, 31	pm3.2i 474	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ)
33	22, 32	pm3.2i 474	. . . . . . 7 ⊢ (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ) ∧ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℝ))
34		2cn 11700	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
35		exp0 13429	. . . . . . . . . 10 ⊢ (2 ∈ ℂ → (2↑0) = 1)
36	34, 35	ax-mp 5	. . . . . . . . 9 ⊢ (2↑0) = 1
37		1le2 11834	. . . . . . . . . 10 ⊢ 1 ≤ 2
38		nn0uz 12268	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
39	19, 38	eleqtri 2888	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘0)
40		leexp2a 13532	. . . . . . . . . 10 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘0)) → (2↑0) ≤ (2↑((𝐾 + 1)↑2)))
41	12, 37, 39, 40	mp3an 1458	. . . . . . . . 9 ⊢ (2↑0) ≤ (2↑((𝐾 + 1)↑2))
42	36, 41	eqbrtrri 5053	. . . . . . . 8 ⊢ 1 ≤ (2↑((𝐾 + 1)↑2))
43		elnn0 11887	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ₀ ↔ (𝑀 ∈ ℕ ∨ 𝑀 = 0))
44		nncn 11633	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
45	44	exp1d 13501	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑀↑1) = 𝑀)
46		nnge1 11653	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
47		nnuz 12269	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
48	28, 47	eleqtri 2888	. . . . . . . . . . . . . 14 ⊢ (𝑀 + (𝐾 + 1)) ∈ (ℤ_≥‘1)
49		leexp2a 13532	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℝ ∧ 1 ≤ 𝑀 ∧ (𝑀 + (𝐾 + 1)) ∈ (ℤ_≥‘1)) → (𝑀↑1) ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
50	24, 48, 49	mp3an13 1449	. . . . . . . . . . . . 13 ⊢ (1 ≤ 𝑀 → (𝑀↑1) ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
51	46, 50	syl 17	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑀↑1) ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
52	45, 51	eqbrtrrd 5054	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
53	30	nn0ge0i 11912	. . . . . . . . . . . 12 ⊢ 0 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))
54		breq1 5033	. . . . . . . . . . . 12 ⊢ (𝑀 = 0 → (𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))) ↔ 0 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))))
55	53, 54	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑀 = 0 → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
56	52, 55	jaoi 854	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∨ 𝑀 = 0) → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
57	43, 56	sylbi 220	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
58	23, 57	ax-mp 5	. . . . . . . 8 ⊢ 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))
59	42, 58	pm3.2i 474	. . . . . . 7 ⊢ (1 ≤ (2↑((𝐾 + 1)↑2)) ∧ 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
60		lemul12a 11487	. . . . . . 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 7142	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑁↑(𝐾 + 1)) = (1↑(𝐾 + 1)))
63	16	nnzi 11994	. . . . . . . . . 10 ⊢ (𝐾 + 1) ∈ ℤ
64		1exp 13454	. . . . . . . . . 10 ⊢ ((𝐾 + 1) ∈ ℤ → (1↑(𝐾 + 1)) = 1)
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ (1↑(𝐾 + 1)) = 1
66	62, 65	eqtrdi 2849	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝑁↑(𝐾 + 1)) = 1)
67		oveq2 7143	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = (𝑀↑1))
68	23	nn0cni 11897	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℂ
69		exp1 13431	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℂ → (𝑀↑1) = 𝑀)
70	68, 69	ax-mp 5	. . . . . . . . 9 ⊢ (𝑀↑1) = 𝑀
71	67, 70	eqtrdi 2849	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = 𝑀)
72	66, 71	oveq12d 7153	. . . . . . 7 ⊢ (𝑁 = 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (1 · 𝑀))
73		fveq2 6645	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (!‘𝑁) = (!‘1))
74		fac1 13633	. . . . . . . . . 10 ⊢ (!‘1) = 1
75	73, 74	eqtrdi 2849	. . . . . . . . 9 ⊢ (𝑁 = 1 → (!‘𝑁) = 1)
76	75	oveq2d 7151	. . . . . . . 8 ⊢ (𝑁 = 1 → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · 1))
77	21	recni 10644	. . . . . . . . . 10 ⊢ (2↑((𝐾 + 1)↑2)) ∈ ℂ
78	30	nn0cni 11897	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℂ
79	77, 78	mulcli 10637	. . . . . . . . 9 ⊢ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) ∈ ℂ
80	79	mulid1i 10634	. . . . . . . 8 ⊢ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · 1) = ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1))))
81	76, 80	eqtrdi 2849	. . . . . . 7 ⊢ (𝑁 = 1 → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))))
82	72, 81	breq12d 5043	. . . . . 6 ⊢ (𝑁 = 1 → (((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) ↔ (1 · 𝑀) ≤ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1))))))
83	61, 82	mpbiri 261	. . . . 5 ⊢ (𝑁 = 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
84	9, 83	sylbir 238	. . . 4 ⊢ (𝑁 ≤ 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
85	84	adantr 484	. . 3 ⊢ ((𝑁 ≤ 1 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
86		reexpcl 13442	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ (𝐾 + 1) ∈ ℕ₀) → (𝑁↑(𝐾 + 1)) ∈ ℝ)
87	2, 17, 86	mp2an 691	. . . . . . 7 ⊢ (𝑁↑(𝐾 + 1)) ∈ ℝ
88	1	nnnn0i 11893	. . . . . . . 8 ⊢ 𝑁 ∈ ℕ₀
89		reexpcl 13442	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ₀) → (𝑀↑𝑁) ∈ ℝ)
90	24, 88, 89	mp2an 691	. . . . . . 7 ⊢ (𝑀↑𝑁) ∈ ℝ
91	87, 90	remulcli 10646	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ
92	91	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ)
93	13, 18	nn0expcli 13451	. . . . . . . . 9 ⊢ (𝐾↑2) ∈ ℕ₀
94		reexpcl 13442	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (𝐾↑2) ∈ ℕ₀) → (2↑(𝐾↑2)) ∈ ℝ)
95	12, 93, 94	mp2an 691	. . . . . . . 8 ⊢ (2↑(𝐾↑2)) ∈ ℝ
96	18, 13	nn0expcli 13451	. . . . . . . . 9 ⊢ (2↑𝐾) ∈ ℕ₀
97	96	nn0rei 11896	. . . . . . . 8 ⊢ (2↑𝐾) ∈ ℝ
98	95, 97	remulcli 10646	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℝ
99		faccl 13639	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (!‘𝑁) ∈ ℕ)
100	88, 99	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) ∈ ℕ
101	100	nnnn0i 11893	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℕ₀
102	30, 101	nn0mulcli 11923	. . . . . . . 8 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℕ₀
103	102	nn0rei 11896	. . . . . . 7 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ
104	98, 103	remulcli 10646	. . . . . 6 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
105	104	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
106	21, 103	remulcli 10646	. . . . . 6 ⊢ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
107	106	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
108	1	nncni 11635	. . . . . . . . 9 ⊢ 𝑁 ∈ ℂ
109		expp1 13432	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 𝐾 ∈ ℕ₀) → (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁))
110	108, 13, 109	mp2an 691	. . . . . . . 8 ⊢ (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁)
111		expm1t 13453	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀))
112	68, 1, 111	mp2an 691	. . . . . . . 8 ⊢ (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀)
113	110, 112	oveq12i 7147	. . . . . . 7 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀))
114		reexpcl 13442	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ₀) → (𝑁↑𝐾) ∈ ℝ)
115	2, 13, 114	mp2an 691	. . . . . . . . 9 ⊢ (𝑁↑𝐾) ∈ ℝ
116	115	recni 10644	. . . . . . . 8 ⊢ (𝑁↑𝐾) ∈ ℂ
117		elnnnn0 11928	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ₀))
118	1, 117	mpbi 233	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ₀)
119	118	simpri 489	. . . . . . . . . . 11 ⊢ (𝑁 − 1) ∈ ℕ₀
120	23, 119	nn0expcli 13451	. . . . . . . . . 10 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℕ₀
121	120, 23	nn0mulcli 11923	. . . . . . . . 9 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℕ₀
122	121	nn0cni 11897	. . . . . . . 8 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℂ
123	116, 108, 122	mulassi 10641	. . . . . . 7 ⊢ (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
124	113, 123	eqtri 2821	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
125	88, 121	nn0mulcli 11923	. . . . . . . . . . 11 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℕ₀
126	125	nn0rei 11896	. . . . . . . . . 10 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ
127	115, 126	remulcli 10646	. . . . . . . . 9 ⊢ ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ)
129	119	nn0rei 11896	. . . . . . . . . . . 12 ⊢ (𝑁 − 1) ∈ ℝ
130		reexpcl 13442	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝐾 ∈ ℕ₀) → ((𝑁 − 1)↑𝐾) ∈ ℝ)
131	129, 13, 130	mp2an 691	. . . . . . . . . . 11 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℝ
132	120	nn0rei 11896	. . . . . . . . . . 11 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℝ
133	131, 132	remulcli 10646	. . . . . . . . . 10 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ
134	96, 88	nn0mulcli 11923	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℕ₀
135	134, 23	nn0mulcli 11923	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℕ₀
136	135	nn0rei 11896	. . . . . . . . . 10 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ
137	133, 136	remulcli 10646	. . . . . . . . 9 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
138	137	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
139	23, 13	nn0addcli 11922	. . . . . . . . . . . . 13 ⊢ (𝑀 + 𝐾) ∈ ℕ₀
140		reexpcl 13442	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ (𝑀 + 𝐾) ∈ ℕ₀) → (𝑀↑(𝑀 + 𝐾)) ∈ ℝ)
141	24, 139, 140	mp2an 691	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℝ
142	95, 141	remulcli 10646	. . . . . . . . . . 11 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℝ
143		faccl 13639	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℕ₀ → (!‘(𝑁 − 1)) ∈ ℕ)
144	119, 143	ax-mp 5	. . . . . . . . . . . 12 ⊢ (!‘(𝑁 − 1)) ∈ ℕ
145	144	nnrei 11634	. . . . . . . . . . 11 ⊢ (!‘(𝑁 − 1)) ∈ ℝ
146	142, 145	remulcli 10646	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ
147	146, 136	remulcli 10646	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
148	147	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
149	97, 131	remulcli 10646	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ
150	125	nn0ge0i 11912	. . . . . . . . . . . . 13 ⊢ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))
151	126, 150	pm3.2i 474	. . . . . . . . . . . 12 ⊢ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
152	115, 149, 151	3pm3.2i 1336	. . . . . . . . . . 11 ⊢ ((𝑁↑𝐾) ∈ ℝ ∧ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ ∧ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
153		nnltp1le 12026	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁))
154	14, 1, 153	mp2an 691	. . . . . . . . . . . . 13 ⊢ (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁)
155		df-2 11688	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
156	155	breq1i 5037	. . . . . . . . . . . . 13 ⊢ (2 ≤ 𝑁 ↔ (1 + 1) ≤ 𝑁)
157	154, 156	bitr4i 281	. . . . . . . . . . . 12 ⊢ (1 < 𝑁 ↔ 2 ≤ 𝑁)
158		expubnd 13537	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ₀ ∧ 2 ≤ 𝑁) → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
159	2, 13, 158	mp3an12 1448	. . . . . . . . . . . 12 ⊢ (2 ≤ 𝑁 → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
160	157, 159	sylbi 220	. . . . . . . . . . 11 ⊢ (1 < 𝑁 → (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)))
161		lemul1a 11483	. . . . . . . . . . 11 ⊢ ((((𝑁↑𝐾) ∈ ℝ ∧ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ ∧ ((𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ ∧ 0 ≤ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))) ∧ (𝑁↑𝐾) ≤ ((2↑𝐾) · ((𝑁 − 1)↑𝐾))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
162	152, 160, 161	sylancr 590	. . . . . . . . . 10 ⊢ (1 < 𝑁 → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))))
163	96	nn0cni 11897	. . . . . . . . . . . 12 ⊢ (2↑𝐾) ∈ ℂ
164	131	recni 10644	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℂ
165	163, 164, 108, 122	mul4i 10826	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
166	120	nn0cni 11897	. . . . . . . . . . . . 13 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℂ
167	164, 166, 68	mulassi 10641	. . . . . . . . . . . 12 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀) = (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀))
168	167	oveq2i 7146	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
169	134	nn0cni 11897	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℂ
170	133	recni 10644	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℂ
171	169, 170, 68	mul12i 10824	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
172	165, 168, 171	3eqtr2i 2827	. . . . . . . . . 10 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
173	162, 172	breqtrdi 5071	. . . . . . . . 9 ⊢ (1 < 𝑁 → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
174	173	adantr 484	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
175	135	nn0ge0i 11912	. . . . . . . . . . . 12 ⊢ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀)
176	136, 175	pm3.2i 474	. . . . . . . . . . 11 ⊢ ((((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ ∧ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀))
177	133, 146, 176	3pm3.2i 1336	. . . . . . . . . 10 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ ∧ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ ∧ ((((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ ∧ 0 ≤ (((2↑𝐾) · 𝑁) · 𝑀)))
178		lemul1a 11483	. . . . . . . . . 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 485	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
181	128, 138, 148, 174, 180	letrd 10786	. . . . . . 7 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
182	163, 108, 68	mul32i 10825	. . . . . . . . 9 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) = (((2↑𝐾) · 𝑀) · 𝑁)
183	182	oveq2i 7146	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁))
184		expp1 13432	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ (𝑀 + 𝐾) ∈ ℕ₀) → (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀))
185	68, 139, 184	mp2an 691	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀)
186	13	nn0cni 11897	. . . . . . . . . . . . . . 15 ⊢ 𝐾 ∈ ℂ
187		ax-1cn 10584	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
188	68, 186, 187	addassi 10640	. . . . . . . . . . . . . 14 ⊢ ((𝑀 + 𝐾) + 1) = (𝑀 + (𝐾 + 1))
189	188	oveq2i 7146	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = (𝑀↑(𝑀 + (𝐾 + 1)))
190	185, 189	eqtr3i 2823	. . . . . . . . . . . 12 ⊢ ((𝑀↑(𝑀 + 𝐾)) · 𝑀) = (𝑀↑(𝑀 + (𝐾 + 1)))
191	190	oveq2i 7146	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1))))
192	95	recni 10644	. . . . . . . . . . . 12 ⊢ (2↑(𝐾↑2)) ∈ ℂ
193	141	recni 10644	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℂ
194	192, 163, 193, 68	mul4i 10826	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
195	191, 194	eqtr3i 2823	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
196		facnn2 13638	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
197	1, 196	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)
198	195, 197	oveq12i 7147	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀)) · ((!‘(𝑁 − 1)) · 𝑁))
199	142	recni 10644	. . . . . . . . . 10 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℂ
200	144	nncni 11635	. . . . . . . . . 10 ⊢ (!‘(𝑁 − 1)) ∈ ℂ
201	163, 68	mulcli 10637	. . . . . . . . . 10 ⊢ ((2↑𝐾) · 𝑀) ∈ ℂ
202	199, 200, 201, 108	mul4i 10826	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀)) · ((!‘(𝑁 − 1)) · 𝑁))
203	198, 202	eqtr4i 2824	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁))
204	98	recni 10644	. . . . . . . . 9 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℂ
205	100	nncni 11635	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℂ
206	204, 78, 205	mulassi 10641	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
207	183, 203, 206	3eqtr2i 2827	. . . . . . 7 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
208	181, 207	breqtrdi 5071	. . . . . 6 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
209	124, 208	eqbrtrid 5065	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
210	102	nn0ge0i 11912	. . . . . . . . 9 ⊢ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))
211	103, 210	pm3.2i 474	. . . . . . . 8 ⊢ (((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ ∧ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
212	98, 21, 211	3pm3.2i 1336	. . . . . . 7 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℝ ∧ (2↑((𝐾 + 1)↑2)) ∈ ℝ ∧ (((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ ∧ 0 ≤ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
213		expadd 13467	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (𝐾↑2) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ₀) → (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾)))
214	34, 93, 13, 213	mp3an 1458	. . . . . . . 8 ⊢ (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾))
215	19	nn0zi 11995	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℤ
216	13	nn0rei 11896	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℝ
217	16	nnrei 11634	. . . . . . . . . . . . 13 ⊢ (𝐾 + 1) ∈ ℝ
218	17	nn0ge0i 11912	. . . . . . . . . . . . . 14 ⊢ 0 ≤ (𝐾 + 1)
219	217, 218	pm3.2i 474	. . . . . . . . . . . . 13 ⊢ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1))
220	216, 217, 219	3pm3.2i 1336	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ ℝ ∧ (𝐾 + 1) ∈ ℝ ∧ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1)))
221	216	ltp1i 11533	. . . . . . . . . . . . 13 ⊢ 𝐾 < (𝐾 + 1)
222	216, 217, 221	ltleii 10752	. . . . . . . . . . . 12 ⊢ 𝐾 ≤ (𝐾 + 1)
223		lemul1a 11483	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ ℝ ∧ (𝐾 + 1) ∈ ℝ ∧ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1))) ∧ 𝐾 ≤ (𝐾 + 1)) → (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1)))
224	220, 222, 223	mp2an 691	. . . . . . . . . . 11 ⊢ (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1))
225	186	sqvali 13539	. . . . . . . . . . . . 13 ⊢ (𝐾↑2) = (𝐾 · 𝐾)
226	186	mulid1i 10634	. . . . . . . . . . . . . 14 ⊢ (𝐾 · 1) = 𝐾
227	226	eqcomi 2807	. . . . . . . . . . . . 13 ⊢ 𝐾 = (𝐾 · 1)
228	225, 227	oveq12i 7147	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) = ((𝐾 · 𝐾) + (𝐾 · 1))
229	186, 186, 187	adddii 10642	. . . . . . . . . . . 12 ⊢ (𝐾 · (𝐾 + 1)) = ((𝐾 · 𝐾) + (𝐾 · 1))
230	228, 229	eqtr4i 2824	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) = (𝐾 · (𝐾 + 1))
231	16	nncni 11635	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℂ
232	231	sqvali 13539	. . . . . . . . . . 11 ⊢ ((𝐾 + 1)↑2) = ((𝐾 + 1) · (𝐾 + 1))
233	224, 230, 232	3brtr4i 5060	. . . . . . . . . 10 ⊢ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)
234	93, 13	nn0addcli 11922	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) ∈ ℕ₀
235	234	nn0zi 11995	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) ∈ ℤ
236	235	eluz1i 12239	. . . . . . . . . 10 ⊢ (((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾)) ↔ (((𝐾 + 1)↑2) ∈ ℤ ∧ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)))
237	215, 233, 236	mpbir2an 710	. . . . . . . . 9 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾))
238		leexp2a 13532	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ 1 ≤ 2 ∧ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾))) → (2↑((𝐾↑2) + 𝐾)) ≤ (2↑((𝐾 + 1)↑2)))
239	12, 37, 237, 238	mp3an 1458	. . . . . . . 8 ⊢ (2↑((𝐾↑2) + 𝐾)) ≤ (2↑((𝐾 + 1)↑2))
240	214, 239	eqbrtrri 5053	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ≤ (2↑((𝐾 + 1)↑2))
241		lemul1a 11483	. . . . . . 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 10786	. . . 4 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
245	77, 78, 205	mulassi 10641	. . . 4 ⊢ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
246	244, 245	breqtrrdi 5072	. . 3 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))
247	85, 246	jaoian 954	. 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 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 class class class wbr 5030 ‘cfv 6324 (class class class)co 7135 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 · cmul 10531 < clt 10664 ≤ cle 10665 − cmin 10859 ℕcn 11625 2c2 11680 ℕ₀cn0 11885 ℤcz 11969 ℤ_≥cuz 12231 ↑cexp 13425 !cfa 13629

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-er 8272 df-en 8493 df-dom 8494 df-sdom 8495 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-n0 11886 df-z 11970 df-uz 12232 df-rp 12378 df-seq 13365 df-exp 13426 df-fac 13630

This theorem is referenced by: faclbnd4lem2 13650

W3C validator