Theorem nzrnz 20424

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ‘cfv 6511  0_gc0g 17402  1_rcur 20090  Ringcrg 20142  NzRingcnzr 20421

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-nzr 20422

This theorem is referenced by:  nzrunit  20433  nrhmzr  20446  lringnz  20452  subrgnzr  20503  rrgnz  20613  fidomndrng  20682  uvcf1  21701  lindfind2  21727  nm1  24555  deg1pw  26026  ply1nz  26027  ply1nzb  26028  mon1pid  26059  lgsqrlem4  27260  unitnz  33190  domnprodn0  33226  fracfld  33258  drngidl  33404  drngidlhash  33405  drnglidl1ne0  33446  drng0mxidl  33447  qsdrngi  33466  ply1moneq  33555  deg1vr  33558  vr1nz  33559  dimlssid  33628  ply1annnr  33693  algextdeglem4  33710  rtelextdg2lem  33716  zrhnm  33957  idomnnzpownz  42120  idomnnzgmulnz  42121  deg1gprod  42128  deg1pow  42129  domnexpgn0cl  42511  abvexp  42520  fiabv  42524  uvcn0  42530  deg1mhm  43189