Proof of Theorem expnbnd
Step | Hyp | Ref
| Expression |
1 | | 1nn 11984 |
. . 3
⊢ 1 ∈
ℕ |
2 | | 1re 10975 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
3 | | lttr 11051 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝐵 ∈
ℝ) → ((𝐴 < 1
∧ 1 < 𝐵) →
𝐴 < 𝐵)) |
4 | 2, 3 | mp3an2 1448 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 1 ∧ 1 < 𝐵) → 𝐴 < 𝐵)) |
5 | 4 | exp4b 431 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 1 → (1 < 𝐵 → 𝐴 < 𝐵)))) |
6 | 5 | com34 91 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 <
𝐵 → (𝐴 < 1 → 𝐴 < 𝐵)))) |
7 | 6 | 3imp1 1346 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → 𝐴 < 𝐵) |
8 | | recn 10961 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
9 | | exp1 13788 |
. . . . . . 7
⊢ (𝐵 ∈ ℂ → (𝐵↑1) = 𝐵) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → (𝐵↑1) = 𝐵) |
11 | 10 | 3ad2ant2 1133 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵↑1) = 𝐵) |
12 | 11 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → (𝐵↑1) = 𝐵) |
13 | 7, 12 | breqtrrd 5102 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → 𝐴 < (𝐵↑1)) |
14 | | oveq2 7283 |
. . . . 5
⊢ (𝑘 = 1 → (𝐵↑𝑘) = (𝐵↑1)) |
15 | 14 | breq2d 5086 |
. . . 4
⊢ (𝑘 = 1 → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑1))) |
16 | 15 | rspcev 3561 |
. . 3
⊢ ((1
∈ ℕ ∧ 𝐴 <
(𝐵↑1)) →
∃𝑘 ∈ ℕ
𝐴 < (𝐵↑𝑘)) |
17 | 1, 13, 16 | sylancr 587 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |
18 | | peano2rem 11288 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ∈
ℝ) |
19 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → (𝐴 − 1) ∈
ℝ) |
20 | | peano2rem 11288 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈
ℝ) |
21 | 20 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵 − 1) ∈
ℝ) |
22 | 21 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → (𝐵 − 1) ∈
ℝ) |
23 | | posdif 11468 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1))) |
24 | 2, 23 | mpan 687 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ → (1 <
𝐵 ↔ 0 < (𝐵 − 1))) |
25 | 24 | biimpa 477 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 < (𝐵 − 1)) |
26 | 25 | gt0ne0d 11539 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵 − 1) ≠
0) |
27 | 26 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → (𝐵 − 1) ≠
0) |
28 | 19, 22, 27 | redivcld 11803 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈
ℝ) |
29 | 28 | adantll 711 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈
ℝ) |
30 | 18 | adantl 482 |
. . . . . . . . . 10
⊢ ((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) → (𝐴 − 1) ∈ ℝ) |
31 | | subge0 11488 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (0 ≤ (𝐴
− 1) ↔ 1 ≤ 𝐴)) |
32 | 2, 31 | mpan2 688 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (0 ≤
(𝐴 − 1) ↔ 1 ≤
𝐴)) |
33 | 32 | biimparc 480 |
. . . . . . . . . 10
⊢ ((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) → 0 ≤ (𝐴 − 1)) |
34 | 30, 33 | jca 512 |
. . . . . . . . 9
⊢ ((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) → ((𝐴 − 1) ∈ ℝ ∧ 0 ≤
(𝐴 −
1))) |
35 | 21, 25 | jca 512 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → ((𝐵 − 1) ∈ ℝ ∧
0 < (𝐵 −
1))) |
36 | | divge0 11844 |
. . . . . . . . 9
⊢ ((((𝐴 − 1) ∈ ℝ ∧
0 ≤ (𝐴 − 1)) ∧
((𝐵 − 1) ∈
ℝ ∧ 0 < (𝐵
− 1))) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1))) |
37 | 34, 35, 36 | syl2an 596 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1))) |
38 | | flge0nn0 13540 |
. . . . . . . 8
⊢ ((((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ ∧ 0 ≤
((𝐴 − 1) / (𝐵 − 1))) →
(⌊‘((𝐴 −
1) / (𝐵 − 1))) ∈
ℕ0) |
39 | 29, 37, 38 | syl2anc 584 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈
ℕ0) |
40 | | nn0p1nn 12272 |
. . . . . . 7
⊢
((⌊‘((𝐴
− 1) / (𝐵 −
1))) ∈ ℕ0 → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈
ℕ) |
41 | 39, 40 | syl 17 |
. . . . . 6
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) →
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ) |
42 | | simplr 766 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 ∈ ℝ) |
43 | 21 | adantl 482 |
. . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵 − 1) ∈ ℝ) |
44 | | peano2nn0 12273 |
. . . . . . . . . . 11
⊢
((⌊‘((𝐴
− 1) / (𝐵 −
1))) ∈ ℕ0 → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈
ℕ0) |
45 | 39, 44 | syl 17 |
. . . . . . . . . 10
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) →
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ0) |
46 | 45 | nn0red 12294 |
. . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) →
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℝ) |
47 | 43, 46 | remulcld 11005 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈
ℝ) |
48 | | peano2re 11148 |
. . . . . . . 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 768 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐵 ∈ ℝ) |
51 | | reexpcl 13799 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ0) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈
ℝ) |
52 | 50, 45, 51 | syl2anc 584 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈
ℝ) |
53 | | flltp1 13520 |
. . . . . . . . . 10
⊢ (((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ → ((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) |
54 | 29, 53 | syl 17 |
. . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) |
55 | 30 | adantr 481 |
. . . . . . . . . 10
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) ∈ ℝ) |
56 | 25 | adantl 482 |
. . . . . . . . . 10
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 < (𝐵 − 1)) |
57 | | ltdivmul 11850 |
. . . . . . . . . 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 1373 |
. . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ↔ (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))) |
59 | 54, 58 | mpbid 231 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
60 | | ltsubadd 11445 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ ((𝐵 −
1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ) →
((𝐴 − 1) < ((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
↔ 𝐴 < (((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
+ 1))) |
61 | 2, 60 | mp3an2 1448 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
∈ ℝ) → ((𝐴
− 1) < ((𝐵 −
1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1))) |
62 | 42, 47, 61 | syl2anc 584 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1))) |
63 | 59, 62 | mpbid 231 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1)) |
64 | | 0lt1 11497 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
65 | | 0re 10977 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
66 | | lttr 11051 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 1 ∧ 1
< 𝐵) → 0 < 𝐵)) |
67 | 65, 2, 66 | mp3an12 1450 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → ((0 <
1 ∧ 1 < 𝐵) → 0
< 𝐵)) |
68 | 64, 67 | mpani 693 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (1 <
𝐵 → 0 < 𝐵)) |
69 | | ltle 11063 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → (0 < 𝐵 → 0 ≤ 𝐵)) |
70 | 65, 69 | mpan 687 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (0 <
𝐵 → 0 ≤ 𝐵)) |
71 | 68, 70 | syld 47 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → (1 <
𝐵 → 0 ≤ 𝐵)) |
72 | 71 | imp 407 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 ≤ 𝐵) |
73 | 72 | adantl 482 |
. . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 ≤ 𝐵) |
74 | | bernneq2 13945 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ0 ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
75 | 50, 45, 73, 74 | syl3anc 1370 |
. . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
76 | 42, 49, 52, 63, 75 | ltletrd 11135 |
. . . . . 6
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
77 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐵↑𝑘) = (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) |
78 | 77 | breq2d 5086 |
. . . . . . 7
⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))) |
79 | 78 | rspcev 3561 |
. . . . . 6
⊢
((((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ ∧
𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |
80 | 41, 76, 79 | syl2anc 584 |
. . . . 5
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |
81 | 80 | exp43 437 |
. . . 4
⊢ (1 ≤
𝐴 → (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 < 𝐵 → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))))) |
82 | 81 | com4l 92 |
. . 3
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 <
𝐵 → (1 ≤ 𝐴 → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))))) |
83 | 82 | 3imp1 1346 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 1 ≤ 𝐴) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |
84 | | simp1 1135 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐴 ∈ ℝ) |
85 | | 1red 10976 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 1 ∈
ℝ) |
86 | 17, 83, 84, 85 | ltlecasei 11083 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |