Theorem elnn0z 12624

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 12526	. 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnnz 12621	. . 3 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
3		eqcom 2742	. . 3 ⊢ (𝑁 = 0 ↔ 0 = 𝑁)
4	2, 3	orbi12i 914	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁))
5		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
6		0z 12622	. . . . . . 7 ⊢ 0 ∈ ℤ
7		eleq1 2827	. . . . . . 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 11261	. . . . 5 ⊢ 0 ∈ ℝ
15		zre 12615	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16		leloe 11345	. . . . 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 1537   ∈ wcel 2106   class class class wbr 5148  ℝcr 11152  0cc0 11153   < clt 11293   ≤ cle 11294  ℕcn 12264  ℕ₀cn0 12524  ℤcz 12611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612

This theorem is referenced by:  zle0orge1  12628  nn0zrab  12644  znn0sub  12662  nn0ind  12711  fnn0ind  12715  fznn0  13656  elfz0ubfz0  13669  elfz0fzfz0  13670  fz0fzelfz0  13671  elfzmlbp  13676  difelfzle  13678  difelfznle  13679  elfzo0z  13738  fzofzim  13746  ubmelm1fzo  13799  flge0nn0  13857  zmodcl  13928  modmuladdnn0  13953  modsumfzodifsn  13982  zsqcl2  14175  swrdnnn0nd  14691  swrdswrdlem  14739  swrdswrd  14740  swrdccatin2  14764  pfxccatin12lem2  14766  pfxccatin12lem3  14767  repswswrd  14819  cshwidxmod  14838  nn0abscl  15348  iseralt  15718  binomrisefac  16075  oexpneg  16379  oddnn02np1  16382  evennn02n  16384  nn0ehalf  16412  nn0oddm1d2  16419  divalglem2  16429  divalglem8  16434  divalglem10  16436  divalgb  16438  bitsinv1lem  16475  dfgcd2  16580  algcvga  16613  hashgcdlem  16822  iserodd  16869  pockthlem  16939  4sqlem14  16992  cshwshashlem2  17131  chfacfscmul0  22880  chfacfpmmul0  22884  taylfvallem1  26413  tayl0  26418  basellem3  27141  bcmono  27336  gausslemma2dlem0h  27422  2sqnn0  27497  crctcshwlkn0lem7  29846  crctcshwlkn0  29851  clwlkclwwlklem2a1  30021  clwlkclwwlklem2fv2  30025  clwlkclwwlklem2a  30027  wwlksubclwwlk  30087  0nn0m1nnn0  35097  knoppndvlem2  36496  aks4d1p1p2  42052  aks4d1p1p4  42053  aks4d1p3  42060  aks4d1p7  42065  aks4d1p8  42069  aks4d1p9  42070  aks6d1c1  42098  hashscontpow1  42103  aks6d1c2lem4  42109  aks6d1c2  42112  aks6d1c5lem3  42119  aks6d1c5lem2  42120  sticksstones10  42137  sticksstones12a  42139  aks6d1c6lem3  42154  aks6d1c6lem4  42155  bcled  42160  bcle2d  42161  aks6d1c7lem1  42162  aks6d1c7lem2  42163  unitscyglem5  42181  irrapxlem1  42810  rmynn0  42946  rmyabs  42947  jm2.22  42984  jm2.23  42985  jm2.27a  42994  jm2.27c  42996  dvnprodlem1  45902  wallispilem4  46024  stirlinglem5  46034  elaa2lem  46189  etransclem3  46193  etransclem7  46197  etransclem10  46200  etransclem19  46209  etransclem20  46210  etransclem21  46211  etransclem22  46212  etransclem24  46214  etransclem27  46217  zm1nn  47252  eluzge0nn0  47262  elfz2z  47265  2elfz2melfz  47268  subsubelfzo0  47276  oexpnegALTV  47602  nn0oALTV  47621  nn0e  47622  gpgusgralem  47946  nn0eo  48378  dig1  48458