Step | Hyp | Ref
| Expression |
1 | | 2re 10967 |
. . . . . 6
⊢ 2 ∈
ℝ |
2 | | ostth2lem1.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 1 < 𝐴) → 𝐵 ∈ ℝ) |
4 | | remulcl 9900 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ) → (2 · 𝐵) ∈ ℝ) |
5 | 1, 3, 4 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 1 < 𝐴) → (2 · 𝐵) ∈ ℝ) |
6 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 1 < 𝐴) → 1 < 𝐴) |
7 | | 1re 9918 |
. . . . . . 7
⊢ 1 ∈
ℝ |
8 | | ostth2lem1.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 1 < 𝐴) → 𝐴 ∈ ℝ) |
10 | | difrp 11744 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ 𝐴
∈ ℝ) → (1 < 𝐴 ↔ (𝐴 − 1) ∈
ℝ+)) |
11 | 7, 9, 10 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 1 < 𝐴) → (1 < 𝐴 ↔ (𝐴 − 1) ∈
ℝ+)) |
12 | 6, 11 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ 1 < 𝐴) → (𝐴 − 1) ∈
ℝ+) |
13 | 5, 12 | rerpdivcld 11779 |
. . . 4
⊢ ((𝜑 ∧ 1 < 𝐴) → ((2 · 𝐵) / (𝐴 − 1)) ∈
ℝ) |
14 | | expnbnd 12855 |
. . . 4
⊢ ((((2
· 𝐵) / (𝐴 − 1)) ∈ ℝ
∧ 𝐴 ∈ ℝ
∧ 1 < 𝐴) →
∃𝑘 ∈ ℕ ((2
· 𝐵) / (𝐴 − 1)) < (𝐴↑𝑘)) |
15 | 13, 9, 6, 14 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 1 < 𝐴) → ∃𝑘 ∈ ℕ ((2 · 𝐵) / (𝐴 − 1)) < (𝐴↑𝑘)) |
16 | | nnnn0 11176 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
17 | | reexpcl 12739 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℝ) |
18 | 9, 16, 17 | syl2an 493 |
. . . . 5
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℝ) |
19 | 13 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ((2 · 𝐵) / (𝐴 − 1)) ∈
ℝ) |
20 | 12 | rpred 11748 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 1 < 𝐴) → (𝐴 − 1) ∈ ℝ) |
21 | 20 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴 − 1) ∈ ℝ) |
22 | | nnre 10904 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
23 | 22 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ) |
24 | 21, 23 | remulcld 9949 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝐴 − 1) · 𝑘) ∈ ℝ) |
25 | 24, 18 | remulcld 9949 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · 𝑘) · (𝐴↑𝑘)) ∈ ℝ) |
26 | 8 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ) |
27 | | 2nn 11062 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
28 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
29 | | nnmulcl 10920 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ) → (2 · 𝑘) ∈ ℕ) |
30 | 27, 28, 29 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈
ℕ) |
31 | | nnnn0 11176 |
. . . . . . . . . . 11
⊢ ((2
· 𝑘) ∈ ℕ
→ (2 · 𝑘)
∈ ℕ0) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈
ℕ0) |
33 | 26, 32 | reexpcld 12887 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴↑(2 · 𝑘)) ∈ ℝ) |
34 | 30 | nnred 10912 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈
ℝ) |
35 | 2 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℝ) |
36 | 34, 35 | remulcld 9949 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) · 𝐵) ∈ ℝ) |
37 | | 0red 9920 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 ∈ ℝ) |
38 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 1 < 𝐴) → 1 ∈ ℝ) |
39 | | 0lt1 10429 |
. . . . . . . . . . . . . . 15
⊢ 0 <
1 |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 < 1) |
41 | 37, 38, 9, 40, 6 | lttrd 10077 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 < 𝐴) |
42 | 9, 41 | elrpd 11745 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 1 < 𝐴) → 𝐴 ∈
ℝ+) |
43 | | nnz 11276 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
44 | | rpexpcl 12741 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (𝐴↑𝑘) ∈
ℝ+) |
45 | 42, 43, 44 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈
ℝ+) |
46 | | peano2re 10088 |
. . . . . . . . . . . . 13
⊢ (((𝐴 − 1) · 𝑘) ∈ ℝ → (((𝐴 − 1) · 𝑘) + 1) ∈
ℝ) |
47 | 24, 46 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · 𝑘) + 1) ∈ ℝ) |
48 | 24 | ltp1d 10833 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝐴 − 1) · 𝑘) < (((𝐴 − 1) · 𝑘) + 1)) |
49 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0) |
50 | 42 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
ℝ+) |
51 | 50 | rpge0d 11752 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 0 ≤ 𝐴) |
52 | | bernneq2 12853 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0
∧ 0 ≤ 𝐴) →
(((𝐴 − 1) ·
𝑘) + 1) ≤ (𝐴↑𝑘)) |
53 | 26, 49, 51, 52 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · 𝑘) + 1) ≤ (𝐴↑𝑘)) |
54 | 24, 47, 18, 48, 53 | ltletrd 10076 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝐴 − 1) · 𝑘) < (𝐴↑𝑘)) |
55 | 24, 18, 45, 54 | ltmul1dd 11803 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · 𝑘) · (𝐴↑𝑘)) < ((𝐴↑𝑘) · (𝐴↑𝑘))) |
56 | 23 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ) |
57 | 56 | 2timesd 11152 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) = (𝑘 + 𝑘)) |
58 | 57 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴↑(2 · 𝑘)) = (𝐴↑(𝑘 + 𝑘))) |
59 | 26 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ) |
60 | 59, 49, 49 | expaddd 12872 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑘 + 𝑘)) = ((𝐴↑𝑘) · (𝐴↑𝑘))) |
61 | 58, 60 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴↑(2 · 𝑘)) = ((𝐴↑𝑘) · (𝐴↑𝑘))) |
62 | 55, 61 | breqtrrd 4611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · 𝑘) · (𝐴↑𝑘)) < (𝐴↑(2 · 𝑘))) |
63 | | ostth2lem1.3 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴↑𝑛) ≤ (𝑛 · 𝐵)) |
64 | 63 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐴↑𝑛) ≤ (𝑛 · 𝐵)) |
65 | 64 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐴↑𝑛) ≤ (𝑛 · 𝐵)) |
66 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑛 = (2 · 𝑘) → (𝐴↑𝑛) = (𝐴↑(2 · 𝑘))) |
67 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑛 = (2 · 𝑘) → (𝑛 · 𝐵) = ((2 · 𝑘) · 𝐵)) |
68 | 66, 67 | breq12d 4596 |
. . . . . . . . . . 11
⊢ (𝑛 = (2 · 𝑘) → ((𝐴↑𝑛) ≤ (𝑛 · 𝐵) ↔ (𝐴↑(2 · 𝑘)) ≤ ((2 · 𝑘) · 𝐵))) |
69 | 68 | rspcv 3278 |
. . . . . . . . . 10
⊢ ((2
· 𝑘) ∈ ℕ
→ (∀𝑛 ∈
ℕ (𝐴↑𝑛) ≤ (𝑛 · 𝐵) → (𝐴↑(2 · 𝑘)) ≤ ((2 · 𝑘) · 𝐵))) |
70 | 30, 65, 69 | sylc 63 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴↑(2 · 𝑘)) ≤ ((2 · 𝑘) · 𝐵)) |
71 | 25, 33, 36, 62, 70 | ltletrd 10076 |
. . . . . . . 8
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · 𝑘) · (𝐴↑𝑘)) < ((2 · 𝑘) · 𝐵)) |
72 | 21 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴 − 1) ∈ ℂ) |
73 | 18 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℂ) |
74 | 72, 73, 56 | mul32d 10125 |
. . . . . . . 8
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · (𝐴↑𝑘)) · 𝑘) = (((𝐴 − 1) · 𝑘) · (𝐴↑𝑘))) |
75 | | 2cnd 10970 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 2 ∈
ℂ) |
76 | 35 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ) |
77 | 75, 76, 56 | mul32d 10125 |
. . . . . . . 8
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ((2 · 𝐵) · 𝑘) = ((2 · 𝑘) · 𝐵)) |
78 | 71, 74, 77 | 3brtr4d 4615 |
. . . . . . 7
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · (𝐴↑𝑘)) · 𝑘) < ((2 · 𝐵) · 𝑘)) |
79 | 21, 18 | remulcld 9949 |
. . . . . . . 8
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝐴 − 1) · (𝐴↑𝑘)) ∈ ℝ) |
80 | 5 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (2 · 𝐵) ∈
ℝ) |
81 | | nngt0 10926 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
82 | 81 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 0 < 𝑘) |
83 | | ltmul1 10752 |
. . . . . . . 8
⊢ ((((𝐴 − 1) · (𝐴↑𝑘)) ∈ ℝ ∧ (2 · 𝐵) ∈ ℝ ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → (((𝐴 − 1) · (𝐴↑𝑘)) < (2 · 𝐵) ↔ (((𝐴 − 1) · (𝐴↑𝑘)) · 𝑘) < ((2 · 𝐵) · 𝑘))) |
84 | 79, 80, 23, 82, 83 | syl112anc 1322 |
. . . . . . 7
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · (𝐴↑𝑘)) < (2 · 𝐵) ↔ (((𝐴 − 1) · (𝐴↑𝑘)) · 𝑘) < ((2 · 𝐵) · 𝑘))) |
85 | 78, 84 | mpbird 246 |
. . . . . 6
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ((𝐴 − 1) · (𝐴↑𝑘)) < (2 · 𝐵)) |
86 | 12 | rpgt0d 11751 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 < (𝐴 − 1)) |
87 | 86 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → 0 < (𝐴 − 1)) |
88 | | ltmuldiv2 10776 |
. . . . . . 7
⊢ (((𝐴↑𝑘) ∈ ℝ ∧ (2 · 𝐵) ∈ ℝ ∧ ((𝐴 − 1) ∈ ℝ ∧
0 < (𝐴 − 1)))
→ (((𝐴 − 1)
· (𝐴↑𝑘)) < (2 · 𝐵) ↔ (𝐴↑𝑘) < ((2 · 𝐵) / (𝐴 − 1)))) |
89 | 18, 80, 21, 87, 88 | syl112anc 1322 |
. . . . . 6
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) · (𝐴↑𝑘)) < (2 · 𝐵) ↔ (𝐴↑𝑘) < ((2 · 𝐵) / (𝐴 − 1)))) |
90 | 85, 89 | mpbid 221 |
. . . . 5
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) < ((2 · 𝐵) / (𝐴 − 1))) |
91 | 18, 19, 90 | ltnsymd 10065 |
. . . 4
⊢ (((𝜑 ∧ 1 < 𝐴) ∧ 𝑘 ∈ ℕ) → ¬ ((2 ·
𝐵) / (𝐴 − 1)) < (𝐴↑𝑘)) |
92 | 91 | nrexdv 2984 |
. . 3
⊢ ((𝜑 ∧ 1 < 𝐴) → ¬ ∃𝑘 ∈ ℕ ((2 · 𝐵) / (𝐴 − 1)) < (𝐴↑𝑘)) |
93 | 15, 92 | pm2.65da 598 |
. 2
⊢ (𝜑 → ¬ 1 < 𝐴) |
94 | | lenlt 9995 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 ≤ 1
↔ ¬ 1 < 𝐴)) |
95 | 8, 7, 94 | sylancl 693 |
. 2
⊢ (𝜑 → (𝐴 ≤ 1 ↔ ¬ 1 < 𝐴)) |
96 | 93, 95 | mpbird 246 |
1
⊢ (𝜑 → 𝐴 ≤ 1) |