Metamath Proof Explorer


Theorem zringunit

Description: The units of ZZ are the integers with norm 1 , i.e. 1 and -u 1 . (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by AV, 10-Jun-2019)

Ref Expression
Assertion zringunit A Unit ring A A = 1

Proof

Step Hyp Ref Expression
1 zringbas = Base ring
2 eqid Unit ring = Unit ring
3 1 2 unitcl A Unit ring A
4 zsubrg SubRing fld
5 zgz x x i
6 5 ssriv i
7 gzsubrg i SubRing fld
8 eqid fld 𝑠 i = fld 𝑠 i
9 8 subsubrg i SubRing fld SubRing fld 𝑠 i SubRing fld i
10 7 9 ax-mp SubRing fld 𝑠 i SubRing fld i
11 4 6 10 mpbir2an SubRing fld 𝑠 i
12 df-zring ring = fld 𝑠
13 ressabs i SubRing fld i fld 𝑠 i 𝑠 = fld 𝑠
14 7 6 13 mp2an fld 𝑠 i 𝑠 = fld 𝑠
15 12 14 eqtr4i ring = fld 𝑠 i 𝑠
16 eqid Unit fld 𝑠 i = Unit fld 𝑠 i
17 15 16 2 subrguss SubRing fld 𝑠 i Unit ring Unit fld 𝑠 i
18 11 17 ax-mp Unit ring Unit fld 𝑠 i
19 18 sseli A Unit ring A Unit fld 𝑠 i
20 8 gzrngunit A Unit fld 𝑠 i A i A = 1
21 20 simprbi A Unit fld 𝑠 i A = 1
22 19 21 syl A Unit ring A = 1
23 3 22 jca A Unit ring A A = 1
24 zcn A A
25 24 adantr A A = 1 A
26 simpr A A = 1 A = 1
27 ax-1ne0 1 0
28 27 a1i A A = 1 1 0
29 26 28 eqnetrd A A = 1 A 0
30 fveq2 A = 0 A = 0
31 abs0 0 = 0
32 30 31 eqtrdi A = 0 A = 0
33 32 necon3i A 0 A 0
34 29 33 syl A A = 1 A 0
35 eldifsn A 0 A A 0
36 25 34 35 sylanbrc A A = 1 A 0
37 simpl A A = 1 A
38 cnfldinv A A 0 inv r fld A = 1 A
39 25 34 38 syl2anc A A = 1 inv r fld A = 1 A
40 zre A A
41 40 adantr A A = 1 A
42 absresq A A 2 = A 2
43 41 42 syl A A = 1 A 2 = A 2
44 26 oveq1d A A = 1 A 2 = 1 2
45 sq1 1 2 = 1
46 44 45 eqtrdi A A = 1 A 2 = 1
47 25 sqvald A A = 1 A 2 = A A
48 43 46 47 3eqtr3rd A A = 1 A A = 1
49 1cnd A A = 1 1
50 49 25 25 34 divmuld A A = 1 1 A = A A A = 1
51 48 50 mpbird A A = 1 1 A = A
52 39 51 eqtrd A A = 1 inv r fld A = A
53 52 37 eqeltrd A A = 1 inv r fld A
54 cnfldbas = Base fld
55 cnfld0 0 = 0 fld
56 cndrng fld DivRing
57 54 55 56 drngui 0 = Unit fld
58 eqid inv r fld = inv r fld
59 12 57 2 58 subrgunit SubRing fld A Unit ring A 0 A inv r fld A
60 4 59 ax-mp A Unit ring A 0 A inv r fld A
61 36 37 53 60 syl3anbrc A A = 1 A Unit ring
62 23 61 impbii A Unit ring A A = 1