Proof of Theorem mulge0
Step | Hyp | Ref
| Expression |
1 | | remulcl 6807 |
. . . . 5
⊢
((A ∈ ℝ ∧
B ∈
ℝ) → (A · B) ∈
ℝ) |
2 | 1 | ad2ant2r 478 |
. . . 4
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → (A
· B) ∈ ℝ) |
3 | | 0re 6825 |
. . . 4
⊢ 0 ∈ ℝ |
4 | | ltnsym2 6905 |
. . . 4
⊢
(((A · B) ∈ ℝ ∧ 0 ∈ ℝ)
→ ¬ ((A · B) < 0 ∧ 0 <
(A · B))) |
5 | 2, 3, 4 | sylancl 392 |
. . 3
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → ¬ ((A · B)
< 0 ∧ 0 < (A · B))) |
6 | | orc 632 |
. . . . . 6
⊢
((A · B) < 0 → ((A · B)
< 0 ∨ 0 < (A · B))) |
7 | | reaplt 7372 |
. . . . . . 7
⊢
(((A · B) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((A · B) # 0 ↔ ((A · B)
< 0 ∨ 0 < (A · B)))) |
8 | 2, 3, 7 | sylancl 392 |
. . . . . 6
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → ((A
· B) # 0 ↔ ((A · B)
< 0 ∨ 0 < (A · B)))) |
9 | 6, 8 | syl5ibr 145 |
. . . . 5
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → ((A
· B) < 0 → (A · B) #
0)) |
10 | | simplll 485 |
. . . . . . 7
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → A ∈ ℝ) |
11 | | simplrl 487 |
. . . . . . 7
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → B ∈ ℝ) |
12 | | recn 6812 |
. . . . . . . . . . . . . 14
⊢ (B ∈ ℝ →
B ∈
ℂ) |
13 | | recn 6812 |
. . . . . . . . . . . . . . 15
⊢ (A ∈ ℝ →
A ∈
ℂ) |
14 | | mulap0r 7399 |
. . . . . . . . . . . . . . 15
⊢
((A ∈ ℂ ∧
B ∈
ℂ ∧ (A · B) #
0) → (A # 0 ∧ B #
0)) |
15 | 13, 14 | syl3an1 1167 |
. . . . . . . . . . . . . 14
⊢
((A ∈ ℝ ∧
B ∈
ℂ ∧ (A · B) #
0) → (A # 0 ∧ B #
0)) |
16 | 12, 15 | syl3an2 1168 |
. . . . . . . . . . . . 13
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (A · B) #
0) → (A # 0 ∧ B #
0)) |
17 | 16 | 3expia 1105 |
. . . . . . . . . . . 12
⊢
((A ∈ ℝ ∧
B ∈
ℝ) → ((A · B) # 0 → (A
# 0 ∧ B #
0))) |
18 | 17 | ad2ant2r 478 |
. . . . . . . . . . 11
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → ((A
· B) # 0 → (A # 0 ∧ B # 0))) |
19 | 18 | imp 115 |
. . . . . . . . . 10
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → (A # 0 ∧ B #
0)) |
20 | 19 | simpld 105 |
. . . . . . . . 9
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → A # 0) |
21 | | reaplt 7372 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧ 0
∈ ℝ) → (A # 0 ↔ (A
< 0 ∨ 0 < A))) |
22 | 3, 21 | mpan2 401 |
. . . . . . . . . 10
⊢ (A ∈ ℝ →
(A # 0 ↔ (A < 0 ∨ 0 <
A))) |
23 | 22 | ad3antrrr 461 |
. . . . . . . . 9
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → (A # 0 ↔ (A < 0 ∨ 0 <
A))) |
24 | 20, 23 | mpbid 135 |
. . . . . . . 8
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → (A < 0
∨ 0 < A)) |
25 | | lenlt 6891 |
. . . . . . . . . . . 12
⊢ ((0 ∈ ℝ ∧
A ∈
ℝ) → (0 ≤ A ↔ ¬
A < 0)) |
26 | 3, 25 | mpan 400 |
. . . . . . . . . . 11
⊢ (A ∈ ℝ →
(0 ≤ A ↔ ¬ A < 0)) |
27 | 26 | biimpa 280 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧ 0 ≤
A) → ¬ A < 0) |
28 | 27 | ad2antrr 457 |
. . . . . . . . 9
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → ¬ A < 0) |
29 | | biorf 662 |
. . . . . . . . 9
⊢ (¬
A < 0 → (0 < A ↔ (A <
0 ∨ 0 < A))) |
30 | 28, 29 | syl 14 |
. . . . . . . 8
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → (0 < A ↔ (A < 0 ∨ 0 <
A))) |
31 | 24, 30 | mpbird 156 |
. . . . . . 7
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → 0 < A) |
32 | 19 | simprd 107 |
. . . . . . . . 9
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → B # 0) |
33 | | reaplt 7372 |
. . . . . . . . . . . 12
⊢
((B ∈ ℝ ∧ 0
∈ ℝ) → (B # 0 ↔ (B
< 0 ∨ 0 < B))) |
34 | 3, 33 | mpan2 401 |
. . . . . . . . . . 11
⊢ (B ∈ ℝ →
(B # 0 ↔ (B < 0 ∨ 0 <
B))) |
35 | 34 | ad2antrl 459 |
. . . . . . . . . 10
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → (B #
0 ↔ (B < 0
∨ 0 < B))) |
36 | 35 | adantr 261 |
. . . . . . . . 9
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → (B # 0 ↔ (B < 0 ∨ 0 <
B))) |
37 | 32, 36 | mpbid 135 |
. . . . . . . 8
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → (B < 0
∨ 0 < B)) |
38 | | lenlt 6891 |
. . . . . . . . . . . 12
⊢ ((0 ∈ ℝ ∧
B ∈
ℝ) → (0 ≤ B ↔ ¬
B < 0)) |
39 | 3, 38 | mpan 400 |
. . . . . . . . . . 11
⊢ (B ∈ ℝ →
(0 ≤ B ↔ ¬ B < 0)) |
40 | 39 | biimpa 280 |
. . . . . . . . . 10
⊢
((B ∈ ℝ ∧ 0 ≤
B) → ¬ B < 0) |
41 | 40 | ad2antlr 458 |
. . . . . . . . 9
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → ¬ B < 0) |
42 | | biorf 662 |
. . . . . . . . 9
⊢ (¬
B < 0 → (0 < B ↔ (B <
0 ∨ 0 < B))) |
43 | 41, 42 | syl 14 |
. . . . . . . 8
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → (0 < B ↔ (B < 0 ∨ 0 <
B))) |
44 | 37, 43 | mpbird 156 |
. . . . . . 7
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → 0 < B) |
45 | 10, 11, 31, 44 | mulgt0d 6934 |
. . . . . 6
⊢
((((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) ∧ (A · B) #
0) → 0 < (A · B)) |
46 | 45 | ex 108 |
. . . . 5
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → ((A
· B) # 0 → 0 < (A · B))) |
47 | 9, 46 | syld 40 |
. . . 4
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → ((A
· B) < 0 → 0 < (A · B))) |
48 | 47 | ancld 308 |
. . 3
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → ((A
· B) < 0 → ((A · B)
< 0 ∧ 0 < (A · B)))) |
49 | 5, 48 | mtod 588 |
. 2
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → ¬ (A · B)
< 0) |
50 | | lenlt 6891 |
. . 3
⊢ ((0 ∈ ℝ ∧
(A · B) ∈ ℝ)
→ (0 ≤ (A · B) ↔ ¬ (A · B)
< 0)) |
51 | 3, 2, 50 | sylancr 393 |
. 2
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → (0 ≤ (A · B)
↔ ¬ (A · B) < 0)) |
52 | 49, 51 | mpbird 156 |
1
⊢
(((A ∈ ℝ ∧ 0 ≤
A) ∧
(B ∈
ℝ ∧ 0 ≤ B)) → 0 ≤ (A · B)) |