Theorem nzrnz 20780

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146   ≠ wne 2959  ‘cfv 6547  0_gc0g 17625  1_rcur 20422  Ringcrg 20474  NzRingcnzr 20777

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555  df-nzr 20778

This theorem is used by:  drnglidl1ne0  20784  nzrunit  20790  nrhmzr  20804  lringnz  20810  subrgnzr  20861  rrgnz  20971  fidomndrng  21046  drngidl  21554  isfieldidl  21555  uvcf1  22113  lindfind2  22139  nm1  25001  deg1pw  26454  ply1nz  26455  ply1nzb  26456  mon1pid  26487  lgsqrlem4  27691  unitnz  33855  domnprodn0  33895  domnprodeq0  33896  ricnzr1  33905  fracfld  33926  drngidlhash  34039  drng0mxidl  34056  qsdrngi  34075  drnglring  34080  deg1prod  34171  ply1moneq  34176  deg1vr  34180  vr1nz  34181  psrnzr  34200  dimlssid  34320  ply1annnr  34391  algextdeglem4  34408  rtelextdg2lem  34414  zrhnm  34655  idomnnzpownz  43325  idomnnzgmulnz  43326  deg1gprod  43333  deg1pow  43334  domnexpgn0cl  43727  abvexp  43739  fiabv  43743  uvcn0  43749  deg1mhm  44345  smprngprmrng  49578