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 ‘ 𝐴 ) = ( 𝑥 · 𝐴 ) ) )