Proof of Theorem recreclt
Step | Hyp | Ref
| Expression |
1 | | recgt0 10746 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (1 / 𝐴)) |
2 | | gt0ne0 10372 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ≠ 0) |
3 | | rereccl 10622 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℝ) |
4 | 2, 3 | syldan 486 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) ∈
ℝ) |
5 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
6 | | ltaddpos 10397 |
. . . . 5
⊢ (((1 /
𝐴) ∈ ℝ ∧ 1
∈ ℝ) → (0 < (1 / 𝐴) ↔ 1 < (1 + (1 / 𝐴)))) |
7 | 4, 5, 6 | sylancl 693 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (0 < (1 /
𝐴) ↔ 1 < (1 + (1 /
𝐴)))) |
8 | 1, 7 | mpbid 221 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 1 < (1 + (1 /
𝐴))) |
9 | | readdcl 9898 |
. . . . 5
⊢ ((1
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (1 + (1 / 𝐴)) ∈
ℝ) |
10 | 5, 4, 9 | sylancr 694 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 + (1 / 𝐴)) ∈
ℝ) |
11 | | 0lt1 10429 |
. . . . . 6
⊢ 0 <
1 |
12 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
13 | | lttr 9993 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (1 + (1 / 𝐴)) ∈ ℝ) → ((0 < 1 ∧ 1
< (1 + (1 / 𝐴))) →
0 < (1 + (1 / 𝐴)))) |
14 | 12, 5, 13 | mp3an12 1406 |
. . . . . . 7
⊢ ((1 + (1
/ 𝐴)) ∈ ℝ →
((0 < 1 ∧ 1 < (1 + (1 / 𝐴))) → 0 < (1 + (1 / 𝐴)))) |
15 | 10, 14 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((0 < 1 ∧
1 < (1 + (1 / 𝐴)))
→ 0 < (1 + (1 / 𝐴)))) |
16 | 11, 15 | mpani 708 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 < (1 + (1 /
𝐴)) → 0 < (1 + (1 /
𝐴)))) |
17 | 8, 16 | mpd 15 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (1 + (1 /
𝐴))) |
18 | | recgt1 10798 |
. . . 4
⊢ (((1 + (1
/ 𝐴)) ∈ ℝ ∧
0 < (1 + (1 / 𝐴)))
→ (1 < (1 + (1 / 𝐴)) ↔ (1 / (1 + (1 / 𝐴))) < 1)) |
19 | 10, 17, 18 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 < (1 + (1 /
𝐴)) ↔ (1 / (1 + (1 /
𝐴))) <
1)) |
20 | 8, 19 | mpbid 221 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / (1 + (1 /
𝐴))) <
1) |
21 | | ltaddpos 10397 |
. . . . . 6
⊢ ((1
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (0 < 1 ↔ (1
/ 𝐴) < ((1 / 𝐴) + 1))) |
22 | 5, 4, 21 | sylancr 694 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (0 < 1 ↔
(1 / 𝐴) < ((1 / 𝐴) + 1))) |
23 | 11, 22 | mpbii 222 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) < ((1 / 𝐴) + 1)) |
24 | 4 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) ∈
ℂ) |
25 | | ax-1cn 9873 |
. . . . 5
⊢ 1 ∈
ℂ |
26 | | addcom 10101 |
. . . . 5
⊢ (((1 /
𝐴) ∈ ℂ ∧ 1
∈ ℂ) → ((1 / 𝐴) + 1) = (1 + (1 / 𝐴))) |
27 | 24, 25, 26 | sylancl 693 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((1 / 𝐴) + 1) = (1 + (1 / 𝐴))) |
28 | 23, 27 | breqtrd 4609 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) < (1 + (1 / 𝐴))) |
29 | | simpl 472 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ∈ ℝ) |
30 | | simpr 476 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < 𝐴) |
31 | | ltrec1 10789 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ ((1 + (1 / 𝐴)) ∈ ℝ ∧ 0 <
(1 + (1 / 𝐴)))) → ((1
/ 𝐴) < (1 + (1 / 𝐴)) ↔ (1 / (1 + (1 / 𝐴))) < 𝐴)) |
32 | 29, 30, 10, 17, 31 | syl22anc 1319 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((1 / 𝐴) < (1 + (1 / 𝐴)) ↔ (1 / (1 + (1 / 𝐴))) < 𝐴)) |
33 | 28, 32 | mpbid 221 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / (1 + (1 /
𝐴))) < 𝐴) |
34 | 20, 33 | jca 553 |
1
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((1 / (1 + (1 /
𝐴))) < 1 ∧ (1 / (1 +
(1 / 𝐴))) < 𝐴)) |