Proof of Theorem expnbnd
Step | Hyp | Ref
| Expression |
1 | | 1nn 11720 |
. . 3
⊢ 1 ∈
ℕ |
2 | | 1re 10712 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
3 | | lttr 10788 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝐵 ∈
ℝ) → ((𝐴 < 1
∧ 1 < 𝐵) →
𝐴 < 𝐵)) |
4 | 2, 3 | mp3an2 1450 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 1 ∧ 1 < 𝐵) → 𝐴 < 𝐵)) |
5 | 4 | exp4b 434 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 1 → (1 < 𝐵 → 𝐴 < 𝐵)))) |
6 | 5 | com34 91 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 <
𝐵 → (𝐴 < 1 → 𝐴 < 𝐵)))) |
7 | 6 | 3imp1 1348 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → 𝐴 < 𝐵) |
8 | | recn 10698 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
9 | | exp1 13520 |
. . . . . . 7
⊢ (𝐵 ∈ ℂ → (𝐵↑1) = 𝐵) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → (𝐵↑1) = 𝐵) |
11 | 10 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵↑1) = 𝐵) |
12 | 11 | adantr 484 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → (𝐵↑1) = 𝐵) |
13 | 7, 12 | breqtrrd 5055 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → 𝐴 < (𝐵↑1)) |
14 | | oveq2 7172 |
. . . . 5
⊢ (𝑘 = 1 → (𝐵↑𝑘) = (𝐵↑1)) |
15 | 14 | breq2d 5039 |
. . . 4
⊢ (𝑘 = 1 → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑1))) |
16 | 15 | rspcev 3524 |
. . 3
⊢ ((1
∈ ℕ ∧ 𝐴 <
(𝐵↑1)) →
∃𝑘 ∈ ℕ
𝐴 < (𝐵↑𝑘)) |
17 | 1, 13, 16 | sylancr 590 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |
18 | | peano2rem 11024 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ∈
ℝ) |
19 | 18 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → (𝐴 − 1) ∈
ℝ) |
20 | | peano2rem 11024 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈
ℝ) |
21 | 20 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵 − 1) ∈
ℝ) |
22 | 21 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → (𝐵 − 1) ∈
ℝ) |
23 | | posdif 11204 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1))) |
24 | 2, 23 | mpan 690 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ → (1 <
𝐵 ↔ 0 < (𝐵 − 1))) |
25 | 24 | biimpa 480 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 < (𝐵 − 1)) |
26 | 25 | gt0ne0d 11275 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵 − 1) ≠
0) |
27 | 26 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → (𝐵 − 1) ≠
0) |
28 | 19, 22, 27 | redivcld 11539 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈
ℝ) |
29 | 28 | adantll 714 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈
ℝ) |
30 | 18 | adantl 485 |
. . . . . . . . . 10
⊢ ((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) → (𝐴 − 1) ∈ ℝ) |
31 | | subge0 11224 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (0 ≤ (𝐴
− 1) ↔ 1 ≤ 𝐴)) |
32 | 2, 31 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (0 ≤
(𝐴 − 1) ↔ 1 ≤
𝐴)) |
33 | 32 | biimparc 483 |
. . . . . . . . . 10
⊢ ((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) → 0 ≤ (𝐴 − 1)) |
34 | 30, 33 | jca 515 |
. . . . . . . . 9
⊢ ((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) → ((𝐴 − 1) ∈ ℝ ∧ 0 ≤
(𝐴 −
1))) |
35 | 21, 25 | jca 515 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → ((𝐵 − 1) ∈ ℝ ∧
0 < (𝐵 −
1))) |
36 | | divge0 11580 |
. . . . . . . . 9
⊢ ((((𝐴 − 1) ∈ ℝ ∧
0 ≤ (𝐴 − 1)) ∧
((𝐵 − 1) ∈
ℝ ∧ 0 < (𝐵
− 1))) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1))) |
37 | 34, 35, 36 | syl2an 599 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1))) |
38 | | flge0nn0 13274 |
. . . . . . . 8
⊢ ((((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ ∧ 0 ≤
((𝐴 − 1) / (𝐵 − 1))) →
(⌊‘((𝐴 −
1) / (𝐵 − 1))) ∈
ℕ0) |
39 | 29, 37, 38 | syl2anc 587 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈
ℕ0) |
40 | | nn0p1nn 12008 |
. . . . . . 7
⊢
((⌊‘((𝐴
− 1) / (𝐵 −
1))) ∈ ℕ0 → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈
ℕ) |
41 | 39, 40 | syl 17 |
. . . . . 6
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) →
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ) |
42 | | simplr 769 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 ∈ ℝ) |
43 | 21 | adantl 485 |
. . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵 − 1) ∈ ℝ) |
44 | | peano2nn0 12009 |
. . . . . . . . . . 11
⊢
((⌊‘((𝐴
− 1) / (𝐵 −
1))) ∈ ℕ0 → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈
ℕ0) |
45 | 39, 44 | syl 17 |
. . . . . . . . . 10
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) →
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ0) |
46 | 45 | nn0red 12030 |
. . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) →
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℝ) |
47 | 43, 46 | remulcld 10742 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈
ℝ) |
48 | | peano2re 10884 |
. . . . . . . 8
⊢ (((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
∈ ℝ → (((𝐵
− 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ∈
ℝ) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ∈
ℝ) |
50 | | simprl 771 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐵 ∈ ℝ) |
51 | | reexpcl 13531 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ0) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈
ℝ) |
52 | 50, 45, 51 | syl2anc 587 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈
ℝ) |
53 | | flltp1 13254 |
. . . . . . . . . 10
⊢ (((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ → ((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) |
54 | 29, 53 | syl 17 |
. . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) |
55 | 30 | adantr 484 |
. . . . . . . . . 10
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) ∈ ℝ) |
56 | 25 | adantl 485 |
. . . . . . . . . 10
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 < (𝐵 − 1)) |
57 | | ltdivmul 11586 |
. . . . . . . . . 10
⊢ (((𝐴 − 1) ∈ ℝ ∧
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℝ ∧ ((𝐵
− 1) ∈ ℝ ∧ 0 < (𝐵 − 1))) → (((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ↔ (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))) |
58 | 55, 46, 43, 56, 57 | syl112anc 1375 |
. . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ↔ (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))) |
59 | 54, 58 | mpbid 235 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
60 | | ltsubadd 11181 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ ((𝐵 −
1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ) →
((𝐴 − 1) < ((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
↔ 𝐴 < (((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
+ 1))) |
61 | 2, 60 | mp3an2 1450 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
∈ ℝ) → ((𝐴
− 1) < ((𝐵 −
1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1))) |
62 | 42, 47, 61 | syl2anc 587 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1))) |
63 | 59, 62 | mpbid 235 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1)) |
64 | | 0lt1 11233 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
65 | | 0re 10714 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
66 | | lttr 10788 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 1 ∧ 1
< 𝐵) → 0 < 𝐵)) |
67 | 65, 2, 66 | mp3an12 1452 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → ((0 <
1 ∧ 1 < 𝐵) → 0
< 𝐵)) |
68 | 64, 67 | mpani 696 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (1 <
𝐵 → 0 < 𝐵)) |
69 | | ltle 10800 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → (0 < 𝐵 → 0 ≤ 𝐵)) |
70 | 65, 69 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (0 <
𝐵 → 0 ≤ 𝐵)) |
71 | 68, 70 | syld 47 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → (1 <
𝐵 → 0 ≤ 𝐵)) |
72 | 71 | imp 410 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 ≤ 𝐵) |
73 | 72 | adantl 485 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 ≤ 𝐵) |
74 | | bernneq2 13676 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ0 ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
75 | 50, 45, 73, 74 | syl3anc 1372 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
76 | 42, 49, 52, 63, 75 | ltletrd 10871 |
. . . . . 6
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
77 | | oveq2 7172 |
. . . . . . . 8
⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐵↑𝑘) = (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
78 | 77 | breq2d 5039 |
. . . . . . 7
⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))) |
79 | 78 | rspcev 3524 |
. . . . . 6
⊢
((((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ ∧
𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |
80 | 41, 76, 79 | syl2anc 587 |
. . . . 5
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |
81 | 80 | exp43 440 |
. . . 4
⊢ (1 ≤
𝐴 → (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 < 𝐵 → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))))) |
82 | 81 | com4l 92 |
. . 3
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 <
𝐵 → (1 ≤ 𝐴 → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))))) |
83 | 82 | 3imp1 1348 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 1 ≤ 𝐴) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |
84 | | simp1 1137 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐴 ∈ ℝ) |
85 | | 1red 10713 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 1 ∈
ℝ) |
86 | 17, 83, 84, 85 | ltlecasei 10819 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |