Theorem nzrnz 20450

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ≠ wne 2932  ‘cfv 6492  0_gc0g 17361  1_rcur 20118  Ringcrg 20170  NzRingcnzr 20447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-nzr 20448

This theorem is referenced by:  nzrunit  20459  nrhmzr  20472  lringnz  20478  subrgnzr  20529  rrgnz  20639  fidomndrng  20708  uvcf1  21749  lindfind2  21775  nm1  24613  deg1pw  26084  ply1nz  26085  ply1nzb  26086  mon1pid  26117  lgsqrlem4  27318  unitnz  33323  domnprodn0  33359  domnprodeq0  33360  fracfld  33392  drngidl  33516  drngidlhash  33517  drnglidl1ne0  33558  drng0mxidl  33559  qsdrngi  33578  deg1prod  33666  ply1moneq  33671  deg1vr  33675  vr1nz  33676  dimlssid  33791  ply1annnr  33862  algextdeglem4  33879  rtelextdg2lem  33885  zrhnm  34126  idomnnzpownz  42408  idomnnzgmulnz  42409  deg1gprod  42416  deg1pow  42417  domnexpgn0cl  42799  abvexp  42808  fiabv  42812  uvcn0  42818  deg1mhm  43463