Proof of Theorem absext
Step | Hyp | Ref
| Expression |
1 | | absval2 9655 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) =
(√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))) |
2 | | absval2 9655 |
. . . . . . 7
⊢ (𝐵 ∈ ℂ →
(abs‘𝐵) =
(√‘(((ℜ‘𝐵)↑2) + ((ℑ‘𝐵)↑2)))) |
3 | 1, 2 | breqan12d 3779 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((abs‘𝐴) #
(abs‘𝐵) ↔
(√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) #
(√‘(((ℜ‘𝐵)↑2) + ((ℑ‘𝐵)↑2))))) |
4 | | simpl 102 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈
ℂ) |
5 | 4 | recld 9538 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐴) ∈
ℝ) |
6 | 5 | resqcld 9406 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘𝐴)↑2)
∈ ℝ) |
7 | 4 | imcld 9539 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐴) ∈
ℝ) |
8 | 7 | resqcld 9406 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℑ‘𝐴)↑2)
∈ ℝ) |
9 | 6, 8 | readdcld 7055 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2)) ∈ ℝ) |
10 | 5 | sqge0d 9407 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 0 ≤
((ℜ‘𝐴)↑2)) |
11 | 7 | sqge0d 9407 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 0 ≤
((ℑ‘𝐴)↑2)) |
12 | 6, 8, 10, 11 | addge0d 7513 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 0 ≤
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2))) |
13 | | simpr 103 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
14 | 13 | recld 9538 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐵) ∈
ℝ) |
15 | 14 | resqcld 9406 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘𝐵)↑2)
∈ ℝ) |
16 | 13 | imcld 9539 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐵) ∈
ℝ) |
17 | 16 | resqcld 9406 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℑ‘𝐵)↑2)
∈ ℝ) |
18 | 15, 17 | readdcld 7055 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐵)↑2)
+ ((ℑ‘𝐵)↑2)) ∈ ℝ) |
19 | 14 | sqge0d 9407 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 0 ≤
((ℜ‘𝐵)↑2)) |
20 | 16 | sqge0d 9407 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 0 ≤
((ℑ‘𝐵)↑2)) |
21 | 15, 17, 19, 20 | addge0d 7513 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 0 ≤
(((ℜ‘𝐵)↑2)
+ ((ℑ‘𝐵)↑2))) |
22 | | sqrt11ap 9636 |
. . . . . . 7
⊢
((((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) ∈ ℝ ∧
0 ≤ (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) ∧
((((ℜ‘𝐵)↑2)
+ ((ℑ‘𝐵)↑2)) ∈ ℝ ∧ 0 ≤
(((ℜ‘𝐵)↑2)
+ ((ℑ‘𝐵)↑2)))) →
((√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) #
(√‘(((ℜ‘𝐵)↑2) + ((ℑ‘𝐵)↑2))) ↔
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2)) # (((ℜ‘𝐵)↑2) +
((ℑ‘𝐵)↑2)))) |
23 | 9, 12, 18, 21, 22 | syl22anc 1136 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) #
(√‘(((ℜ‘𝐵)↑2) + ((ℑ‘𝐵)↑2))) ↔
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2)) # (((ℜ‘𝐵)↑2) +
((ℑ‘𝐵)↑2)))) |
24 | 3, 23 | bitrd 177 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((abs‘𝐴) #
(abs‘𝐵) ↔
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2)) # (((ℜ‘𝐵)↑2) +
((ℑ‘𝐵)↑2)))) |
25 | 6 | recnd 7054 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘𝐴)↑2)
∈ ℂ) |
26 | 8 | recnd 7054 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℑ‘𝐴)↑2)
∈ ℂ) |
27 | 15 | recnd 7054 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘𝐵)↑2)
∈ ℂ) |
28 | 17 | recnd 7054 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℑ‘𝐵)↑2)
∈ ℂ) |
29 | | addext 7601 |
. . . . . 6
⊢
(((((ℜ‘𝐴)↑2) ∈ ℂ ∧
((ℑ‘𝐴)↑2)
∈ ℂ) ∧ (((ℜ‘𝐵)↑2) ∈ ℂ ∧
((ℑ‘𝐵)↑2)
∈ ℂ)) → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) #
(((ℜ‘𝐵)↑2)
+ ((ℑ‘𝐵)↑2)) → (((ℜ‘𝐴)↑2) # ((ℜ‘𝐵)↑2) ∨
((ℑ‘𝐴)↑2)
# ((ℑ‘𝐵)↑2)))) |
30 | 25, 26, 27, 28, 29 | syl22anc 1136 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2)) # (((ℜ‘𝐵)↑2) +
((ℑ‘𝐵)↑2))
→ (((ℜ‘𝐴)↑2) # ((ℜ‘𝐵)↑2) ∨ ((ℑ‘𝐴)↑2) #
((ℑ‘𝐵)↑2)))) |
31 | 24, 30 | sylbid 139 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((abs‘𝐴) #
(abs‘𝐵) →
(((ℜ‘𝐴)↑2)
# ((ℜ‘𝐵)↑2)
∨ ((ℑ‘𝐴)↑2) # ((ℑ‘𝐵)↑2)))) |
32 | 5 | recnd 7054 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐴) ∈
ℂ) |
33 | 32 | sqvald 9378 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘𝐴)↑2) =
((ℜ‘𝐴) ·
(ℜ‘𝐴))) |
34 | 14 | recnd 7054 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐵) ∈
ℂ) |
35 | 34 | sqvald 9378 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘𝐵)↑2) =
((ℜ‘𝐵) ·
(ℜ‘𝐵))) |
36 | 33, 35 | breq12d 3777 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴)↑2)
# ((ℜ‘𝐵)↑2)
↔ ((ℜ‘𝐴)
· (ℜ‘𝐴))
# ((ℜ‘𝐵)
· (ℜ‘𝐵)))) |
37 | | mulext 7605 |
. . . . . . . 8
⊢
((((ℜ‘𝐴)
∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) ∧ ((ℜ‘𝐵) ∈ ℂ ∧
(ℜ‘𝐵) ∈
ℂ)) → (((ℜ‘𝐴) · (ℜ‘𝐴)) # ((ℜ‘𝐵) · (ℜ‘𝐵)) → ((ℜ‘𝐴) # (ℜ‘𝐵) ∨ (ℜ‘𝐴) # (ℜ‘𝐵)))) |
38 | 32, 32, 34, 34, 37 | syl22anc 1136 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴) ·
(ℜ‘𝐴)) #
((ℜ‘𝐵) ·
(ℜ‘𝐵)) →
((ℜ‘𝐴) #
(ℜ‘𝐵) ∨
(ℜ‘𝐴) #
(ℜ‘𝐵)))) |
39 | 36, 38 | sylbid 139 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴)↑2)
# ((ℜ‘𝐵)↑2)
→ ((ℜ‘𝐴) #
(ℜ‘𝐵) ∨
(ℜ‘𝐴) #
(ℜ‘𝐵)))) |
40 | | oridm 674 |
. . . . . 6
⊢
(((ℜ‘𝐴) #
(ℜ‘𝐵) ∨
(ℜ‘𝐴) #
(ℜ‘𝐵)) ↔
(ℜ‘𝐴) #
(ℜ‘𝐵)) |
41 | 39, 40 | syl6ib 150 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴)↑2)
# ((ℜ‘𝐵)↑2)
→ (ℜ‘𝐴) #
(ℜ‘𝐵))) |
42 | 7 | recnd 7054 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐴) ∈
ℂ) |
43 | 42 | sqvald 9378 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℑ‘𝐴)↑2)
= ((ℑ‘𝐴)
· (ℑ‘𝐴))) |
44 | 16 | recnd 7054 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐵) ∈
ℂ) |
45 | 44 | sqvald 9378 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℑ‘𝐵)↑2)
= ((ℑ‘𝐵)
· (ℑ‘𝐵))) |
46 | 43, 45 | breq12d 3777 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℑ‘𝐴)↑2)
# ((ℑ‘𝐵)↑2) ↔ ((ℑ‘𝐴) · (ℑ‘𝐴)) # ((ℑ‘𝐵) · (ℑ‘𝐵)))) |
47 | | mulext 7605 |
. . . . . . . 8
⊢
((((ℑ‘𝐴)
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) ∧
((ℑ‘𝐵) ∈
ℂ ∧ (ℑ‘𝐵) ∈ ℂ)) →
(((ℑ‘𝐴)
· (ℑ‘𝐴))
# ((ℑ‘𝐵)
· (ℑ‘𝐵))
→ ((ℑ‘𝐴) #
(ℑ‘𝐵) ∨
(ℑ‘𝐴) #
(ℑ‘𝐵)))) |
48 | 42, 42, 44, 44, 47 | syl22anc 1136 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℑ‘𝐴)
· (ℑ‘𝐴))
# ((ℑ‘𝐵)
· (ℑ‘𝐵))
→ ((ℑ‘𝐴) #
(ℑ‘𝐵) ∨
(ℑ‘𝐴) #
(ℑ‘𝐵)))) |
49 | 46, 48 | sylbid 139 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℑ‘𝐴)↑2)
# ((ℑ‘𝐵)↑2) → ((ℑ‘𝐴) # (ℑ‘𝐵) ∨ (ℑ‘𝐴) # (ℑ‘𝐵)))) |
50 | | oridm 674 |
. . . . . 6
⊢
(((ℑ‘𝐴)
# (ℑ‘𝐵) ∨
(ℑ‘𝐴) #
(ℑ‘𝐵)) ↔
(ℑ‘𝐴) #
(ℑ‘𝐵)) |
51 | 49, 50 | syl6ib 150 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℑ‘𝐴)↑2)
# ((ℑ‘𝐵)↑2) → (ℑ‘𝐴) # (ℑ‘𝐵))) |
52 | 41, 51 | orim12d 700 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((ℜ‘𝐴)↑2)
# ((ℜ‘𝐵)↑2)
∨ ((ℑ‘𝐴)↑2) # ((ℑ‘𝐵)↑2)) →
((ℜ‘𝐴) #
(ℜ‘𝐵) ∨
(ℑ‘𝐴) #
(ℑ‘𝐵)))) |
53 | 31, 52 | syld 40 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((abs‘𝐴) #
(abs‘𝐵) →
((ℜ‘𝐴) #
(ℜ‘𝐵) ∨
(ℑ‘𝐴) #
(ℑ‘𝐵)))) |
54 | | apreim 7594 |
. . . 4
⊢
((((ℜ‘𝐴)
∈ ℝ ∧ (ℑ‘𝐴) ∈ ℝ) ∧ ((ℜ‘𝐵) ∈ ℝ ∧
(ℑ‘𝐵) ∈
ℝ)) → (((ℜ‘𝐴) + (i · (ℑ‘𝐴))) # ((ℜ‘𝐵) + (i ·
(ℑ‘𝐵))) ↔
((ℜ‘𝐴) #
(ℜ‘𝐵) ∨
(ℑ‘𝐴) #
(ℑ‘𝐵)))) |
55 | 5, 7, 14, 16, 54 | syl22anc 1136 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴) + (i
· (ℑ‘𝐴))) # ((ℜ‘𝐵) + (i · (ℑ‘𝐵))) ↔ ((ℜ‘𝐴) # (ℜ‘𝐵) ∨ (ℑ‘𝐴) # (ℑ‘𝐵)))) |
56 | 53, 55 | sylibrd 158 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((abs‘𝐴) #
(abs‘𝐵) →
((ℜ‘𝐴) + (i
· (ℑ‘𝐴))) # ((ℜ‘𝐵) + (i · (ℑ‘𝐵))))) |
57 | 4 | replimd 9541 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
58 | 13 | replimd 9541 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 = ((ℜ‘𝐵) + (i ·
(ℑ‘𝐵)))) |
59 | 57, 58 | breq12d 3777 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 # 𝐵 ↔ ((ℜ‘𝐴) + (i · (ℑ‘𝐴))) # ((ℜ‘𝐵) + (i ·
(ℑ‘𝐵))))) |
60 | 56, 59 | sylibrd 158 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((abs‘𝐴) #
(abs‘𝐵) → 𝐴 # 𝐵)) |