Theorem elnn0z 12501

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 12403	. 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnnz 12498	. . 3 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
3		eqcom 2743	. . 3 ⊢ (𝑁 = 0 ↔ 0 = 𝑁)
4	2, 3	orbi12i 914	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁))
5		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
6		0z 12499	. . . . . . 7 ⊢ 0 ∈ ℤ
7		eleq1 2824	. . . . . . 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 11134	. . . . 5 ⊢ 0 ∈ ℝ
15		zre 12492	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16		leloe 11219	. . . . 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 1541   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025  0cc0 11026   < clt 11166   ≤ cle 11167  ℕcn 12145  ℕ₀cn0 12401  ℤcz 12488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-n0 12402  df-z 12489

This theorem is referenced by:  zle0orge1  12505  nn0zrab  12520  znn0sub  12538  nn0ind  12587  fnn0ind  12591  fznn0  13535  elfz0ubfz0  13548  elfz0fzfz0  13549  fz0fzelfz0  13550  elfzmlbp  13555  difelfzle  13557  difelfznle  13558  elfzo0z  13617  fzofzim  13625  ubmelm1fzo  13679  flge0nn0  13740  zmodcl  13811  modmuladdnn0  13838  modsumfzodifsn  13867  zsqcl2  14061  swrdnnn0nd  14580  swrdswrdlem  14627  swrdswrd  14628  swrdccatin2  14652  pfxccatin12lem2  14654  pfxccatin12lem3  14655  repswswrd  14707  cshwidxmod  14726  nn0abscl  15235  iseralt  15608  binomrisefac  15965  oexpneg  16272  oddnn02np1  16275  evennn02n  16277  nn0ehalf  16305  nn0oddm1d2  16312  divalglem2  16322  divalglem8  16327  divalglem10  16329  divalgb  16331  bitsinv1lem  16368  dfgcd2  16473  algcvga  16506  hashgcdlem  16715  iserodd  16763  pockthlem  16833  4sqlem14  16886  cshwshashlem2  17024  chfacfscmul0  22802  chfacfpmmul0  22806  taylfvallem1  26320  tayl0  26325  basellem3  27049  bcmono  27244  gausslemma2dlem0h  27330  2sqnn0  27405  crctcshwlkn0lem7  29889  crctcshwlkn0  29894  clwlkclwwlklem2a1  30067  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a  30073  wwlksubclwwlk  30133  0nn0m1nnn0  35307  knoppndvlem2  36713  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p3  42332  aks4d1p7  42337  aks4d1p8  42341  aks4d1p9  42342  aks6d1c1  42370  hashscontpow1  42375  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c5lem3  42391  aks6d1c5lem2  42392  sticksstones10  42409  sticksstones12a  42411  aks6d1c6lem3  42426  aks6d1c6lem4  42427  bcled  42432  bcle2d  42433  aks6d1c7lem1  42434  aks6d1c7lem2  42435  unitscyglem5  42453  irrapxlem1  43064  rmynn0  43199  rmyabs  43200  jm2.22  43237  jm2.23  43238  jm2.27a  43247  jm2.27c  43249  dvnprodlem1  46190  wallispilem4  46312  stirlinglem5  46322  elaa2lem  46477  etransclem3  46481  etransclem7  46485  etransclem10  46488  etransclem19  46497  etransclem20  46498  etransclem21  46499  etransclem22  46500  etransclem24  46502  etransclem27  46505  ormkglobd  47119  zm1nn  47548  eluzge0nn0  47558  elfz2z  47561  2elfz2melfz  47564  subsubelfzo0  47572  oexpnegALTV  47923  nn0oALTV  47942  nn0e  47943  gpgusgralem  48302  nn0eo  48774  dig1  48854