Theorem nn0ge0 11168

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 11144	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 10899	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2616	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 537	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 206	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 9897	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 11151	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 9976	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
10	7, 8, 9	sylancr 694	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
11	6, 10	mpbird 246	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   = wceq 1475   ∈ wcel 1977   class class class wbr 4578  ℝcr 9792  0cc0 9793   < clt 9931   ≤ cle 9932  ℕcn 10870  ℕ₀cn0 11142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-nn 10871  df-n0 11143

This theorem is referenced by:  nn0nlt0  11169  nn0ge0i  11170  nn0le0eq0  11171  nn0p1gt0  11172  0mnnnnn0  11175  nn0addge1  11189  nn0addge2  11190  nn0negleid  11195  nn0ge0d  11204  nn0ge0div  11281  nn0pnfge0  11806  nn0rp0  12109  0elfz  12263  fz0fzelfz0  12272  fz0fzdiffz0  12275  fzctr  12278  difelfzle  12279  nn0p1elfzo  12336  elfzodifsumelfzo  12359  fvinim0ffz  12407  subfzo0  12410  adddivflid  12439  modmuladdnn0  12534  addmodid  12538  modifeq2int  12552  modfzo0difsn  12562  bernneq  12810  bernneq3  12812  faclbnd  12897  faclbnd6  12906  facubnd  12907  bcval5  12925  hashneq0  12971  fi1uzind  13083  brfi1indALT  13086  fi1uzindOLD  13089  brfi1indALTOLD  13092  ccat2s1fvw  13216  repswswrd  13331  rprisefaccl  14542  dvdseq  14823  evennn02n  14861  nn0ehalf  14882  nn0oddm1d2  14888  bitsinv1  14951  smuval2  14991  gcdn0gt0  15026  nn0gcdid0  15029  absmulgcd  15053  algcvgblem  15077  algcvga  15079  lcmgcdnn  15111  lcmfun  15145  lcmfass  15146  nonsq  15254  hashgcdlem  15280  odzdvds  15287  pcfaclem  15389  coe1sclmul  19422  coe1sclmul2  19424  prmirredlem  19608  prmirred  19610  fvmptnn04ifb  20423  mdegle0  23586  plypf1  23717  dgrlt  23771  fta1  23812  taylfval  23862  eldmgm  24493  basellem3  24554  bcmono  24747  lgsdinn0  24815  dchrisumlem1  24923  dchrisumlem2  24924  wlkonwlk  25859  nvnencycllem  25965  wwlkextwrd  26050  wwlkextfun  26051  wwlkextinj  26052  wwlkextproplem1  26063  wwlkextproplem2  26064  wwlkextproplem3  26065  nn0sqeq1  28695  xrsmulgzz  28803  hashf2  29267  hasheuni  29268  faclimlem1  30676  rrntotbnd  32599  pell14qrgt0  36235  pell1qrgaplem  36249  monotoddzzfi  36319  jm2.17a  36339  jm2.22  36374  rmxdiophlem  36394  wallispilem3  38754  stirlinglem7  38767  iccpartigtl  39756  sqrtpwpw2p  39783  flsqrt  39841  nn0e  39941  elfz2z  40169  fz0addge0  40173  elfzlble  40174  2ffzoeq  40178  xnn0xrge0  40195  xnn0ge0  40203  xnn0xadd0  40207  wwlksnextwrd  41095  wwlksnextfun  41096  wwlksnextinj  41097  wwlksnextproplem2  41108  wwlksnextproplem3  41109  nn0sumltlt  41913  nn0eo  42108  fllog2  42152  dignn0fr  42185  dignnld  42187  dig1  42192