Proof of Theorem recgt0
Step | Hyp | Ref
| Expression |
1 | | 0lt1 6938 |
. . . . 5
⊢ 0 <
1 |
2 | | 0re 6825 |
. . . . . 6
⊢ 0 ∈ ℝ |
3 | | 1re 6824 |
. . . . . 6
⊢ 1 ∈ ℝ |
4 | 2, 3 | ltnsymi 6914 |
. . . . 5
⊢ (0 < 1
→ ¬ 1 < 0) |
5 | 1, 4 | ax-mp 7 |
. . . 4
⊢ ¬ 1
< 0 |
6 | | simpll 481 |
. . . . . . . . . 10
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → A ∈
ℝ) |
7 | | gt0ap0 7408 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧ 0 <
A) → A # 0) |
8 | 7 | adantr 261 |
. . . . . . . . . 10
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → A # 0) |
9 | 6, 8 | rerecclapd 7588 |
. . . . . . . . 9
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → (1 / A) ∈
ℝ) |
10 | 9 | renegcld 7174 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → -(1 / A) ∈
ℝ) |
11 | | simpr 103 |
. . . . . . . . 9
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → (1 / A) < 0) |
12 | | simpl 102 |
. . . . . . . . . . . 12
⊢
((A ∈ ℝ ∧ 0 <
A) → A ∈
ℝ) |
13 | 12, 7 | rerecclapd 7588 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧ 0 <
A) → (1 / A) ∈
ℝ) |
14 | 13 | adantr 261 |
. . . . . . . . . 10
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → (1 / A) ∈
ℝ) |
15 | 14 | lt0neg1d 7302 |
. . . . . . . . 9
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → ((1 / A) < 0 ↔ 0 < -(1 / A))) |
16 | 11, 15 | mpbid 135 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → 0 < -(1 / A)) |
17 | | simplr 482 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → 0 < A) |
18 | 10, 6, 16, 17 | mulgt0d 6934 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → 0 < (-(1 / A) · A)) |
19 | 12 | recnd 6851 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧ 0 <
A) → A ∈
ℂ) |
20 | 19 | adantr 261 |
. . . . . . . . . 10
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → A ∈
ℂ) |
21 | | recclap 7440 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
A # 0) → (1 / A) ∈
ℂ) |
22 | 20, 8, 21 | syl2anc 391 |
. . . . . . . . 9
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → (1 / A) ∈
ℂ) |
23 | 22, 20 | mulneg1d 7204 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → (-(1 / A) · A) =
-((1 / A) · A)) |
24 | | recidap2 7448 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
A # 0) → ((1 / A) · A) =
1) |
25 | 20, 8, 24 | syl2anc 391 |
. . . . . . . . 9
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → ((1 / A) · A) =
1) |
26 | 25 | negeqd 7003 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → -((1 / A) · A) =
-1) |
27 | 23, 26 | eqtrd 2069 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → (-(1 / A) · A) =
-1) |
28 | 18, 27 | breqtrd 3779 |
. . . . . 6
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → 0 <
-1) |
29 | | 1red 6840 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → 1 ∈ ℝ) |
30 | 29 | lt0neg1d 7302 |
. . . . . 6
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → (1 < 0 ↔ 0 <
-1)) |
31 | 28, 30 | mpbird 156 |
. . . . 5
⊢
(((A ∈ ℝ ∧ 0 <
A) ∧ (1 /
A) < 0) → 1 <
0) |
32 | 31 | ex 108 |
. . . 4
⊢
((A ∈ ℝ ∧ 0 <
A) → ((1 / A) < 0 → 1 < 0)) |
33 | 5, 32 | mtoi 589 |
. . 3
⊢
((A ∈ ℝ ∧ 0 <
A) → ¬ (1 / A) < 0) |
34 | | lenlt 6891 |
. . . 4
⊢ ((0 ∈ ℝ ∧ (1 /
A) ∈
ℝ) → (0 ≤ (1 / A) ↔
¬ (1 / A) < 0)) |
35 | 2, 13, 34 | sylancr 393 |
. . 3
⊢
((A ∈ ℝ ∧ 0 <
A) → (0 ≤ (1 / A) ↔ ¬ (1 / A) < 0)) |
36 | 33, 35 | mpbird 156 |
. 2
⊢
((A ∈ ℝ ∧ 0 <
A) → 0 ≤ (1 / A)) |
37 | | recap0 7446 |
. . . 4
⊢
((A ∈ ℂ ∧
A # 0) → (1 / A) # 0) |
38 | 19, 7, 37 | syl2anc 391 |
. . 3
⊢
((A ∈ ℝ ∧ 0 <
A) → (1 / A) # 0) |
39 | 19, 7, 21 | syl2anc 391 |
. . . 4
⊢
((A ∈ ℝ ∧ 0 <
A) → (1 / A) ∈
ℂ) |
40 | | 0cn 6817 |
. . . 4
⊢ 0 ∈ ℂ |
41 | | apsym 7390 |
. . . 4
⊢ (((1 /
A) ∈
ℂ ∧ 0 ∈ ℂ) → ((1 / A) # 0 ↔ 0 # (1 / A))) |
42 | 39, 40, 41 | sylancl 392 |
. . 3
⊢
((A ∈ ℝ ∧ 0 <
A) → ((1 / A) # 0 ↔ 0 # (1 / A))) |
43 | 38, 42 | mpbid 135 |
. 2
⊢
((A ∈ ℝ ∧ 0 <
A) → 0 # (1 / A)) |
44 | | ltleap 7413 |
. . 3
⊢ ((0 ∈ ℝ ∧ (1 /
A) ∈
ℝ) → (0 < (1 / A) ↔ (0
≤ (1 / A) ∧ 0 # (1 / A)))) |
45 | 2, 13, 44 | sylancr 393 |
. 2
⊢
((A ∈ ℝ ∧ 0 <
A) → (0 < (1 / A) ↔ (0 ≤ (1 / A) ∧ 0 # (1 /
A)))) |
46 | 36, 43, 45 | mpbir2and 850 |
1
⊢
((A ∈ ℝ ∧ 0 <
A) → 0 < (1 / A)) |