Theorem nzrnz 20515

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ‘cfv 6561  0_gc0g 17484  1_rcur 20178  Ringcrg 20230  NzRingcnzr 20512

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-nzr 20513

This theorem is referenced by:  nzrunit  20524  nrhmzr  20537  lringnz  20543  subrgnzr  20594  rrgnz  20704  fidomndrng  20774  uvcf1  21812  lindfind2  21838  nm1  24688  deg1pw  26160  ply1nz  26161  ply1nzb  26162  mon1pid  26193  lgsqrlem4  27393  unitnz  33243  domnprodn0  33279  fracfld  33310  drngidl  33461  drngidlhash  33462  drnglidl1ne0  33503  drng0mxidl  33504  qsdrngi  33523  ply1moneq  33611  deg1vr  33614  dimlssid  33683  ply1annnr  33746  algextdeglem4  33761  rtelextdg2lem  33767  zrhnm  33968  idomnnzpownz  42133  idomnnzgmulnz  42134  deg1gprod  42141  deg1pow  42142  domnexpgn0cl  42533  abvexp  42542  fiabv  42546  uvcn0  42552  deg1mhm  43212