Theorem nn0ge0 12426

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 12403	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12176	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 22	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2742	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 908	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 217	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11134	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12410	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11219	. . 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 1541   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025  0cc0 11026   < clt 11166   ≤ cle 11167  ℕcn 12145  ℕ₀cn0 12401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-n0 12402

This theorem is referenced by:  nn0nlt0  12427  nn0ge0i  12428  nn0le0eq0  12429  nn0p1gt0  12430  0mnnnnn0  12433  nn0addge1  12447  nn0addge2  12448  nn0negleid  12453  nn0ge0d  12465  nn0ge0div  12561  xnn0ge0  13048  xnn0xadd0  13162  nn0rp0  13371  xnn0xrge0  13422  0elfz  13540  fz0fzelfz0  13550  fz0fzdiffz0  13553  fzctr  13556  difelfzle  13557  fzoun  13612  nn0p1elfzo  13618  elfzodifsumelfzo  13647  fvinim0ffz  13705  subfzo0  13708  adddivflid  13738  modmuladdnn0  13838  addmodid  13842  modifeq2int  13856  modfzo0difsn  13866  nn0sq11  14055  zzlesq  14129  bernneq  14152  bernneq3  14154  faclbnd  14213  faclbnd6  14222  facubnd  14223  bcval5  14241  hashneq0  14287  fi1uzind  14430  ccat0  14499  ccat2s1fvw  14562  repswswrd  14707  nn0sqeq1  15199  nn0absid  15353  rprisefaccl  15946  dvdseq  16241  evennn02n  16277  nn0ehalf  16305  nn0oddm1d2  16312  bitsinv1  16369  smuval2  16409  gcdn0gt0  16445  nn0gcdid0  16448  absmulgcd  16476  algcvgblem  16504  algcvga  16506  lcmgcdnn  16538  lcmfun  16572  lcmfass  16573  2mulprm  16620  nonsq  16686  hashgcdlem  16715  odzdvds  16723  pcfaclem  16826  prmirredlem  21427  prmirred  21429  coe1sclmul  22224  coe1sclmul2  22226  fvmptnn04ifb  22795  mdegle0  26038  plypf1  26173  dgrlt  26228  fta1  26272  taylfval  26322  logbgcd1irr  26760  eldmgm  26988  basellem3  27049  bcmono  27244  lgsdinn0  27312  2sq2  27400  2sqnn0  27405  2sqreulem1  27413  dchrisumlem1  27456  dchrisumlem2  27457  wwlksnextwrd  29970  wwlksnextfun  29971  wwlksnextinj  29972  wwlksnextproplem2  29983  wwlksnextproplem3  29984  wrdt2ind  33035  xrsmulgzz  33091  hashf2  34241  hasheuni  34242  reprinfz1  34779  0nn0m1nnn0  35307  faclimlem1  35937  rrntotbnd  38037  gcdnn0id  42584  pell14qrgt0  43101  pell1qrgaplem  43115  monotoddzzfi  43184  jm2.17a  43202  jm2.22  43237  rmxdiophlem  43257  rexanuz2nf  45736  wallispilem3  46311  stirlinglem7  46324  elfz2z  47561  fz0addge0  47565  elfzlble  47566  2ffzoeq  47573  addmodne  47590  iccpartigtl  47669  sqrtpwpw2p  47784  flsqrt  47839  nn0e  47943  nn0sumltlt  48596  nn0eo  48774  fllog2  48814  dignn0fr  48847  dignnld  48849  dig1  48854  itcovalt2lem2lem1  48919