Theorem cnmsgnsubg

Description: The signs form a multiplicative subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypothesis	cnmsgnsubg.m	⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
Assertion	cnmsgnsubg	⊢ { 1 , - 1 } ∈ ( SubGrp ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		cnmsgnsubg.m	⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
2		elpri	⊢ ( 𝑥 ∈ { 1 , - 1 } → ( 𝑥 = 1 ∨ 𝑥 = - 1 ) )
3		id	⊢ ( 𝑥 = 1 → 𝑥 = 1 )
4		ax-1cn	⊢ 1 ∈ ℂ
5	3 4	eqeltrdi	⊢ ( 𝑥 = 1 → 𝑥 ∈ ℂ )
6		id	⊢ ( 𝑥 = - 1 → 𝑥 = - 1 )
7		neg1cn	⊢ - 1 ∈ ℂ
8	6 7	eqeltrdi	⊢ ( 𝑥 = - 1 → 𝑥 ∈ ℂ )
9	5 8	jaoi	⊢ ( ( 𝑥 = 1 ∨ 𝑥 = - 1 ) → 𝑥 ∈ ℂ )
10	2 9	syl	⊢ ( 𝑥 ∈ { 1 , - 1 } → 𝑥 ∈ ℂ )
11		ax-1ne0	⊢ 1 ≠ 0
12	11	a1i	⊢ ( 𝑥 = 1 → 1 ≠ 0 )
13	3 12	eqnetrd	⊢ ( 𝑥 = 1 → 𝑥 ≠ 0 )
14		neg1ne0	⊢ - 1 ≠ 0
15	14	a1i	⊢ ( 𝑥 = - 1 → - 1 ≠ 0 )
16	6 15	eqnetrd	⊢ ( 𝑥 = - 1 → 𝑥 ≠ 0 )
17	13 16	jaoi	⊢ ( ( 𝑥 = 1 ∨ 𝑥 = - 1 ) → 𝑥 ≠ 0 )
18	2 17	syl	⊢ ( 𝑥 ∈ { 1 , - 1 } → 𝑥 ≠ 0 )
19		elpri	⊢ ( 𝑦 ∈ { 1 , - 1 } → ( 𝑦 = 1 ∨ 𝑦 = - 1 ) )
20		oveq12	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 1 ) → ( 𝑥 · 𝑦 ) = ( 1 · 1 ) )
21	4	mulridi	⊢ ( 1 · 1 ) = 1
22		1ex	⊢ 1 ∈ V
23	22	prid1	⊢ 1 ∈ { 1 , - 1 }
24	21 23	eqeltri	⊢ ( 1 · 1 ) ∈ { 1 , - 1 }
25	20 24	eqeltrdi	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 1 ) → ( 𝑥 · 𝑦 ) ∈ { 1 , - 1 } )
26		oveq12	⊢ ( ( 𝑥 = - 1 ∧ 𝑦 = 1 ) → ( 𝑥 · 𝑦 ) = ( - 1 · 1 ) )
27	7	mulridi	⊢ ( - 1 · 1 ) = - 1
28		negex	⊢ - 1 ∈ V
29	28	prid2	⊢ - 1 ∈ { 1 , - 1 }
30	27 29	eqeltri	⊢ ( - 1 · 1 ) ∈ { 1 , - 1 }
31	26 30	eqeltrdi	⊢ ( ( 𝑥 = - 1 ∧ 𝑦 = 1 ) → ( 𝑥 · 𝑦 ) ∈ { 1 , - 1 } )
32		oveq12	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = - 1 ) → ( 𝑥 · 𝑦 ) = ( 1 · - 1 ) )
33	7	mullidi	⊢ ( 1 · - 1 ) = - 1
34	33 29	eqeltri	⊢ ( 1 · - 1 ) ∈ { 1 , - 1 }
35	32 34	eqeltrdi	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = - 1 ) → ( 𝑥 · 𝑦 ) ∈ { 1 , - 1 } )
36		oveq12	⊢ ( ( 𝑥 = - 1 ∧ 𝑦 = - 1 ) → ( 𝑥 · 𝑦 ) = ( - 1 · - 1 ) )
37		neg1mulneg1e1	⊢ ( - 1 · - 1 ) = 1
38	37 23	eqeltri	⊢ ( - 1 · - 1 ) ∈ { 1 , - 1 }
39	36 38	eqeltrdi	⊢ ( ( 𝑥 = - 1 ∧ 𝑦 = - 1 ) → ( 𝑥 · 𝑦 ) ∈ { 1 , - 1 } )
40	25 31 35 39	ccase	⊢ ( ( ( 𝑥 = 1 ∨ 𝑥 = - 1 ) ∧ ( 𝑦 = 1 ∨ 𝑦 = - 1 ) ) → ( 𝑥 · 𝑦 ) ∈ { 1 , - 1 } )
41	2 19 40	syl2an	⊢ ( ( 𝑥 ∈ { 1 , - 1 } ∧ 𝑦 ∈ { 1 , - 1 } ) → ( 𝑥 · 𝑦 ) ∈ { 1 , - 1 } )
42		oveq2	⊢ ( 𝑥 = 1 → ( 1 / 𝑥 ) = ( 1 / 1 ) )
43		1div1e1	⊢ ( 1 / 1 ) = 1
44	43 23	eqeltri	⊢ ( 1 / 1 ) ∈ { 1 , - 1 }
45	42 44	eqeltrdi	⊢ ( 𝑥 = 1 → ( 1 / 𝑥 ) ∈ { 1 , - 1 } )
46		oveq2	⊢ ( 𝑥 = - 1 → ( 1 / 𝑥 ) = ( 1 / - 1 ) )
47		divneg2	⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → - ( 1 / 1 ) = ( 1 / - 1 ) )
48	4 4 11 47	mp3an	⊢ - ( 1 / 1 ) = ( 1 / - 1 )
49	43	negeqi	⊢ - ( 1 / 1 ) = - 1
50	48 49	eqtr3i	⊢ ( 1 / - 1 ) = - 1
51	50 29	eqeltri	⊢ ( 1 / - 1 ) ∈ { 1 , - 1 }
52	46 51	eqeltrdi	⊢ ( 𝑥 = - 1 → ( 1 / 𝑥 ) ∈ { 1 , - 1 } )
53	45 52	jaoi	⊢ ( ( 𝑥 = 1 ∨ 𝑥 = - 1 ) → ( 1 / 𝑥 ) ∈ { 1 , - 1 } )
54	2 53	syl	⊢ ( 𝑥 ∈ { 1 , - 1 } → ( 1 / 𝑥 ) ∈ { 1 , - 1 } )
55	1 10 18 41 23 54	cnmsubglem	⊢ { 1 , - 1 } ∈ ( SubGrp ‘ 𝑀 )