Proof of Theorem abs1m
| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . 6
⊢ (𝐴 = 0 → (abs‘𝐴) =
(abs‘0)) |
| 2 | | abs0 15324 |
. . . . . 6
⊢
(abs‘0) = 0 |
| 3 | 1, 2 | eqtrdi 2793 |
. . . . 5
⊢ (𝐴 = 0 → (abs‘𝐴) = 0) |
| 4 | | oveq2 7439 |
. . . . 5
⊢ (𝐴 = 0 → (𝑥 · 𝐴) = (𝑥 · 0)) |
| 5 | 3, 4 | eqeq12d 2753 |
. . . 4
⊢ (𝐴 = 0 → ((abs‘𝐴) = (𝑥 · 𝐴) ↔ 0 = (𝑥 · 0))) |
| 6 | 5 | anbi2d 630 |
. . 3
⊢ (𝐴 = 0 → (((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴)) ↔ ((abs‘𝑥) = 1 ∧ 0 = (𝑥 · 0)))) |
| 7 | 6 | rexbidv 3179 |
. 2
⊢ (𝐴 = 0 → (∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧
(abs‘𝐴) = (𝑥 · 𝐴)) ↔ ∃𝑥 ∈ ℂ ((abs‘𝑥) = 1 ∧ 0 = (𝑥 · 0)))) |
| 8 | | simpl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
| 9 | 8 | cjcld 15235 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(∗‘𝐴) ∈
ℂ) |
| 10 | | abscl 15317 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
| 11 | 10 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ) |
| 12 | 11 | recnd 11289 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℂ) |
| 13 | | abs00 15328 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) = 0 ↔
𝐴 = 0)) |
| 14 | 13 | necon3bid 2985 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) ≠ 0
↔ 𝐴 ≠
0)) |
| 15 | 14 | biimpar 477 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ≠ 0) |
| 16 | 9, 12, 15 | divcld 12043 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((∗‘𝐴) /
(abs‘𝐴)) ∈
ℂ) |
| 17 | | absdiv 15334 |
. . . . 5
⊢
(((∗‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ≠ 0) →
(abs‘((∗‘𝐴) / (abs‘𝐴))) = ((abs‘(∗‘𝐴)) / (abs‘(abs‘𝐴)))) |
| 18 | 9, 12, 15, 17 | syl3anc 1373 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘((∗‘𝐴) / (abs‘𝐴))) = ((abs‘(∗‘𝐴)) / (abs‘(abs‘𝐴)))) |
| 19 | | abscj 15318 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(∗‘𝐴)) = (abs‘𝐴)) |
| 20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘(∗‘𝐴)) = (abs‘𝐴)) |
| 21 | | absidm 15362 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(abs‘𝐴)) =
(abs‘𝐴)) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘(abs‘𝐴)) =
(abs‘𝐴)) |
| 23 | 20, 22 | oveq12d 7449 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘(∗‘𝐴)) / (abs‘(abs‘𝐴))) = ((abs‘𝐴) / (abs‘𝐴))) |
| 24 | 12, 15 | dividd 12041 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴) /
(abs‘𝐴)) =
1) |
| 25 | 18, 23, 24 | 3eqtrd 2781 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(abs‘((∗‘𝐴) / (abs‘𝐴))) = 1) |
| 26 | 8, 9, 12, 15 | divassd 12078 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴 · (∗‘𝐴)) / (abs‘𝐴)) = (𝐴 · ((∗‘𝐴) / (abs‘𝐴)))) |
| 27 | 12 | sqvald 14183 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴)↑2) =
((abs‘𝐴) ·
(abs‘𝐴))) |
| 28 | | absvalsq 15319 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
| 30 | 27, 29 | eqtr3d 2779 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴) ·
(abs‘𝐴)) = (𝐴 · (∗‘𝐴))) |
| 31 | 12, 12, 15, 30 | mvllmuld 12099 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) = ((𝐴 · (∗‘𝐴)) / (abs‘𝐴))) |
| 32 | 16, 8 | mulcomd 11282 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(((∗‘𝐴) /
(abs‘𝐴)) ·
𝐴) = (𝐴 · ((∗‘𝐴) / (abs‘𝐴)))) |
| 33 | 26, 31, 32 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴)) |
| 34 | | fveqeq2 6915 |
. . . . 5
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → ((abs‘𝑥) = 1 ↔
(abs‘((∗‘𝐴) / (abs‘𝐴))) = 1)) |
| 35 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → (𝑥 · 𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴)) |
| 36 | 35 | eqeq2d 2748 |
. . . . 5
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → ((abs‘𝐴) = (𝑥 · 𝐴) ↔ (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴))) |
| 37 | 34, 36 | anbi12d 632 |
. . . 4
⊢ (𝑥 = ((∗‘𝐴) / (abs‘𝐴)) → (((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴)) ↔ ((abs‘((∗‘𝐴) / (abs‘𝐴))) = 1 ∧ (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴)))) |
| 38 | 37 | rspcev 3622 |
. . 3
⊢
((((∗‘𝐴) / (abs‘𝐴)) ∈ ℂ ∧
((abs‘((∗‘𝐴) / (abs‘𝐴))) = 1 ∧ (abs‘𝐴) = (((∗‘𝐴) / (abs‘𝐴)) · 𝐴))) → ∃𝑥 ∈ ℂ ((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴))) |
| 39 | 16, 25, 33, 38 | syl12anc 837 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧
(abs‘𝐴) = (𝑥 · 𝐴))) |
| 40 | | ax-icn 11214 |
. . . 4
⊢ i ∈
ℂ |
| 41 | | absi 15325 |
. . . . 5
⊢
(abs‘i) = 1 |
| 42 | | it0e0 12488 |
. . . . . 6
⊢ (i
· 0) = 0 |
| 43 | 42 | eqcomi 2746 |
. . . . 5
⊢ 0 = (i
· 0) |
| 44 | 41, 43 | pm3.2i 470 |
. . . 4
⊢
((abs‘i) = 1 ∧ 0 = (i · 0)) |
| 45 | | fveqeq2 6915 |
. . . . . 6
⊢ (𝑥 = i → ((abs‘𝑥) = 1 ↔ (abs‘i) =
1)) |
| 46 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = i → (𝑥 · 0) = (i ·
0)) |
| 47 | 46 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑥 = i → (0 = (𝑥 · 0) ↔ 0 = (i
· 0))) |
| 48 | 45, 47 | anbi12d 632 |
. . . . 5
⊢ (𝑥 = i → (((abs‘𝑥) = 1 ∧ 0 = (𝑥 · 0)) ↔
((abs‘i) = 1 ∧ 0 = (i · 0)))) |
| 49 | 48 | rspcev 3622 |
. . . 4
⊢ ((i
∈ ℂ ∧ ((abs‘i) = 1 ∧ 0 = (i · 0))) →
∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧ 0
= (𝑥 ·
0))) |
| 50 | 40, 44, 49 | mp2an 692 |
. . 3
⊢
∃𝑥 ∈
ℂ ((abs‘𝑥) = 1
∧ 0 = (𝑥 ·
0)) |
| 51 | 50 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧ 0
= (𝑥 ·
0))) |
| 52 | 7, 39, 51 | pm2.61ne 3027 |
1
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
((abs‘𝑥) = 1 ∧
(abs‘𝐴) = (𝑥 · 𝐴))) |