Theorem nzrnz 20463

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ‘cfv 6500  0_gc0g 17371  1_rcur 20131  Ringcrg 20183  NzRingcnzr 20460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-nzr 20461

This theorem is referenced by:  nzrunit  20472  nrhmzr  20485  lringnz  20491  subrgnzr  20542  rrgnz  20652  fidomndrng  20721  uvcf1  21762  lindfind2  21788  nm1  24626  deg1pw  26097  ply1nz  26098  ply1nzb  26099  mon1pid  26130  lgsqrlem4  27331  unitnz  33337  domnprodn0  33373  domnprodeq0  33374  fracfld  33406  drngidl  33530  drngidlhash  33531  drnglidl1ne0  33572  drng0mxidl  33573  qsdrngi  33592  deg1prod  33680  ply1moneq  33685  deg1vr  33689  vr1nz  33690  dimlssid  33814  ply1annnr  33885  algextdeglem4  33902  rtelextdg2lem  33908  zrhnm  34149  idomnnzpownz  42506  idomnnzgmulnz  42507  deg1gprod  42514  deg1pow  42515  domnexpgn0cl  42897  abvexp  42906  fiabv  42910  uvcn0  42916  deg1mhm  43561