Theorem nzrnz 20471

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ≠ wne 2929  ‘cfv 6549  0_gc0g 17429  1_rcur 20138  Ringcrg 20190  NzRingcnzr 20468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-nzr 20469

This theorem is referenced by:  nzrunit  20478  nrhmzr  20491  lringnz  20497  subrgnzr  20550  fidomndrng  21283  uvcf1  21748  lindfind2  21774  nm1  24633  deg1pw  26106  ply1nz  26107  ply1nzb  26108  mon1pid  26139  lgsqrlem4  27332  unitnz  33044  domnprodn0  33070  rrgnz  33075  fracfld  33099  drngidl  33250  drngidlhash  33251  drnglidl1ne0  33292  drng0mxidl  33293  qsdrngi  33312  ply1moneq  33397  ply1annnr  33507  algextdeglem4  33521  zrhnm  33703  idomnnzpownz  41737  idomnnzgmulnz  41738  deg1gprod  41745  deg1pow  41746  uvcn0  41912  deg1mhm  42772