Theorem nn0ge0 12494

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 12471	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12240	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2739	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 908	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 216	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11213	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12478	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11297	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
10	7, 8, 9	sylancr 588	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
11	6, 10	mpbird 257	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 846   = wceq 1542   ∈ wcel 2107   class class class wbr 5148  ℝcr 11106  0cc0 11107   < clt 11245   ≤ cle 11246  ℕcn 12209  ℕ₀cn0 12469

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-n0 12470

This theorem is referenced by:  nn0nlt0  12495  nn0ge0i  12496  nn0le0eq0  12497  nn0p1gt0  12498  0mnnnnn0  12501  nn0addge1  12515  nn0addge2  12516  nn0negleid  12521  nn0ge0d  12532  nn0ge0div  12628  xnn0ge0  13110  xnn0xadd0  13223  nn0rp0  13429  xnn0xrge0  13480  0elfz  13595  fz0fzelfz0  13604  fz0fzdiffz0  13607  fzctr  13610  difelfzle  13611  fzoun  13666  nn0p1elfzo  13672  elfzodifsumelfzo  13695  fvinim0ffz  13748  subfzo0  13751  adddivflid  13780  modmuladdnn0  13877  addmodid  13881  modifeq2int  13895  modfzo0difsn  13905  nn0sq11  14094  zzlesq  14167  bernneq  14189  bernneq3  14191  faclbnd  14247  faclbnd6  14256  facubnd  14257  bcval5  14275  hashneq0  14321  fi1uzind  14455  ccat0  14523  ccat2s1fvw  14585  repswswrd  14731  nn0sqeq1  15220  rprisefaccl  15964  dvdseq  16254  evennn02n  16290  nn0ehalf  16318  nn0oddm1d2  16325  bitsinv1  16380  smuval2  16420  gcdn0gt0  16456  nn0gcdid0  16459  absmulgcd  16488  algcvgblem  16511  algcvga  16513  lcmgcdnn  16545  lcmfun  16579  lcmfass  16580  2mulprm  16627  nonsq  16692  hashgcdlem  16718  odzdvds  16725  pcfaclem  16828  prmirredlem  21034  prmirred  21036  coe1sclmul  21796  coe1sclmul2  21798  fvmptnn04ifb  22345  mdegle0  25587  plypf1  25718  dgrlt  25772  fta1  25813  taylfval  25863  logbgcd1irr  26289  eldmgm  26516  basellem3  26577  bcmono  26770  lgsdinn0  26838  2sq2  26926  2sqnn0  26931  2sqreulem1  26939  dchrisumlem1  26982  dchrisumlem2  26983  wwlksnextwrd  29141  wwlksnextfun  29142  wwlksnextinj  29143  wwlksnextproplem2  29154  wwlksnextproplem3  29155  wrdt2ind  32105  xrsmulgzz  32167  hashf2  33071  hasheuni  33072  reprinfz1  33623  0nn0m1nnn0  34091  faclimlem1  34702  rrntotbnd  36693  factwoffsmonot  41012  gcdnn0id  41216  pell14qrgt0  41583  pell1qrgaplem  41597  monotoddzzfi  41667  jm2.17a  41685  jm2.22  41720  rmxdiophlem  41740  rexanuz2nf  44190  wallispilem3  44770  stirlinglem7  44783  elfz2z  46010  fz0addge0  46014  elfzlble  46015  2ffzoeq  46023  iccpartigtl  46078  sqrtpwpw2p  46193  flsqrt  46248  nn0e  46352  nn0sumltlt  46980  nn0eo  47168  fllog2  47208  dignn0fr  47241  dignnld  47243  dig1  47248  itcovalt2lem2lem1  47313