Theorem nn0ge0 12635

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 12612	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12373	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 23	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2766	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 922	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 220	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11314	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12619	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11400	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
10	7, 8, 9	sylancr 599	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
11	6, 10	mpbird 260	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861   = wceq 1569   ∈ wcel 2144   class class class wbr 5102  ℝcr 11203  0cc0 11204   < clt 11347   ≤ cle 11348  ℕcn 12339  ℕ₀cn0 12610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-nn 12340  df-n0 12611

This theorem is used by:  nn0nlt0  12636  nn0ge0i  12637  nn0le0eq0  12638  nn0p1gt0  12639  0mnnnnn0  12642  nn0addge1  12656  nn0addge2  12657  nn0negleid  12662  nn0ge0d  12674  0nn0m1nnn0  12757  nn0ge0div  12772  xnn0ge0  13267  xnn0xadd0  13381  nn0rp0  13590  xnn0xrge0  13641  0elfz  13762  fz0fzelfz0  13772  fz0fzdiffz0  13775  fzctr  13778  difelfzle  13779  fzoun  13835  nn0p1elfzo  13841  elfzodifsumelfzo  13870  fvinim0ffz  13928  subfzo0  13932  adddivflid  13962  modmuladdnn0  14062  addmodid  14066  modifeq2int  14080  modfzo0difsn  14090  nn0sq11  14279  zzlesq  14354  bernneq  14377  bernneq3  14379  faclbnd  14438  faclbnd6  14447  facubnd  14448  bcval5  14466  hashneq0  14512  fi1uzind  14656  ccat0  14725  ccat2s1fvw  14791  repswswrd  14940  nn0sqeq1  15449  nn0absid  15603  rprisefaccl  16196  dvdseq  16490  evennn02n  16526  nn0ehalf  16554  nn0oddm1d2  16561  bitsinv1  16618  smuval2  16658  gcdn0gt0  16696  nn0gcdid0  16699  gcdnn0id  16706  absmulgcd  16728  algcvgblem  16758  algcvga  16760  lcmgcdnn  16792  lcmfun  16826  lcmfass  16827  2mulprm  16874  nonsq  16941  hashgcdlem  16971  odzdvds  16979  pcfaclem  17082  prmirredlem  21784  prmirred  21786  coe1sclmul  22607  coe1sclmul2  22609  fvmptnn04ifb  23175  mdegle0  26401  plypf1  26537  dgrlt  26591  fta1  26635  taylfval  26692  logbgcd1irr  27128  eldmgm  27355  basellem3  27416  bcmono  27610  lgsdinn0  27678  2sq2  27766  2sqnn0  27771  2sqreulem1  27779  dchrisumlem1  27822  dchrisumlem2  27823  wwlksnextwrd  30492  wwlksnextfun  30493  wwlksnextinj  30494  wwlksnextproplem2  30505  wwlksnextproplem3  30506  wrdt2ind  33563  xrsmulgzz  33617  hashf2  34763  hasheuni  34764  reprinfz1  35298  faclimlem1  36601  rrntotbnd  38864  pell14qrgt0  43960  pell1qrgaplem  43974  monotoddzzfi  44043  jm2.17a  44061  jm2.22  44096  rmxdiophlem  44116  rexanuz2nf  46596  wallispilem3  47171  stirlinglem7  47184  elfz2z  48479  fz0addge0  48483  elfzlble  48484  2ffzoeq  48492  addmodne  48514  iccpartigtl  48599  sqrtpwpw2p  48717  flsqrt  48772  nn0e  48889  nn0sumltlt  49556  nn0eo  49734  fllog2  49774  dignn0fr  49807  dignnld  49809  dig1  49814  itcovalt2lem2lem1  49879