This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑀 )