Theorem nn0ge0d 9441

Description: A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	|- ( ph -> A e. NN0 )

Assertion

Ref	Expression
nn0ge0d	|- ( ph -> 0 <_ A )

Proof of Theorem nn0ge0d

Step	Hyp	Ref	Expression
1		nn0red.1	. 2 |- ( ph -> A e. NN0 )
2		nn0ge0 9410	. 2 |- ( A e. NN0 -> 0 <_ A )
3	1, 2	syl 14	1 |- ( ph -> 0 <_ A )

Syntax hints:   -> wi 4   e. wcel 2200   class class class wbr 4083   0cc0 8015   <_ cle 8198   NN0cn0 9385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4259  ax-pr 4294  ax-un 4525  ax-setind 4630  ax-cnex 8106  ax-resscn 8107  ax-1cn 8108  ax-1re 8109  ax-icn 8110  ax-addcl 8111  ax-addrcl 8112  ax-mulcl 8113  ax-i2m1 8120  ax-0lt1 8121  ax-0id 8123  ax-rnegex 8124  ax-pre-ltirr 8127  ax-pre-ltwlin 8128  ax-pre-lttrn 8129  ax-pre-ltadd 8131

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-xp 4726  df-cnv 4728  df-iota 5281  df-fv 5329  df-ov 6013  df-pnf 8199  df-mnf 8200  df-xr 8201  df-ltxr 8202  df-le 8203  df-inn 9127  df-n0 9386

This theorem is referenced by:  flqmulnn0  10536  zmodfz  10585  addmodid  10611  modifeq2int  10625  modaddmodlo  10627  modsumfzodifsn  10635  addmodlteq  10637  expnnval  10781  nn0le2msqd  10958  facwordi  10979  faclbnd  10980  faclbnd6  10983  facavg  10985  geolim2  12044  mertenslemi1  12067  eftabs  12188  efcllemp  12190  efaddlem  12206  eftlub  12222  oexpneg  12409  divalglemnn  12450  divalglemnqt  12452  divalglemeunn  12453  divalg2  12458  bitsfzolem  12486  bitsmod  12488  dfgcd2  12556  gcdmultiple  12562  gcdmultiplez  12563  dvdssqlem  12572  nn0seqcvgd  12584  mulgcddvds  12637  isprm5lem  12684  nn0sqrtelqelz  12749  nonsq  12750  phibndlem  12759  dfphi2  12763  modprm0  12798  pythagtriplem3  12811  pythagtriplem10  12813  pythagtriplem6  12814  pythagtriplem7  12815  pythagtriplem12  12819  pythagtriplem14  12821  pcge0  12857  pcprmpw2  12877  pcmptdvds  12889  fldivp1  12892  pcbc  12895  qexpz  12896  pockthlem  12900  pockthg  12901  mul4sqlem  12937  4sqlem12  12946  4sqlem14  12948  4sqlem16  12950  2expltfac  12983  ennnfoneleminc  13003  logbgcd1irraplemexp  15663  wilthlem1  15675  perfectlem2  15695  lgsval2lem  15710  lgsval4a  15722  gausslemma2dlem0c  15751  gausslemma2dlem0d  15752  lgseisenlem1  15770  lgseisenlem2  15771  lgsquadlem1  15777  2lgslem1a1  15786  2sqlem3  15817  2sqlem7  15821  2sqlem8  15823  vtxd0nedgbfi  16085