Theorem nzrnz 20664

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ‘cfv 6540  0_gc0g 17516  1_rcur 20309  Ringcrg 20361  NzRingcnzr 20661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-nzr 20662

This theorem is used by:  drnglidl1ne0  20668  nzrunit  20674  nrhmzr  20688  lringnz  20694  subrgnzr  20745  rrgnz  20855  fidomndrng  20929  drngidl  21437  isfieldidl  21438  uvcf1  21994  lindfind2  22020  nm1  24877  deg1pw  26331  ply1nz  26332  ply1nzb  26333  mon1pid  26364  lgsqrlem4  27566  unitnz  33624  domnprodn0  33664  domnprodeq0  33665  ricnzr1  33674  fracfld  33695  drngidlhash  33807  drng0mxidl  33824  qsdrngi  33843  drnglring  33848  deg1prod  33939  ply1moneq  33944  deg1vr  33948  vr1nz  33949  psrnzr  33968  dimlssid  34088  ply1annnr  34159  algextdeglem4  34176  rtelextdg2lem  34182  zrhnm  34423  idomnnzpownz  42959  idomnnzgmulnz  42960  deg1gprod  42967  deg1pow  42968  domnexpgn0cl  43351  abvexp  43360  fiabv  43364  uvcn0  43370  deg1mhm  43987  smprngprmrng  49163