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 ⊢M=mulGrpℂfld↾𝑠ℂ∖0
Assertion cnmsgnsubg ⊢1−1∈SubGrp⁡M

Proof

Step Hyp Ref Expression
1 cnmsgnsubg.m ⊢M=mulGrpℂfld↾𝑠ℂ∖0
2 elpri ⊢x∈1−1→x=1∨x=−1
3 id ⊢x=1→x=1
4 ax-1cn ⊢1∈ℂ
5 3 4 eqeltrdi ⊢x=1→x∈ℂ
6 id ⊢x=−1→x=−1
7 neg1cn ⊢−1∈ℂ
8 6 7 eqeltrdi ⊢x=−1→x∈ℂ
9 5 8 jaoi ⊢x=1∨x=−1→x∈ℂ
10 2 9 syl ⊢x∈1−1→x∈ℂ
11 ax-1ne0 ⊢1≠0
12 11 a1i ⊢x=1→1≠0
13 3 12 eqnetrd ⊢x=1→x≠0
14 neg1ne0 ⊢−1≠0
15 14 a1i ⊢x=−1→−1≠0
16 6 15 eqnetrd ⊢x=−1→x≠0
17 13 16 jaoi ⊢x=1∨x=−1→x≠0
18 2 17 syl ⊢x∈1−1→x≠0
19 elpri ⊢y∈1−1→y=1∨y=−1
20 oveq12 ⊢x=1∧y=1→x⁢y=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 ⊢x=1∧y=1→x⁢y∈1−1
26 oveq12 ⊢x=−1∧y=1→x⁢y=-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 ⊢x=−1∧y=1→x⁢y∈1−1
32 oveq12 ⊢x=1∧y=−1→x⁢y=1⁢-1
33 7 mullidi ⊢1⁢-1=−1
34 33 29 eqeltri ⊢1⁢-1∈1−1
35 32 34 eqeltrdi ⊢x=1∧y=−1→x⁢y∈1−1
36 oveq12 ⊢x=−1∧y=−1→x⁢y=-1⁢-1
37 neg1mulneg1e1 ⊢-1⁢-1=1
38 37 23 eqeltri ⊢-1⁢-1∈1−1
39 36 38 eqeltrdi ⊢x=−1∧y=−1→x⁢y∈1−1
40 25 31 35 39 ccase ⊢x=1∨x=−1∧y=1∨y=−1→x⁢y∈1−1
41 2 19 40 syl2an ⊢x∈1−1∧y∈1−1→x⁢y∈1−1
42 oveq2 ⊢x=1→1x=11
43 1div1e1 ⊢11=1
44 43 23 eqeltri ⊢11∈1−1
45 42 44 eqeltrdi ⊢x=1→1x∈1−1
46 oveq2 ⊢x=−1→1x=1−1
47 divneg2 ⊢1∈ℂ∧1∈ℂ∧1≠0→−11=1−1
48 4 4 11 47 mp3an ⊢−11=1−1
49 43 negeqi ⊢−11=−1
50 48 49 eqtr3i ⊢1−1=−1
51 50 29 eqeltri ⊢1−1∈1−1
52 46 51 eqeltrdi ⊢x=−1→1x∈1−1
53 45 52 jaoi ⊢x=1∨x=−1→1x∈1−1
54 2 53 syl ⊢x∈1−1→1x∈1−1
55 1 10 18 41 23 54 cnmsubglem ⊢1−1∈SubGrp⁡M