Theorem elnn0z 12628

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 12530	. 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnnz 12625	. . 3 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
3		eqcom 2743	. . 3 ⊢ (𝑁 = 0 ↔ 0 = 𝑁)
4	2, 3	orbi12i 914	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁))
5		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
6		0z 12626	. . . . . . 7 ⊢ 0 ∈ ℤ
7		eleq1 2828	. . . . . . 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 11264	. . . . 5 ⊢ 0 ∈ ℝ
15		zre 12619	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16		leloe 11348	. . . . 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 1539   ∈ wcel 2107   class class class wbr 5142  ℝcr 11155  0cc0 11156   < clt 11296   ≤ cle 11297  ℕcn 12267  ℕ₀cn0 12528  ℤcz 12615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-er 8746  df-en 8987  df-dom 8988  df-sdom 8989  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-n0 12529  df-z 12616

This theorem is referenced by:  zle0orge1  12632  nn0zrab  12648  znn0sub  12666  nn0ind  12715  fnn0ind  12719  fznn0  13660  elfz0ubfz0  13673  elfz0fzfz0  13674  fz0fzelfz0  13675  elfzmlbp  13680  difelfzle  13682  difelfznle  13683  elfzo0z  13742  fzofzim  13750  ubmelm1fzo  13803  flge0nn0  13861  zmodcl  13932  modmuladdnn0  13957  modsumfzodifsn  13986  zsqcl2  14179  swrdnnn0nd  14695  swrdswrdlem  14743  swrdswrd  14744  swrdccatin2  14768  pfxccatin12lem2  14770  pfxccatin12lem3  14771  repswswrd  14823  cshwidxmod  14842  nn0abscl  15352  iseralt  15722  binomrisefac  16079  oexpneg  16383  oddnn02np1  16386  evennn02n  16388  nn0ehalf  16416  nn0oddm1d2  16423  divalglem2  16433  divalglem8  16438  divalglem10  16440  divalgb  16442  bitsinv1lem  16479  dfgcd2  16584  algcvga  16617  hashgcdlem  16826  iserodd  16874  pockthlem  16944  4sqlem14  16997  cshwshashlem2  17135  chfacfscmul0  22865  chfacfpmmul0  22869  taylfvallem1  26399  tayl0  26404  basellem3  27127  bcmono  27322  gausslemma2dlem0h  27408  2sqnn0  27483  crctcshwlkn0lem7  29837  crctcshwlkn0  29842  clwlkclwwlklem2a1  30012  clwlkclwwlklem2fv2  30016  clwlkclwwlklem2a  30018  wwlksubclwwlk  30078  0nn0m1nnn0  35119  knoppndvlem2  36515  aks4d1p1p2  42072  aks4d1p1p4  42073  aks4d1p3  42080  aks4d1p7  42085  aks4d1p8  42089  aks4d1p9  42090  aks6d1c1  42118  hashscontpow1  42123  aks6d1c2lem4  42129  aks6d1c2  42132  aks6d1c5lem3  42139  aks6d1c5lem2  42140  sticksstones10  42157  sticksstones12a  42159  aks6d1c6lem3  42174  aks6d1c6lem4  42175  bcled  42180  bcle2d  42181  aks6d1c7lem1  42182  aks6d1c7lem2  42183  unitscyglem5  42201  irrapxlem1  42838  rmynn0  42974  rmyabs  42975  jm2.22  43012  jm2.23  43013  jm2.27a  43022  jm2.27c  43024  dvnprodlem1  45966  wallispilem4  46088  stirlinglem5  46098  elaa2lem  46253  etransclem3  46257  etransclem7  46261  etransclem10  46264  etransclem19  46273  etransclem20  46274  etransclem21  46275  etransclem22  46276  etransclem24  46278  etransclem27  46281  ormkglobd  46895  zm1nn  47319  eluzge0nn0  47329  elfz2z  47332  2elfz2melfz  47335  subsubelfzo0  47343  oexpnegALTV  47669  nn0oALTV  47688  nn0e  47689  gpgusgralem  48016  nn0eo  48454  dig1  48534