Metamath Proof Explorer

Theorem abs1m

Description: For any complex number, there exists a unit-magnitude multiplier that produces its absolute value. Part of proof of Theorem 13-2.12 of Gleason p. 195. (Contributed by NM, 26-Mar-2005)

Ref Expression
Assertion abs1m ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
2 abs0 ⊢ ( abs ‘ 0 ) = 0
3 1 2 eqtrdi ⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = 0 )
4 oveq2 ⊢ ( 𝐴 = 0 → ( 𝑥 · 𝐴 ) = ( 𝑥 · 0 ) )
5 3 4 eqeq12d ⊢ ( 𝐴 = 0 → ( ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ↔ 0 = ( 𝑥 · 0 ) ) )
6 5 anbi2d ⊢ ( 𝐴 = 0 → ( ( ( abs ‘ 𝑥 ) = 1 ∧ ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ) ↔ ( ( abs ‘ 𝑥 ) = 1 ∧ 0 = ( 𝑥 · 0 ) ) ) )
7 6 rexbidv ⊢ ( 𝐴 = 0 → ( ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ) ↔ ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ 0 = ( 𝑥 · 0 ) ) ) )
8 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
9 8 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
10 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
11 10 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
12 11 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
13 abs00 ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
14 13 necon3bid ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
15 14 biimpar ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
16 9 12 15 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ∈ ℂ )
17 absdiv ⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( abs ‘ 𝐴 ) ∈ ℂ ∧ ( abs ‘ 𝐴 ) ≠ 0 ) → ( abs ‘ ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ) = ( ( abs ‘ ( ∗ ‘ 𝐴 ) ) / ( abs ‘ ( abs ‘ 𝐴 ) ) ) )
18 9 12 15 17 syl3anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ) = ( ( abs ‘ ( ∗ ‘ 𝐴 ) ) / ( abs ‘ ( abs ‘ 𝐴 ) ) ) )
19 abscj ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ∗ ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
20 19 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ∗ ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
21 absidm ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
22 21 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
23 20 22 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ ( ∗ ‘ 𝐴 ) ) / ( abs ‘ ( abs ‘ 𝐴 ) ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) )
24 12 15 dividd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) = 1 )
25 18 23 24 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ) = 1 )
26 8 9 12 15 divassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) = ( 𝐴 · ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ) )
27 12 sqvald ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) )
28 absvalsq ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
29 28 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
30 27 29 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
31 12 12 15 30 mvllmuld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) )
32 16 8 mulcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) · 𝐴 ) = ( 𝐴 · ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ) )
33 26 31 32 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) = ( ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) · 𝐴 ) )
34 fveqeq2 ⊢ ( 𝑥 = ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) → ( ( abs ‘ 𝑥 ) = 1 ↔ ( abs ‘ ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ) = 1 ) )
35 oveq1 ⊢ ( 𝑥 = ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) → ( 𝑥 · 𝐴 ) = ( ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) · 𝐴 ) )
36 35 eqeq2d ⊢ ( 𝑥 = ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ↔ ( abs ‘ 𝐴 ) = ( ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) · 𝐴 ) ) )
37 34 36 anbi12d ⊢ ( 𝑥 = ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) → ( ( ( abs ‘ 𝑥 ) = 1 ∧ ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ) ↔ ( ( abs ‘ ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ) = 1 ∧ ( abs ‘ 𝐴 ) = ( ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) · 𝐴 ) ) ) )
38 37 rspcev ⊢ ( ( ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ∈ ℂ ∧ ( ( abs ‘ ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) ) = 1 ∧ ( abs ‘ 𝐴 ) = ( ( ( ∗ ‘ 𝐴 ) / ( abs ‘ 𝐴 ) ) · 𝐴 ) ) ) → ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ) )
39 16 25 33 38 syl12anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ) )
40 ax-icn ⊢ i ∈ ℂ
41 absi ⊢ ( abs ‘ i ) = 1
42 it0e0 ⊢ ( i · 0 ) = 0
43 42 eqcomi ⊢ 0 = ( i · 0 )
44 41 43 pm3.2i ⊢ ( ( abs ‘ i ) = 1 ∧ 0 = ( i · 0 ) )
45 fveqeq2 ⊢ ( 𝑥 = i → ( ( abs ‘ 𝑥 ) = 1 ↔ ( abs ‘ i ) = 1 ) )
46 oveq1 ⊢ ( 𝑥 = i → ( 𝑥 · 0 ) = ( i · 0 ) )
47 46 eqeq2d ⊢ ( 𝑥 = i → ( 0 = ( 𝑥 · 0 ) ↔ 0 = ( i · 0 ) ) )
48 45 47 anbi12d ⊢ ( 𝑥 = i → ( ( ( abs ‘ 𝑥 ) = 1 ∧ 0 = ( 𝑥 · 0 ) ) ↔ ( ( abs ‘ i ) = 1 ∧ 0 = ( i · 0 ) ) ) )
49 48 rspcev ⊢ ( ( i ∈ ℂ ∧ ( ( abs ‘ i ) = 1 ∧ 0 = ( i · 0 ) ) ) → ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ 0 = ( 𝑥 · 0 ) ) )
50 40 44 49 mp2an ⊢ ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ 0 = ( 𝑥 · 0 ) )
51 50 a1i ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ 0 = ( 𝑥 · 0 ) ) )
52 7 39 51 pm2.61ne ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( ( abs ‘ 𝑥 ) = 1 ∧ ( abs ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ) )