Theorem nzrnz 20678

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ‘cfv 6533  0_gc0g 17527  1_rcur 20323  Ringcrg 20375  NzRingcnzr 20675

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-nzr 20676

This theorem is used by:  drnglidl1ne0  20682  nzrunit  20688  nrhmzr  20702  lringnz  20708  subrgnzr  20759  rrgnz  20869  fidomndrng  20943  drngidl  21451  isfieldidl  21452  uvcf1  22008  lindfind2  22034  nm1  24896  deg1pw  26349  ply1nz  26350  ply1nzb  26351  mon1pid  26382  lgsqrlem4  27588  unitnz  33681  domnprodn0  33721  domnprodeq0  33722  ricnzr1  33731  fracfld  33752  drngidlhash  33864  drng0mxidl  33881  qsdrngi  33900  drnglring  33905  deg1prod  33996  ply1moneq  34001  deg1vr  34005  vr1nz  34006  psrnzr  34025  dimlssid  34145  ply1annnr  34216  algextdeglem4  34233  rtelextdg2lem  34239  zrhnm  34480  idomnnzpownz  43001  idomnnzgmulnz  43002  deg1gprod  43009  deg1pow  43010  domnexpgn0cl  43408  abvexp  43417  fiabv  43421  uvcn0  43427  deg1mhm  44044  smprngprmrng  49257