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 ⊢ 𝑍 = ( ℂfld ↾s ℤ[i] )
Assertion gzrngunit ( 𝐴 ∈ ( Unit ‘ 𝑍 ) ↔ ( 𝐴 ∈ ℤ[i] ∧ ( abs ‘ 𝐴 ) = 1 ) )

Proof

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