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

Theorem nzrnz 20515
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 20514 . 2 (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 10 ))
43simprbi 496 1 (𝑅 ∈ NzRing → 10 )
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  wne 2940  cfv 6561  0gc0g 17484  1rcur 20178  Ringcrg 20230  NzRingcnzr 20512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-nzr 20513
This theorem is referenced by:  nzrunit  20524  nrhmzr  20537  lringnz  20543  subrgnzr  20594  rrgnz  20704  fidomndrng  20774  uvcf1  21812  lindfind2  21838  nm1  24688  deg1pw  26160  ply1nz  26161  ply1nzb  26162  mon1pid  26193  lgsqrlem4  27393  unitnz  33243  domnprodn0  33279  fracfld  33310  drngidl  33461  drngidlhash  33462  drnglidl1ne0  33503  drng0mxidl  33504  qsdrngi  33523  ply1moneq  33611  deg1vr  33614  dimlssid  33683  ply1annnr  33746  algextdeglem4  33761  rtelextdg2lem  33767  zrhnm  33968  idomnnzpownz  42133  idomnnzgmulnz  42134  deg1gprod  42141  deg1pow  42142  domnexpgn0cl  42533  abvexp  42542  fiabv  42546  uvcn0  42552  deg1mhm  43212
  Copyright terms: Public domain W3C validator