Theorem nzrnz 20491

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

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121   ≠ wne 2936  ‘cfv 6489  0_gc0g 17397  1_rcur 20157  Ringcrg 20209  NzRingcnzr 20488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-nzr 20489

This theorem is referenced by:  nzrunit  20500  nrhmzr  20513  lringnz  20519  subrgnzr  20570  rrgnz  20680  fidomndrng  20749  uvcf1  21771  lindfind2  21797  nm1  24654  deg1pw  26108  ply1nz  26109  ply1nzb  26110  mon1pid  26141  lgsqrlem4  27334  unitnz  33324  domnprodn0  33360  domnprodeq0  33361  ricnzr1  33373  fracfld  33396  drngidl  33520  drngidlhash  33521  drnglidl1ne0  33562  drng0mxidl  33563  qsdrngi  33582  drnglring  33587  deg1prod  33678  ply1moneq  33683  deg1vr  33687  vr1nz  33688  psrnzr  33708  dimlssid  33828  ply1annnr  33899  algextdeglem4  33916  rtelextdg2lem  33922  zrhnm  34163  idomnnzpownz  42632  idomnnzgmulnz  42633  deg1gprod  42640  deg1pow  42641  domnexpgn0cl  43024  abvexp  43033  fiabv  43037  uvcn0  43043  deg1mhm  43660