Theorem elnn0z 12189

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 12092	. 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnnz 12186	. . 3 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
3		eqcom 2744	. . 3 ⊢ (𝑁 = 0 ↔ 0 = 𝑁)
4	2, 3	orbi12i 915	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) ↔ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁))
5		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℤ)
6		0z 12187	. . . . . . 7 ⊢ 0 ∈ ℤ
7		eleq1 2825	. . . . . . 7 ⊢ (0 = 𝑁 → (0 ∈ ℤ ↔ 𝑁 ∈ ℤ))
8	6, 7	mpbii 236	. . . . . 6 ⊢ (0 = 𝑁 → 𝑁 ∈ ℤ)
9	5, 8	jaoi 857	. . . . 5 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) → 𝑁 ∈ ℤ)
10		orc 867	. . . . 5 ⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℤ ∨ 0 = 𝑁))
11	9, 10	impbii 212	. . . 4 ⊢ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ↔ 𝑁 ∈ ℤ)
12	11	anbi1i 627	. . 3 ⊢ (((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
13		ordir 1007	. . 3 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ ((𝑁 ∈ ℤ ∨ 0 = 𝑁) ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
14		0re 10835	. . . . 5 ⊢ 0 ∈ ℝ
15		zre 12180	. . . . 5 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16		leloe 10919	. . . . 5 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
17	14, 15, 16	sylancr 590	. . . 4 ⊢ (𝑁 ∈ ℤ → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
18	17	pm5.32i 578	. . 3 ⊢ ((𝑁 ∈ ℤ ∧ 0 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ (0 < 𝑁 ∨ 0 = 𝑁)))
19	12, 13, 18	3bitr4i 306	. 2 ⊢ (((𝑁 ∈ ℤ ∧ 0 < 𝑁) ∨ 0 = 𝑁) ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))
20	1, 4, 19	3bitri 300	1 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∨ wo 847   = wceq 1543   ∈ wcel 2110   class class class wbr 5053  ℝcr 10728  0cc0 10729   < clt 10867   ≤ cle 10868  ℕcn 11830  ℕ₀cn0 12090  ℤcz 12176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-n0 12091  df-z 12177

This theorem is referenced by:  zle0orge1  12193  nn0zrab  12206  znn0sub  12224  nn0ind  12272  fnn0ind  12276  fznn0  13204  elfz0ubfz0  13216  elfz0fzfz0  13217  fz0fzelfz0  13218  elfzmlbp  13223  difelfzle  13225  difelfznle  13226  elfzo0z  13284  fzofzim  13289  ubmelm1fzo  13338  flge0nn0  13395  zmodcl  13464  modmuladdnn0  13488  modsumfzodifsn  13517  zsqcl2  13708  swrdnnn0nd  14221  swrdswrdlem  14269  swrdswrd  14270  swrdccatin2  14294  pfxccatin12lem2  14296  pfxccatin12lem3  14297  repswswrd  14349  cshwidxmod  14368  nn0abscl  14876  iseralt  15248  binomrisefac  15604  oexpneg  15906  oddnn02np1  15909  evennn02n  15911  nn0ehalf  15939  nn0oddm1d2  15946  divalglem2  15956  divalglem8  15961  divalglem10  15963  divalgb  15965  bitsinv1lem  16000  dfgcd2  16106  algcvga  16136  hashgcdlem  16341  iserodd  16388  pockthlem  16458  4sqlem14  16511  cshwshashlem2  16650  chfacfscmul0  21755  chfacfpmmul0  21759  taylfvallem1  25249  tayl0  25254  basellem3  25965  bcmono  26158  gausslemma2dlem0h  26244  2sqnn0  26319  crctcshwlkn0lem7  27900  crctcshwlkn0  27905  clwlkclwwlklem2a1  28075  clwlkclwwlklem2fv2  28079  clwlkclwwlklem2a  28081  wwlksubclwwlk  28141  0nn0m1nnn0  32784  knoppndvlem2  34430  aks4d1p1p2  39811  aks4d1p1p4  39812  aks4d1p3  39819  sticksstones10  39833  sticksstones12a  39835  irrapxlem1  40347  rmynn0  40482  rmyabs  40483  jm2.22  40520  jm2.23  40521  jm2.27a  40530  jm2.27c  40532  dvnprodlem1  43162  wallispilem4  43284  stirlinglem5  43294  elaa2lem  43449  etransclem3  43453  etransclem7  43457  etransclem10  43460  etransclem19  43469  etransclem20  43470  etransclem21  43471  etransclem22  43472  etransclem24  43474  etransclem27  43477  zm1nn  44467  eluzge0nn0  44477  elfz2z  44480  2elfz2melfz  44483  subsubelfzo0  44491  oexpnegALTV  44802  nn0oALTV  44821  nn0e  44822  nn0eo  45547  dig1  45627