expmulnbnd - Metamath Proof Explorer

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

Theorem expmulnbnd 14284

Description: Exponentiation with a base greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015.)

**Assertion**
Ref	Expression
expmulnbnd	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))

Distinct variable groups: 𝑗,𝑘,𝐴 𝐵,𝑗,𝑘

Proof of Theorem expmulnbnd Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2re 12367	. . . . 5 ⊢ 2 ∈ ℝ
2		simp1 1136	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐴 ∈ ℝ)
3		remulcl 11269	. . . . 5 ⊢ ((2 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (2 · 𝐴) ∈ ℝ)
4	1, 2, 3	sylancr 586	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (2 · 𝐴) ∈ ℝ)
5		simp3 1138	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 1 < 𝐵)
6		1re 11290	. . . . . 6 ⊢ 1 ∈ ℝ
7		simp2 1137	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐵 ∈ ℝ)
8		difrp 13095	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 ↔ (𝐵 − 1) ∈ ℝ⁺))
9	6, 7, 8	sylancr 586	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (1 < 𝐵 ↔ (𝐵 − 1) ∈ ℝ⁺))
10	5, 9	mpbid 232	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) ∈ ℝ⁺)
11	4, 10	rerpdivcld 13130	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ)
12		expnbnd 14281	. . 3 ⊢ ((((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
13	11, 7, 5, 12	syl3anc 1371	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
14		2nn0 12570	. . . 4 ⊢ 2 ∈ ℕ₀
15		nnnn0 12560	. . . . 5 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
16	15	ad2antrl 727	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ₀)
17		nn0mulcl 12589	. . . 4 ⊢ ((2 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀) → (2 · 𝑛) ∈ ℕ₀)
18	14, 16, 17	sylancr 586	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ₀)
19	2	ad2antrr 725	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐴 ∈ ℝ)
20		2nn 12366	. . . . . . . . 9 ⊢ 2 ∈ ℕ
21		simprl 770	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ)
22		nnmulcl 12317	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
23	20, 21, 22	sylancr 586	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ)
24		eluznn 12983	. . . . . . . 8 ⊢ (((2 · 𝑛) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
25	23, 24	sylan 579	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
26	25	nnred 12308	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℝ)
27	19, 26	remulcld 11320	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ∈ ℝ)
28		0re 11292	. . . . . . . 8 ⊢ 0 ∈ ℝ
29		ifcl 4593	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
30	19, 28, 29	sylancl 585	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
31		remulcl 11269	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ)
32	1, 30, 31	sylancr 586	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ)
33		simplrl 776	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℕ)
34	33	nnred 12308	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℝ)
35	26, 34	resubcld 11718	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℝ)
36	32, 35	remulcld 11320	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) ∈ ℝ)
37	7	ad2antrr 725	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ∈ ℝ)
38	25	nnnn0d 12613	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ₀)
39		reexpcl 14129	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (𝐵↑𝑘) ∈ ℝ)
40	37, 38, 39	syl2anc 583	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑘) ∈ ℝ)
41		remulcl 11269	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℝ) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
42	1, 35, 41	sylancr 586	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
43	38	nn0ge0d 12616	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ 𝑘)
44		max1 13247	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
45	28, 19, 44	sylancr 586	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
46		remulcl 11269	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (2 · 𝑛) ∈ ℝ)
47	1, 34, 46	sylancr 586	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) ∈ ℝ)
48		eluzle 12916	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘(2 · 𝑛)) → (2 · 𝑛) ≤ 𝑘)
49	48	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) ≤ 𝑘)
50	47, 26, 26, 49	leadd2dd 11905	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (𝑘 + 𝑘))
51	26	recnd 11318	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℂ)
52	51	2timesd 12536	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑘) = (𝑘 + 𝑘))
53	50, 52	breqtrrd 5194	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘))
54		remulcl 11269	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (2 · 𝑘) ∈ ℝ)
55	1, 26, 54	sylancr 586	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑘) ∈ ℝ)
56		leaddsub 11766	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℝ ∧ (2 · 𝑛) ∈ ℝ ∧ (2 · 𝑘) ∈ ℝ) → ((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))))
57	26, 47, 55, 56	syl3anc 1371	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))))
58	53, 57	mpbid 232	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛)))
59		2cnd 12371	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 2 ∈ ℂ)
60	34	recnd 11318	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℂ)
61	59, 51, 60	subdid 11746	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
62	58, 61	breqtrrd 5194	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ≤ (2 · (𝑘 − 𝑛)))
63		max2 13249	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(0 ≤ 𝐴, 𝐴, 0))
64	28, 19, 63	sylancr 586	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐴 ≤ if(0 ≤ 𝐴, 𝐴, 0))
65	26, 42, 19, 30, 43, 45, 62, 64	lemul12bd 12238	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 · 𝐴) ≤ ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
66	19	recnd 11318	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐴 ∈ ℂ)
67	66, 51	mulcomd 11311	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) = (𝑘 · 𝐴))
68	30	recnd 11318	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℂ)
69	35	recnd 11318	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℂ)
70	59, 68, 69	mul32d 11500	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) = ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
71	65, 67, 70	3brtr4d 5198	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ≤ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)))
72	10	ad2antrr 725	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ⁺)
73	72	rpred 13099	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ)
74	73, 35	remulcld 11320	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ)
75	33	nnnn0d 12613	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℕ₀)
76		reexpcl 14129	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) → (𝐵↑𝑛) ∈ ℝ)
77	37, 75, 76	syl2anc 583	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℝ)
78	74, 77	remulcld 11320	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) ∈ ℝ)
79		simplrr 777	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
80	1, 19, 3	sylancr 586	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝐴) ∈ ℝ)
81	80, 77, 72	ltdivmuld 13150	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛) ↔ (2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛))))
82	79, 81	mpbid 232	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)))
83	5	ad2antrr 725	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 1 < 𝐵)
84		posdif 11783	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
85	6, 37, 84	sylancr 586	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
86	83, 85	mpbid 232	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝐵 − 1))
87	33	nnzd 12666	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℤ)
88	28	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ∈ ℝ)
89	6	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 1 ∈ ℝ)
90		0lt1 11812	. . . . . . . . . . . . 13 ⊢ 0 < 1
91	90	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < 1)
92	88, 89, 37, 91, 83	lttrd 11451	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < 𝐵)
93		expgt0 14146	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 0 < 𝐵) → 0 < (𝐵↑𝑛))
94	37, 87, 92, 93	syl3anc 1371	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝐵↑𝑛))
95	73, 77, 86, 94	mulgt0d 11445	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < ((𝐵 − 1) · (𝐵↑𝑛)))
96		oveq2 7456	. . . . . . . . . . 11 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 𝐴) = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
97	96	breq1d 5176	. . . . . . . . . 10 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → ((2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
98		2t0e0 12462	. . . . . . . . . . . 12 ⊢ (2 · 0) = 0
99		oveq2 7456	. . . . . . . . . . . 12 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 0) = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
100	98, 99	eqtr3id 2794	. . . . . . . . . . 11 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → 0 = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
101	100	breq1d 5176	. . . . . . . . . 10 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → (0 < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
102	97, 101	ifboth 4587	. . . . . . . . 9 ⊢ (((2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ∧ 0 < ((𝐵 − 1) · (𝐵↑𝑛))) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)))
103	82, 95, 102	syl2anc 583	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)))
104	73, 77	remulcld 11320	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝐵↑𝑛)) ∈ ℝ)
105		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ_≥‘(2 · 𝑛)))
106	60	2timesd 12536	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) = (𝑛 + 𝑛))
107	106	fveq2d 6924	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (ℤ_≥‘(2 · 𝑛)) = (ℤ_≥‘(𝑛 + 𝑛)))
108	105, 107	eleqtrd 2846	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ_≥‘(𝑛 + 𝑛)))
109		eluzsub 12933	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑘 ∈ (ℤ_≥‘(𝑛 + 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛))
110	87, 87, 108, 109	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛))
111		eluznn 12983	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛)) → (𝑘 − 𝑛) ∈ ℕ)
112	33, 110, 111	syl2anc 583	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ)
113	112	nngt0d 12342	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝑘 − 𝑛))
114		ltmul1 12144	. . . . . . . . 9 ⊢ (((2 · if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ ∧ ((𝐵 − 1) · (𝐵↑𝑛)) ∈ ℝ ∧ ((𝑘 − 𝑛) ∈ ℝ ∧ 0 < (𝑘 − 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛))))
115	32, 104, 35, 113, 114	syl112anc 1374	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛))))
116	103, 115	mpbid 232	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)))
117	73	recnd 11318	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℂ)
118	77	recnd 11318	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℂ)
119	117, 118, 69	mul32d 11500	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)) = (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
120	116, 119	breqtrd 5192	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
121		peano2re 11463	. . . . . . . . . 10 ⊢ (((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
122	74, 121	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
123	112	nnnn0d 12613	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ₀)
124		reexpcl 14129	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ₀) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
125	37, 123, 124	syl2anc 583	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
126	74	ltp1d 12225	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) + 1))
127	88, 37, 92	ltled 11438	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ 𝐵)
128		bernneq2 14279	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ₀ ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛)))
129	37, 123, 127, 128	syl3anc 1371	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛)))
130	74, 122, 125, 126, 129	ltletrd 11450	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (𝐵↑(𝑘 − 𝑛)))
131	37	recnd 11318	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ∈ ℂ)
132	92	gt0ne0d 11854	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ≠ 0)
133		eluzelz 12913	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘(2 · 𝑛)) → 𝑘 ∈ ℤ)
134	133	adantl 481	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℤ)
135		expsub 14161	. . . . . . . . 9 ⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
136	131, 132, 134, 87, 135	syl22anc 838	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
137	130, 136	breqtrd 5192	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛)))
138		ltmuldiv 12168	. . . . . . . 8 ⊢ ((((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ ∧ (𝐵↑𝑘) ∈ ℝ ∧ ((𝐵↑𝑛) ∈ ℝ ∧ 0 < (𝐵↑𝑛))) → ((((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛))))
139	74, 40, 77, 94, 138	syl112anc 1374	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛))))
140	137, 139	mpbird 257	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘))
141	36, 78, 40, 120, 140	lttrd 11451	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (𝐵↑𝑘))
142	27, 36, 40, 71, 141	lelttrd 11448	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) < (𝐵↑𝑘))
143	142	ralrimiva 3152	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘))
144		fveq2 6920	. . . . 5 ⊢ (𝑗 = (2 · 𝑛) → (ℤ_≥‘𝑗) = (ℤ_≥‘(2 · 𝑛)))
145	144	raleqdv 3334	. . . 4 ⊢ (𝑗 = (2 · 𝑛) → (∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)))
146	145	rspcev 3635	. . 3 ⊢ (((2 · 𝑛) ∈ ℕ₀ ∧ ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
147	18, 143, 146	syl2anc 583	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
148	13, 147	rexlimddv 3167	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 ifcif 4548 class class class wbr 5166 ‘cfv 6573 (class class class)co 7448 ℂcc 11182 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 < clt 11324 ≤ cle 11325 − cmin 11520 / cdiv 11947 ℕcn 12293 2c2 12348 ℕ₀cn0 12553 ℤcz 12639 ℤ_≥cuz 12903 ℝ⁺crp 13057 ↑cexp 14112

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-sup 9511 df-inf 9512 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-n0 12554 df-z 12640 df-uz 12904 df-rp 13058 df-fl 13843 df-seq 14053 df-exp 14113

This theorem is referenced by: geomulcvg 15924

W3C validator