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 13950

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 12047	. . . . 5 ⊢ 2 ∈ ℝ
2		simp1 1135	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐴 ∈ ℝ)
3		remulcl 10956	. . . . 5 ⊢ ((2 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (2 · 𝐴) ∈ ℝ)
4	1, 2, 3	sylancr 587	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (2 · 𝐴) ∈ ℝ)
5		simp3 1137	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 1 < 𝐵)
6		1re 10975	. . . . . 6 ⊢ 1 ∈ ℝ
7		simp2 1136	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐵 ∈ ℝ)
8		difrp 12768	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 ↔ (𝐵 − 1) ∈ ℝ⁺))
9	6, 7, 8	sylancr 587	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (1 < 𝐵 ↔ (𝐵 − 1) ∈ ℝ⁺))
10	5, 9	mpbid 231	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) ∈ ℝ⁺)
11	4, 10	rerpdivcld 12803	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ)
12		expnbnd 13947	. . 3 ⊢ ((((2 · 𝐴) / (𝐵 − 1)) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
13	11, 7, 5, 12	syl3anc 1370	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑛 ∈ ℕ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
14		2nn0 12250	. . . 4 ⊢ 2 ∈ ℕ₀
15		nnnn0 12240	. . . . 5 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
16	15	ad2antrl 725	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ₀)
17		nn0mulcl 12269	. . . 4 ⊢ ((2 ∈ ℕ₀ ∧ 𝑛 ∈ ℕ₀) → (2 · 𝑛) ∈ ℕ₀)
18	14, 16, 17	sylancr 587	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ₀)
19	2	ad2antrr 723	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐴 ∈ ℝ)
20		2nn 12046	. . . . . . . . 9 ⊢ 2 ∈ ℕ
21		simprl 768	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → 𝑛 ∈ ℕ)
22		nnmulcl 11997	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
23	20, 21, 22	sylancr 587	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → (2 · 𝑛) ∈ ℕ)
24		eluznn 12658	. . . . . . . 8 ⊢ (((2 · 𝑛) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
25	23, 24	sylan 580	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ)
26	25	nnred 11988	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℝ)
27	19, 26	remulcld 11005	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ∈ ℝ)
28		0re 10977	. . . . . . . 8 ⊢ 0 ∈ ℝ
29		ifcl 4504	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
30	19, 28, 29	sylancl 586	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℝ)
31		remulcl 10956	. . . . . . 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 774	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℕ)
34	33	nnred 11988	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℝ)
35	26, 34	resubcld 11403	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℝ)
36	32, 35	remulcld 11005	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) ∈ ℝ)
37	7	ad2antrr 723	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ∈ ℝ)
38	25	nnnn0d 12293	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℕ₀)
39		reexpcl 13799	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (𝐵↑𝑘) ∈ ℝ)
40	37, 38, 39	syl2anc 584	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑘) ∈ ℝ)
41		remulcl 10956	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℝ) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
42	1, 35, 41	sylancr 587	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) ∈ ℝ)
43	38	nn0ge0d 12296	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ 𝑘)
44		max1 12919	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
45	28, 19, 44	sylancr 587	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ if(0 ≤ 𝐴, 𝐴, 0))
46		remulcl 10956	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (2 · 𝑛) ∈ ℝ)
47	1, 34, 46	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) ∈ ℝ)
48		eluzle 12595	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘(2 · 𝑛)) → (2 · 𝑛) ≤ 𝑘)
49	48	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) ≤ 𝑘)
50	47, 26, 26, 49	leadd2dd 11590	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (𝑘 + 𝑘))
51	26	recnd 11003	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℂ)
52	51	2timesd 12216	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑘) = (𝑘 + 𝑘))
53	50, 52	breqtrrd 5102	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘))
54		remulcl 10956	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (2 · 𝑘) ∈ ℝ)
55	1, 26, 54	sylancr 587	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑘) ∈ ℝ)
56		leaddsub 11451	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℝ ∧ (2 · 𝑛) ∈ ℝ ∧ (2 · 𝑘) ∈ ℝ) → ((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))))
57	26, 47, 55, 56	syl3anc 1370	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝑘 + (2 · 𝑛)) ≤ (2 · 𝑘) ↔ 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛))))
58	53, 57	mpbid 231	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ≤ ((2 · 𝑘) − (2 · 𝑛)))
59		2cnd 12051	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 2 ∈ ℂ)
60	34	recnd 11003	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℂ)
61	59, 51, 60	subdid 11431	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
62	58, 61	breqtrrd 5102	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ≤ (2 · (𝑘 − 𝑛)))
63		max2 12921	. . . . . . . 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 11918	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 · 𝐴) ≤ ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
66	19	recnd 11003	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐴 ∈ ℂ)
67	66, 51	mulcomd 10996	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) = (𝑘 · 𝐴))
68	30	recnd 11003	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → if(0 ≤ 𝐴, 𝐴, 0) ∈ ℂ)
69	35	recnd 11003	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℂ)
70	59, 68, 69	mul32d 11185	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) = ((2 · (𝑘 − 𝑛)) · if(0 ≤ 𝐴, 𝐴, 0)))
71	65, 67, 70	3brtr4d 5106	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) ≤ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)))
72	10	ad2antrr 723	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ⁺)
73	72	rpred 12772	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℝ)
74	73, 35	remulcld 11005	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ)
75	33	nnnn0d 12293	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑛 ∈ ℕ₀)
76		reexpcl 13799	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) → (𝐵↑𝑛) ∈ ℝ)
77	37, 75, 76	syl2anc 584	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℝ)
78	74, 77	remulcld 11005	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) ∈ ℝ)
79		simplrr 775	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))
80	1, 19, 3	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝐴) ∈ ℝ)
81	80, 77, 72	ltdivmuld 12823	. . . . . . . . . 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 11468	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
85	6, 37, 84	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
86	83, 85	mpbid 231	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝐵 − 1))
87	33	nnzd 12425	. . . . . . . . . . 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 11497	. . . . . . . . . . . . 13 ⊢ 0 < 1
91	90	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < 1)
92	88, 89, 37, 91, 83	lttrd 11136	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < 𝐵)
93		expgt0 13816	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 0 < 𝐵) → 0 < (𝐵↑𝑛))
94	37, 87, 92, 93	syl3anc 1370	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝐵↑𝑛))
95	73, 77, 86, 94	mulgt0d 11130	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < ((𝐵 − 1) · (𝐵↑𝑛)))
96		oveq2 7283	. . . . . . . . . . 11 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 𝐴) = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
97	96	breq1d 5084	. . . . . . . . . 10 ⊢ (𝐴 = if(0 ≤ 𝐴, 𝐴, 0) → ((2 · 𝐴) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
98		2t0e0 12142	. . . . . . . . . . . 12 ⊢ (2 · 0) = 0
99		oveq2 7283	. . . . . . . . . . . 12 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → (2 · 0) = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
100	98, 99	eqtr3id 2792	. . . . . . . . . . 11 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → 0 = (2 · if(0 ≤ 𝐴, 𝐴, 0)))
101	100	breq1d 5084	. . . . . . . . . 10 ⊢ (0 = if(0 ≤ 𝐴, 𝐴, 0) → (0 < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ (2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛))))
102	97, 101	ifboth 4498	. . . . . . . . 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 11005	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝐵↑𝑛)) ∈ ℝ)
105		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ_≥‘(2 · 𝑛)))
106	60	2timesd 12216	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (2 · 𝑛) = (𝑛 + 𝑛))
107	106	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (ℤ_≥‘(2 · 𝑛)) = (ℤ_≥‘(𝑛 + 𝑛)))
108	105, 107	eleqtrd 2841	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ (ℤ_≥‘(𝑛 + 𝑛)))
109		eluzsub 12614	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑘 ∈ (ℤ_≥‘(𝑛 + 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛))
110	87, 87, 108, 109	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛))
111		eluznn 12658	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ (𝑘 − 𝑛) ∈ (ℤ_≥‘𝑛)) → (𝑘 − 𝑛) ∈ ℕ)
112	33, 110, 111	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ)
113	112	nngt0d 12022	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 < (𝑘 − 𝑛))
114		ltmul1 11825	. . . . . . . . 9 ⊢ (((2 · if(0 ≤ 𝐴, 𝐴, 0)) ∈ ℝ ∧ ((𝐵 − 1) · (𝐵↑𝑛)) ∈ ℝ ∧ ((𝑘 − 𝑛) ∈ ℝ ∧ 0 < (𝑘 − 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) < ((𝐵 − 1) · (𝐵↑𝑛)) ↔ ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛))))
115	32, 104, 35, 113, 114	syl112anc 1373	. . . . . . . 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 11003	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵 − 1) ∈ ℂ)
118	77	recnd 11003	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑𝑛) ∈ ℂ)
119	117, 118, 69	mul32d 11185	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝐵↑𝑛)) · (𝑘 − 𝑛)) = (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
120	116, 119	breqtrd 5100	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)))
121		peano2re 11148	. . . . . . . . . 10 ⊢ (((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
122	74, 121	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ∈ ℝ)
123	112	nnnn0d 12293	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝑘 − 𝑛) ∈ ℕ₀)
124		reexpcl 13799	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ₀) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
125	37, 123, 124	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) ∈ ℝ)
126	74	ltp1d 11905	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (((𝐵 − 1) · (𝑘 − 𝑛)) + 1))
127	88, 37, 92	ltled 11123	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 0 ≤ 𝐵)
128		bernneq2 13945	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ (𝑘 − 𝑛) ∈ ℕ₀ ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛)))
129	37, 123, 127, 128	syl3anc 1370	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) + 1) ≤ (𝐵↑(𝑘 − 𝑛)))
130	74, 122, 125, 126, 129	ltletrd 11135	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < (𝐵↑(𝑘 − 𝑛)))
131	37	recnd 11003	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ∈ ℂ)
132	92	gt0ne0d 11539	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝐵 ≠ 0)
133		eluzelz 12592	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘(2 · 𝑛)) → 𝑘 ∈ ℤ)
134	133	adantl 482	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → 𝑘 ∈ ℤ)
135		expsub 13831	. . . . . . . . 9 ⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
136	131, 132, 134, 87, 135	syl22anc 836	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐵↑(𝑘 − 𝑛)) = ((𝐵↑𝑘) / (𝐵↑𝑛)))
137	130, 136	breqtrd 5100	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛)))
138		ltmuldiv 11848	. . . . . . . 8 ⊢ ((((𝐵 − 1) · (𝑘 − 𝑛)) ∈ ℝ ∧ (𝐵↑𝑘) ∈ ℝ ∧ ((𝐵↑𝑛) ∈ ℝ ∧ 0 < (𝐵↑𝑛))) → ((((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛))))
139	74, 40, 77, 94, 138	syl112anc 1373	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘) ↔ ((𝐵 − 1) · (𝑘 − 𝑛)) < ((𝐵↑𝑘) / (𝐵↑𝑛))))
140	137, 139	mpbird 256	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (((𝐵 − 1) · (𝑘 − 𝑛)) · (𝐵↑𝑛)) < (𝐵↑𝑘))
141	36, 78, 40, 120, 140	lttrd 11136	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → ((2 · if(0 ≤ 𝐴, 𝐴, 0)) · (𝑘 − 𝑛)) < (𝐵↑𝑘))
142	27, 36, 40, 71, 141	lelttrd 11133	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) ∧ 𝑘 ∈ (ℤ_≥‘(2 · 𝑛))) → (𝐴 · 𝑘) < (𝐵↑𝑘))
143	142	ralrimiva 3103	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘))
144		fveq2 6774	. . . . 5 ⊢ (𝑗 = (2 · 𝑛) → (ℤ_≥‘𝑗) = (ℤ_≥‘(2 · 𝑛)))
145	144	raleqdv 3348	. . . 4 ⊢ (𝑗 = (2 · 𝑛) → (∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘) ↔ ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)))
146	145	rspcev 3561	. . 3 ⊢ (((2 · 𝑛) ∈ ℕ₀ ∧ ∀𝑘 ∈ (ℤ_≥‘(2 · 𝑛))(𝐴 · 𝑘) < (𝐵↑𝑘)) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
147	18, 143, 146	syl2anc 584	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ (𝑛 ∈ ℕ ∧ ((2 · 𝐴) / (𝐵 − 1)) < (𝐵↑𝑛))) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))
148	13, 147	rexlimddv 3220	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ₀ ∀𝑘 ∈ (ℤ_≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 ifcif 4459 class class class wbr 5074 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 < clt 11009 ≤ cle 11010 − cmin 11205 / cdiv 11632 ℕcn 11973 2c2 12028 ℕ₀cn0 12233 ℤcz 12319 ℤ_≥cuz 12582 ℝ⁺crp 12730 ↑cexp 13782

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-sup 9201 df-inf 9202 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-n0 12234 df-z 12320 df-uz 12583 df-rp 12731 df-fl 13512 df-seq 13722 df-exp 13783

This theorem is referenced by: geomulcvg 15588

W3C validator