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 x x = 1 A = x A

Proof

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