Theorem nzrnz 20612

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ‘cfv 6536  0_gc0g 17487  1_rcur 20258  Ringcrg 20310  NzRingcnzr 20609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-nzr 20610

This theorem is referenced by:  drnglidl1ne0  20616  nzrunit  20622  nrhmzr  20636  lringnz  20642  subrgnzr  20693  rrgnz  20803  fidomndrng  20877  drngidl  21385  isfieldidl  21386  uvcf1  21942  lindfind2  21968  nm1  24824  deg1pw  26278  ply1nz  26279  ply1nzb  26280  mon1pid  26311  lgsqrlem4  27513  unitnz  33558  domnprodn0  33598  domnprodeq0  33599  ricnzr1  33608  fracfld  33629  drngidlhash  33741  drng0mxidl  33758  qsdrngi  33777  drnglring  33782  deg1prod  33873  ply1moneq  33878  deg1vr  33882  vr1nz  33883  psrnzr  33902  dimlssid  34022  ply1annnr  34093  algextdeglem4  34110  rtelextdg2lem  34116  zrhnm  34357  idomnnzpownz  42919  idomnnzgmulnz  42920  deg1gprod  42927  deg1pow  42928  domnexpgn0cl  43311  abvexp  43320  fiabv  43324  uvcn0  43330  deg1mhm  43947  smprngprmrng  49124