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 14258

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 12319	. . . . 5 ⊢ 2 ∈ ℝ
2		simp1 1136	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐴 ∈ ℝ)
3		remulcl 11219	. . . . 5 ⊢ ((2 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (2 · 𝐴) ∈ ℝ)
4	1, 2, 3	sylancr 587	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (2 · 𝐴) ∈ ℝ)
5		simp3 1138	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 1 < 𝐵)
6		1re 11240	. . . . . 6 ⊢ 1 ∈ ℝ
7		simp2 1137	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐵 ∈ ℝ)
8		difrp 13052	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 ↔ (𝐵 − 1) ∈ ℝ⁺))
9	6, 7, 8	sylancr 587	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (1 < 𝐵 ↔ (𝐵 − 1) ∈ ℝ⁺))
10	5, 9	mpbid 232	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) ∈ ℝ⁺)
11	4, 10	rerpdivcld 13087	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ)
12		expnbnd 14255	. . 3 ⊢ ((((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
13	11, 7, 5, 12	syl3anc 1373	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
14		2nn0 12523	. . . 4 ⊢ 2 ∈ ℕ₀
15		nnnn0 12513	. . . . 5 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
16	15	ad2antrl 728	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ₀)
17		nn0mulcl 12542	. . . 4 ⊢ ((2 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀) → (2 · 𝑛) ∈ ℕ₀)
18	14, 16, 17	sylancr 587	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ₀)
19	2	ad2antrr 726	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐴 ∈ ℝ)
20		2nn 12318	. . . . . . . . 9 ⊢ 2 ∈ ℕ
21		simprl 770	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ)
22		nnmulcl 12269	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
23	20, 21, 22	sylancr 587	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ)
24		eluznn 12939	. . . . . . . 8 ⊢ (((2 · 𝑛) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
25	23, 24	sylan 580	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
26	25	nnred 12260	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℝ)
27	19, 26	remulcld 11270	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ∈ ℝ)
28		0re 11242	. . . . . . . 8 ⊢ 0 ∈ ℝ
29		ifcl 4551	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
30	19, 28, 29	sylancl 586	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
31		remulcl 11219	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ)
32	1, 30, 31	sylancr 587	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ)
33		simplrl 776	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℕ)
34	33	nnred 12260	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℝ)
35	26, 34	resubcld 11670	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℝ)
36	32, 35	remulcld 11270	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) ∈ ℝ)
37	7	ad2antrr 726	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ∈ ℝ)
38	25	nnnn0d 12567	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ₀)
39		reexpcl 14101	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (𝐵↑𝑘) ∈ ℝ)
40	37, 38, 39	syl2anc 584	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑘) ∈ ℝ)
41		remulcl 11219	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℝ) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
42	1, 35, 41	sylancr 587	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
43	38	nn0ge0d 12570	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ 𝑘)
44		max1 13206	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
45	28, 19, 44	sylancr 587	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
46		remulcl 11219	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (2 · 𝑛) ∈ ℝ)
47	1, 34, 46	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) ∈ ℝ)
48		eluzle 12870	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘(2 · 𝑛)) → (2 · 𝑛) ≤ 𝑘)
49	48	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) ≤ 𝑘)
50	47, 26, 26, 49	leadd2dd 11857	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (𝑘 + 𝑘))
51	26	recnd 11268	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℂ)
52	51	2timesd 12489	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑘) = (𝑘 + 𝑘))
53	50, 52	breqtrrd 5152	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘))
54		remulcl 11219	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (2 · 𝑘) ∈ ℝ)
55	1, 26, 54	sylancr 587	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑘) ∈ ℝ)
56		leaddsub 11718	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℝ ∧ (2 · 𝑛) ∈ ℝ ∧ (2 · 𝑘) ∈ ℝ) → ((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))))
57	26, 47, 55, 56	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))))
58	53, 57	mpbid 232	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛)))
59		2cnd 12323	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 2 ∈ ℂ)
60	34	recnd 11268	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℂ)
61	59, 51, 60	subdid 11698	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
62	58, 61	breqtrrd 5152	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ≤ (2 · (𝑘 − 𝑛)))
63		max2 13208	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(0 ≤ 𝐴, 𝐴, 0))
64	28, 19, 63	sylancr 587	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐴 ≤ if(0 ≤ 𝐴, 𝐴, 0))
65	26, 42, 19, 30, 43, 45, 62, 64	lemul12bd 12190	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 · 𝐴) ≤ ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
66	19	recnd 11268	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐴 ∈ ℂ)
67	66, 51	mulcomd 11261	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) = (𝑘 · 𝐴))
68	30	recnd 11268	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℂ)
69	35	recnd 11268	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℂ)
70	59, 68, 69	mul32d 11450	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) = ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
71	65, 67, 70	3brtr4d 5156	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ≤ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)))
72	10	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ⁺)
73	72	rpred 13056	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ)
74	73, 35	remulcld 11270	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ)
75	33	nnnn0d 12567	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℕ₀)
76		reexpcl 14101	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) → (𝐵↑𝑛) ∈ ℝ)
77	37, 75, 76	syl2anc 584	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℝ)
78	74, 77	remulcld 11270	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) ∈ ℝ)
79		simplrr 777	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
80	1, 19, 3	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝐴) ∈ ℝ)
81	80, 77, 72	ltdivmuld 13107	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛) ↔ (2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛))))
82	79, 81	mpbid 232	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)))
83	5	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 1 < 𝐵)
84		posdif 11735	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
85	6, 37, 84	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
86	83, 85	mpbid 232	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝐵 − 1))
87	33	nnzd 12620	. . . . . . . . . . 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 11764	. . . . . . . . . . . . 13 ⊢ 0 < 1
91	90	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < 1)
92	88, 89, 37, 91, 83	lttrd 11401	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < 𝐵)
93		expgt0 14118	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 0 < 𝐵) → 0 < (𝐵↑𝑛))
94	37, 87, 92, 93	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝐵↑𝑛))
95	73, 77, 86, 94	mulgt0d 11395	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < ((𝐵 − 1) · (𝐵↑𝑛)))
96		oveq2 7418	. . . . . . . . . . 11 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 𝐴) = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
97	96	breq1d 5134	. . . . . . . . . 10 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → ((2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
98		2t0e0 12414	. . . . . . . . . . . 12 ⊢ (2 · 0) = 0
99		oveq2 7418	. . . . . . . . . . . 12 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 0) = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
100	98, 99	eqtr3id 2785	. . . . . . . . . . 11 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → 0 = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
101	100	breq1d 5134	. . . . . . . . . 10 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → (0 < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
102	97, 101	ifboth 4545	. . . . . . . . 9 ⊢ (((2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ∧ 0 < ((𝐵 − 1) · (𝐵↑𝑛))) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)))
103	82, 95, 102	syl2anc 584	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)))
104	73, 77	remulcld 11270	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝐵↑𝑛)) ∈ ℝ)
105		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ_≥‘(2 · 𝑛)))
106	60	2timesd 12489	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) = (𝑛 + 𝑛))
107	106	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (ℤ_≥‘(2 · 𝑛)) = (ℤ_≥‘(𝑛 + 𝑛)))
108	105, 107	eleqtrd 2837	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ_≥‘(𝑛 + 𝑛)))
109		eluzsub 12887	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑘 ∈ (ℤ_≥‘(𝑛 + 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛))
110	87, 87, 108, 109	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛))
111		eluznn 12939	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛)) → (𝑘 − 𝑛) ∈ ℕ)
112	33, 110, 111	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ)
113	112	nngt0d 12294	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝑘 − 𝑛))
114		ltmul1 12096	. . . . . . . . 9 ⊢ (((2 · if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ ∧ ((𝐵 − 1) · (𝐵↑𝑛)) ∈ ℝ ∧ ((𝑘 − 𝑛) ∈ ℝ ∧ 0 < (𝑘 − 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛))))
115	32, 104, 35, 113, 114	syl112anc 1376	. . . . . . . 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 11268	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℂ)
118	77	recnd 11268	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℂ)
119	117, 118, 69	mul32d 11450	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)) = (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
120	116, 119	breqtrd 5150	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
121		peano2re 11413	. . . . . . . . . 10 ⊢ (((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
122	74, 121	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
123	112	nnnn0d 12567	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ₀)
124		reexpcl 14101	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ₀) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
125	37, 123, 124	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
126	74	ltp1d 12177	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) + 1))
127	88, 37, 92	ltled 11388	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ 𝐵)
128		bernneq2 14253	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ₀ ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛)))
129	37, 123, 127, 128	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛)))
130	74, 122, 125, 126, 129	ltletrd 11400	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (𝐵↑(𝑘 − 𝑛)))
131	37	recnd 11268	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ∈ ℂ)
132	92	gt0ne0d 11806	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ≠ 0)
133		eluzelz 12867	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘(2 · 𝑛)) → 𝑘 ∈ ℤ)
134	133	adantl 481	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℤ)
135		expsub 14133	. . . . . . . . 9 ⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
136	131, 132, 134, 87, 135	syl22anc 838	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
137	130, 136	breqtrd 5150	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛)))
138		ltmuldiv 12120	. . . . . . . 8 ⊢ ((((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ ∧ (𝐵↑𝑘) ∈ ℝ ∧ ((𝐵↑𝑛) ∈ ℝ ∧ 0 < (𝐵↑𝑛))) → ((((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛))))
139	74, 40, 77, 94, 138	syl112anc 1376	. . . . . . 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 11401	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (𝐵↑𝑘))
142	27, 36, 40, 71, 141	lelttrd 11398	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) < (𝐵↑𝑘))
143	142	ralrimiva 3133	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘))
144		fveq2 6881	. . . . 5 ⊢ (𝑗 = (2 · 𝑛) → (ℤ_≥‘𝑗) = (ℤ_≥‘(2 · 𝑛)))
145	144	raleqdv 3309	. . . 4 ⊢ (𝑗 = (2 · 𝑛) → (∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)))
146	145	rspcev 3606	. . 3 ⊢ (((2 · 𝑛) ∈ ℕ₀ ∧ ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
147	18, 143, 146	syl2anc 584	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
148	13, 147	rexlimddv 3148	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 ifcif 4505 class class class wbr 5124 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 · cmul 11139 < clt 11274 ≤ cle 11275 − cmin 11471 / cdiv 11899 ℕcn 12245 2c2 12300 ℕ₀cn0 12506 ℤcz 12593 ℤ_≥cuz 12857 ℝ⁺crp 13013 ↑cexp 14084

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-er 8724 df-en 8965 df-dom 8966 df-sdom 8967 df-sup 9459 df-inf 9460 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-n0 12507 df-z 12594 df-uz 12858 df-rp 13014 df-fl 13814 df-seq 14025 df-exp 14085

This theorem is referenced by: geomulcvg 15897

W3C validator