Proof of Theorem abs1m
Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . 6
⊢ (𝐴 = 0 → (abs‘𝐴) =
(abs‘0)) |
2 | | abs0 13873 |
. . . . . 6
⊢
(abs‘0) = 0 |
3 | 1, 2 | syl6eq 2660 |
. . . . 5
⊢ (𝐴 = 0 → (abs‘𝐴) = 0) |
4 | | oveq2 6557 |
. . . . 5
⊢ (𝐴 = 0 → (𝑥 · 𝐴) = (𝑥 · 0)) |
5 | 3, 4 | eqeq12d 2625 |
. . . 4
⊢ (𝐴 = 0 → ((abs‘𝐴) = (𝑥 · 𝐴) ↔ 0 = (𝑥 · 0))) |
6 | 5 | anbi2d 736 |
. . 3
⊢ (𝐴 = 0 → (((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴)) ↔ ((abs‘𝑥) = 1 ∧ 0 = (𝑥 · 0)))) |
7 | 6 | rexbidv 3034 |
. 2
⊢ (𝐴 = 0 → (∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧
(abs‘𝐴) = (𝑥 · 𝐴)) ↔ ∃𝑥 ∈ ℂ ((abs‘𝑥) = 1 ∧ 0 = (𝑥 · 0)))) |
8 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
9 | 8 | cjcld 13784 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(∗‘𝐴) ∈
ℂ) |
10 | | abscl 13866 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
11 | 10 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ) |
12 | 11 | recnd 9947 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℂ) |
13 | | abs00 13877 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) = 0 ↔
𝐴 = 0)) |
14 | 13 | necon3bid 2826 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) ≠ 0
↔ 𝐴 ≠
0)) |
15 | 14 | biimpar 501 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ≠ 0) |
16 | 9, 12, 15 | divcld 10680 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((∗‘𝐴) /
(abs‘𝐴)) ∈
ℂ) |
17 | | absdiv 13883 |
. . . . 5
⊢
(((∗‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ≠ 0) →
(abs‘((∗‘𝐴) / (abs‘𝐴))) = ((abs‘(∗‘𝐴)) / (abs‘(abs‘𝐴)))) |
18 | 9, 12, 15, 17 | syl3anc 1318 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘((∗‘𝐴) / (abs‘𝐴))) = ((abs‘(∗‘𝐴)) / (abs‘(abs‘𝐴)))) |
19 | | abscj 13867 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(∗‘𝐴)) = (abs‘𝐴)) |
20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘(∗‘𝐴)) = (abs‘𝐴)) |
21 | | absidm 13911 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(abs‘𝐴)) =
(abs‘𝐴)) |
22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘(abs‘𝐴)) =
(abs‘𝐴)) |
23 | 20, 22 | oveq12d 6567 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘(∗‘𝐴)) / (abs‘(abs‘𝐴))) = ((abs‘𝐴) / (abs‘𝐴))) |
24 | 12, 15 | dividd 10678 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴) /
(abs‘𝐴)) =
1) |
25 | 18, 23, 24 | 3eqtrd 2648 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘((∗‘𝐴) / (abs‘𝐴))) = 1) |
26 | 8, 9, 12, 15 | divassd 10715 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴 · (∗‘𝐴)) / (abs‘𝐴)) = (𝐴 · ((∗‘𝐴) / (abs‘𝐴)))) |
27 | 12 | sqvald 12867 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴)↑2) =
((abs‘𝐴) ·
(abs‘𝐴))) |
28 | | absvalsq 13868 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
30 | 27, 29 | eqtr3d 2646 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴) ·
(abs‘𝐴)) = (𝐴 · (∗‘𝐴))) |
31 | 12, 12, 15, 30 | mvllmuld 10736 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) = ((𝐴 · (∗‘𝐴)) / (abs‘𝐴))) |
32 | 16, 8 | mulcomd 9940 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(((∗‘𝐴) /
(abs‘𝐴)) ·
𝐴) = (𝐴 · ((∗‘𝐴) / (abs‘𝐴)))) |
33 | 26, 31, 32 | 3eqtr4d 2654 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴)) |
34 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → (abs‘𝑥) = (abs‘((∗‘𝐴) / (abs‘𝐴)))) |
35 | 34 | eqeq1d 2612 |
. . . . 5
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → ((abs‘𝑥) = 1 ↔
(abs‘((∗‘𝐴) / (abs‘𝐴))) = 1)) |
36 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → (𝑥 · 𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴)) |
37 | 36 | eqeq2d 2620 |
. . . . 5
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → ((abs‘𝐴) = (𝑥 · 𝐴) ↔ (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴))) |
38 | 35, 37 | anbi12d 743 |
. . . 4
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → (((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴)) ↔ ((abs‘((∗‘𝐴) / (abs‘𝐴))) = 1 ∧ (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴)))) |
39 | 38 | rspcev 3282 |
. . 3
⊢
((((∗‘𝐴) / (abs‘𝐴)) ∈ ℂ ∧
((abs‘((∗‘𝐴) / (abs‘𝐴))) = 1 ∧ (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴))) → ∃𝑥 ∈ ℂ ((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴))) |
40 | 16, 25, 33, 39 | syl12anc 1316 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧
(abs‘𝐴) = (𝑥 · 𝐴))) |
41 | | ax-icn 9874 |
. . . 4
⊢ i ∈
ℂ |
42 | | absi 13874 |
. . . . 5
⊢
(abs‘i) = 1 |
43 | | it0e0 11131 |
. . . . . 6
⊢ (i
· 0) = 0 |
44 | 43 | eqcomi 2619 |
. . . . 5
⊢ 0 = (i
· 0) |
45 | 42, 44 | pm3.2i 470 |
. . . 4
⊢
((abs‘i) = 1 ∧ 0 = (i · 0)) |
46 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = i → (abs‘𝑥) =
(abs‘i)) |
47 | 46 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 = i → ((abs‘𝑥) = 1 ↔ (abs‘i) =
1)) |
48 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = i → (𝑥 · 0) = (i ·
0)) |
49 | 48 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑥 = i → (0 = (𝑥 · 0) ↔ 0 = (i
· 0))) |
50 | 47, 49 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = i → (((abs‘𝑥) = 1 ∧ 0 = (𝑥 · 0)) ↔
((abs‘i) = 1 ∧ 0 = (i · 0)))) |
51 | 50 | rspcev 3282 |
. . . 4
⊢ ((i
∈ ℂ ∧ ((abs‘i) = 1 ∧ 0 = (i · 0))) →
∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧ 0
= (𝑥 ·
0))) |
52 | 41, 45, 51 | mp2an 704 |
. . 3
⊢
∃𝑥 ∈
ℂ ((abs‘𝑥) = 1
∧ 0 = (𝑥 ·
0)) |
53 | 52 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧ 0
= (𝑥 ·
0))) |
54 | 7, 40, 53 | pm2.61ne 2867 |
1
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧
(abs‘𝐴) = (𝑥 · 𝐴))) |