Theorem nzrnz 20566

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

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143   ≠ wne 2958  ‘cfv 6522  0_gc0g 17469  1_rcur 20232  Ringcrg 20284  NzRingcnzr 20563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6478  df-fv 6530  df-nzr 20564

This theorem is referenced by:  nzrunit  20575  nrhmzr  20588  lringnz  20594  subrgnzr  20645  rrgnz  20755  fidomndrng  20824  uvcf1  21845  lindfind2  21871  nm1  24728  deg1pw  26182  ply1nz  26183  ply1nzb  26184  mon1pid  26215  lgsqrlem4  27414  unitnz  33420  domnprodn0  33460  domnprodeq0  33461  ricnzr1  33473  fracfld  33496  drngidl  33620  drngidlhash  33621  drnglidl1ne0  33664  drng0mxidl  33665  qsdrngi  33684  drnglring  33689  deg1prod  33780  ply1moneq  33785  deg1vr  33789  vr1nz  33790  psrnzr  33810  dimlssid  33930  ply1annnr  34001  algextdeglem4  34018  rtelextdg2lem  34024  zrhnm  34265  idomnnzpownz  42750  idomnnzgmulnz  42751  deg1gprod  42758  deg1pow  42759  domnexpgn0cl  43142  abvexp  43151  fiabv  43155  uvcn0  43161  deg1mhm  43778