Theorem nn0ge0 12531

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 12508	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12276	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2742	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 908	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 217	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11242	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12515	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11326	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
10	7, 8, 9	sylancr 587	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
11	6, 10	mpbird 257	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847   = wceq 1540   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133  0cc0 11134   < clt 11274   ≤ cle 11275  ℕcn 12245  ℕ₀cn0 12506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-n0 12507

This theorem is referenced by:  nn0nlt0  12532  nn0ge0i  12533  nn0le0eq0  12534  nn0p1gt0  12535  0mnnnnn0  12538  nn0addge1  12552  nn0addge2  12553  nn0negleid  12558  nn0ge0d  12570  nn0ge0div  12667  xnn0ge0  13155  xnn0xadd0  13268  nn0rp0  13477  xnn0xrge0  13528  0elfz  13646  fz0fzelfz0  13656  fz0fzdiffz0  13659  fzctr  13662  difelfzle  13663  fzoun  13718  nn0p1elfzo  13724  elfzodifsumelfzo  13752  fvinim0ffz  13807  subfzo0  13810  adddivflid  13840  modmuladdnn0  13938  addmodid  13942  modifeq2int  13956  modfzo0difsn  13966  nn0sq11  14155  zzlesq  14229  bernneq  14252  bernneq3  14254  faclbnd  14313  faclbnd6  14322  facubnd  14323  bcval5  14341  hashneq0  14387  fi1uzind  14530  ccat0  14599  ccat2s1fvw  14661  repswswrd  14807  nn0sqeq1  15300  rprisefaccl  16044  dvdseq  16338  evennn02n  16374  nn0ehalf  16402  nn0oddm1d2  16409  bitsinv1  16466  smuval2  16506  gcdn0gt0  16542  nn0gcdid0  16545  absmulgcd  16573  algcvgblem  16601  algcvga  16603  lcmgcdnn  16635  lcmfun  16669  lcmfass  16670  2mulprm  16717  nonsq  16783  hashgcdlem  16812  odzdvds  16820  pcfaclem  16923  prmirredlem  21438  prmirred  21440  coe1sclmul  22224  coe1sclmul2  22226  fvmptnn04ifb  22794  mdegle0  26039  plypf1  26174  dgrlt  26229  fta1  26273  taylfval  26323  logbgcd1irr  26761  eldmgm  26989  basellem3  27050  bcmono  27245  lgsdinn0  27313  2sq2  27401  2sqnn0  27406  2sqreulem1  27414  dchrisumlem1  27457  dchrisumlem2  27458  wwlksnextwrd  29884  wwlksnextfun  29885  wwlksnextinj  29886  wwlksnextproplem2  29897  wwlksnextproplem3  29898  wrdt2ind  32934  xrsmulgzz  33006  hashf2  34120  hasheuni  34121  reprinfz1  34659  0nn0m1nnn0  35140  faclimlem1  35765  rrntotbnd  37865  gcdnn0id  42347  pell14qrgt0  42857  pell1qrgaplem  42871  monotoddzzfi  42941  jm2.17a  42959  jm2.22  42994  rmxdiophlem  43014  rexanuz2nf  45499  wallispilem3  46076  stirlinglem7  46089  elfz2z  47324  fz0addge0  47328  elfzlble  47329  2ffzoeq  47336  addmodne  47353  iccpartigtl  47417  sqrtpwpw2p  47532  flsqrt  47587  nn0e  47691  nn0sumltlt  48305  nn0eo  48488  fllog2  48528  dignn0fr  48561  dignnld  48563  dig1  48568  itcovalt2lem2lem1  48633