Proof of Theorem abs1m
Step | Hyp | Ref
| Expression |
1 | | fveq2 6433 |
. . . . . 6
⊢ (𝐴 = 0 → (abs‘𝐴) =
(abs‘0)) |
2 | | abs0 14402 |
. . . . . 6
⊢
(abs‘0) = 0 |
3 | 1, 2 | syl6eq 2877 |
. . . . 5
⊢ (𝐴 = 0 → (abs‘𝐴) = 0) |
4 | | oveq2 6913 |
. . . . 5
⊢ (𝐴 = 0 → (𝑥 · 𝐴) = (𝑥 · 0)) |
5 | 3, 4 | eqeq12d 2840 |
. . . 4
⊢ (𝐴 = 0 → ((abs‘𝐴) = (𝑥 · 𝐴) ↔ 0 = (𝑥 · 0))) |
6 | 5 | anbi2d 624 |
. . 3
⊢ (𝐴 = 0 → (((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴)) ↔ ((abs‘𝑥) = 1 ∧ 0 = (𝑥 · 0)))) |
7 | 6 | rexbidv 3262 |
. 2
⊢ (𝐴 = 0 → (∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧
(abs‘𝐴) = (𝑥 · 𝐴)) ↔ ∃𝑥 ∈ ℂ ((abs‘𝑥) = 1 ∧ 0 = (𝑥 · 0)))) |
8 | | simpl 476 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
9 | 8 | cjcld 14313 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(∗‘𝐴) ∈
ℂ) |
10 | | abscl 14395 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
11 | 10 | adantr 474 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ) |
12 | 11 | recnd 10385 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℂ) |
13 | | abs00 14406 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) = 0 ↔
𝐴 = 0)) |
14 | 13 | necon3bid 3043 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) ≠ 0
↔ 𝐴 ≠
0)) |
15 | 14 | biimpar 471 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ≠ 0) |
16 | 9, 12, 15 | divcld 11127 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((∗‘𝐴) /
(abs‘𝐴)) ∈
ℂ) |
17 | | absdiv 14412 |
. . . . 5
⊢
(((∗‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ≠ 0) →
(abs‘((∗‘𝐴) / (abs‘𝐴))) = ((abs‘(∗‘𝐴)) / (abs‘(abs‘𝐴)))) |
18 | 9, 12, 15, 17 | syl3anc 1496 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘((∗‘𝐴) / (abs‘𝐴))) = ((abs‘(∗‘𝐴)) / (abs‘(abs‘𝐴)))) |
19 | | abscj 14396 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(∗‘𝐴)) = (abs‘𝐴)) |
20 | 19 | adantr 474 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘(∗‘𝐴)) = (abs‘𝐴)) |
21 | | absidm 14440 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(abs‘𝐴)) =
(abs‘𝐴)) |
22 | 21 | adantr 474 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘(abs‘𝐴)) =
(abs‘𝐴)) |
23 | 20, 22 | oveq12d 6923 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘(∗‘𝐴)) / (abs‘(abs‘𝐴))) = ((abs‘𝐴) / (abs‘𝐴))) |
24 | 12, 15 | dividd 11125 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴) /
(abs‘𝐴)) =
1) |
25 | 18, 23, 24 | 3eqtrd 2865 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘((∗‘𝐴) / (abs‘𝐴))) = 1) |
26 | 8, 9, 12, 15 | divassd 11162 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴 · (∗‘𝐴)) / (abs‘𝐴)) = (𝐴 · ((∗‘𝐴) / (abs‘𝐴)))) |
27 | 12 | sqvald 13299 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴)↑2) =
((abs‘𝐴) ·
(abs‘𝐴))) |
28 | | absvalsq 14397 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
29 | 28 | adantr 474 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
30 | 27, 29 | eqtr3d 2863 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴) ·
(abs‘𝐴)) = (𝐴 · (∗‘𝐴))) |
31 | 12, 12, 15, 30 | mvllmuld 11183 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) = ((𝐴 · (∗‘𝐴)) / (abs‘𝐴))) |
32 | 16, 8 | mulcomd 10378 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(((∗‘𝐴) /
(abs‘𝐴)) ·
𝐴) = (𝐴 · ((∗‘𝐴) / (abs‘𝐴)))) |
33 | 26, 31, 32 | 3eqtr4d 2871 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴)) |
34 | | fveqeq2 6442 |
. . . . 5
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → ((abs‘𝑥) = 1 ↔
(abs‘((∗‘𝐴) / (abs‘𝐴))) = 1)) |
35 | | oveq1 6912 |
. . . . . 6
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → (𝑥 · 𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴)) |
36 | 35 | eqeq2d 2835 |
. . . . 5
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → ((abs‘𝐴) = (𝑥 · 𝐴) ↔ (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴))) |
37 | 34, 36 | anbi12d 626 |
. . . 4
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → (((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴)) ↔ ((abs‘((∗‘𝐴) / (abs‘𝐴))) = 1 ∧ (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴)))) |
38 | 37 | rspcev 3526 |
. . 3
⊢
((((∗‘𝐴) / (abs‘𝐴)) ∈ ℂ ∧
((abs‘((∗‘𝐴) / (abs‘𝐴))) = 1 ∧ (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴))) → ∃𝑥 ∈ ℂ ((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴))) |
39 | 16, 25, 33, 38 | syl12anc 872 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧
(abs‘𝐴) = (𝑥 · 𝐴))) |
40 | | ax-icn 10311 |
. . . 4
⊢ i ∈
ℂ |
41 | | absi 14403 |
. . . . 5
⊢
(abs‘i) = 1 |
42 | | it0e0 11580 |
. . . . . 6
⊢ (i
· 0) = 0 |
43 | 42 | eqcomi 2834 |
. . . . 5
⊢ 0 = (i
· 0) |
44 | 41, 43 | pm3.2i 464 |
. . . 4
⊢
((abs‘i) = 1 ∧ 0 = (i · 0)) |
45 | | fveqeq2 6442 |
. . . . . 6
⊢ (𝑥 = i → ((abs‘𝑥) = 1 ↔ (abs‘i) =
1)) |
46 | | oveq1 6912 |
. . . . . . 7
⊢ (𝑥 = i → (𝑥 · 0) = (i ·
0)) |
47 | 46 | eqeq2d 2835 |
. . . . . 6
⊢ (𝑥 = i → (0 = (𝑥 · 0) ↔ 0 = (i
· 0))) |
48 | 45, 47 | anbi12d 626 |
. . . . 5
⊢ (𝑥 = i → (((abs‘𝑥) = 1 ∧ 0 = (𝑥 · 0)) ↔
((abs‘i) = 1 ∧ 0 = (i · 0)))) |
49 | 48 | rspcev 3526 |
. . . 4
⊢ ((i
∈ ℂ ∧ ((abs‘i) = 1 ∧ 0 = (i · 0))) →
∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧ 0
= (𝑥 ·
0))) |
50 | 40, 44, 49 | mp2an 685 |
. . 3
⊢
∃𝑥 ∈
ℂ ((abs‘𝑥) = 1
∧ 0 = (𝑥 ·
0)) |
51 | 50 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧ 0
= (𝑥 ·
0))) |
52 | 7, 39, 51 | pm2.61ne 3084 |
1
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧
(abs‘𝐴) = (𝑥 · 𝐴))) |