Theorem nzrnz 20435

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ‘cfv 6499  0_gc0g 17378  1_rcur 20101  Ringcrg 20153  NzRingcnzr 20432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-nzr 20433

This theorem is referenced by:  nzrunit  20444  nrhmzr  20457  lringnz  20463  subrgnzr  20514  rrgnz  20624  fidomndrng  20693  uvcf1  21734  lindfind2  21760  nm1  24588  deg1pw  26059  ply1nz  26060  ply1nzb  26061  mon1pid  26092  lgsqrlem4  27293  unitnz  33206  domnprodn0  33242  fracfld  33274  drngidl  33397  drngidlhash  33398  drnglidl1ne0  33439  drng0mxidl  33440  qsdrngi  33459  ply1moneq  33548  deg1vr  33551  vr1nz  33552  dimlssid  33621  ply1annnr  33686  algextdeglem4  33703  rtelextdg2lem  33709  zrhnm  33950  idomnnzpownz  42113  idomnnzgmulnz  42114  deg1gprod  42121  deg1pow  42122  domnexpgn0cl  42504  abvexp  42513  fiabv  42517  uvcn0  42523  deg1mhm  43182