Theorem nzrnz 20431

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 20430	. 2 ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 ≠ 0 ))
4	3	simprbi 496	1 ⊢ (𝑅 ∈ NzRing → 1 ≠ 0 )

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ‘cfv 6514  0_gc0g 17409  1_rcur 20097  Ringcrg 20149  NzRingcnzr 20428

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-nzr 20429

This theorem is referenced by:  nzrunit  20440  nrhmzr  20453  lringnz  20459  subrgnzr  20510  rrgnz  20620  fidomndrng  20689  uvcf1  21708  lindfind2  21734  nm1  24562  deg1pw  26033  ply1nz  26034  ply1nzb  26035  mon1pid  26066  lgsqrlem4  27267  unitnz  33197  domnprodn0  33233  fracfld  33265  drngidl  33411  drngidlhash  33412  drnglidl1ne0  33453  drng0mxidl  33454  qsdrngi  33473  ply1moneq  33562  deg1vr  33565  vr1nz  33566  dimlssid  33635  ply1annnr  33700  algextdeglem4  33717  rtelextdg2lem  33723  zrhnm  33964  idomnnzpownz  42127  idomnnzgmulnz  42128  deg1gprod  42135  deg1pow  42136  domnexpgn0cl  42518  abvexp  42527  fiabv  42531  uvcn0  42537  deg1mhm  43196