Theorem expmulnbnd 14194

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 < 𝐵) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))

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

Proof of Theorem expmulnbnd

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2re 12282	. . . . 5 ⊢ 2 ∈ ℝ
2		simp1 1133	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐴 ∈ ℝ)
3		remulcl 11190	. . . . 5 ⊢ ((2 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (2 · 𝐴) ∈ ℝ)
4	1, 2, 3	sylancr 586	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (2 · 𝐴) ∈ ℝ)
5		simp3 1135	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 1 < 𝐵)
6		1re 11210	. . . . . 6 ⊢ 1 ∈ ℝ
7		simp2 1134	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐵 ∈ ℝ)
8		difrp 13008	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 ↔ (𝐵 − 1) ∈ ℝ+))
9	6, 7, 8	sylancr 586	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (1 < 𝐵 ↔ (𝐵 − 1) ∈ ℝ+))
10	5, 9	mpbid 231	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) ∈ ℝ+)
11	4, 10	rerpdivcld 13043	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ)
12		expnbnd 14191	. . 3 ⊢ ((((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
13	11, 7, 5, 12	syl3anc 1368	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
14		2nn0 12485	. . . 4 ⊢ 2 ∈ ℕ0
15		nnnn0 12475	. . . . 5 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
16	15	ad2antrl 725	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ0)
17		nn0mulcl 12504	. . . 4 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
18	14, 16, 17	sylancr 586	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ0)
19	2	ad2antrr 723	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝐴 ∈ ℝ)
20		2nn 12281	. . . . . . . . 9 ⊢ 2 ∈ ℕ
21		simprl 768	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ)
22		nnmulcl 12232	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
23	20, 21, 22	sylancr 586	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ)
24		eluznn 12898	. . . . . . . 8 ⊢ (((2 · 𝑛) ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
25	23, 24	sylan 579	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
26	25	nnred 12223	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ ℝ)
27	19, 26	remulcld 11240	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ∈ ℝ)
28		0re 11212	. . . . . . . 8 ⊢ 0 ∈ ℝ
29		ifcl 4565	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
30	19, 28, 29	sylancl 585	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
31		remulcl 11190	. . . . . . 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 774	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑛 ∈ ℕ)
34	33	nnred 12223	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑛 ∈ ℝ)
35	26, 34	resubcld 11638	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℝ)
36	32, 35	remulcld 11240	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) ∈ ℝ)
37	7	ad2antrr 723	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝐵 ∈ ℝ)
38	25	nnnn0d 12528	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ0)
39		reexpcl 14040	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (𝐵↑𝑘) ∈ ℝ)
40	37, 38, 39	syl2anc 583	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐵↑𝑘) ∈ ℝ)
41		remulcl 11190	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℝ) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
42	1, 35, 41	sylancr 586	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
43	38	nn0ge0d 12531	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 0 ≤ 𝑘)
44		max1 13160	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
45	28, 19, 44	sylancr 586	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
46		remulcl 11190	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (2 · 𝑛) ∈ ℝ)
47	1, 34, 46	sylancr 586	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (2 · 𝑛) ∈ ℝ)
48		eluzle 12831	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘(2 · 𝑛)) → (2 · 𝑛) ≤ 𝑘)
49	48	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (2 · 𝑛) ≤ 𝑘)
50	47, 26, 26, 49	leadd2dd 11825	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (𝑘 + 𝑘))
51	26	recnd 11238	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ ℂ)
52	51	2timesd 12451	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (2 · 𝑘) = (𝑘 + 𝑘))
53	50, 52	breqtrrd 5166	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘))
54		remulcl 11190	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (2 · 𝑘) ∈ ℝ)
55	1, 26, 54	sylancr 586	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (2 · 𝑘) ∈ ℝ)
56		leaddsub 11686	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℝ ∧ (2 · 𝑛) ∈ ℝ ∧ (2 · 𝑘) ∈ ℝ) → ((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))))
57	26, 47, 55, 56	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))))
58	53, 57	mpbid 231	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛)))
59		2cnd 12286	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 2 ∈ ℂ)
60	34	recnd 11238	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑛 ∈ ℂ)
61	59, 51, 60	subdid 11666	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
62	58, 61	breqtrrd 5166	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ≤ (2 · (𝑘 − 𝑛)))
63		max2 13162	. . . . . . . 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 12153	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝑘 · 𝐴) ≤ ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
66	19	recnd 11238	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝐴 ∈ ℂ)
67	66, 51	mulcomd 11231	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐴 · 𝑘) = (𝑘 · 𝐴))
68	30	recnd 11238	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℂ)
69	35	recnd 11238	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℂ)
70	59, 68, 69	mul32d 11420	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) = ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
71	65, 67, 70	3brtr4d 5170	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ≤ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)))
72	10	ad2antrr 723	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ+)
73	72	rpred 13012	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ)
74	73, 35	remulcld 11240	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ)
75	33	nnnn0d 12528	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑛 ∈ ℕ0)
76		reexpcl 14040	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℕ0) → (𝐵↑𝑛) ∈ ℝ)
77	37, 75, 76	syl2anc 583	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℝ)
78	74, 77	remulcld 11240	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) ∈ ℝ)
79		simplrr 775	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
80	1, 19, 3	sylancr 586	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (2 · 𝐴) ∈ ℝ)
81	80, 77, 72	ltdivmuld 13063	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛) ↔ (2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛))))
82	79, 81	mpbid 231	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)))
83	5	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 1 < 𝐵)
84		posdif 11703	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
85	6, 37, 84	sylancr 586	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
86	83, 85	mpbid 231	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 0 < (𝐵 − 1))
87	33	nnzd 12581	. . . . . . . . . . 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 11732	. . . . . . . . . . . . 13 ⊢ 0 < 1
91	90	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 0 < 1)
92	88, 89, 37, 91, 83	lttrd 11371	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 0 < 𝐵)
93		expgt0 14057	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 0 < 𝐵) → 0 < (𝐵↑𝑛))
94	37, 87, 92, 93	syl3anc 1368	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 0 < (𝐵↑𝑛))
95	73, 77, 86, 94	mulgt0d 11365	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 0 < ((𝐵 − 1) · (𝐵↑𝑛)))
96		oveq2 7409	. . . . . . . . . . 11 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 𝐴) = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
97	96	breq1d 5148	. . . . . . . . . 10 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → ((2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
98		2t0e0 12377	. . . . . . . . . . . 12 ⊢ (2 · 0) = 0
99		oveq2 7409	. . . . . . . . . . . 12 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 0) = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
100	98, 99	eqtr3id 2778	. . . . . . . . . . 11 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → 0 = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
101	100	breq1d 5148	. . . . . . . . . 10 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → (0 < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
102	97, 101	ifboth 4559	. . . . . . . . 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 11240	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝐵↑𝑛)) ∈ ℝ)
105		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ≥‘(2 · 𝑛)))
106	60	2timesd 12451	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (2 · 𝑛) = (𝑛 + 𝑛))
107	106	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (ℤ≥‘(2 · 𝑛)) = (ℤ≥‘(𝑛 + 𝑛)))
108	105, 107	eleqtrd 2827	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ≥‘(𝑛 + 𝑛)))
109		eluzsub 12848	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ≥‘𝑛))
110	87, 87, 108, 109	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ≥‘𝑛))
111		eluznn 12898	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ (𝑘 − 𝑛) ∈ (ℤ≥‘𝑛)) → (𝑘 − 𝑛) ∈ ℕ)
112	33, 110, 111	syl2anc 583	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ)
113	112	nngt0d 12257	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 0 < (𝑘 − 𝑛))
114		ltmul1 12060	. . . . . . . . 9 ⊢ (((2 · if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ ∧ ((𝐵 − 1) · (𝐵↑𝑛)) ∈ ℝ ∧ ((𝑘 − 𝑛) ∈ ℝ ∧ 0 < (𝑘 − 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛))))
115	32, 104, 35, 113, 114	syl112anc 1371	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛))))
116	103, 115	mpbid 231	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)))
117	73	recnd 11238	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℂ)
118	77	recnd 11238	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℂ)
119	117, 118, 69	mul32d 11420	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)) = (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
120	116, 119	breqtrd 5164	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
121		peano2re 11383	. . . . . . . . . 10 ⊢ (((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
122	74, 121	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
123	112	nnnn0d 12528	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ0)
124		reexpcl 14040	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ0) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
125	37, 123, 124	syl2anc 583	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
126	74	ltp1d 12140	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) + 1))
127	88, 37, 92	ltled 11358	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 0 ≤ 𝐵)
128		bernneq2 14189	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ0 ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛)))
129	37, 123, 127, 128	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛)))
130	74, 122, 125, 126, 129	ltletrd 11370	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (𝐵↑(𝑘 − 𝑛)))
131	37	recnd 11238	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝐵 ∈ ℂ)
132	92	gt0ne0d 11774	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝐵 ≠ 0)
133		eluzelz 12828	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ≥‘(2 · 𝑛)) → 𝑘 ∈ ℤ)
134	133	adantl 481	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → 𝑘 ∈ ℤ)
135		expsub 14072	. . . . . . . . 9 ⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
136	131, 132, 134, 87, 135	syl22anc 836	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
137	130, 136	breqtrd 5164	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛)))
138		ltmuldiv 12083	. . . . . . . 8 ⊢ ((((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ ∧ (𝐵↑𝑘) ∈ ℝ ∧ ((𝐵↑𝑛) ∈ ℝ ∧ 0 < (𝐵↑𝑛))) → ((((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛))))
139	74, 40, 77, 94, 138	syl112anc 1371	. . . . . . 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 11371	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (𝐵↑𝑘))
142	27, 36, 40, 71, 141	lelttrd 11368	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ≥‘(2 · 𝑛))) → (𝐴 · 𝑘) < (𝐵↑𝑘))
143	142	ralrimiva 3138	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∀𝑘 ∈ (ℤ≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘))
144		fveq2 6881	. . . . 5 ⊢ (𝑗 = (2 · 𝑛) → (ℤ≥‘𝑗) = (ℤ≥‘(2 · 𝑛)))
145	144	raleqdv 3317	. . . 4 ⊢ (𝑗 = (2 · 𝑛) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘) ↔ ∀𝑘 ∈ (ℤ≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)))
146	145	rspcev 3604	. . 3 ⊢ (((2 · 𝑛) ∈ ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
147	18, 143, 146	syl2anc 583	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
148	13, 147	rexlimddv 3153	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2932  ∀wral 3053  ∃wrex 3062  ifcif 4520   class class class wbr 5138  ‘cfv 6533  (class class class)co 7401  ℂcc 11103  ℝcr 11104  0cc0 11105  1c1 11106   + caddc 11108   · cmul 11110   < clt 11244   ≤ cle 11245   − cmin 11440   / cdiv 11867  ℕcn 12208  2c2 12263  ℕ₀cn0 12468  ℤcz 12554  ℤ_≥cuz 12818  ℝ⁺crp 12970  ↑cexp 14023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-er 8698  df-en 8935  df-dom 8936  df-sdom 8937  df-sup 9432  df-inf 9433  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-fl 13753  df-seq 13963  df-exp 14024

This theorem is referenced by:  geomulcvg  15818