Theorem nn0ge0d 8447

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

Syntax hints:   -> wi 4   e. wcel 1434   class class class wbr 3806   0cc0 7079   <_ cle 7252   NN0cn0 8391

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3917  ax-pow 3969  ax-pr 3993  ax-un 4217  ax-setind 4309  ax-cnex 7165  ax-resscn 7166  ax-1cn 7167  ax-1re 7168  ax-icn 7169  ax-addcl 7170  ax-addrcl 7171  ax-mulcl 7172  ax-i2m1 7179  ax-0lt1 7180  ax-0id 7182  ax-rnegex 7183  ax-pre-ltirr 7186  ax-pre-ltwlin 7187  ax-pre-lttrn 7188  ax-pre-ltadd 7190

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-rab 2362  df-v 2612  df-dif 2985  df-un 2987  df-in 2989  df-ss 2996  df-pw 3403  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-int 3658  df-br 3807  df-opab 3861  df-xp 4398  df-cnv 4400  df-iota 4918  df-fv 4961  df-ov 5567  df-pnf 7253  df-mnf 7254  df-xr 7255  df-ltxr 7256  df-le 7257  df-inn 8143  df-n0 8392

This theorem is referenced by:  flqmulnn0  9417  zmodfz  9464  addmodid  9490  modifeq2int  9504  modaddmodlo  9506  modsumfzodifsn  9514  addmodlteq  9516  expinnval  9612  nn0le2msqd  9779  facwordi  9800  faclbnd  9801  faclbnd6  9804  facavg  9806  oexpneg  10468  divalglemnn  10509  divalglemnqt  10511  divalglemeunn  10512  divalg2  10517  dfgcd2  10594  gcdmultiple  10600  gcdmultiplez  10601  dvdssqlem  10610  nn0seqcvgd  10614  mulgcddvds  10667  nn0sqrtelqelz  10775  nonsq  10776  phibndlem  10783  dfphi2  10787