Proof of Theorem reapmul1
Step | Hyp | Ref
| Expression |
1 | | 0re 6825 |
. . . . 5
⊢ 0 ∈ ℝ |
2 | | reaplt 7372 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧ 0
∈ ℝ) → (𝐶 # 0 ↔ (𝐶 < 0 ∨ 0
< 𝐶))) |
3 | 1, 2 | mpan2 401 |
. . . 4
⊢ (𝐶 ∈ ℝ → (𝐶 # 0 ↔ (𝐶 < 0 ∨ 0
< 𝐶))) |
4 | 3 | pm5.32i 427 |
. . 3
⊢ ((𝐶 ∈ ℝ ∧ 𝐶 # 0) ↔ (𝐶 ∈ ℝ
∧ (𝐶 < 0 ∨ 0
< 𝐶))) |
5 | | simp1 903 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → A ∈
ℝ) |
6 | 5 | recnd 6851 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → A ∈
ℂ) |
7 | | simp3l 931 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → 𝐶 ∈
ℝ) |
8 | 7 | recnd 6851 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → 𝐶 ∈
ℂ) |
9 | 6, 8 | mulneg2d 7205 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (A · -𝐶) = -(A
· 𝐶)) |
10 | | simp2 904 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → B ∈
ℝ) |
11 | 10 | recnd 6851 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → B ∈
ℂ) |
12 | 11, 8 | mulneg2d 7205 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (B · -𝐶) = -(B
· 𝐶)) |
13 | 9, 12 | breq12d 3768 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → ((A · -𝐶) # (B
· -𝐶) ↔
-(A · 𝐶) # -(B
· 𝐶))) |
14 | 7 | renegcld 7174 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → -𝐶 ∈
ℝ) |
15 | | simp3r 932 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → 𝐶 < 0) |
16 | 7 | lt0neg1d 7302 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (𝐶 < 0 ↔ 0 < -𝐶)) |
17 | 15, 16 | mpbid 135 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → 0 < -𝐶) |
18 | | reapmul1lem 7378 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (-𝐶 ∈ ℝ
∧ 0 < -𝐶)) → (A # B ↔
(A · -𝐶) # (B
· -𝐶))) |
19 | 5, 10, 14, 17, 18 | syl112anc 1138 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (A # B ↔
(A · -𝐶) # (B
· -𝐶))) |
20 | 5, 7 | remulcld 6853 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (A · 𝐶) ∈
ℝ) |
21 | 10, 7 | remulcld 6853 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (B · 𝐶) ∈
ℝ) |
22 | 20, 21 | ltnegd 7309 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → ((A · 𝐶) < (B · 𝐶) ↔ -(B · 𝐶) < -(A · 𝐶))) |
23 | 21, 20 | ltnegd 7309 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → ((B · 𝐶) < (A · 𝐶) ↔ -(A · 𝐶) < -(B · 𝐶))) |
24 | 22, 23 | orbi12d 706 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (((A · 𝐶) < (B · 𝐶) ∨
(B · 𝐶) < (A · 𝐶)) ↔ (-(B · 𝐶) < -(A · 𝐶) ∨
-(A · 𝐶) < -(B · 𝐶)))) |
25 | | reaplt 7372 |
. . . . . . . . . 10
⊢
(((A · 𝐶) ∈
ℝ ∧ (B · 𝐶) ∈
ℝ) → ((A · 𝐶) # (B · 𝐶) ↔ ((A · 𝐶) < (B · 𝐶) ∨
(B · 𝐶) < (A · 𝐶)))) |
26 | 20, 21, 25 | syl2anc 391 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → ((A · 𝐶) # (B
· 𝐶) ↔
((A · 𝐶) < (B · 𝐶) ∨
(B · 𝐶) < (A · 𝐶)))) |
27 | 20 | renegcld 7174 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → -(A · 𝐶) ∈
ℝ) |
28 | 21 | renegcld 7174 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → -(B · 𝐶) ∈
ℝ) |
29 | | reaplt 7372 |
. . . . . . . . . . 11
⊢
((-(A · 𝐶) ∈
ℝ ∧ -(B · 𝐶) ∈
ℝ) → (-(A · 𝐶) # -(B · 𝐶) ↔ (-(A · 𝐶) < -(B · 𝐶) ∨
-(B · 𝐶) < -(A · 𝐶)))) |
30 | 27, 28, 29 | syl2anc 391 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (-(A · 𝐶) # -(B
· 𝐶) ↔
(-(A · 𝐶) < -(B · 𝐶) ∨
-(B · 𝐶) < -(A · 𝐶)))) |
31 | | orcom 646 |
. . . . . . . . . 10
⊢
((-(A · 𝐶) < -(B · 𝐶) ∨
-(B · 𝐶) < -(A · 𝐶)) ↔ (-(B · 𝐶) < -(A · 𝐶) ∨
-(A · 𝐶) < -(B · 𝐶))) |
32 | 30, 31 | syl6bb 185 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (-(A · 𝐶) # -(B
· 𝐶) ↔
(-(B · 𝐶) < -(A · 𝐶) ∨
-(A · 𝐶) < -(B · 𝐶)))) |
33 | 24, 26, 32 | 3bitr4d 209 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → ((A · 𝐶) # (B
· 𝐶) ↔
-(A · 𝐶) # -(B
· 𝐶))) |
34 | 13, 19, 33 | 3bitr4d 209 |
. . . . . . 7
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |
35 | 34 | 3expa 1103 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐶 < 0)) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |
36 | 35 | anassrs 380 |
. . . . 5
⊢
((((A ∈ ℝ ∧
B ∈
ℝ) ∧ 𝐶 ∈
ℝ) ∧ 𝐶 < 0) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |
37 | | reapmul1lem 7378 |
. . . . . . 7
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 0 < 𝐶)) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |
38 | 37 | 3expa 1103 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 0 < 𝐶)) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |
39 | 38 | anassrs 380 |
. . . . 5
⊢
((((A ∈ ℝ ∧
B ∈
ℝ) ∧ 𝐶 ∈
ℝ) ∧ 0 < 𝐶) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |
40 | 36, 39 | jaodan 709 |
. . . 4
⊢
((((A ∈ ℝ ∧
B ∈
ℝ) ∧ 𝐶 ∈
ℝ) ∧ (𝐶 < 0 ∨ 0
< 𝐶)) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |
41 | 40 | anasss 379 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ (𝐶 < 0 ∨ 0
< 𝐶))) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |
42 | 4, 41 | sylan2b 271 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐶 # 0)) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |
43 | 42 | 3impa 1098 |
1
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ (𝐶 ∈ ℝ
∧ 𝐶 # 0)) → (A # B ↔
(A · 𝐶) # (B
· 𝐶))) |