Theorem nn0ge0 12496

Description: A nonnegative integer is greater than or equal to zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.)

Assertion

Ref	Expression
nn0ge0	⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Proof of Theorem nn0ge0

Step	Hyp	Ref	Expression
1		elnn0 12473	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12234	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2762	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 917	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 219	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11173	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12480	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11259	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
10	7, 8, 9	sylancr 595	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
11	6, 10	mpbird 259	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Syntax hints:   → wi 4   ↔ wb 208   ∨ wo 856   = wceq 1554   ∈ wcel 2136   class class class wbr 5094  ℝcr 11062  0cc0 11063   < clt 11206   ≤ cle 11207  ℕcn 12200  ℕ₀cn0 12471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-resscn 11120  ax-1cn 11121  ax-icn 11122  ax-addcl 11123  ax-addrcl 11124  ax-mulcl 11125  ax-mulrcl 11126  ax-mulcom 11127  ax-addass 11128  ax-mulass 11129  ax-distr 11130  ax-i2m1 11131  ax-1ne0 11132  ax-1rid 11133  ax-rnegex 11134  ax-rrecex 11135  ax-cnre 11136  ax-pre-lttri 11137  ax-pre-lttrn 11138  ax-pre-ltadd 11139  ax-pre-mulgt0 11140

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-nel 3056  df-ral 3071  df-rex 3081  df-reu 3362  df-rab 3409  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4945  df-br 5095  df-opab 5157  df-mpt 5176  df-tr 5202  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-fv 6518  df-riota 7342  df-ov 7388  df-oprab 7389  df-mpo 7390  df-om 7836  df-2nd 7960  df-frecs 8250  df-wrecs 8281  df-recs 8330  df-rdg 8369  df-er 8666  df-en 8917  df-dom 8918  df-sdom 8919  df-pnf 11208  df-mnf 11209  df-xr 11210  df-ltxr 11211  df-le 11212  df-sub 11406  df-neg 11407  df-nn 12201  df-n0 12472

This theorem is referenced by:  nn0nlt0  12497  nn0ge0i  12498  nn0le0eq0  12499  nn0p1gt0  12500  0mnnnnn0  12503  nn0addge1  12517  nn0addge2  12518  nn0negleid  12523  nn0ge0d  12535  nn0ge0div  12632  xnn0ge0  13126  xnn0xadd0  13240  nn0rp0  13449  xnn0xrge0  13500  0elfz  13619  fz0fzelfz0  13629  fz0fzdiffz0  13632  fzctr  13635  difelfzle  13636  fzoun  13692  nn0p1elfzo  13698  elfzodifsumelfzo  13727  fvinim0ffz  13785  subfzo0  13788  adddivflid  13818  modmuladdnn0  13918  addmodid  13922  modifeq2int  13936  modfzo0difsn  13946  nn0sq11  14135  zzlesq  14209  bernneq  14232  bernneq3  14234  faclbnd  14293  faclbnd6  14302  facubnd  14303  bcval5  14321  hashneq0  14367  fi1uzind  14510  ccat0  14579  ccat2s1fvw  14642  repswswrd  14787  nn0sqeq1  15279  nn0absid  15433  rprisefaccl  16029  dvdseq  16324  evennn02n  16360  nn0ehalf  16388  nn0oddm1d2  16395  bitsinv1  16452  smuval2  16492  gcdn0gt0  16528  nn0gcdid0  16531  absmulgcd  16559  algcvgblem  16587  algcvga  16589  lcmgcdnn  16621  lcmfun  16655  lcmfass  16656  2mulprm  16703  nonsq  16770  hashgcdlem  16799  odzdvds  16807  pcfaclem  16910  prmirredlem  21497  prmirred  21499  coe1sclmul  22318  coe1sclmul2  22320  fvmptnn04ifb  22884  mdegle0  26110  plypf1  26245  dgrlt  26299  fta1  26342  taylfval  26392  logbgcd1irr  26829  eldmgm  27056  basellem3  27117  bcmono  27311  lgsdinn0  27379  2sq2  27467  2sqnn0  27472  2sqreulem1  27480  dchrisumlem1  27523  dchrisumlem2  27524  wwlksnextwrd  30036  wwlksnextfun  30037  wwlksnextinj  30038  wwlksnextproplem2  30049  wwlksnextproplem3  30050  wrdt2ind  33085  xrsmulgzz  33141  hashf2  34335  hasheuni  34336  reprinfz1  34873  0nn0m1nnn0  35411  faclimlem1  36041  rrntotbnd  38283  gcdnn0id  42886  pell14qrgt0  43384  pell1qrgaplem  43398  monotoddzzfi  43467  jm2.17a  43485  jm2.22  43520  rmxdiophlem  43540  rexanuz2nf  46014  wallispilem3  46589  stirlinglem7  46602  elfz2z  47857  fz0addge0  47861  elfzlble  47862  2ffzoeq  47870  addmodne  47892  iccpartigtl  47977  sqrtpwpw2p  48095  flsqrt  48150  nn0e  48267  nn0sumltlt  48920  nn0eo  49098  fllog2  49138  dignn0fr  49171  dignnld  49173  dig1  49178  itcovalt2lem2lem1  49243