Theorem nzrnz 20446

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ≠ wne 2930  ‘cfv 6490  0_gc0g 17357  1_rcur 20114  Ringcrg 20166  NzRingcnzr 20443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-nzr 20444

This theorem is referenced by:  nzrunit  20455  nrhmzr  20468  lringnz  20474  subrgnzr  20525  rrgnz  20635  fidomndrng  20704  uvcf1  21745  lindfind2  21771  nm1  24609  deg1pw  26080  ply1nz  26081  ply1nzb  26082  mon1pid  26113  lgsqrlem4  27314  unitnz  33270  domnprodn0  33306  domnprodeq0  33307  fracfld  33339  drngidl  33463  drngidlhash  33464  drnglidl1ne0  33505  drng0mxidl  33506  qsdrngi  33525  deg1prod  33613  ply1moneq  33618  deg1vr  33622  vr1nz  33623  dimlssid  33738  ply1annnr  33809  algextdeglem4  33826  rtelextdg2lem  33832  zrhnm  34073  idomnnzpownz  42325  idomnnzgmulnz  42326  deg1gprod  42333  deg1pow  42334  domnexpgn0cl  42720  abvexp  42729  fiabv  42733  uvcn0  42739  deg1mhm  43384