Theorem nzrnz 20532

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106   ≠ wne 2938  ‘cfv 6563  0_gc0g 17486  1_rcur 20199  Ringcrg 20251  NzRingcnzr 20529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-nzr 20530

This theorem is referenced by:  nzrunit  20541  nrhmzr  20554  lringnz  20560  subrgnzr  20611  rrgnz  20721  fidomndrng  20791  uvcf1  21830  lindfind2  21856  nm1  24704  deg1pw  26175  ply1nz  26176  ply1nzb  26177  mon1pid  26208  lgsqrlem4  27408  unitnz  33229  domnprodn0  33262  fracfld  33290  drngidl  33441  drngidlhash  33442  drnglidl1ne0  33483  drng0mxidl  33484  qsdrngi  33503  ply1moneq  33591  deg1vr  33594  dimlssid  33660  ply1annnr  33711  algextdeglem4  33726  rtelextdg2lem  33732  zrhnm  33930  idomnnzpownz  42114  idomnnzgmulnz  42115  deg1gprod  42122  deg1pow  42123  domnexpgn0cl  42510  abvexp  42519  fiabv  42523  uvcn0  42529  deg1mhm  43189