MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zringunit Structured version   Visualization version   GIF version

Theorem zringunit 19927
Description: The units of are the integers with norm 1, i.e. 1 and -1. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.)
Assertion
Ref Expression
zringunit (𝐴 ∈ (Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1))

Proof of Theorem zringunit
StepHypRef Expression
1 zringbas 19915 . . . 4 ℤ = (Base‘ℤring)
2 eqid 2692 . . . 4 (Unit‘ℤring) = (Unit‘ℤring)
31, 2unitcl 18748 . . 3 (𝐴 ∈ (Unit‘ℤring) → 𝐴 ∈ ℤ)
4 zsubrg 19890 . . . . . . 7 ℤ ∈ (SubRing‘ℂfld)
5 zgz 15728 . . . . . . . 8 (𝑥 ∈ ℤ → 𝑥 ∈ ℤ[i])
65ssriv 3681 . . . . . . 7 ℤ ⊆ ℤ[i]
7 gzsubrg 19891 . . . . . . . 8 ℤ[i] ∈ (SubRing‘ℂfld)
8 eqid 2692 . . . . . . . . 9 (ℂflds ℤ[i]) = (ℂflds ℤ[i])
98subsubrg 18897 . . . . . . . 8 (ℤ[i] ∈ (SubRing‘ℂfld) → (ℤ ∈ (SubRing‘(ℂflds ℤ[i])) ↔ (ℤ ∈ (SubRing‘ℂfld) ∧ ℤ ⊆ ℤ[i])))
107, 9ax-mp 5 . . . . . . 7 (ℤ ∈ (SubRing‘(ℂflds ℤ[i])) ↔ (ℤ ∈ (SubRing‘ℂfld) ∧ ℤ ⊆ ℤ[i]))
114, 6, 10mpbir2an 993 . . . . . 6 ℤ ∈ (SubRing‘(ℂflds ℤ[i]))
12 df-zring 19910 . . . . . . . 8 ring = (ℂflds ℤ)
13 ressabs 16030 . . . . . . . . 9 ((ℤ[i] ∈ (SubRing‘ℂfld) ∧ ℤ ⊆ ℤ[i]) → ((ℂflds ℤ[i]) ↾s ℤ) = (ℂflds ℤ))
147, 6, 13mp2an 710 . . . . . . . 8 ((ℂflds ℤ[i]) ↾s ℤ) = (ℂflds ℤ)
1512, 14eqtr4i 2717 . . . . . . 7 ring = ((ℂflds ℤ[i]) ↾s ℤ)
16 eqid 2692 . . . . . . 7 (Unit‘(ℂflds ℤ[i])) = (Unit‘(ℂflds ℤ[i]))
1715, 16, 2subrguss 18886 . . . . . 6 (ℤ ∈ (SubRing‘(ℂflds ℤ[i])) → (Unit‘ℤring) ⊆ (Unit‘(ℂflds ℤ[i])))
1811, 17ax-mp 5 . . . . 5 (Unit‘ℤring) ⊆ (Unit‘(ℂflds ℤ[i]))
1918sseli 3673 . . . 4 (𝐴 ∈ (Unit‘ℤring) → 𝐴 ∈ (Unit‘(ℂflds ℤ[i])))
208gzrngunit 19903 . . . . 5 (𝐴 ∈ (Unit‘(ℂflds ℤ[i])) ↔ (𝐴 ∈ ℤ[i] ∧ (abs‘𝐴) = 1))
2120simprbi 483 . . . 4 (𝐴 ∈ (Unit‘(ℂflds ℤ[i])) → (abs‘𝐴) = 1)
2219, 21syl 17 . . 3 (𝐴 ∈ (Unit‘ℤring) → (abs‘𝐴) = 1)
233, 22jca 555 . 2 (𝐴 ∈ (Unit‘ℤring) → (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1))
24 zcn 11463 . . . . 5 (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
2524adantr 472 . . . 4 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → 𝐴 ∈ ℂ)
26 simpr 479 . . . . . 6 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → (abs‘𝐴) = 1)
27 ax-1ne0 10086 . . . . . . 7 1 ≠ 0
2827a1i 11 . . . . . 6 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → 1 ≠ 0)
2926, 28eqnetrd 2931 . . . . 5 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → (abs‘𝐴) ≠ 0)
30 fveq2 6272 . . . . . . 7 (𝐴 = 0 → (abs‘𝐴) = (abs‘0))
31 abs0 14113 . . . . . . 7 (abs‘0) = 0
3230, 31syl6eq 2742 . . . . . 6 (𝐴 = 0 → (abs‘𝐴) = 0)
3332necon3i 2896 . . . . 5 ((abs‘𝐴) ≠ 0 → 𝐴 ≠ 0)
3429, 33syl 17 . . . 4 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → 𝐴 ≠ 0)
35 eldifsn 4393 . . . 4 (𝐴 ∈ (ℂ ∖ {0}) ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
3625, 34, 35sylanbrc 701 . . 3 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → 𝐴 ∈ (ℂ ∖ {0}))
37 simpl 474 . . 3 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → 𝐴 ∈ ℤ)
38 cnfldinv 19868 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((invr‘ℂfld)‘𝐴) = (1 / 𝐴))
3925, 34, 38syl2anc 696 . . . . 5 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → ((invr‘ℂfld)‘𝐴) = (1 / 𝐴))
40 zre 11462 . . . . . . . . 9 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
4140adantr 472 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → 𝐴 ∈ ℝ)
42 absresq 14130 . . . . . . . 8 (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2))
4341, 42syl 17 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → ((abs‘𝐴)↑2) = (𝐴↑2))
4426oveq1d 6748 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → ((abs‘𝐴)↑2) = (1↑2))
45 sq1 13041 . . . . . . . 8 (1↑2) = 1
4644, 45syl6eq 2742 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → ((abs‘𝐴)↑2) = 1)
4725sqvald 13088 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → (𝐴↑2) = (𝐴 · 𝐴))
4843, 46, 473eqtr3rd 2735 . . . . . 6 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → (𝐴 · 𝐴) = 1)
49 1cnd 10137 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → 1 ∈ ℂ)
5049, 25, 25, 34divmuld 10904 . . . . . 6 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → ((1 / 𝐴) = 𝐴 ↔ (𝐴 · 𝐴) = 1))
5148, 50mpbird 247 . . . . 5 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → (1 / 𝐴) = 𝐴)
5239, 51eqtrd 2726 . . . 4 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → ((invr‘ℂfld)‘𝐴) = 𝐴)
5352, 37eqeltrd 2771 . . 3 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → ((invr‘ℂfld)‘𝐴) ∈ ℤ)
54 cnfldbas 19841 . . . . . 6 ℂ = (Base‘ℂfld)
55 cnfld0 19861 . . . . . 6 0 = (0g‘ℂfld)
56 cndrng 19866 . . . . . 6 fld ∈ DivRing
5754, 55, 56drngui 18844 . . . . 5 (ℂ ∖ {0}) = (Unit‘ℂfld)
58 eqid 2692 . . . . 5 (invr‘ℂfld) = (invr‘ℂfld)
5912, 57, 2, 58subrgunit 18889 . . . 4 (ℤ ∈ (SubRing‘ℂfld) → (𝐴 ∈ (Unit‘ℤring) ↔ (𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐴 ∈ ℤ ∧ ((invr‘ℂfld)‘𝐴) ∈ ℤ)))
604, 59ax-mp 5 . . 3 (𝐴 ∈ (Unit‘ℤring) ↔ (𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐴 ∈ ℤ ∧ ((invr‘ℂfld)‘𝐴) ∈ ℤ))
6136, 37, 53, 60syl3anbrc 1319 . 2 ((𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1) → 𝐴 ∈ (Unit‘ℤring))
6223, 61impbii 199 1 (𝐴 ∈ (Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1072   = wceq 1564  wcel 2071  wne 2864  cdif 3645  wss 3648  {csn 4253  cfv 5969  (class class class)co 6733  cc 10015  cr 10016  0cc0 10017  1c1 10018   · cmul 10022   / cdiv 10765  2c2 11151  cz 11458  cexp 12943  abscabs 14062  ℤ[i]cgz 15724  s cress 15949  Unitcui 18728  invrcinvr 18760  SubRingcsubrg 18867  fldccnfld 19837  ringzring 19909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-rep 4847  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034  ax-cnex 10073  ax-resscn 10074  ax-1cn 10075  ax-icn 10076  ax-addcl 10077  ax-addrcl 10078  ax-mulcl 10079  ax-mulrcl 10080  ax-mulcom 10081  ax-addass 10082  ax-mulass 10083  ax-distr 10084  ax-i2m1 10085  ax-1ne0 10086  ax-1rid 10087  ax-rnegex 10088  ax-rrecex 10089  ax-cnre 10090  ax-pre-lttri 10091  ax-pre-lttrn 10092  ax-pre-ltadd 10093  ax-pre-mulgt0 10094  ax-pre-sup 10095  ax-addf 10096  ax-mulf 10097
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-nel 2968  df-ral 2987  df-rex 2988  df-reu 2989  df-rmo 2990  df-rab 2991  df-v 3274  df-sbc 3510  df-csb 3608  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-pss 3664  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-tp 4258  df-op 4260  df-uni 4513  df-int 4552  df-iun 4598  df-br 4729  df-opab 4789  df-mpt 4806  df-tr 4829  df-id 5096  df-eprel 5101  df-po 5107  df-so 5108  df-fr 5145  df-we 5147  df-xp 5192  df-rel 5193  df-cnv 5194  df-co 5195  df-dm 5196  df-rn 5197  df-res 5198  df-ima 5199  df-pred 5761  df-ord 5807  df-on 5808  df-lim 5809  df-suc 5810  df-iota 5932  df-fun 5971  df-fn 5972  df-f 5973  df-f1 5974  df-fo 5975  df-f1o 5976  df-fv 5977  df-riota 6694  df-ov 6736  df-oprab 6737  df-mpt2 6738  df-om 7151  df-1st 7253  df-2nd 7254  df-tpos 7440  df-wrecs 7495  df-recs 7556  df-rdg 7594  df-1o 7648  df-oadd 7652  df-er 7830  df-en 8041  df-dom 8042  df-sdom 8043  df-fin 8044  df-sup 8432  df-pnf 10157  df-mnf 10158  df-xr 10159  df-ltxr 10160  df-le 10161  df-sub 10349  df-neg 10350  df-div 10766  df-nn 11102  df-2 11160  df-3 11161  df-4 11162  df-5 11163  df-6 11164  df-7 11165  df-8 11166  df-9 11167  df-n0 11374  df-z 11459  df-dec 11575  df-uz 11769  df-rp 11915  df-fz 12409  df-seq 12885  df-exp 12944  df-cj 13927  df-re 13928  df-im 13929  df-sqrt 14063  df-abs 14064  df-gz 15725  df-struct 15950  df-ndx 15951  df-slot 15952  df-base 15954  df-sets 15955  df-ress 15956  df-plusg 16045  df-mulr 16046  df-starv 16047  df-tset 16051  df-ple 16052  df-ds 16055  df-unif 16056  df-0g 16193  df-mgm 17332  df-sgrp 17374  df-mnd 17385  df-grp 17515  df-minusg 17516  df-subg 17681  df-cmn 18284  df-mgp 18579  df-ur 18591  df-ring 18638  df-cring 18639  df-oppr 18712  df-dvdsr 18730  df-unit 18731  df-invr 18761  df-dvr 18772  df-drng 18840  df-subrg 18869  df-cnfld 19838  df-zring 19910
This theorem is referenced by:  zringndrg  19929  prmirredlem  19932  qqhval2lem  30223
  Copyright terms: Public domain W3C validator