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

Theorem nzrnz 20029
Description: One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
Hypotheses
Ref Expression
isnzr.o 1 = (1r𝑅)
isnzr.z 0 = (0g𝑅)
Assertion
Ref Expression
nzrnz (𝑅 ∈ NzRing → 10 )

Proof of Theorem nzrnz
StepHypRef Expression
1 isnzr.o . . 3 1 = (1r𝑅)
2 isnzr.z . . 3 0 = (0g𝑅)
31, 2isnzr 20028 . 2 (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 10 ))
43simprbi 500 1 (𝑅 ∈ NzRing → 10 )
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112  wne 2990  cfv 6328  0gc0g 16708  1rcur 19247  Ringcrg 19293  NzRingcnzr 20026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-nzr 20027
This theorem is referenced by:  nzrunit  20036  subrgnzr  20037  fidomndrng  20076  uvcf1  20484  lindfind2  20510  nm1  23276  deg1pw  24724  ply1nz  24725  ply1nzb  24726  lgsqrlem4  25936  zrhnm  31318  uvcn0  39442  mon1pid  40136  deg1mhm  40138  nrhmzr  44484
  Copyright terms: Public domain W3C validator