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  33180  domnprodn0  33216  fracfld  33248  drngidl  33371  drngidlhash  33372  drnglidl1ne0  33413  drng0mxidl  33414  qsdrngi  33433  ply1moneq  33523  deg1vr  33526  vr1nz  33527  dimlssid  33605  ply1annnr  33676  algextdeglem4  33693  rtelextdg2lem  33699  zrhnm  33940  idomnnzpownz  42115  idomnnzgmulnz  42116  deg1gprod  42123  deg1pow  42124  domnexpgn0cl  42506  abvexp  42515  fiabv  42519  uvcn0  42525  deg1mhm  43183