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 ${⊢}{A}\in ℂ\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{x}\right|=1\wedge \left|{A}\right|={x}{A}\right)$

Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{A}=0\to \left|{A}\right|=\left|0\right|$
2 abs0 ${⊢}\left|0\right|=0$
3 1 2 syl6eq ${⊢}{A}=0\to \left|{A}\right|=0$
4 oveq2 ${⊢}{A}=0\to {x}{A}={x}\cdot 0$
5 3 4 eqeq12d ${⊢}{A}=0\to \left(\left|{A}\right|={x}{A}↔0={x}\cdot 0\right)$
6 5 anbi2d ${⊢}{A}=0\to \left(\left(\left|{x}\right|=1\wedge \left|{A}\right|={x}{A}\right)↔\left(\left|{x}\right|=1\wedge 0={x}\cdot 0\right)\right)$
7 6 rexbidv ${⊢}{A}=0\to \left(\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{x}\right|=1\wedge \left|{A}\right|={x}{A}\right)↔\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{x}\right|=1\wedge 0={x}\cdot 0\right)\right)$
8 simpl ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {A}\in ℂ$
9 8 cjcld ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \stackrel{‾}{{A}}\in ℂ$
10 abscl ${⊢}{A}\in ℂ\to \left|{A}\right|\in ℝ$
11 10 adantr ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|{A}\right|\in ℝ$
12 11 recnd ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|{A}\right|\in ℂ$
13 abs00 ${⊢}{A}\in ℂ\to \left(\left|{A}\right|=0↔{A}=0\right)$
14 13 necon3bid ${⊢}{A}\in ℂ\to \left(\left|{A}\right|\ne 0↔{A}\ne 0\right)$
15 14 biimpar ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|{A}\right|\ne 0$
16 9 12 15 divcld ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\in ℂ$
17 absdiv ${⊢}\left(\stackrel{‾}{{A}}\in ℂ\wedge \left|{A}\right|\in ℂ\wedge \left|{A}\right|\ne 0\right)\to \left|\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right|=\frac{\left|\stackrel{‾}{{A}}\right|}{\left|\left|{A}\right|\right|}$
18 9 12 15 17 syl3anc ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right|=\frac{\left|\stackrel{‾}{{A}}\right|}{\left|\left|{A}\right|\right|}$
19 abscj ${⊢}{A}\in ℂ\to \left|\stackrel{‾}{{A}}\right|=\left|{A}\right|$
20 19 adantr ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|\stackrel{‾}{{A}}\right|=\left|{A}\right|$
21 absidm ${⊢}{A}\in ℂ\to \left|\left|{A}\right|\right|=\left|{A}\right|$
22 21 adantr ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|\left|{A}\right|\right|=\left|{A}\right|$
23 20 22 oveq12d ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \frac{\left|\stackrel{‾}{{A}}\right|}{\left|\left|{A}\right|\right|}=\frac{\left|{A}\right|}{\left|{A}\right|}$
24 12 15 dividd ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \frac{\left|{A}\right|}{\left|{A}\right|}=1$
25 18 23 24 3eqtrd ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right|=1$
26 8 9 12 15 divassd ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \frac{{A}\stackrel{‾}{{A}}}{\left|{A}\right|}={A}\left(\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right)$
27 12 sqvald ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {\left|{A}\right|}^{2}=\left|{A}\right|\left|{A}\right|$
28 absvalsq ${⊢}{A}\in ℂ\to {\left|{A}\right|}^{2}={A}\stackrel{‾}{{A}}$
29 28 adantr ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {\left|{A}\right|}^{2}={A}\stackrel{‾}{{A}}$
30 27 29 eqtr3d ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|{A}\right|\left|{A}\right|={A}\stackrel{‾}{{A}}$
31 12 12 15 30 mvllmuld ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|{A}\right|=\frac{{A}\stackrel{‾}{{A}}}{\left|{A}\right|}$
32 16 8 mulcomd ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left(\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right){A}={A}\left(\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right)$
33 26 31 32 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|{A}\right|=\left(\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right){A}$
34 fveqeq2 ${⊢}{x}=\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\to \left(\left|{x}\right|=1↔\left|\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right|=1\right)$
35 oveq1 ${⊢}{x}=\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\to {x}{A}=\left(\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right){A}$
36 35 eqeq2d ${⊢}{x}=\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\to \left(\left|{A}\right|={x}{A}↔\left|{A}\right|=\left(\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right){A}\right)$
37 34 36 anbi12d ${⊢}{x}=\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\to \left(\left(\left|{x}\right|=1\wedge \left|{A}\right|={x}{A}\right)↔\left(\left|\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right|=1\wedge \left|{A}\right|=\left(\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right){A}\right)\right)$
38 37 rspcev ${⊢}\left(\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\in ℂ\wedge \left(\left|\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right|=1\wedge \left|{A}\right|=\left(\frac{\stackrel{‾}{{A}}}{\left|{A}\right|}\right){A}\right)\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{x}\right|=1\wedge \left|{A}\right|={x}{A}\right)$
39 16 25 33 38 syl12anc ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{x}\right|=1\wedge \left|{A}\right|={x}{A}\right)$
40 ax-icn ${⊢}\mathrm{i}\in ℂ$
41 absi ${⊢}\left|\mathrm{i}\right|=1$
42 it0e0 ${⊢}\mathrm{i}\cdot 0=0$
43 42 eqcomi ${⊢}0=\mathrm{i}\cdot 0$
44 41 43 pm3.2i ${⊢}\left(\left|\mathrm{i}\right|=1\wedge 0=\mathrm{i}\cdot 0\right)$
45 fveqeq2 ${⊢}{x}=\mathrm{i}\to \left(\left|{x}\right|=1↔\left|\mathrm{i}\right|=1\right)$
46 oveq1 ${⊢}{x}=\mathrm{i}\to {x}\cdot 0=\mathrm{i}\cdot 0$
47 46 eqeq2d ${⊢}{x}=\mathrm{i}\to \left(0={x}\cdot 0↔0=\mathrm{i}\cdot 0\right)$
48 45 47 anbi12d ${⊢}{x}=\mathrm{i}\to \left(\left(\left|{x}\right|=1\wedge 0={x}\cdot 0\right)↔\left(\left|\mathrm{i}\right|=1\wedge 0=\mathrm{i}\cdot 0\right)\right)$
49 48 rspcev ${⊢}\left(\mathrm{i}\in ℂ\wedge \left(\left|\mathrm{i}\right|=1\wedge 0=\mathrm{i}\cdot 0\right)\right)\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{x}\right|=1\wedge 0={x}\cdot 0\right)$
50 40 44 49 mp2an ${⊢}\exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{x}\right|=1\wedge 0={x}\cdot 0\right)$
51 50 a1i ${⊢}{A}\in ℂ\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{x}\right|=1\wedge 0={x}\cdot 0\right)$
52 7 39 51 pm2.61ne ${⊢}{A}\in ℂ\to \exists {x}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{x}\right|=1\wedge \left|{A}\right|={x}{A}\right)$