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 14200

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 12260	. . . . 5 ⊢ 2 ∈ ℝ
2		simp1 1136	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐴 ∈ ℝ)
3		remulcl 11153	. . . . 5 ⊢ ((2 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (2 · 𝐴) ∈ ℝ)
4	1, 2, 3	sylancr 587	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (2 · 𝐴) ∈ ℝ)
5		simp3 1138	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 1 < 𝐵)
6		1re 11174	. . . . . 6 ⊢ 1 ∈ ℝ
7		simp2 1137	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐵 ∈ ℝ)
8		difrp 12991	. . . . . 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 13026	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ)
12		expnbnd 14197	. . 3 ⊢ ((((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
13	11, 7, 5, 12	syl3anc 1373	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
14		2nn0 12459	. . . 4 ⊢ 2 ∈ ℕ₀
15		nnnn0 12449	. . . . 5 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
16	15	ad2antrl 728	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ₀)
17		nn0mulcl 12478	. . . 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 12259	. . . . . . . . 9 ⊢ 2 ∈ ℕ
21		simprl 770	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ)
22		nnmulcl 12210	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
23	20, 21, 22	sylancr 587	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ)
24		eluznn 12877	. . . . . . . 8 ⊢ (((2 · 𝑛) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
25	23, 24	sylan 580	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
26	25	nnred 12201	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℝ)
27	19, 26	remulcld 11204	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ∈ ℝ)
28		0re 11176	. . . . . . . 8 ⊢ 0 ∈ ℝ
29		ifcl 4534	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
30	19, 28, 29	sylancl 586	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
31		remulcl 11153	. . . . . . 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 12201	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℝ)
35	26, 34	resubcld 11606	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℝ)
36	32, 35	remulcld 11204	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) ∈ ℝ)
37	7	ad2antrr 726	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ∈ ℝ)
38	25	nnnn0d 12503	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ₀)
39		reexpcl 14043	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (𝐵↑𝑘) ∈ ℝ)
40	37, 38, 39	syl2anc 584	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑘) ∈ ℝ)
41		remulcl 11153	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℝ) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
42	1, 35, 41	sylancr 587	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
43	38	nn0ge0d 12506	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ 𝑘)
44		max1 13145	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
45	28, 19, 44	sylancr 587	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
46		remulcl 11153	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (2 · 𝑛) ∈ ℝ)
47	1, 34, 46	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) ∈ ℝ)
48		eluzle 12806	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘(2 · 𝑛)) → (2 · 𝑛) ≤ 𝑘)
49	48	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) ≤ 𝑘)
50	47, 26, 26, 49	leadd2dd 11793	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (𝑘 + 𝑘))
51	26	recnd 11202	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℂ)
52	51	2timesd 12425	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑘) = (𝑘 + 𝑘))
53	50, 52	breqtrrd 5135	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘))
54		remulcl 11153	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (2 · 𝑘) ∈ ℝ)
55	1, 26, 54	sylancr 587	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑘) ∈ ℝ)
56		leaddsub 11654	. . . . . . . . . 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 12264	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 2 ∈ ℂ)
60	34	recnd 11202	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℂ)
61	59, 51, 60	subdid 11634	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
62	58, 61	breqtrrd 5135	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ≤ (2 · (𝑘 − 𝑛)))
63		max2 13147	. . . . . . . 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 12126	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 · 𝐴) ≤ ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
66	19	recnd 11202	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐴 ∈ ℂ)
67	66, 51	mulcomd 11195	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) = (𝑘 · 𝐴))
68	30	recnd 11202	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℂ)
69	35	recnd 11202	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℂ)
70	59, 68, 69	mul32d 11384	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) = ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
71	65, 67, 70	3brtr4d 5139	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ≤ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)))
72	10	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ⁺)
73	72	rpred 12995	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ)
74	73, 35	remulcld 11204	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ)
75	33	nnnn0d 12503	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℕ₀)
76		reexpcl 14043	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) → (𝐵↑𝑛) ∈ ℝ)
77	37, 75, 76	syl2anc 584	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℝ)
78	74, 77	remulcld 11204	. . . . . 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 13046	. . . . . . . . . 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 11671	. . . . . . . . . . . 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 12556	. . . . . . . . . . 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 11700	. . . . . . . . . . . . 13 ⊢ 0 < 1
91	90	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < 1)
92	88, 89, 37, 91, 83	lttrd 11335	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < 𝐵)
93		expgt0 14060	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 0 < 𝐵) → 0 < (𝐵↑𝑛))
94	37, 87, 92, 93	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝐵↑𝑛))
95	73, 77, 86, 94	mulgt0d 11329	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < ((𝐵 − 1) · (𝐵↑𝑛)))
96		oveq2 7395	. . . . . . . . . . 11 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 𝐴) = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
97	96	breq1d 5117	. . . . . . . . . 10 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → ((2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
98		2t0e0 12350	. . . . . . . . . . . 12 ⊢ (2 · 0) = 0
99		oveq2 7395	. . . . . . . . . . . 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 5117	. . . . . . . . . 10 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → (0 < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
102	97, 101	ifboth 4528	. . . . . . . . 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 11204	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝐵↑𝑛)) ∈ ℝ)
105		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ_≥‘(2 · 𝑛)))
106	60	2timesd 12425	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) = (𝑛 + 𝑛))
107	106	fveq2d 6862	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (ℤ_≥‘(2 · 𝑛)) = (ℤ_≥‘(𝑛 + 𝑛)))
108	105, 107	eleqtrd 2830	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ_≥‘(𝑛 + 𝑛)))
109		eluzsub 12823	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑘 ∈ (ℤ_≥‘(𝑛 + 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛))
110	87, 87, 108, 109	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛))
111		eluznn 12877	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛)) → (𝑘 − 𝑛) ∈ ℕ)
112	33, 110, 111	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ)
113	112	nngt0d 12235	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝑘 − 𝑛))
114		ltmul1 12032	. . . . . . . . 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 11202	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℂ)
118	77	recnd 11202	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℂ)
119	117, 118, 69	mul32d 11384	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)) = (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
120	116, 119	breqtrd 5133	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
121		peano2re 11347	. . . . . . . . . 10 ⊢ (((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
122	74, 121	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
123	112	nnnn0d 12503	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ₀)
124		reexpcl 14043	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ₀) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
125	37, 123, 124	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
126	74	ltp1d 12113	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) + 1))
127	88, 37, 92	ltled 11322	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ 𝐵)
128		bernneq2 14195	. . . . . . . . . 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 11334	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (𝐵↑(𝑘 − 𝑛)))
131	37	recnd 11202	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ∈ ℂ)
132	92	gt0ne0d 11742	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ≠ 0)
133		eluzelz 12803	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘(2 · 𝑛)) → 𝑘 ∈ ℤ)
134	133	adantl 481	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℤ)
135		expsub 14075	. . . . . . . . 9 ⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
136	131, 132, 134, 87, 135	syl22anc 838	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
137	130, 136	breqtrd 5133	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛)))
138		ltmuldiv 12056	. . . . . . . 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 11335	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (𝐵↑𝑘))
142	27, 36, 40, 71, 141	lelttrd 11332	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) < (𝐵↑𝑘))
143	142	ralrimiva 3125	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘))
144		fveq2 6858	. . . . 5 ⊢ (𝑗 = (2 · 𝑛) → (ℤ_≥‘𝑗) = (ℤ_≥‘(2 · 𝑛)))
145	144	raleqdv 3299	. . . 4 ⊢ (𝑗 = (2 · 𝑛) → (∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)))
146	145	rspcev 3588	. . 3 ⊢ (((2 · 𝑛) ∈ ℕ₀ ∧ ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
147	18, 143, 146	syl2anc 584	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
148	13, 147	rexlimddv 3140	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 ifcif 4488 class class class wbr 5107 ‘cfv 6511 (class class class)co 7387 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 < clt 11208 ≤ cle 11209 − cmin 11405 / cdiv 11835 ℕcn 12186 2c2 12241 ℕ₀cn0 12442 ℤcz 12529 ℤ_≥cuz 12793 ℝ⁺crp 12951 ↑cexp 14026

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 2701 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-sup 9393 df-inf 9394 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-n0 12443 df-z 12530 df-uz 12794 df-rp 12952 df-fl 13754 df-seq 13967 df-exp 14027

This theorem is referenced by: geomulcvg 15842

W3C validator