Theorem elnn0z 12567

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 12470	. 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnnz 12564	. . 3 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
3		eqcom 2739	. . 3 ⊢ (𝑁 = 0 ↔ 0 = 𝑁)
4	2, 3	orbi12i 913	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁))
5		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
6		0z 12565	. . . . . . 7 ⊢ 0 ∈ ℤ
7		eleq1 2821	. . . . . . 7 ⊢ (0 = 𝑁 → (0 ∈ ℤ ↔ 𝑁 ∈ ℤ))
8	6, 7	mpbii 232	. . . . . 6 ⊢ (0 = 𝑁 → 𝑁 ∈ ℤ)
9	5, 8	jaoi 855	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) → 𝑁 ∈ ℤ)
10		orc 865	. . . . 5 ⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℤ ∨ 0 = 𝑁))
11	9, 10	impbii 208	. . . 4 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ↔ 𝑁 ∈ ℤ)
12	11	anbi1i 624	. . 3 ⊢ (((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
13		ordir 1005	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
14		0re 11212	. . . . 5 ⊢ 0 ∈ ℝ
15		zre 12558	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16		leloe 11296	. . . . 5 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
17	14, 15, 16	sylancr 587	. . . 4 ⊢ (𝑁 ∈ ℤ → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
18	17	pm5.32i 575	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
19	12, 13, 18	3bitr4i 302	. 2 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
20	1, 4, 19	3bitri 296	1 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   class class class wbr 5147  ℝcr 11105  0cc0 11106   < clt 11244   ≤ cle 11245  ℕcn 12208  ℕ₀cn0 12468  ℤcz 12554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555

This theorem is referenced by:  zle0orge1  12571  nn0zrab  12587  znn0sub  12605  nn0ind  12653  fnn0ind  12657  fznn0  13589  elfz0ubfz0  13601  elfz0fzfz0  13602  fz0fzelfz0  13603  elfzmlbp  13608  difelfzle  13610  difelfznle  13611  elfzo0z  13670  fzofzim  13675  ubmelm1fzo  13724  flge0nn0  13781  zmodcl  13852  modmuladdnn0  13876  modsumfzodifsn  13905  zsqcl2  14099  swrdnnn0nd  14602  swrdswrdlem  14650  swrdswrd  14651  swrdccatin2  14675  pfxccatin12lem2  14677  pfxccatin12lem3  14678  repswswrd  14730  cshwidxmod  14749  nn0abscl  15255  iseralt  15627  binomrisefac  15982  oexpneg  16284  oddnn02np1  16287  evennn02n  16289  nn0ehalf  16317  nn0oddm1d2  16324  divalglem2  16334  divalglem8  16339  divalglem10  16341  divalgb  16343  bitsinv1lem  16378  dfgcd2  16484  algcvga  16512  hashgcdlem  16717  iserodd  16764  pockthlem  16834  4sqlem14  16887  cshwshashlem2  17026  chfacfscmul0  22351  chfacfpmmul0  22355  taylfvallem1  25860  tayl0  25865  basellem3  26576  bcmono  26769  gausslemma2dlem0h  26855  2sqnn0  26930  crctcshwlkn0lem7  29059  crctcshwlkn0  29064  clwlkclwwlklem2a1  29234  clwlkclwwlklem2fv2  29238  clwlkclwwlklem2a  29240  wwlksubclwwlk  29300  0nn0m1nnn0  34090  knoppndvlem2  35377  aks4d1p1p2  40923  aks4d1p1p4  40924  aks4d1p3  40931  aks4d1p7  40936  aks4d1p8  40940  aks4d1p9  40941  sticksstones10  40959  sticksstones12a  40961  irrapxlem1  41545  rmynn0  41681  rmyabs  41682  jm2.22  41719  jm2.23  41720  jm2.27a  41729  jm2.27c  41731  dvnprodlem1  44648  wallispilem4  44770  stirlinglem5  44780  elaa2lem  44935  etransclem3  44939  etransclem7  44943  etransclem10  44946  etransclem19  44955  etransclem20  44956  etransclem21  44957  etransclem22  44958  etransclem24  44960  etransclem27  44963  zm1nn  45996  eluzge0nn0  46006  elfz2z  46009  2elfz2melfz  46012  subsubelfzo0  46020  oexpnegALTV  46331  nn0oALTV  46350  nn0e  46351  nn0eo  47167  dig1  47247