Theorem nn0ge0d 9218

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 9187	. 2 |- ( A e. NN0 -> 0 <_ A )
3	1, 2	syl 14	1 |- ( ph -> 0 <_ A )

Syntax hints:   -> wi 4   e. wcel 2148   class class class wbr 4000   0cc0 7799   <_ cle 7980   NN0cn0 9162

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7890  ax-resscn 7891  ax-1cn 7892  ax-1re 7893  ax-icn 7894  ax-addcl 7895  ax-addrcl 7896  ax-mulcl 7897  ax-i2m1 7904  ax-0lt1 7905  ax-0id 7907  ax-rnegex 7908  ax-pre-ltirr 7911  ax-pre-ltwlin 7912  ax-pre-lttrn 7913  ax-pre-ltadd 7915

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-xp 4629  df-cnv 4631  df-iota 5174  df-fv 5220  df-ov 5872  df-pnf 7981  df-mnf 7982  df-xr 7983  df-ltxr 7984  df-le 7985  df-inn 8906  df-n0 9163

This theorem is referenced by:  flqmulnn0  10282  zmodfz  10329  addmodid  10355  modifeq2int  10369  modaddmodlo  10371  modsumfzodifsn  10379  addmodlteq  10381  expnnval  10506  nn0le2msqd  10680  facwordi  10701  faclbnd  10702  faclbnd6  10705  facavg  10707  geolim2  11501  mertenslemi1  11524  eftabs  11645  efcllemp  11647  efaddlem  11663  eftlub  11679  oexpneg  11862  divalglemnn  11903  divalglemnqt  11905  divalglemeunn  11906  divalg2  11911  dfgcd2  11995  gcdmultiple  12001  gcdmultiplez  12002  dvdssqlem  12011  nn0seqcvgd  12021  mulgcddvds  12074  isprm5lem  12121  nn0sqrtelqelz  12186  nonsq  12187  phibndlem  12196  dfphi2  12200  modprm0  12234  pythagtriplem3  12247  pythagtriplem10  12249  pythagtriplem6  12250  pythagtriplem7  12251  pythagtriplem12  12255  pythagtriplem14  12257  pcge0  12292  pcprmpw2  12312  pcmptdvds  12323  fldivp1  12326  pcbc  12329  qexpz  12330  pockthlem  12334  pockthg  12335  mul4sqlem  12371  ennnfoneleminc  12392  logbgcd1irraplemexp  14046  lgsval2lem  14071  lgsval4a  14083  2sqlem3  14113  2sqlem7  14117  2sqlem8  14119