Theorem elnn0z 12606

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 12508	. 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnnz 12603	. . 3 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
3		eqcom 2743	. . 3 ⊢ (𝑁 = 0 ↔ 0 = 𝑁)
4	2, 3	orbi12i 914	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁))
5		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
6		0z 12604	. . . . . . 7 ⊢ 0 ∈ ℤ
7		eleq1 2823	. . . . . . 7 ⊢ (0 = 𝑁 → (0 ∈ ℤ ↔ 𝑁 ∈ ℤ))
8	6, 7	mpbii 233	. . . . . 6 ⊢ (0 = 𝑁 → 𝑁 ∈ ℤ)
9	5, 8	jaoi 857	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) → 𝑁 ∈ ℤ)
10		orc 867	. . . . 5 ⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℤ ∨ 0 = 𝑁))
11	9, 10	impbii 209	. . . 4 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ↔ 𝑁 ∈ ℤ)
12	11	anbi1i 624	. . 3 ⊢ (((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
13		ordir 1008	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
14		0re 11242	. . . . 5 ⊢ 0 ∈ ℝ
15		zre 12597	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16		leloe 11326	. . . . 5 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
17	14, 15, 16	sylancr 587	. . . 4 ⊢ (𝑁 ∈ ℤ → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
18	17	pm5.32i 574	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
19	12, 13, 18	3bitr4i 303	. 2 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
20	1, 4, 19	3bitri 297	1 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133  0cc0 11134   < clt 11274   ≤ cle 11275  ℕcn 12245  ℕ₀cn0 12506  ℤcz 12593

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  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 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-n0 12507  df-z 12594

This theorem is referenced by:  zle0orge1  12610  nn0zrab  12626  znn0sub  12644  nn0ind  12693  fnn0ind  12697  fznn0  13641  elfz0ubfz0  13654  elfz0fzfz0  13655  fz0fzelfz0  13656  elfzmlbp  13661  difelfzle  13663  difelfznle  13664  elfzo0z  13723  fzofzim  13731  ubmelm1fzo  13784  flge0nn0  13842  zmodcl  13913  modmuladdnn0  13938  modsumfzodifsn  13967  zsqcl2  14161  swrdnnn0nd  14679  swrdswrdlem  14727  swrdswrd  14728  swrdccatin2  14752  pfxccatin12lem2  14754  pfxccatin12lem3  14755  repswswrd  14807  cshwidxmod  14826  nn0abscl  15336  iseralt  15706  binomrisefac  16063  oexpneg  16369  oddnn02np1  16372  evennn02n  16374  nn0ehalf  16402  nn0oddm1d2  16409  divalglem2  16419  divalglem8  16424  divalglem10  16426  divalgb  16428  bitsinv1lem  16465  dfgcd2  16570  algcvga  16603  hashgcdlem  16812  iserodd  16860  pockthlem  16930  4sqlem14  16983  cshwshashlem2  17121  chfacfscmul0  22801  chfacfpmmul0  22805  taylfvallem1  26321  tayl0  26326  basellem3  27050  bcmono  27245  gausslemma2dlem0h  27331  2sqnn0  27406  crctcshwlkn0lem7  29803  crctcshwlkn0  29808  clwlkclwwlklem2a1  29978  clwlkclwwlklem2fv2  29982  clwlkclwwlklem2a  29984  wwlksubclwwlk  30044  0nn0m1nnn0  35140  knoppndvlem2  36536  aks4d1p1p2  42088  aks4d1p1p4  42089  aks4d1p3  42096  aks4d1p7  42101  aks4d1p8  42105  aks4d1p9  42106  aks6d1c1  42134  hashscontpow1  42139  aks6d1c2lem4  42145  aks6d1c2  42148  aks6d1c5lem3  42155  aks6d1c5lem2  42156  sticksstones10  42173  sticksstones12a  42175  aks6d1c6lem3  42190  aks6d1c6lem4  42191  bcled  42196  bcle2d  42197  aks6d1c7lem1  42198  aks6d1c7lem2  42199  unitscyglem5  42217  irrapxlem1  42820  rmynn0  42956  rmyabs  42957  jm2.22  42994  jm2.23  42995  jm2.27a  43004  jm2.27c  43006  dvnprodlem1  45955  wallispilem4  46077  stirlinglem5  46087  elaa2lem  46242  etransclem3  46246  etransclem7  46250  etransclem10  46253  etransclem19  46262  etransclem20  46263  etransclem21  46264  etransclem22  46265  etransclem24  46267  etransclem27  46270  ormkglobd  46884  zm1nn  47311  eluzge0nn0  47321  elfz2z  47324  2elfz2melfz  47327  subsubelfzo0  47335  oexpnegALTV  47671  nn0oALTV  47690  nn0e  47691  gpgusgralem  48040  nn0eo  48488  dig1  48568