Theorem nn0ge0 12258

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 12235	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12004	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2744	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 906	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 216	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 10977	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12242	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11061	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
10	7, 8, 9	sylancr 587	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
11	6, 10	mpbird 256	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 844   = wceq 1539   ∈ wcel 2106   class class class wbr 5074  ℝcr 10870  0cc0 10871   < clt 11009   ≤ cle 11010  ℕcn 11973  ℕ₀cn0 12233

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234

This theorem is referenced by:  nn0nlt0  12259  nn0ge0i  12260  nn0le0eq0  12261  nn0p1gt0  12262  0mnnnnn0  12265  nn0addge1  12279  nn0addge2  12280  nn0negleid  12285  nn0ge0d  12296  nn0ge0div  12389  xnn0ge0  12869  xnn0xadd0  12981  nn0rp0  13187  xnn0xrge0  13238  0elfz  13353  fz0fzelfz0  13362  fz0fzdiffz0  13365  fzctr  13368  difelfzle  13369  fzoun  13424  nn0p1elfzo  13430  elfzodifsumelfzo  13453  fvinim0ffz  13506  subfzo0  13509  adddivflid  13538  modmuladdnn0  13635  addmodid  13639  modifeq2int  13653  modfzo0difsn  13663  nn0sq11  13851  bernneq  13944  bernneq3  13946  faclbnd  14004  faclbnd6  14013  facubnd  14014  bcval5  14032  hashneq0  14079  fi1uzind  14211  ccat0  14280  ccat2s1fvw  14349  ccat2s1fvwOLD  14350  repswswrd  14497  nn0sqeq1  14988  rprisefaccl  15733  dvdseq  16023  evennn02n  16059  nn0ehalf  16087  nn0oddm1d2  16094  bitsinv1  16149  smuval2  16189  gcdn0gt0  16225  nn0gcdid0  16228  absmulgcd  16257  algcvgblem  16282  algcvga  16284  lcmgcdnn  16316  lcmfun  16350  lcmfass  16351  2mulprm  16398  nonsq  16463  hashgcdlem  16489  odzdvds  16496  pcfaclem  16599  prmirredlem  20694  prmirred  20696  coe1sclmul  21453  coe1sclmul2  21455  fvmptnn04ifb  22000  mdegle0  25242  plypf1  25373  dgrlt  25427  fta1  25468  taylfval  25518  logbgcd1irr  25944  eldmgm  26171  basellem3  26232  bcmono  26425  lgsdinn0  26493  2sq2  26581  2sqnn0  26586  2sqreulem1  26594  dchrisumlem1  26637  dchrisumlem2  26638  wwlksnextwrd  28262  wwlksnextfun  28263  wwlksnextinj  28264  wwlksnextproplem2  28275  wwlksnextproplem3  28276  wrdt2ind  31225  xrsmulgzz  31287  hashf2  32052  hasheuni  32053  reprinfz1  32602  0nn0m1nnn0  33071  faclimlem1  33709  rrntotbnd  35994  factwoffsmonot  40163  gcdnn0id  40329  pell14qrgt0  40681  pell1qrgaplem  40695  monotoddzzfi  40764  jm2.17a  40782  jm2.22  40817  rmxdiophlem  40837  wallispilem3  43608  stirlinglem7  43621  elfz2z  44807  fz0addge0  44811  elfzlble  44812  2ffzoeq  44820  iccpartigtl  44875  sqrtpwpw2p  44990  flsqrt  45045  nn0e  45149  nn0sumltlt  45686  nn0eo  45874  fllog2  45914  dignn0fr  45947  dignnld  45949  dig1  45954  itcovalt2lem2lem1  46019