Theorem nn0ge0 12525

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 12502	. . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		nngt0 12263	. . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
3		id 23	. . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0)
4	3	eqcomd 2775	. . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁)
5	2, 4	orim12i 921	. . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁))
6	1, 5	sylbi 220	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁))
7		0re 11206	. . 3 ⊢ 0 ∈ ℝ
8		nn0re 12509	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
9		leloe 11292	. . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
10	7, 8, 9	sylancr 598	. 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
11	6, 10	mpbird 260	1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁)

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860   = wceq 1567   ∈ wcel 2149   class class class wbr 5110  ℝcr 11095  0cc0 11096   < clt 11239   ≤ cle 11240  ℕcn 12229  ℕ₀cn0 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-nn 12230  df-n0 12501

This theorem is referenced by:  nn0nlt0  12526  nn0ge0i  12527  nn0le0eq0  12528  nn0p1gt0  12529  0mnnnnn0  12532  nn0addge1  12546  nn0addge2  12547  nn0negleid  12552  nn0ge0d  12564  nn0ge0div  12661  xnn0ge0  13155  xnn0xadd0  13269  nn0rp0  13478  xnn0xrge0  13529  0elfz  13648  fz0fzelfz0  13658  fz0fzdiffz0  13661  fzctr  13664  difelfzle  13665  fzoun  13721  nn0p1elfzo  13727  elfzodifsumelfzo  13756  fvinim0ffz  13814  subfzo0  13817  adddivflid  13847  modmuladdnn0  13947  addmodid  13951  modifeq2int  13965  modfzo0difsn  13975  nn0sq11  14164  zzlesq  14238  bernneq  14261  bernneq3  14263  faclbnd  14322  faclbnd6  14331  facubnd  14332  bcval5  14350  hashneq0  14396  fi1uzind  14540  ccat0  14609  ccat2s1fvw  14672  repswswrd  14817  nn0sqeq1  15323  nn0absid  15477  rprisefaccl  16073  dvdseq  16368  evennn02n  16404  nn0ehalf  16432  nn0oddm1d2  16439  bitsinv1  16496  smuval2  16536  gcdn0gt0  16572  nn0gcdid0  16575  absmulgcd  16603  algcvgblem  16631  algcvga  16633  lcmgcdnn  16665  lcmfun  16699  lcmfass  16700  2mulprm  16747  nonsq  16814  hashgcdlem  16843  odzdvds  16851  pcfaclem  16954  prmirredlem  21587  prmirred  21589  coe1sclmul  22408  coe1sclmul2  22410  fvmptnn04ifb  22973  mdegle0  26199  plypf1  26334  dgrlt  26388  fta1  26434  taylfval  26484  logbgcd1irr  26921  eldmgm  27148  basellem3  27209  bcmono  27403  lgsdinn0  27471  2sq2  27559  2sqnn0  27564  2sqreulem1  27572  dchrisumlem1  27615  dchrisumlem2  27616  wwlksnextwrd  30183  wwlksnextfun  30184  wwlksnextinj  30185  wwlksnextproplem2  30196  wwlksnextproplem3  30197  wrdt2ind  33210  xrsmulgzz  33266  hashf2  34415  hasheuni  34416  reprinfz1  34950  0nn0m1nnn0  35499  faclimlem1  36130  rrntotbnd  38370  gcdnn0id  42973  pell14qrgt0  43471  pell1qrgaplem  43485  monotoddzzfi  43554  jm2.17a  43572  jm2.22  43607  rmxdiophlem  43627  rexanuz2nf  46091  wallispilem3  46666  stirlinglem7  46679  elfz2z  47934  fz0addge0  47938  elfzlble  47939  2ffzoeq  47947  addmodne  47969  iccpartigtl  48054  sqrtpwpw2p  48172  flsqrt  48227  nn0e  48344  nn0sumltlt  49008  nn0eo  49186  fllog2  49226  dignn0fr  49259  dignnld  49261  dig1  49266  itcovalt2lem2lem1  49331