gzrngunit

Description: The units on ZZ [ _i ] are the gaussian integers with norm 1 . (Contributed by Mario Carneiro, 4-Dec-2014)

		Ref	Expression
	Hypothesis	gzrng.1	\|- Z = ( CCfld \|`s Z[i] )
	Assertion	gzrngunit	\|- ( A e. ( Unit ` Z ) <-> ( A e. Z[i] /\ ( abs ` A ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		gzrng.1	\|- Z = ( CCfld \|`s Z[i] )
2		gzsubrg	\|- Z[i] e. ( SubRing ` CCfld )
3	1	subrgbas	\|- ( Z[i] e. ( SubRing ` CCfld ) -> Z[i] = ( Base ` Z ) )
4	2 3	ax-mp	\|- Z[i] = ( Base ` Z )
5		eqid	\|- ( Unit ` Z ) = ( Unit ` Z )
6	4 5	unitcl	\|- ( A e. ( Unit ` Z ) -> A e. Z[i] )
7		eqid	\|- ( invr ` CCfld ) = ( invr ` CCfld )
8		eqid	\|- ( invr ` Z ) = ( invr ` Z )
9	1 7 5 8	subrginv	\|- ( ( Z[i] e. ( SubRing ` CCfld ) /\ A e. ( Unit ` Z ) ) -> ( ( invr ` CCfld ) ` A ) = ( ( invr ` Z ) ` A ) )
10	2 9	mpan	\|- ( A e. ( Unit ` Z ) -> ( ( invr ` CCfld ) ` A ) = ( ( invr ` Z ) ` A ) )
11		gzcn	\|- ( A e. Z[i] -> A e. CC )
12	6 11	syl	\|- ( A e. ( Unit ` Z ) -> A e. CC )
13		0red	\|- ( A e. ( Unit ` Z ) -> 0 e. RR )
14		1re	\|- 1 e. RR
15	14	a1i	\|- ( A e. ( Unit ` Z ) -> 1 e. RR )
16	12	abscld	\|- ( A e. ( Unit ` Z ) -> ( abs ` A ) e. RR )
17		0lt1	\|- 0 < 1
18	17	a1i	\|- ( A e. ( Unit ` Z ) -> 0 < 1 )
19	1	gzrngunitlem	\|- ( A e. ( Unit ` Z ) -> 1 <_ ( abs ` A ) )
20	13 15 16 18 19	ltletrd	\|- ( A e. ( Unit ` Z ) -> 0 < ( abs ` A ) )
21	20	gt0ne0d	\|- ( A e. ( Unit ` Z ) -> ( abs ` A ) =/= 0 )
22	12	abs00ad	\|- ( A e. ( Unit ` Z ) -> ( ( abs ` A ) = 0 <-> A = 0 ) )
23	22	necon3bid	\|- ( A e. ( Unit ` Z ) -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) )
24	21 23	mpbid	\|- ( A e. ( Unit ` Z ) -> A =/= 0 )
25		cnfldinv	\|- ( ( A e. CC /\ A =/= 0 ) -> ( ( invr ` CCfld ) ` A ) = ( 1 / A ) )
26	12 24 25	syl2anc	\|- ( A e. ( Unit ` Z ) -> ( ( invr ` CCfld ) ` A ) = ( 1 / A ) )
27	10 26	eqtr3d	\|- ( A e. ( Unit ` Z ) -> ( ( invr ` Z ) ` A ) = ( 1 / A ) )
28	1	subrgring	\|- ( Z[i] e. ( SubRing ` CCfld ) -> Z e. Ring )
29	2 28	ax-mp	\|- Z e. Ring
30	5 8	unitinvcl	\|- ( ( Z e. Ring /\ A e. ( Unit ` Z ) ) -> ( ( invr ` Z ) ` A ) e. ( Unit ` Z ) )
31	29 30	mpan	\|- ( A e. ( Unit ` Z ) -> ( ( invr ` Z ) ` A ) e. ( Unit ` Z ) )
32	27 31	eqeltrrd	\|- ( A e. ( Unit ` Z ) -> ( 1 / A ) e. ( Unit ` Z ) )
33	1	gzrngunitlem	\|- ( ( 1 / A ) e. ( Unit ` Z ) -> 1 <_ ( abs ` ( 1 / A ) ) )
34	32 33	syl	\|- ( A e. ( Unit ` Z ) -> 1 <_ ( abs ` ( 1 / A ) ) )
35		1cnd	\|- ( A e. ( Unit ` Z ) -> 1 e. CC )
36	35 12 24	absdivd	\|- ( A e. ( Unit ` Z ) -> ( abs ` ( 1 / A ) ) = ( ( abs ` 1 ) / ( abs ` A ) ) )
37	34 36	breqtrd	\|- ( A e. ( Unit ` Z ) -> 1 <_ ( ( abs ` 1 ) / ( abs ` A ) ) )
38		1div1e1	\|- ( 1 / 1 ) = 1
39		abs1	\|- ( abs ` 1 ) = 1
40	39	eqcomi	\|- 1 = ( abs ` 1 )
41	40	oveq1i	\|- ( 1 / ( abs ` A ) ) = ( ( abs ` 1 ) / ( abs ` A ) )
42	37 38 41	3brtr4g	\|- ( A e. ( Unit ` Z ) -> ( 1 / 1 ) <_ ( 1 / ( abs ` A ) ) )
43		lerec	\|- ( ( ( ( abs ` A ) e. RR /\ 0 < ( abs ` A ) ) /\ ( 1 e. RR /\ 0 < 1 ) ) -> ( ( abs ` A ) <_ 1 <-> ( 1 / 1 ) <_ ( 1 / ( abs ` A ) ) ) )
44	16 20 15 18 43	syl22anc	\|- ( A e. ( Unit ` Z ) -> ( ( abs ` A ) <_ 1 <-> ( 1 / 1 ) <_ ( 1 / ( abs ` A ) ) ) )
45	42 44	mpbird	\|- ( A e. ( Unit ` Z ) -> ( abs ` A ) <_ 1 )
46		letri3	\|- ( ( ( abs ` A ) e. RR /\ 1 e. RR ) -> ( ( abs ` A ) = 1 <-> ( ( abs ` A ) <_ 1 /\ 1 <_ ( abs ` A ) ) ) )
47	16 14 46	sylancl	\|- ( A e. ( Unit ` Z ) -> ( ( abs ` A ) = 1 <-> ( ( abs ` A ) <_ 1 /\ 1 <_ ( abs ` A ) ) ) )
48	45 19 47	mpbir2and	\|- ( A e. ( Unit ` Z ) -> ( abs ` A ) = 1 )
49	6 48	jca	\|- ( A e. ( Unit ` Z ) -> ( A e. Z[i] /\ ( abs ` A ) = 1 ) )
50	11	adantr	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A e. CC )
51		simpr	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( abs ` A ) = 1 )
52		ax-1ne0	\|- 1 =/= 0
53	52	a1i	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> 1 =/= 0 )
54	51 53	eqnetrd	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( abs ` A ) =/= 0 )
55		fveq2	\|- ( A = 0 -> ( abs ` A ) = ( abs ` 0 ) )
56		abs0	\|- ( abs ` 0 ) = 0
57	55 56	eqtrdi	\|- ( A = 0 -> ( abs ` A ) = 0 )
58	57	necon3i	\|- ( ( abs ` A ) =/= 0 -> A =/= 0 )
59	54 58	syl	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A =/= 0 )
60		eldifsn	\|- ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
61	50 59 60	sylanbrc	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A e. ( CC \ { 0 } ) )
62		simpl	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A e. Z[i] )
63	50 59 25	syl2anc	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( invr ` CCfld ) ` A ) = ( 1 / A ) )
64	50	absvalsqd	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
65	51	oveq1d	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( abs ` A ) ^ 2 ) = ( 1 ^ 2 ) )
66		sq1	\|- ( 1 ^ 2 ) = 1
67	65 66	eqtrdi	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( abs ` A ) ^ 2 ) = 1 )
68	64 67	eqtr3d	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( A x. ( * ` A ) ) = 1 )
69	68	oveq1d	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( A x. ( * ` A ) ) / A ) = ( 1 / A ) )
70	50	cjcld	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( * ` A ) e. CC )
71	70 50 59	divcan3d	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( A x. ( * ` A ) ) / A ) = ( * ` A ) )
72	63 69 71	3eqtr2d	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( invr ` CCfld ) ` A ) = ( * ` A ) )
73		gzcjcl	\|- ( A e. Z[i] -> ( * ` A ) e. Z[i] )
74	73	adantr	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( * ` A ) e. Z[i] )
75	72 74	eqeltrd	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( invr ` CCfld ) ` A ) e. Z[i] )
76		cnfldbas	\|- CC = ( Base ` CCfld )
77		cnfld0	\|- 0 = ( 0g ` CCfld )
78		cndrng	\|- CCfld e. DivRing
79	76 77 78	drngui	\|- ( CC \ { 0 } ) = ( Unit ` CCfld )
80	1 79 5 7	subrgunit	\|- ( Z[i] e. ( SubRing ` CCfld ) -> ( A e. ( Unit ` Z ) <-> ( A e. ( CC \ { 0 } ) /\ A e. Z[i] /\ ( ( invr ` CCfld ) ` A ) e. Z[i] ) ) )
81	2 80	ax-mp	\|- ( A e. ( Unit ` Z ) <-> ( A e. ( CC \ { 0 } ) /\ A e. Z[i] /\ ( ( invr ` CCfld ) ` A ) e. Z[i] ) )
82	61 62 75 81	syl3anbrc	\|- ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A e. ( Unit ` Z ) )
83	49 82	impbii	\|- ( A e. ( Unit ` Z ) <-> ( A e. Z[i] /\ ( abs ` A ) = 1 ) )

Metamath Proof Explorer

Theorem gzrngunit

Proof