Theorem nn0ge0 12427

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 12404	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12177	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2735	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 908	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 217	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11136	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12411	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11220	. . 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 5095  ℝcr 11027  0cc0 11028   < clt 11168   ≤ cle 11169  ℕcn 12146  ℕ₀cn0 12402

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 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-nn 12147  df-n0 12403

This theorem is referenced by:  nn0nlt0  12428  nn0ge0i  12429  nn0le0eq0  12430  nn0p1gt0  12431  0mnnnnn0  12434  nn0addge1  12448  nn0addge2  12449  nn0negleid  12454  nn0ge0d  12466  nn0ge0div  12563  xnn0ge0  13054  xnn0xadd0  13167  nn0rp0  13376  xnn0xrge0  13427  0elfz  13545  fz0fzelfz0  13555  fz0fzdiffz0  13558  fzctr  13561  difelfzle  13562  fzoun  13617  nn0p1elfzo  13623  elfzodifsumelfzo  13652  fvinim0ffz  13707  subfzo0  13710  adddivflid  13740  modmuladdnn0  13840  addmodid  13844  modifeq2int  13858  modfzo0difsn  13868  nn0sq11  14057  zzlesq  14131  bernneq  14154  bernneq3  14156  faclbnd  14215  faclbnd6  14224  facubnd  14225  bcval5  14243  hashneq0  14289  fi1uzind  14432  ccat0  14501  ccat2s1fvw  14563  repswswrd  14708  nn0sqeq1  15201  nn0absid  15355  rprisefaccl  15948  dvdseq  16243  evennn02n  16279  nn0ehalf  16307  nn0oddm1d2  16314  bitsinv1  16371  smuval2  16411  gcdn0gt0  16447  nn0gcdid0  16450  absmulgcd  16478  algcvgblem  16506  algcvga  16508  lcmgcdnn  16540  lcmfun  16574  lcmfass  16575  2mulprm  16622  nonsq  16688  hashgcdlem  16717  odzdvds  16725  pcfaclem  16828  prmirredlem  21397  prmirred  21399  coe1sclmul  22184  coe1sclmul2  22186  fvmptnn04ifb  22754  mdegle0  25998  plypf1  26133  dgrlt  26188  fta1  26232  taylfval  26282  logbgcd1irr  26720  eldmgm  26948  basellem3  27009  bcmono  27204  lgsdinn0  27272  2sq2  27360  2sqnn0  27365  2sqreulem1  27373  dchrisumlem1  27416  dchrisumlem2  27417  wwlksnextwrd  29860  wwlksnextfun  29861  wwlksnextinj  29862  wwlksnextproplem2  29873  wwlksnextproplem3  29874  wrdt2ind  32908  xrsmulgzz  32976  hashf2  34053  hasheuni  34054  reprinfz1  34592  0nn0m1nnn0  35088  faclimlem1  35718  rrntotbnd  37818  gcdnn0id  42305  pell14qrgt0  42835  pell1qrgaplem  42849  monotoddzzfi  42918  jm2.17a  42936  jm2.22  42971  rmxdiophlem  42991  rexanuz2nf  45475  wallispilem3  46052  stirlinglem7  46065  elfz2z  47303  fz0addge0  47307  elfzlble  47308  2ffzoeq  47315  addmodne  47332  iccpartigtl  47411  sqrtpwpw2p  47526  flsqrt  47581  nn0e  47685  nn0sumltlt  48338  nn0eo  48517  fllog2  48557  dignn0fr  48590  dignnld  48592  dig1  48597  itcovalt2lem2lem1  48662