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 13643

Description: Lemma for faclbnd4 13647. 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 11633	. . 3 ⊢ 𝑁 ∈ ℝ
3		1re 10627	. . 3 ⊢ 1 ∈ ℝ
4		lelttric 10733	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 ≤ 1 ∨ 1 < 𝑁))
5	2, 3, 4	mp2an 690	. 2 ⊢ (𝑁 ≤ 1 ∨ 1 < 𝑁)
6		nnge1 11652	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 1 ≤ 𝑁)
7	1, 6	ax-mp 5	. . . . . 6 ⊢ 1 ≤ 𝑁
8	2, 3	letri3i 10742	. . . . . 6 ⊢ (𝑁 = 1 ↔ (𝑁 ≤ 1 ∧ 1 ≤ 𝑁))
9	7, 8	mpbiran2 708	. . . . 5 ⊢ (𝑁 = 1 ↔ 𝑁 ≤ 1)
10		0le1 11149	. . . . . . . . . 10 ⊢ 0 ≤ 1
11	3, 10	pm3.2i 473	. . . . . . . . 9 ⊢ (1 ∈ ℝ ∧ 0 ≤ 1)
12		2re 11698	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
13		faclbnd4lem1.2	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℕ₀
14		1nn 11635	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
15		nn0nnaddcl 11915	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ₀ ∧ 1 ∈ ℕ) → (𝐾 + 1) ∈ ℕ)
16	13, 14, 15	mp2an 690	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℕ
17	16	nnnn0i 11892	. . . . . . . . . . 11 ⊢ (𝐾 + 1) ∈ ℕ₀
18		2nn0 11901	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
19	17, 18	nn0expcli 13445	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℕ₀
20		reexpcl 13436	. . . . . . . . . 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 11895	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℝ
25	23	nn0ge0i 11911	. . . . . . . . . 10 ⊢ 0 ≤ 𝑀
26	24, 25	pm3.2i 473	. . . . . . . . 9 ⊢ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀)
27		nn0nnaddcl 11915	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ₀ ∧ (𝐾 + 1) ∈ ℕ) → (𝑀 + (𝐾 + 1)) ∈ ℕ)
28	23, 16, 27	mp2an 690	. . . . . . . . . . . 12 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ
29	28	nnnn0i 11892	. . . . . . . . . . 11 ⊢ (𝑀 + (𝐾 + 1)) ∈ ℕ₀
30	23, 29	nn0expcli 13445	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℕ₀
31	30	nn0rei 11895	. . . . . . . . 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 11699	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
35		exp0 13423	. . . . . . . . . 10 ⊢ (2 ∈ ℂ → (2↑0) = 1)
36	34, 35	ax-mp 5	. . . . . . . . 9 ⊢ (2↑0) = 1
37		1le2 11833	. . . . . . . . . 10 ⊢ 1 ≤ 2
38		nn0uz 12267	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
39	19, 38	eleqtri 2911	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘0)
40		leexp2a 13526	. . . . . . . . . 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 5075	. . . . . . . 8 ⊢ 1 ≤ (2↑((𝐾 + 1)↑2))
43		elnn0 11886	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ₀ ↔ (𝑀 ∈ ℕ ∨ 𝑀 = 0))
44		nncn 11632	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
45	44	exp1d 13495	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑀↑1) = 𝑀)
46		nnge1 11652	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 1 ≤ 𝑀)
47		nnuz 12268	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
48	28, 47	eleqtri 2911	. . . . . . . . . . . . . 14 ⊢ (𝑀 + (𝐾 + 1)) ∈ (ℤ_≥‘1)
49		leexp2a 13526	. . . . . . . . . . . . . 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 5076	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀↑(𝑀 + (𝐾 + 1))))
53	30	nn0ge0i 11911	. . . . . . . . . . . 12 ⊢ 0 ≤ (𝑀↑(𝑀 + (𝐾 + 1)))
54		breq1 5055	. . . . . . . . . . . 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 11484	. . . . . . 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 7149	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑁↑(𝐾 + 1)) = (1↑(𝐾 + 1)))
63	16	nnzi 11993	. . . . . . . . . 10 ⊢ (𝐾 + 1) ∈ ℤ
64		1exp 13448	. . . . . . . . . 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 7150	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = (𝑀↑1))
68	23	nn0cni 11896	. . . . . . . . . 10 ⊢ 𝑀 ∈ ℂ
69		exp1 13425	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℂ → (𝑀↑1) = 𝑀)
70	68, 69	ax-mp 5	. . . . . . . . 9 ⊢ (𝑀↑1) = 𝑀
71	67, 70	syl6eq 2872	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝑀↑𝑁) = 𝑀)
72	66, 71	oveq12d 7160	. . . . . . 7 ⊢ (𝑁 = 1 → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (1 · 𝑀))
73		fveq2 6656	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (!‘𝑁) = (!‘1))
74		fac1 13627	. . . . . . . . . 10 ⊢ (!‘1) = 1
75	73, 74	syl6eq 2872	. . . . . . . . 9 ⊢ (𝑁 = 1 → (!‘𝑁) = 1)
76	75	oveq2d 7158	. . . . . . . 8 ⊢ (𝑁 = 1 → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · 1))
77	21	recni 10641	. . . . . . . . . 10 ⊢ (2↑((𝐾 + 1)↑2)) ∈ ℂ
78	30	nn0cni 11896	. . . . . . . . . 10 ⊢ (𝑀↑(𝑀 + (𝐾 + 1))) ∈ ℂ
79	77, 78	mulcli 10634	. . . . . . . . 9 ⊢ ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) ∈ ℂ
80	79	mulid1i 10631	. . . . . . . 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 5065	. . . . . 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 13436	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ (𝐾 + 1) ∈ ℕ₀) → (𝑁↑(𝐾 + 1)) ∈ ℝ)
87	2, 17, 86	mp2an 690	. . . . . . 7 ⊢ (𝑁↑(𝐾 + 1)) ∈ ℝ
88	1	nnnn0i 11892	. . . . . . . 8 ⊢ 𝑁 ∈ ℕ₀
89		reexpcl 13436	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ₀) → (𝑀↑𝑁) ∈ ℝ)
90	24, 88, 89	mp2an 690	. . . . . . 7 ⊢ (𝑀↑𝑁) ∈ ℝ
91	87, 90	remulcli 10643	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ
92	91	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ∈ ℝ)
93	13, 18	nn0expcli 13445	. . . . . . . . 9 ⊢ (𝐾↑2) ∈ ℕ₀
94		reexpcl 13436	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (𝐾↑2) ∈ ℕ₀) → (2↑(𝐾↑2)) ∈ ℝ)
95	12, 93, 94	mp2an 690	. . . . . . . 8 ⊢ (2↑(𝐾↑2)) ∈ ℝ
96	18, 13	nn0expcli 13445	. . . . . . . . 9 ⊢ (2↑𝐾) ∈ ℕ₀
97	96	nn0rei 11895	. . . . . . . 8 ⊢ (2↑𝐾) ∈ ℝ
98	95, 97	remulcli 10643	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℝ
99		faccl 13633	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (!‘𝑁) ∈ ℕ)
100	88, 99	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) ∈ ℕ
101	100	nnnn0i 11892	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℕ₀
102	30, 101	nn0mulcli 11922	. . . . . . . 8 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℕ₀
103	102	nn0rei 11895	. . . . . . 7 ⊢ ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)) ∈ ℝ
104	98, 103	remulcli 10643	. . . . . 6 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
105	104	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
106	21, 103	remulcli 10643	. . . . . 6 ⊢ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ
107	106	a1i 11	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))) ∈ ℝ)
108	1	nncni 11634	. . . . . . . . 9 ⊢ 𝑁 ∈ ℂ
109		expp1 13426	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 𝐾 ∈ ℕ₀) → (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁))
110	108, 13, 109	mp2an 690	. . . . . . . 8 ⊢ (𝑁↑(𝐾 + 1)) = ((𝑁↑𝐾) · 𝑁)
111		expm1t 13447	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀))
112	68, 1, 111	mp2an 690	. . . . . . . 8 ⊢ (𝑀↑𝑁) = ((𝑀↑(𝑁 − 1)) · 𝑀)
113	110, 112	oveq12i 7154	. . . . . . 7 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀))
114		reexpcl 13436	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ₀) → (𝑁↑𝐾) ∈ ℝ)
115	2, 13, 114	mp2an 690	. . . . . . . . 9 ⊢ (𝑁↑𝐾) ∈ ℝ
116	115	recni 10641	. . . . . . . 8 ⊢ (𝑁↑𝐾) ∈ ℂ
117		elnnnn0 11927	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ₀))
118	1, 117	mpbi 232	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ₀)
119	118	simpri 488	. . . . . . . . . . 11 ⊢ (𝑁 − 1) ∈ ℕ₀
120	23, 119	nn0expcli 13445	. . . . . . . . . 10 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℕ₀
121	120, 23	nn0mulcli 11922	. . . . . . . . 9 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℕ₀
122	121	nn0cni 11896	. . . . . . . 8 ⊢ ((𝑀↑(𝑁 − 1)) · 𝑀) ∈ ℂ
123	116, 108, 122	mulassi 10638	. . . . . . 7 ⊢ (((𝑁↑𝐾) · 𝑁) · ((𝑀↑(𝑁 − 1)) · 𝑀)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
124	113, 123	eqtri 2844	. . . . . 6 ⊢ ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)))
125	88, 121	nn0mulcli 11922	. . . . . . . . . . 11 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℕ₀
126	125	nn0rei 11895	. . . . . . . . . 10 ⊢ (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀)) ∈ ℝ
127	115, 126	remulcli 10643	. . . . . . . . 9 ⊢ ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ∈ ℝ)
129	119	nn0rei 11895	. . . . . . . . . . . 12 ⊢ (𝑁 − 1) ∈ ℝ
130		reexpcl 13436	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝐾 ∈ ℕ₀) → ((𝑁 − 1)↑𝐾) ∈ ℝ)
131	129, 13, 130	mp2an 690	. . . . . . . . . . 11 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℝ
132	120	nn0rei 11895	. . . . . . . . . . 11 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℝ
133	131, 132	remulcli 10643	. . . . . . . . . 10 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℝ
134	96, 88	nn0mulcli 11922	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℕ₀
135	134, 23	nn0mulcli 11922	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℕ₀
136	135	nn0rei 11895	. . . . . . . . . 10 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) ∈ ℝ
137	133, 136	remulcli 10643	. . . . . . . . 9 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
138	137	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
139	23, 13	nn0addcli 11921	. . . . . . . . . . . . 13 ⊢ (𝑀 + 𝐾) ∈ ℕ₀
140		reexpcl 13436	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℝ ∧ (𝑀 + 𝐾) ∈ ℕ₀) → (𝑀↑(𝑀 + 𝐾)) ∈ ℝ)
141	24, 139, 140	mp2an 690	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℝ
142	95, 141	remulcli 10643	. . . . . . . . . . 11 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℝ
143		faccl 13633	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℕ₀ → (!‘(𝑁 − 1)) ∈ ℕ)
144	119, 143	ax-mp 5	. . . . . . . . . . . 12 ⊢ (!‘(𝑁 − 1)) ∈ ℕ
145	144	nnrei 11633	. . . . . . . . . . 11 ⊢ (!‘(𝑁 − 1)) ∈ ℝ
146	142, 145	remulcli 10643	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ∈ ℝ
147	146, 136	remulcli 10643	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ
148	147	a1i 11	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) ∈ ℝ)
149	97, 131	remulcli 10643	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · ((𝑁 − 1)↑𝐾)) ∈ ℝ
150	125	nn0ge0i 11911	. . . . . . . . . . . . 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 12025	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁))
154	14, 1, 153	mp2an 690	. . . . . . . . . . . . 13 ⊢ (1 < 𝑁 ↔ (1 + 1) ≤ 𝑁)
155		df-2 11687	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
156	155	breq1i 5059	. . . . . . . . . . . . 13 ⊢ (2 ≤ 𝑁 ↔ (1 + 1) ≤ 𝑁)
157	154, 156	bitr4i 280	. . . . . . . . . . . 12 ⊢ (1 < 𝑁 ↔ 2 ≤ 𝑁)
158		expubnd 13531	. . . . . . . . . . . . 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 11480	. . . . . . . . . . 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 11896	. . . . . . . . . . . 12 ⊢ (2↑𝐾) ∈ ℂ
164	131	recni 10641	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1)↑𝐾) ∈ ℂ
165	163, 164, 108, 122	mul4i 10823	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
166	120	nn0cni 11896	. . . . . . . . . . . . 13 ⊢ (𝑀↑(𝑁 − 1)) ∈ ℂ
167	164, 166, 68	mulassi 10638	. . . . . . . . . . . 12 ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀) = (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀))
168	167	oveq2i 7153	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = (((2↑𝐾) · 𝑁) · (((𝑁 − 1)↑𝐾) · ((𝑀↑(𝑁 − 1)) · 𝑀)))
169	134	nn0cni 11896	. . . . . . . . . . . 12 ⊢ ((2↑𝐾) · 𝑁) ∈ ℂ
170	133	recni 10641	. . . . . . . . . . . 12 ⊢ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ∈ ℂ
171	169, 170, 68	mul12i 10821	. . . . . . . . . . 11 ⊢ (((2↑𝐾) · 𝑁) · ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · 𝑀)) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
172	165, 168, 171	3eqtr2i 2850	. . . . . . . . . 10 ⊢ (((2↑𝐾) · ((𝑁 − 1)↑𝐾)) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) = ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀))
173	162, 172	breqtrdi 5093	. . . . . . . . 9 ⊢ (1 < 𝑁 → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
174	173	adantr 483	. . . . . . . 8 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
175	135	nn0ge0i 11911	. . . . . . . . . . . 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 11480	. . . . . . . . . 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 10783	. . . . . . 7 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)))
182	163, 108, 68	mul32i 10822	. . . . . . . . 9 ⊢ (((2↑𝐾) · 𝑁) · 𝑀) = (((2↑𝐾) · 𝑀) · 𝑁)
183	182	oveq2i 7153	. . . . . . . 8 ⊢ ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑁) · 𝑀)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) · (((2↑𝐾) · 𝑀) · 𝑁))
184		expp1 13426	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ (𝑀 + 𝐾) ∈ ℕ₀) → (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀))
185	68, 139, 184	mp2an 690	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = ((𝑀↑(𝑀 + 𝐾)) · 𝑀)
186	13	nn0cni 11896	. . . . . . . . . . . . . . 15 ⊢ 𝐾 ∈ ℂ
187		ax-1cn 10581	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
188	68, 186, 187	addassi 10637	. . . . . . . . . . . . . 14 ⊢ ((𝑀 + 𝐾) + 1) = (𝑀 + (𝐾 + 1))
189	188	oveq2i 7153	. . . . . . . . . . . . 13 ⊢ (𝑀↑((𝑀 + 𝐾) + 1)) = (𝑀↑(𝑀 + (𝐾 + 1)))
190	185, 189	eqtr3i 2846	. . . . . . . . . . . 12 ⊢ ((𝑀↑(𝑀 + 𝐾)) · 𝑀) = (𝑀↑(𝑀 + (𝐾 + 1)))
191	190	oveq2i 7153	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1))))
192	95	recni 10641	. . . . . . . . . . . 12 ⊢ (2↑(𝐾↑2)) ∈ ℂ
193	141	recni 10641	. . . . . . . . . . . 12 ⊢ (𝑀↑(𝑀 + 𝐾)) ∈ ℂ
194	192, 163, 193, 68	mul4i 10823	. . . . . . . . . . 11 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + 𝐾)) · 𝑀)) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
195	191, 194	eqtr3i 2846	. . . . . . . . . 10 ⊢ (((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀))
196		facnn2 13632	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
197	1, 196	ax-mp 5	. . . . . . . . . 10 ⊢ (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)
198	195, 197	oveq12i 7154	. . . . . . . . 9 ⊢ ((((2↑(𝐾↑2)) · (2↑𝐾)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · ((2↑𝐾) · 𝑀)) · ((!‘(𝑁 − 1)) · 𝑁))
199	142	recni 10641	. . . . . . . . . 10 ⊢ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℂ
200	144	nncni 11634	. . . . . . . . . 10 ⊢ (!‘(𝑁 − 1)) ∈ ℂ
201	163, 68	mulcli 10634	. . . . . . . . . 10 ⊢ ((2↑𝐾) · 𝑀) ∈ ℂ
202	199, 200, 201, 108	mul4i 10823	. . . . . . . . 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 10641	. . . . . . . . 9 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ∈ ℂ
205	100	nncni 11634	. . . . . . . . 9 ⊢ (!‘𝑁) ∈ ℂ
206	204, 78, 205	mulassi 10638	. . . . . . . 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 5093	. . . . . 6 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑𝐾) · (𝑁 · ((𝑀↑(𝑁 − 1)) · 𝑀))) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
209	124, 208	eqbrtrid 5087	. . . . 5 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (2↑𝐾)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
210	102	nn0ge0i 11911	. . . . . . . . 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 13461	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (𝐾↑2) ∈ ℕ₀ ∧ 𝐾 ∈ ℕ₀) → (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾)))
214	34, 93, 13, 213	mp3an 1457	. . . . . . . 8 ⊢ (2↑((𝐾↑2) + 𝐾)) = ((2↑(𝐾↑2)) · (2↑𝐾))
215	19	nn0zi 11994	. . . . . . . . . 10 ⊢ ((𝐾 + 1)↑2) ∈ ℤ
216	13	nn0rei 11895	. . . . . . . . . . . . 13 ⊢ 𝐾 ∈ ℝ
217	16	nnrei 11633	. . . . . . . . . . . . 13 ⊢ (𝐾 + 1) ∈ ℝ
218	17	nn0ge0i 11911	. . . . . . . . . . . . . 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 11530	. . . . . . . . . . . . 13 ⊢ 𝐾 < (𝐾 + 1)
222	216, 217, 221	ltleii 10749	. . . . . . . . . . . 12 ⊢ 𝐾 ≤ (𝐾 + 1)
223		lemul1a 11480	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ ℝ ∧ (𝐾 + 1) ∈ ℝ ∧ ((𝐾 + 1) ∈ ℝ ∧ 0 ≤ (𝐾 + 1))) ∧ 𝐾 ≤ (𝐾 + 1)) → (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1)))
224	220, 222, 223	mp2an 690	. . . . . . . . . . 11 ⊢ (𝐾 · (𝐾 + 1)) ≤ ((𝐾 + 1) · (𝐾 + 1))
225	186	sqvali 13533	. . . . . . . . . . . . 13 ⊢ (𝐾↑2) = (𝐾 · 𝐾)
226	186	mulid1i 10631	. . . . . . . . . . . . . 14 ⊢ (𝐾 · 1) = 𝐾
227	226	eqcomi 2830	. . . . . . . . . . . . 13 ⊢ 𝐾 = (𝐾 · 1)
228	225, 227	oveq12i 7154	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) = ((𝐾 · 𝐾) + (𝐾 · 1))
229	186, 186, 187	adddii 10639	. . . . . . . . . . . 12 ⊢ (𝐾 · (𝐾 + 1)) = ((𝐾 · 𝐾) + (𝐾 · 1))
230	228, 229	eqtr4i 2847	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) = (𝐾 · (𝐾 + 1))
231	16	nncni 11634	. . . . . . . . . . . 12 ⊢ (𝐾 + 1) ∈ ℂ
232	231	sqvali 13533	. . . . . . . . . . 11 ⊢ ((𝐾 + 1)↑2) = ((𝐾 + 1) · (𝐾 + 1))
233	224, 230, 232	3brtr4i 5082	. . . . . . . . . 10 ⊢ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)
234	93, 13	nn0addcli 11921	. . . . . . . . . . . 12 ⊢ ((𝐾↑2) + 𝐾) ∈ ℕ₀
235	234	nn0zi 11994	. . . . . . . . . . 11 ⊢ ((𝐾↑2) + 𝐾) ∈ ℤ
236	235	eluz1i 12238	. . . . . . . . . 10 ⊢ (((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾)) ↔ (((𝐾 + 1)↑2) ∈ ℤ ∧ ((𝐾↑2) + 𝐾) ≤ ((𝐾 + 1)↑2)))
237	215, 233, 236	mpbir2an 709	. . . . . . . . 9 ⊢ ((𝐾 + 1)↑2) ∈ (ℤ_≥‘((𝐾↑2) + 𝐾))
238		leexp2a 13526	. . . . . . . . 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 5075	. . . . . . 7 ⊢ ((2↑(𝐾↑2)) · (2↑𝐾)) ≤ (2↑((𝐾 + 1)↑2))
241		lemul1a 11480	. . . . . . 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 10783	. . . 4 ⊢ ((1 < 𝑁 ∧ (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1)))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁))))
245	77, 78, 205	mulassi 10638	. . . 4 ⊢ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = ((2↑((𝐾 + 1)↑2)) · ((𝑀↑(𝑀 + (𝐾 + 1))) · (!‘𝑁)))
246	244, 245	breqtrrdi 5094	. . 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 1537 ∈ wcel 2114 class class class wbr 5052 ‘cfv 6341 (class class class)co 7142 ℂcc 10521 ℝcr 10522 0cc0 10523 1c1 10524 + caddc 10526 · cmul 10528 < clt 10661 ≤ cle 10662 − cmin 10856 ℕcn 11624 2c2 11679 ℕ₀cn0 11884 ℤcz 11968 ℤ_≥cuz 12230 ↑cexp 13419 !cfa 13623

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 ax-un 7447 ax-cnex 10579 ax-resscn 10580 ax-1cn 10581 ax-icn 10582 ax-addcl 10583 ax-addrcl 10584 ax-mulcl 10585 ax-mulrcl 10586 ax-mulcom 10587 ax-addass 10588 ax-mulass 10589 ax-distr 10590 ax-i2m1 10591 ax-1ne0 10592 ax-1rid 10593 ax-rnegex 10594 ax-rrecex 10595 ax-cnre 10596 ax-pre-lttri 10597 ax-pre-lttrn 10598 ax-pre-ltadd 10599 ax-pre-mulgt0 10600

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 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 3488 df-sbc 3764 df-csb 3872 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-pss 3942 df-nul 4280 df-if 4454 df-pw 4527 df-sn 4554 df-pr 4556 df-tp 4558 df-op 4560 df-uni 4825 df-iun 4907 df-br 5053 df-opab 5115 df-mpt 5133 df-tr 5159 df-id 5446 df-eprel 5451 df-po 5460 df-so 5461 df-fr 5500 df-we 5502 df-xp 5547 df-rel 5548 df-cnv 5549 df-co 5550 df-dm 5551 df-rn 5552 df-res 5553 df-ima 5554 df-pred 6134 df-ord 6180 df-on 6181 df-lim 6182 df-suc 6183 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-riota 7100 df-ov 7145 df-oprab 7146 df-mpo 7147 df-om 7567 df-2nd 7676 df-wrecs 7933 df-recs 7994 df-rdg 8032 df-er 8275 df-en 8496 df-dom 8497 df-sdom 8498 df-pnf 10663 df-mnf 10664 df-xr 10665 df-ltxr 10666 df-le 10667 df-sub 10858 df-neg 10859 df-div 11284 df-nn 11625 df-2 11687 df-n0 11885 df-z 11969 df-uz 12231 df-rp 12377 df-seq 13360 df-exp 13420 df-fac 13624

This theorem is referenced by: faclbnd4lem2 13644

W3C validator