Proof of Theorem recreclt
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | recgt0 12114 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (1 / 𝐴)) | 
| 2 |  | gt0ne0 11729 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ≠ 0) | 
| 3 |  | rereccl 11986 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℝ) | 
| 4 | 2, 3 | syldan 591 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) ∈
ℝ) | 
| 5 |  | 1re 11262 | . . . . 5
⊢ 1 ∈
ℝ | 
| 6 |  | ltaddpos 11754 | . . . . 5
⊢ (((1 /
𝐴) ∈ ℝ ∧ 1
∈ ℝ) → (0 < (1 / 𝐴) ↔ 1 < (1 + (1 / 𝐴)))) | 
| 7 | 4, 5, 6 | sylancl 586 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (0 < (1 /
𝐴) ↔ 1 < (1 + (1 /
𝐴)))) | 
| 8 | 1, 7 | mpbid 232 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 1 < (1 + (1 /
𝐴))) | 
| 9 |  | readdcl 11239 | . . . . 5
⊢ ((1
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (1 + (1 / 𝐴)) ∈
ℝ) | 
| 10 | 5, 4, 9 | sylancr 587 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 + (1 / 𝐴)) ∈
ℝ) | 
| 11 |  | 0lt1 11786 | . . . . . 6
⊢ 0 <
1 | 
| 12 |  | 0re 11264 | . . . . . . 7
⊢ 0 ∈
ℝ | 
| 13 |  | lttr 11338 | . . . . . . 7
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (1 + (1 / 𝐴)) ∈ ℝ) → ((0 < 1 ∧ 1
< (1 + (1 / 𝐴))) →
0 < (1 + (1 / 𝐴)))) | 
| 14 | 12, 5, 10, 13 | mp3an12i 1466 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((0 < 1 ∧
1 < (1 + (1 / 𝐴)))
→ 0 < (1 + (1 / 𝐴)))) | 
| 15 | 11, 14 | mpani 696 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 < (1 + (1 /
𝐴)) → 0 < (1 + (1 /
𝐴)))) | 
| 16 | 8, 15 | mpd 15 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (1 + (1 /
𝐴))) | 
| 17 |  | recgt1 12165 | . . . 4
⊢ (((1 + (1
/ 𝐴)) ∈ ℝ ∧
0 < (1 + (1 / 𝐴)))
→ (1 < (1 + (1 / 𝐴)) ↔ (1 / (1 + (1 / 𝐴))) < 1)) | 
| 18 | 10, 16, 17 | syl2anc 584 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 < (1 + (1 /
𝐴)) ↔ (1 / (1 + (1 /
𝐴))) <
1)) | 
| 19 | 8, 18 | mpbid 232 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / (1 + (1 /
𝐴))) <
1) | 
| 20 |  | ltaddpos 11754 | . . . . . 6
⊢ ((1
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (0 < 1 ↔ (1
/ 𝐴) < ((1 / 𝐴) + 1))) | 
| 21 | 5, 4, 20 | sylancr 587 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (0 < 1 ↔
(1 / 𝐴) < ((1 / 𝐴) + 1))) | 
| 22 | 11, 21 | mpbii 233 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) < ((1 / 𝐴) + 1)) | 
| 23 | 4 | recnd 11290 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) ∈
ℂ) | 
| 24 |  | ax-1cn 11214 | . . . . 5
⊢ 1 ∈
ℂ | 
| 25 |  | addcom 11448 | . . . . 5
⊢ (((1 /
𝐴) ∈ ℂ ∧ 1
∈ ℂ) → ((1 / 𝐴) + 1) = (1 + (1 / 𝐴))) | 
| 26 | 23, 24, 25 | sylancl 586 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((1 / 𝐴) + 1) = (1 + (1 / 𝐴))) | 
| 27 | 22, 26 | breqtrd 5168 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) < (1 + (1 / 𝐴))) | 
| 28 |  | simpl 482 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ∈ ℝ) | 
| 29 |  | simpr 484 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < 𝐴) | 
| 30 |  | ltrec1 12156 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ ((1 + (1 / 𝐴)) ∈ ℝ ∧ 0 <
(1 + (1 / 𝐴)))) → ((1
/ 𝐴) < (1 + (1 / 𝐴)) ↔ (1 / (1 + (1 / 𝐴))) < 𝐴)) | 
| 31 | 28, 29, 10, 16, 30 | syl22anc 838 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((1 / 𝐴) < (1 + (1 / 𝐴)) ↔ (1 / (1 + (1 / 𝐴))) < 𝐴)) | 
| 32 | 27, 31 | mpbid 232 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / (1 + (1 /
𝐴))) < 𝐴) | 
| 33 | 19, 32 | jca 511 | 1
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((1 / (1 + (1 /
𝐴))) < 1 ∧ (1 / (1 +
(1 / 𝐴))) < 𝐴)) |