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={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
Assertion	cnmsgnsubg	$$⊢\left\{1,-1\right\}\in \mathrm{SubGrp}\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmsgnsubg.m	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
2		elpri	$$⊢x\in \left\{1,-1\right\}\to \left(x=1\vee x=-1\right)$$
3		id	$$⊢x=1\to x=1$$
4		ax-1cn	$$⊢1\in ℂ$$
5	3 4	eqeltrdi	$$⊢x=1\to x\in ℂ$$
6		id	$$⊢x=-1\to x=-1$$
7		neg1cn	$$⊢-1\in ℂ$$
8	6 7	eqeltrdi	$$⊢x=-1\to x\in ℂ$$
9	5 8	jaoi	$$⊢\left(x=1\vee x=-1\right)\to x\in ℂ$$
10	2 9	syl	$$⊢x\in \left\{1,-1\right\}\to x\in ℂ$$
11		ax-1ne0	$$⊢1\ne 0$$
12	11	a1i	$$⊢x=1\to 1\ne 0$$
13	3 12	eqnetrd	$$⊢x=1\to x\ne 0$$
14		neg1ne0	$$⊢-1\ne 0$$
15	14	a1i	$$⊢x=-1\to -1\ne 0$$
16	6 15	eqnetrd	$$⊢x=-1\to x\ne 0$$
17	13 16	jaoi	$$⊢\left(x=1\vee x=-1\right)\to x\ne 0$$
18	2 17	syl	$$⊢x\in \left\{1,-1\right\}\to x\ne 0$$
19		elpri	$$⊢y\in \left\{1,-1\right\}\to \left(y=1\vee y=-1\right)$$
20		oveq12	$$⊢\left(x=1\wedge y=1\right)\to xy=1\cdot 1$$
21	4	mulid1i	$$⊢1\cdot 1=1$$
22		1ex	$$⊢1\in \mathrm{V}$$
23	22	prid1	$$⊢1\in \left\{1,-1\right\}$$
24	21 23	eqeltri	$$⊢1\cdot 1\in \left\{1,-1\right\}$$
25	20 24	eqeltrdi	$$⊢\left(x=1\wedge y=1\right)\to xy\in \left\{1,-1\right\}$$
26		oveq12	$$⊢\left(x=-1\wedge y=1\right)\to xy=-1\cdot 1$$
27	7	mulid1i	$$⊢-1\cdot 1=-1$$
28		negex	$$⊢-1\in \mathrm{V}$$
29	28	prid2	$$⊢-1\in \left\{1,-1\right\}$$
30	27 29	eqeltri	$$⊢-1\cdot 1\in \left\{1,-1\right\}$$
31	26 30	eqeltrdi	$$⊢\left(x=-1\wedge y=1\right)\to xy\in \left\{1,-1\right\}$$
32		oveq12	$$⊢\left(x=1\wedge y=-1\right)\to xy=1-1$$
33	7	mulid2i	$$⊢1-1=-1$$
34	33 29	eqeltri	$$⊢1-1\in \left\{1,-1\right\}$$
35	32 34	eqeltrdi	$$⊢\left(x=1\wedge y=-1\right)\to xy\in \left\{1,-1\right\}$$
36		oveq12	$$⊢\left(x=-1\wedge y=-1\right)\to xy=-1-1$$
37		neg1mulneg1e1	$$⊢-1-1=1$$
38	37 23	eqeltri	$$⊢-1-1\in \left\{1,-1\right\}$$
39	36 38	eqeltrdi	$$⊢\left(x=-1\wedge y=-1\right)\to xy\in \left\{1,-1\right\}$$
40	25 31 35 39	ccase	$$⊢\left(\left(x=1\vee x=-1\right)\wedge \left(y=1\vee y=-1\right)\right)\to xy\in \left\{1,-1\right\}$$
41	2 19 40	syl2an	$$⊢\left(x\in \left\{1,-1\right\}\wedge y\in \left\{1,-1\right\}\right)\to xy\in \left\{1,-1\right\}$$
42		oveq2	$$⊢x=1\to \frac{1}{x}=\frac{1}{1}$$
43		1div1e1	$$⊢\frac{1}{1}=1$$
44	43 23	eqeltri	$$⊢\frac{1}{1}\in \left\{1,-1\right\}$$
45	42 44	eqeltrdi	$$⊢x=1\to \frac{1}{x}\in \left\{1,-1\right\}$$
46		oveq2	$$⊢x=-1\to \frac{1}{x}=\frac{1}{-1}$$
47		divneg2	$$⊢\left(1\in ℂ\wedge 1\in ℂ\wedge 1\ne 0\right)\to -\frac{1}{1}=\frac{1}{-1}$$
48	4 4 11 47	mp3an	$$⊢-\frac{1}{1}=\frac{1}{-1}$$
49	43	negeqi	$$⊢-\frac{1}{1}=-1$$
50	48 49	eqtr3i	$$⊢\frac{1}{-1}=-1$$
51	50 29	eqeltri	$$⊢\frac{1}{-1}\in \left\{1,-1\right\}$$
52	46 51	eqeltrdi	$$⊢x=-1\to \frac{1}{x}\in \left\{1,-1\right\}$$
53	45 52	jaoi	$$⊢\left(x=1\vee x=-1\right)\to \frac{1}{x}\in \left\{1,-1\right\}$$
54	2 53	syl	$$⊢x\in \left\{1,-1\right\}\to \frac{1}{x}\in \left\{1,-1\right\}$$
55	1 10 18 41 23 54	cnmsubglem	$$⊢\left\{1,-1\right\}\in \mathrm{SubGrp}\left(M\right)$$