Metamath Proof Explorer

Theorem 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=ℂfld↾𝑠ℤi
Assertion gzrngunit ⊢A∈Unit⁡Z↔A∈ℤi∧A=1

Proof

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