Proof of Theorem recgt0
Step | Hyp | Ref
| Expression |
1 | | 0lt1 7760 |
. . . . 5
⊢ 0 <
1 |
2 | | 0re 7638 |
. . . . . 6
⊢ 0 ∈
ℝ |
3 | | 1re 7637 |
. . . . . 6
⊢ 1 ∈
ℝ |
4 | 2, 3 | ltnsymi 7734 |
. . . . 5
⊢ (0 < 1
→ ¬ 1 < 0) |
5 | 1, 4 | ax-mp 7 |
. . . 4
⊢ ¬ 1
< 0 |
6 | | simpll 499 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → 𝐴 ∈
ℝ) |
7 | | gt0ap0 8254 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 # 0) |
8 | 7 | adantr 272 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → 𝐴 # 0) |
9 | 6, 8 | rerecclapd 8454 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → (1 / 𝐴) ∈
ℝ) |
10 | 9 | renegcld 8009 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → -(1 / 𝐴) ∈
ℝ) |
11 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → (1 / 𝐴) < 0) |
12 | | simpl 108 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ∈ ℝ) |
13 | 12, 7 | rerecclapd 8454 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) ∈
ℝ) |
14 | 13 | adantr 272 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → (1 / 𝐴) ∈
ℝ) |
15 | 14 | lt0neg1d 8144 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → ((1 / 𝐴) < 0 ↔ 0 < -(1 /
𝐴))) |
16 | 11, 15 | mpbid 146 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → 0 < -(1 /
𝐴)) |
17 | | simplr 500 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → 0 < 𝐴) |
18 | 10, 6, 16, 17 | mulgt0d 7756 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → 0 < (-(1 /
𝐴) · 𝐴)) |
19 | 12 | recnd 7666 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ∈ ℂ) |
20 | 19 | adantr 272 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → 𝐴 ∈
ℂ) |
21 | | recclap 8300 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) ∈
ℂ) |
22 | 20, 8, 21 | syl2anc 406 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → (1 / 𝐴) ∈
ℂ) |
23 | 22, 20 | mulneg1d 8040 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → (-(1 / 𝐴) · 𝐴) = -((1 / 𝐴) · 𝐴)) |
24 | | recidap2 8308 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((1 / 𝐴) · 𝐴) = 1) |
25 | 20, 8, 24 | syl2anc 406 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → ((1 / 𝐴) · 𝐴) = 1) |
26 | 25 | negeqd 7828 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → -((1 / 𝐴) · 𝐴) = -1) |
27 | 23, 26 | eqtrd 2132 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → (-(1 / 𝐴) · 𝐴) = -1) |
28 | 18, 27 | breqtrd 3899 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → 0 <
-1) |
29 | | 1red 7653 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → 1 ∈
ℝ) |
30 | 29 | lt0neg1d 8144 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → (1 < 0
↔ 0 < -1)) |
31 | 28, 30 | mpbird 166 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 / 𝐴) < 0) → 1 <
0) |
32 | 31 | ex 114 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((1 / 𝐴) < 0 → 1 <
0)) |
33 | 5, 32 | mtoi 631 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ¬ (1 / 𝐴) < 0) |
34 | | lenlt 7711 |
. . . 4
⊢ ((0
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (0 ≤ (1 / 𝐴) ↔ ¬ (1 / 𝐴) < 0)) |
35 | 2, 13, 34 | sylancr 408 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (0 ≤ (1 /
𝐴) ↔ ¬ (1 / 𝐴) < 0)) |
36 | 33, 35 | mpbird 166 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 ≤ (1 / 𝐴)) |
37 | | recap0 8306 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) # 0) |
38 | 19, 7, 37 | syl2anc 406 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) # 0) |
39 | 19, 7, 21 | syl2anc 406 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) ∈
ℂ) |
40 | | 0cn 7630 |
. . . 4
⊢ 0 ∈
ℂ |
41 | | apsym 8234 |
. . . 4
⊢ (((1 /
𝐴) ∈ ℂ ∧ 0
∈ ℂ) → ((1 / 𝐴) # 0 ↔ 0 # (1 / 𝐴))) |
42 | 39, 40, 41 | sylancl 407 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((1 / 𝐴) # 0 ↔ 0 # (1 / 𝐴))) |
43 | 38, 42 | mpbid 146 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 # (1 / 𝐴)) |
44 | | ltleap 8259 |
. . 3
⊢ ((0
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (0 < (1 / 𝐴) ↔ (0 ≤ (1 / 𝐴) ∧ 0 # (1 / 𝐴)))) |
45 | 2, 13, 44 | sylancr 408 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (0 < (1 /
𝐴) ↔ (0 ≤ (1 /
𝐴) ∧ 0 # (1 / 𝐴)))) |
46 | 36, 43, 45 | mpbir2and 896 |
1
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (1 / 𝐴)) |