Step | Hyp | Ref
| Expression |
1 | | cnre 7874 |
. . 3
⊢ (𝐵 ∈ ℂ →
∃𝑧 ∈ ℝ
∃𝑤 ∈ ℝ
𝐵 = (𝑧 + (i · 𝑤))) |
2 | 1 | adantl 275 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
∃𝑧 ∈ ℝ
∃𝑤 ∈ ℝ
𝐵 = (𝑧 + (i · 𝑤))) |
3 | | cnre 7874 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℝ
∃𝑦 ∈ ℝ
𝐴 = (𝑥 + (i · 𝑦))) |
4 | 3 | ad3antrrr 484 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) |
5 | | simpr 109 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝐴 = (𝑥 + (i · 𝑦))) |
6 | | simpllr 524 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝐵 = (𝑧 + (i · 𝑤))) |
7 | 5, 6 | breq12d 3978 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝐴 # 𝐵 ↔ (𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤)))) |
8 | | simplrl 525 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑥 ∈ ℝ) |
9 | | simplrr 526 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑦 ∈ ℝ) |
10 | | simprl 521 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑧 ∈
ℝ) |
11 | 10 | ad3antrrr 484 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑧 ∈ ℝ) |
12 | | simprr 522 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑤 ∈
ℝ) |
13 | 12 | ad3antrrr 484 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑤 ∈ ℝ) |
14 | | apreim 8478 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → ((𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤)) ↔ (𝑥 # 𝑧 ∨ 𝑦 # 𝑤))) |
15 | 8, 9, 11, 13, 14 | syl22anc 1221 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤)) ↔ (𝑥 # 𝑧 ∨ 𝑦 # 𝑤))) |
16 | 8 | renegcld 8255 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -𝑥 ∈ ℝ) |
17 | 9 | renegcld 8255 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -𝑦 ∈ ℝ) |
18 | 11 | renegcld 8255 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -𝑧 ∈ ℝ) |
19 | 13 | renegcld 8255 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -𝑤 ∈ ℝ) |
20 | | apreim 8478 |
. . . . . . . . . 10
⊢ (((-𝑥 ∈ ℝ ∧ -𝑦 ∈ ℝ) ∧ (-𝑧 ∈ ℝ ∧ -𝑤 ∈ ℝ)) →
((-𝑥 + (i · -𝑦)) # (-𝑧 + (i · -𝑤)) ↔ (-𝑥 # -𝑧 ∨ -𝑦 # -𝑤))) |
21 | 16, 17, 18, 19, 20 | syl22anc 1221 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((-𝑥 + (i · -𝑦)) # (-𝑧 + (i · -𝑤)) ↔ (-𝑥 # -𝑧 ∨ -𝑦 # -𝑤))) |
22 | 8 | recnd 7906 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑥 ∈ ℂ) |
23 | | ax-icn 7827 |
. . . . . . . . . . . . . 14
⊢ i ∈
ℂ |
24 | 23 | a1i 9 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → i ∈ ℂ) |
25 | 9 | recnd 7906 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑦 ∈ ℂ) |
26 | 24, 25 | mulcld 7898 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (i · 𝑦) ∈ ℂ) |
27 | 22, 26 | negdid 8199 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑥 + (i · 𝑦)) = (-𝑥 + -(i · 𝑦))) |
28 | 5 | negeqd 8070 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -𝐴 = -(𝑥 + (i · 𝑦))) |
29 | 24, 25 | mulneg2d 8287 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (i · -𝑦) = -(i · 𝑦)) |
30 | 29 | oveq2d 5840 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (-𝑥 + (i · -𝑦)) = (-𝑥 + -(i · 𝑦))) |
31 | 27, 28, 30 | 3eqtr4d 2200 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -𝐴 = (-𝑥 + (i · -𝑦))) |
32 | 11 | recnd 7906 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑧 ∈ ℂ) |
33 | 13 | recnd 7906 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑤 ∈ ℂ) |
34 | 24, 33 | mulcld 7898 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (i · 𝑤) ∈ ℂ) |
35 | 32, 34 | negdid 8199 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑧 + (i · 𝑤)) = (-𝑧 + -(i · 𝑤))) |
36 | 6 | negeqd 8070 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -𝐵 = -(𝑧 + (i · 𝑤))) |
37 | 24, 33 | mulneg2d 8287 |
. . . . . . . . . . . 12
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (i · -𝑤) = -(i · 𝑤)) |
38 | 37 | oveq2d 5840 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (-𝑧 + (i · -𝑤)) = (-𝑧 + -(i · 𝑤))) |
39 | 35, 36, 38 | 3eqtr4d 2200 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -𝐵 = (-𝑧 + (i · -𝑤))) |
40 | 31, 39 | breq12d 3978 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (-𝐴 # -𝐵 ↔ (-𝑥 + (i · -𝑦)) # (-𝑧 + (i · -𝑤)))) |
41 | | reapneg 8472 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 # 𝑧 ↔ -𝑥 # -𝑧)) |
42 | 8, 11, 41 | syl2anc 409 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑥 # 𝑧 ↔ -𝑥 # -𝑧)) |
43 | | reapneg 8472 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝑤 ∈ ℝ) → (𝑦 # 𝑤 ↔ -𝑦 # -𝑤)) |
44 | 9, 13, 43 | syl2anc 409 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑦 # 𝑤 ↔ -𝑦 # -𝑤)) |
45 | 42, 44 | orbi12d 783 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 # 𝑧 ∨ 𝑦 # 𝑤) ↔ (-𝑥 # -𝑧 ∨ -𝑦 # -𝑤))) |
46 | 21, 40, 45 | 3bitr4rd 220 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 # 𝑧 ∨ 𝑦 # 𝑤) ↔ -𝐴 # -𝐵)) |
47 | 7, 15, 46 | 3bitrd 213 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝐴 # 𝐵 ↔ -𝐴 # -𝐵)) |
48 | 47 | ex 114 |
. . . . . 6
⊢
(((((𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ) ∧ (𝑧 ∈
ℝ ∧ 𝑤 ∈
ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 # 𝐵 ↔ -𝐴 # -𝐵))) |
49 | 48 | rexlimdvva 2582 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) → (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 # 𝐵 ↔ -𝐴 # -𝐵))) |
50 | 4, 49 | mpd 13 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) → (𝐴 # 𝐵 ↔ -𝐴 # -𝐵)) |
51 | 50 | ex 114 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → (𝐵 = (𝑧 + (i · 𝑤)) → (𝐴 # 𝐵 ↔ -𝐴 # -𝐵))) |
52 | 51 | rexlimdvva 2582 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∃𝑧 ∈ ℝ
∃𝑤 ∈ ℝ
𝐵 = (𝑧 + (i · 𝑤)) → (𝐴 # 𝐵 ↔ -𝐴 # -𝐵))) |
53 | 2, 52 | mpd 13 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 # 𝐵 ↔ -𝐴 # -𝐵)) |