Theorem elnn0z 12600

Description: Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
elnn0z	⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))

Proof of Theorem elnn0z

Step	Hyp	Ref	Expression
1		elnn0 12502	. 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnnz 12597	. . 3 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
3		eqcom 2776	. . 3 ⊢ (𝑁 = 0 ↔ 0 = 𝑁)
4	2, 3	orbi12i 927	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁))
5		id 23	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
6		0z 12598	. . . . . . 7 ⊢ 0 ∈ ℤ
7		eleq1 2857	. . . . . . 7 ⊢ (0 = 𝑁 → (0 ∈ ℤ ↔ 𝑁 ∈ ℤ))
8	6, 7	mpbii 236	. . . . . 6 ⊢ (0 = 𝑁 → 𝑁 ∈ ℤ)
9	5, 8	jaoi 870	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) → 𝑁 ∈ ℤ)
10		orc 880	. . . . 5 ⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℤ ∨ 0 = 𝑁))
11	9, 10	impbii 212	. . . 4 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ↔ 𝑁 ∈ ℤ)
12	11	anbi1i 635	. . 3 ⊢ (((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
13		ordir 1022	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
14		0re 11206	. . . . 5 ⊢ 0 ∈ ℝ
15		zre 12591	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16		leloe 11292	. . . . 5 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
17	14, 15, 16	sylancr 598	. . . 4 ⊢ (𝑁 ∈ ℤ → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
18	17	pm5.32i 584	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
19	12, 13, 18	3bitr4i 306	. 2 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
20	1, 4, 19	3bitri 300	1 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1567   ∈ wcel 2149   class class class wbr 5110  ℝcr 11095  0cc0 11096   < clt 11239   ≤ cle 11240  ℕcn 12229  ℕ₀cn0 12500  ℤcz 12587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6300  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-nn 12230  df-n0 12501  df-z 12588

This theorem is referenced by:  zle0orge1  12604  nn0zrab  12619  znn0sub  12637  nn0ind  12687  fnn0ind  12691  fznn0  13643  elfz0ubfz0  13656  elfz0fzfz0  13657  fz0fzelfz0  13658  elfzmlbp  13663  difelfzle  13665  difelfznle  13666  elfzo0z  13726  fzofzim  13734  ubmelm1fzo  13788  flge0nn0  13849  zmodcl  13920  modmuladdnn0  13947  modsumfzodifsn  13976  zsqcl2  14170  swrdnnn0nd  14690  swrdswrdlem  14737  swrdswrd  14738  swrdccatin2  14762  pfxccatin12lem2  14764  pfxccatin12lem3  14765  repswswrd  14817  cshwidxmod  14836  nn0abscl  15359  iseralt  15732  binomrisefac  16092  oexpneg  16399  oddnn02np1  16402  evennn02n  16404  nn0ehalf  16432  nn0oddm1d2  16439  divalglem2  16449  divalglem8  16454  divalglem10  16456  divalgb  16458  bitsinv1lem  16495  dfgcd2  16600  algcvga  16633  hashgcdlem  16843  iserodd  16891  pockthlem  16961  4sqlem14  17014  cshwshashlem2  17152  chfacfscmul0  22980  chfacfpmmul0  22984  taylfvallem1  26482  tayl0  26487  basellem3  27209  bcmono  27403  gausslemma2dlem0h  27489  2sqnn0  27564  crctcshwlkn0lem7  30102  crctcshwlkn0  30107  clwlkclwwlklem2a1  30280  clwlkclwwlklem2fv2  30284  clwlkclwwlklem2a  30286  wwlksubclwwlk  30346  0nn0m1nnn0  35499  knoppndvlem2  36987  aks4d1p1p2  42722  aks4d1p1p4  42723  aks4d1p3  42730  aks4d1p7  42735  aks4d1p8  42739  aks4d1p9  42740  aks6d1c1  42768  hashscontpow1  42773  aks6d1c2lem4  42779  aks6d1c2  42782  aks6d1c5lem3  42789  aks6d1c5lem2  42790  sticksstones10  42807  sticksstones12a  42809  aks6d1c6lem3  42824  aks6d1c6lem4  42825  bcled  42830  bcle2d  42831  aks6d1c7lem1  42832  aks6d1c7lem2  42833  unitscyglem5  42851  irrapxlem1  43436  rmynn0  43571  rmyabs  43572  jm2.22  43609  jm2.23  43610  jm2.27a  43619  jm2.27c  43621  dvnprodlem1  46547  wallispilem4  46669  stirlinglem5  46679  elaa2lem  46834  etransclem3  46838  etransclem7  46842  etransclem10  46845  etransclem19  46854  etransclem20  46855  etransclem21  46856  etransclem22  46857  etransclem24  46859  etransclem27  46862  ormkglobd  47478  zm1nn  47923  eluzge0nn0  47933  elfz2z  47936  2elfz2melfz  47939  subsubelfzo0  47948  oexpnegALTV  48326  nn0oALTV  48345  nn0e  48346  gpgusgralem  48705  nn0eo  49188  dig1  49268