Theorem nzrnz 20400

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 → 1 ≠ 0 )

Proof of Theorem nzrnz

Step	Hyp	Ref	Expression
1		isnzr.o	. . 3 ⊢ 1 = (1r‘𝑅)
2		isnzr.z	. . 3 ⊢ 0 = (0g‘𝑅)
3	1, 2	isnzr 20399	. 2 ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 ≠ 0 ))
4	3	simprbi 496	1 ⊢ (𝑅 ∈ NzRing → 1 ≠ 0 )

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ‘cfv 6482  0_gc0g 17343  1_rcur 20066  Ringcrg 20118  NzRingcnzr 20397

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-nzr 20398

This theorem is referenced by:  nzrunit  20409  nrhmzr  20422  lringnz  20428  subrgnzr  20479  rrgnz  20589  fidomndrng  20658  uvcf1  21699  lindfind2  21725  nm1  24553  deg1pw  26024  ply1nz  26025  ply1nzb  26026  mon1pid  26057  lgsqrlem4  27258  unitnz  33188  domnprodn0  33224  fracfld  33256  drngidl  33379  drngidlhash  33380  drnglidl1ne0  33421  drng0mxidl  33422  qsdrngi  33441  ply1moneq  33531  deg1vr  33534  vr1nz  33535  dimlssid  33615  ply1annnr  33686  algextdeglem4  33703  rtelextdg2lem  33709  zrhnm  33950  idomnnzpownz  42125  idomnnzgmulnz  42126  deg1gprod  42133  deg1pow  42134  domnexpgn0cl  42516  abvexp  42525  fiabv  42529  uvcn0  42535  deg1mhm  43193