This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gzrngunitlem

Description: Lemma for gzrngunit . (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypothesis gzrng.1 ⊢ 𝑍 = ( ℂfld ↾s ℤ[i] )
Assertion gzrngunitlem ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → 1 ≤ ( abs ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 gzrng.1 ⊢ 𝑍 = ( ℂfld ↾s ℤ[i] )
2 sq1 ⊢ ( 1 ↑ 2 ) = 1
3 ax-1ne0 ⊢ 1 ≠ 0
4 gzsubrg ⊢ ℤ[i] ∈ ( SubRing ‘ ℂfld )
5 1 subrgring ⊢ ( ℤ[i] ∈ ( SubRing ‘ ℂfld ) → 𝑍 ∈ Ring )
6 eqid ⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
7 subrgsubg ⊢ ( ℤ[i] ∈ ( SubRing ‘ ℂfld ) → ℤ[i] ∈ ( SubGrp ‘ ℂfld ) )
8 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
9 1 8 subg0 ⊢ ( ℤ[i] ∈ ( SubGrp ‘ ℂfld ) → 0 = ( 0g ‘ 𝑍 ) )
10 4 7 9 mp2b ⊢ 0 = ( 0g ‘ 𝑍 )
11 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
12 1 11 subrg1 ⊢ ( ℤ[i] ∈ ( SubRing ‘ ℂfld ) → 1 = ( 1r ‘ 𝑍 ) )
13 4 12 ax-mp ⊢ 1 = ( 1r ‘ 𝑍 )
14 6 10 13 0unit ⊢ ( 𝑍 ∈ Ring → ( 0 ∈ ( Unit ‘ 𝑍 ) ↔ 1 = 0 ) )
15 4 5 14 mp2b ⊢ ( 0 ∈ ( Unit ‘ 𝑍 ) ↔ 1 = 0 )
16 3 15 nemtbir ⊢ ¬ 0 ∈ ( Unit ‘ 𝑍 )
17 1 subrgbas ⊢ ( ℤ[i] ∈ ( SubRing ‘ ℂfld ) → ℤ[i] = ( Base ‘ 𝑍 ) )
18 4 17 ax-mp ⊢ ℤ[i] = ( Base ‘ 𝑍 )
19 18 6 unitcl ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → 𝐴 ∈ ℤ[i] )
20 gzabssqcl ⊢ ( 𝐴 ∈ ℤ[i] → ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ0 )
21 19 20 syl ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ0 )
22 elnn0 ⊢ ( ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ0 ↔ ( ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ ∨ ( ( abs ‘ 𝐴 ) ↑ 2 ) = 0 ) )
23 21 22 sylib ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ ∨ ( ( abs ‘ 𝐴 ) ↑ 2 ) = 0 ) )
24 23 ord ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( ¬ ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = 0 ) )
25 gzcn ⊢ ( 𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ )
26 19 25 syl ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → 𝐴 ∈ ℂ )
27 26 abscld ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
28 27 recnd ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
29 sqeq0 ⊢ ( ( abs ‘ 𝐴 ) ∈ ℂ → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) = 0 ↔ ( abs ‘ 𝐴 ) = 0 ) )
30 28 29 syl ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) = 0 ↔ ( abs ‘ 𝐴 ) = 0 ) )
31 26 abs00ad ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
32 eleq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ∈ ( Unit ‘ 𝑍 ) ↔ 0 ∈ ( Unit ‘ 𝑍 ) ) )
33 32 biimpcd ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( 𝐴 = 0 → 0 ∈ ( Unit ‘ 𝑍 ) ) )
34 31 33 sylbid ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( ( abs ‘ 𝐴 ) = 0 → 0 ∈ ( Unit ‘ 𝑍 ) ) )
35 30 34 sylbid ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) = 0 → 0 ∈ ( Unit ‘ 𝑍 ) ) )
36 24 35 syld ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( ¬ ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ → 0 ∈ ( Unit ‘ 𝑍 ) ) )
37 16 36 mt3i ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℕ )
38 37 nnge1d ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → 1 ≤ ( ( abs ‘ 𝐴 ) ↑ 2 ) )
39 2 38 eqbrtrid ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( 1 ↑ 2 ) ≤ ( ( abs ‘ 𝐴 ) ↑ 2 ) )
40 26 absge0d ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → 0 ≤ ( abs ‘ 𝐴 ) )
41 1re ⊢ 1 ∈ ℝ
42 0le1 ⊢ 0 ≤ 1
43 le2sq ⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ) → ( 1 ≤ ( abs ‘ 𝐴 ) ↔ ( 1 ↑ 2 ) ≤ ( ( abs ‘ 𝐴 ) ↑ 2 ) ) )
44 41 42 43 mpanl12 ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) → ( 1 ≤ ( abs ‘ 𝐴 ) ↔ ( 1 ↑ 2 ) ≤ ( ( abs ‘ 𝐴 ) ↑ 2 ) ) )
45 27 40 44 syl2anc ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → ( 1 ≤ ( abs ‘ 𝐴 ) ↔ ( 1 ↑ 2 ) ≤ ( ( abs ‘ 𝐴 ) ↑ 2 ) ) )
46 39 45 mpbird ⊢ ( 𝐴 ∈ ( Unit ‘ 𝑍 ) → 1 ≤ ( abs ‘ 𝐴 ) )