Step | Hyp | Ref
| Expression |
1 | | cnre 6821 |
. . 3
⊢ (A ∈ ℂ →
∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y))) |
2 | 1 | adantr 261 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y))) |
3 | | cnre 6821 |
. . . . . 6
⊢ (B ∈ ℂ →
∃z ∈ ℝ ∃w ∈ ℝ B =
(z + (i · w))) |
4 | 3 | ad3antlr 462 |
. . . . 5
⊢
((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) → ∃z ∈ ℝ ∃w ∈ ℝ B =
(z + (i · w))) |
5 | | simplrr 488 |
. . . . . . . . . . . 12
⊢
((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) → y ∈
ℝ) |
6 | 5 | ad2antrr 457 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → y ∈
ℝ) |
7 | 6 | recnd 6851 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → y ∈
ℂ) |
8 | | simplrr 488 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → w ∈
ℝ) |
9 | 8 | recnd 6851 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → w ∈
ℂ) |
10 | | apneg 7395 |
. . . . . . . . . 10
⊢
((y ∈ ℂ ∧
w ∈
ℂ) → (y # w ↔ -y #
-w)) |
11 | 7, 9, 10 | syl2anc 391 |
. . . . . . . . 9
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → (y # w ↔
-y # -w)) |
12 | 11 | orbi2d 703 |
. . . . . . . 8
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → ((x # z ∨ y # w) ↔ (x #
z ∨
-y # -w))) |
13 | | simpllr 486 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → A = (x + (i
· y))) |
14 | | simpr 103 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → B = (z + (i
· w))) |
15 | 13, 14 | breq12d 3768 |
. . . . . . . . 9
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → (A # B ↔
(x + (i · y)) # (z + (i
· w)))) |
16 | | simplrl 487 |
. . . . . . . . . . 11
⊢
((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) → x ∈
ℝ) |
17 | 16 | ad2antrr 457 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → x ∈
ℝ) |
18 | | simplrl 487 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → z ∈
ℝ) |
19 | | apreim 7387 |
. . . . . . . . . 10
⊢
(((x ∈ ℝ ∧
y ∈
ℝ) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) → ((x + (i · y)) # (z + (i
· w)) ↔ (x # z ∨ y # w))) |
20 | 17, 6, 18, 8, 19 | syl22anc 1135 |
. . . . . . . . 9
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → ((x + (i · y)) # (z + (i
· w)) ↔ (x # z ∨ y # w))) |
21 | 15, 20 | bitrd 177 |
. . . . . . . 8
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → (A # B ↔
(x # z
∨ y #
w))) |
22 | 13 | fveq2d 5125 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) →
(∗‘A) =
(∗‘(x + (i · y)))) |
23 | | cjreim 9131 |
. . . . . . . . . . . 12
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → (∗‘(x + (i
· y))) = (x − (i · y))) |
24 | 17, 6, 23 | syl2anc 391 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) →
(∗‘(x + (i · y))) = (x
− (i · y))) |
25 | 22, 24 | eqtrd 2069 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) →
(∗‘A) = (x − (i · y))) |
26 | 14 | fveq2d 5125 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) →
(∗‘B) =
(∗‘(z + (i · w)))) |
27 | | cjreim 9131 |
. . . . . . . . . . . 12
⊢
((z ∈ ℝ ∧
w ∈
ℝ) → (∗‘(z + (i
· w))) = (z − (i · w))) |
28 | 18, 8, 27 | syl2anc 391 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) →
(∗‘(z + (i · w))) = (z
− (i · w))) |
29 | 26, 28 | eqtrd 2069 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) →
(∗‘B) = (z − (i · w))) |
30 | 25, 29 | breq12d 3768 |
. . . . . . . . 9
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) →
((∗‘A) #
(∗‘B) ↔ (x − (i · y)) # (z −
(i · w)))) |
31 | 17 | recnd 6851 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → x ∈
ℂ) |
32 | | ax-icn 6778 |
. . . . . . . . . . . 12
⊢ i ∈ ℂ |
33 | 32 | a1i 9 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → i ∈ ℂ) |
34 | | submul2 7192 |
. . . . . . . . . . 11
⊢
((x ∈ ℂ ∧ i
∈ ℂ ∧
y ∈
ℂ) → (x − (i ·
y)) = (x + (i · -y))) |
35 | 31, 33, 7, 34 | syl3anc 1134 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → (x − (i · y)) = (x + (i
· -y))) |
36 | 18 | recnd 6851 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → z ∈
ℂ) |
37 | | submul2 7192 |
. . . . . . . . . . 11
⊢
((z ∈ ℂ ∧ i
∈ ℂ ∧
w ∈
ℂ) → (z − (i ·
w)) = (z + (i · -w))) |
38 | 36, 33, 9, 37 | syl3anc 1134 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → (z − (i · w)) = (z + (i
· -w))) |
39 | 35, 38 | breq12d 3768 |
. . . . . . . . 9
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → ((x − (i · y)) # (z −
(i · w)) ↔ (x + (i · -y)) # (z + (i
· -w)))) |
40 | 6 | renegcld 7174 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → -y ∈
ℝ) |
41 | 8 | renegcld 7174 |
. . . . . . . . . 10
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → -w ∈
ℝ) |
42 | | apreim 7387 |
. . . . . . . . . 10
⊢
(((x ∈ ℝ ∧
-y ∈
ℝ) ∧ (z ∈ ℝ ∧ -w ∈ ℝ)) → ((x + (i · -y)) # (z + (i
· -w)) ↔ (x # z ∨ -y # -w))) |
43 | 17, 40, 18, 41, 42 | syl22anc 1135 |
. . . . . . . . 9
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) → ((x + (i · -y)) # (z + (i
· -w)) ↔ (x # z ∨ -y # -w))) |
44 | 30, 39, 43 | 3bitrd 203 |
. . . . . . . 8
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) →
((∗‘A) #
(∗‘B) ↔ (x # z ∨ -y # -w))) |
45 | 12, 21, 44 | 3bitr4rd 210 |
. . . . . . 7
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) ∧ B = (z + (i
· w))) →
((∗‘A) #
(∗‘B) ↔ A # B)) |
46 | 45 | ex 108 |
. . . . . 6
⊢
(((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) ∧ (z ∈ ℝ ∧
w ∈
ℝ)) → (B = (z + (i · w)) → ((∗‘A) # (∗‘B) ↔ A #
B))) |
47 | 46 | rexlimdvva 2434 |
. . . . 5
⊢
((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) → (∃z ∈ ℝ ∃w ∈ ℝ B =
(z + (i · w)) → ((∗‘A) # (∗‘B) ↔ A #
B))) |
48 | 4, 47 | mpd 13 |
. . . 4
⊢
((((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) ∧
A = (x
+ (i · y))) →
((∗‘A) #
(∗‘B) ↔ A # B)) |
49 | 48 | ex 108 |
. . 3
⊢
(((A ∈ ℂ ∧
B ∈
ℂ) ∧ (x ∈ ℝ ∧ y ∈ ℝ)) → (A = (x + (i
· y)) →
((∗‘A) #
(∗‘B) ↔ A # B))) |
50 | 49 | rexlimdvva 2434 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y)) → ((∗‘A) # (∗‘B) ↔ A #
B))) |
51 | 2, 50 | mpd 13 |
1
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((∗‘A) #
(∗‘B) ↔ A # B)) |