Theorem nn0ge0 12521

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 12498	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12267	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2734	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 907	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 216	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11240	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12505	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11324	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
10	7, 8, 9	sylancr 586	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
11	6, 10	mpbird 257	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 846   = wceq 1534   ∈ wcel 2099   class class class wbr 5142  ℝcr 11131  0cc0 11132   < clt 11272   ≤ cle 11273  ℕcn 12236  ℕ₀cn0 12496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-mulcom 11196  ax-addass 11197  ax-mulass 11198  ax-distr 11199  ax-i2m1 11200  ax-1ne0 11201  ax-1rid 11202  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205  ax-pre-lttri 11206  ax-pre-lttrn 11207  ax-pre-ltadd 11208  ax-pre-mulgt0 11209

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11274  df-mnf 11275  df-xr 11276  df-ltxr 11277  df-le 11278  df-sub 11470  df-neg 11471  df-nn 12237  df-n0 12497

This theorem is referenced by:  nn0nlt0  12522  nn0ge0i  12523  nn0le0eq0  12524  nn0p1gt0  12525  0mnnnnn0  12528  nn0addge1  12542  nn0addge2  12543  nn0negleid  12548  nn0ge0d  12559  nn0ge0div  12655  xnn0ge0  13139  xnn0xadd0  13252  nn0rp0  13458  xnn0xrge0  13509  0elfz  13624  fz0fzelfz0  13633  fz0fzdiffz0  13636  fzctr  13639  difelfzle  13640  fzoun  13695  nn0p1elfzo  13701  elfzodifsumelfzo  13724  fvinim0ffz  13777  subfzo0  13780  adddivflid  13809  modmuladdnn0  13906  addmodid  13910  modifeq2int  13924  modfzo0difsn  13934  nn0sq11  14122  zzlesq  14195  bernneq  14217  bernneq3  14219  faclbnd  14275  faclbnd6  14284  facubnd  14285  bcval5  14303  hashneq0  14349  fi1uzind  14484  ccat0  14552  ccat2s1fvw  14614  repswswrd  14760  nn0sqeq1  15249  rprisefaccl  15993  dvdseq  16284  evennn02n  16320  nn0ehalf  16348  nn0oddm1d2  16355  bitsinv1  16410  smuval2  16450  gcdn0gt0  16486  nn0gcdid0  16489  absmulgcd  16518  algcvgblem  16541  algcvga  16543  lcmgcdnn  16575  lcmfun  16609  lcmfass  16610  2mulprm  16657  nonsq  16724  hashgcdlem  16750  odzdvds  16757  pcfaclem  16860  prmirredlem  21391  prmirred  21393  coe1sclmul  22194  coe1sclmul2  22196  fvmptnn04ifb  22746  mdegle0  26006  plypf1  26139  dgrlt  26194  fta1  26236  taylfval  26286  logbgcd1irr  26719  eldmgm  26947  basellem3  27008  bcmono  27203  lgsdinn0  27271  2sq2  27359  2sqnn0  27364  2sqreulem1  27372  dchrisumlem1  27415  dchrisumlem2  27416  wwlksnextwrd  29701  wwlksnextfun  29702  wwlksnextinj  29703  wwlksnextproplem2  29714  wwlksnextproplem3  29715  wrdt2ind  32668  xrsmulgzz  32730  hashf2  33697  hasheuni  33698  reprinfz1  34248  0nn0m1nnn0  34716  faclimlem1  35331  rrntotbnd  37303  factwoffsmonot  41688  gcdnn0id  41883  pell14qrgt0  42273  pell1qrgaplem  42287  monotoddzzfi  42357  jm2.17a  42375  jm2.22  42410  rmxdiophlem  42430  rexanuz2nf  44869  wallispilem3  45449  stirlinglem7  45462  elfz2z  46689  fz0addge0  46693  elfzlble  46694  2ffzoeq  46702  iccpartigtl  46757  sqrtpwpw2p  46872  flsqrt  46927  nn0e  47031  nn0sumltlt  47408  nn0eo  47595  fllog2  47635  dignn0fr  47668  dignnld  47670  dig1  47675  itcovalt2lem2lem1  47740