Theorem nzrnz 20765

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 20764	. 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 2956  ‘cfv 6538  0_gc0g 17610  1_rcur 20407  Ringcrg 20459  NzRingcnzr 20762

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  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 6494  df-fv 6546  df-nzr 20763

This theorem is used by:  drnglidl1ne0  20769  nzrunit  20775  nrhmzr  20789  lringnz  20795  subrgnzr  20846  rrgnz  20956  fidomndrng  21031  drngidl  21539  isfieldidl  21540  uvcf1  22098  lindfind2  22124  nm1  24986  deg1pw  26439  ply1nz  26440  ply1nzb  26441  mon1pid  26472  lgsqrlem4  27676  unitnz  33799  domnprodn0  33839  domnprodeq0  33840  ricnzr1  33849  fracfld  33870  drngidlhash  33983  drng0mxidl  34000  qsdrngi  34019  drnglring  34024  deg1prod  34115  ply1moneq  34120  deg1vr  34124  vr1nz  34125  psrnzr  34144  dimlssid  34264  ply1annnr  34335  algextdeglem4  34352  rtelextdg2lem  34358  zrhnm  34599  idomnnzpownz  43182  idomnnzgmulnz  43183  deg1gprod  43190  deg1pow  43191  domnexpgn0cl  43584  abvexp  43596  fiabv  43600  uvcn0  43606  deg1mhm  44201  smprngprmrng  49435