Theorem nn0ge0 12534

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 12511	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12279	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2740	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 908	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 217	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11245	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12518	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11329	. . 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 1539   ∈ wcel 2107   class class class wbr 5123  ℝcr 11136  0cc0 11137   < clt 11277   ≤ cle 11278  ℕcn 12248  ℕ₀cn0 12509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  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 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-n0 12510

This theorem is referenced by:  nn0nlt0  12535  nn0ge0i  12536  nn0le0eq0  12537  nn0p1gt0  12538  0mnnnnn0  12541  nn0addge1  12555  nn0addge2  12556  nn0negleid  12561  nn0ge0d  12573  nn0ge0div  12670  xnn0ge0  13158  xnn0xadd0  13271  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  14228  bernneq  14251  bernneq3  14253  faclbnd  14312  faclbnd6  14321  facubnd  14322  bcval5  14340  hashneq0  14386  fi1uzind  14529  ccat0  14597  ccat2s1fvw  14659  repswswrd  14805  nn0sqeq1  15298  rprisefaccl  16042  dvdseq  16334  evennn02n  16370  nn0ehalf  16398  nn0oddm1d2  16405  bitsinv1  16462  smuval2  16502  gcdn0gt0  16538  nn0gcdid0  16541  absmulgcd  16569  algcvgblem  16597  algcvga  16599  lcmgcdnn  16631  lcmfun  16665  lcmfass  16666  2mulprm  16713  nonsq  16779  hashgcdlem  16808  odzdvds  16816  pcfaclem  16919  prmirredlem  21446  prmirred  21448  coe1sclmul  22234  coe1sclmul2  22236  fvmptnn04ifb  22806  mdegle0  26053  plypf1  26188  dgrlt  26243  fta1  26287  taylfval  26337  logbgcd1irr  26774  eldmgm  27002  basellem3  27063  bcmono  27258  lgsdinn0  27326  2sq2  27414  2sqnn0  27419  2sqreulem1  27427  dchrisumlem1  27470  dchrisumlem2  27471  wwlksnextwrd  29846  wwlksnextfun  29847  wwlksnextinj  29848  wwlksnextproplem2  29859  wwlksnextproplem3  29860  wrdt2ind  32883  xrsmulgzz  32955  hashf2  34060  hasheuni  34061  reprinfz1  34612  0nn0m1nnn0  35093  faclimlem1  35718  rrntotbnd  37818  factwoffsmonot  42218  gcdnn0id  42343  pell14qrgt0  42848  pell1qrgaplem  42862  monotoddzzfi  42932  jm2.17a  42950  jm2.22  42985  rmxdiophlem  43005  rexanuz2nf  45475  wallispilem3  46054  stirlinglem7  46067  elfz2z  47300  fz0addge0  47304  elfzlble  47305  2ffzoeq  47312  addmodne  47319  iccpartigtl  47383  sqrtpwpw2p  47498  flsqrt  47553  nn0e  47657  nn0sumltlt  48239  nn0eo  48422  fllog2  48462  dignn0fr  48495  dignnld  48497  dig1  48502  itcovalt2lem2lem1  48567