Theorem 2ap0 9329

Description: The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)

Assertion

Ref	Expression
2ap0	⊢ 2 # 0

Proof of Theorem 2ap0

Step	Hyp	Ref	Expression
1		2re 9306	. 2 ⊢ 2 ∈ ℝ
2		2pos 9327	. 2 ⊢ 0 < 2
3	1, 2	gt0ap0ii 8901	1 ⊢ 2 # 0

Syntax hints:   class class class wbr 4108  0cc0 8126   # cap 8854  2c2 9287

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-cnex 8217  ax-resscn 8218  ax-1cn 8219  ax-1re 8220  ax-icn 8221  ax-addcl 8222  ax-addrcl 8223  ax-mulcl 8224  ax-mulrcl 8225  ax-addcom 8226  ax-mulcom 8227  ax-addass 8228  ax-mulass 8229  ax-distr 8230  ax-i2m1 8231  ax-0lt1 8232  ax-1rid 8233  ax-0id 8234  ax-rnegex 8235  ax-precex 8236  ax-cnre 8237  ax-pre-ltirr 8238  ax-pre-lttrn 8240  ax-pre-apti 8241  ax-pre-ltadd 8242  ax-pre-mulgt0 8243

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2814  df-sbc 3042  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-iota 5311  df-fun 5353  df-fv 5359  df-riota 6002  df-ov 6052  df-oprab 6053  df-mpo 6054  df-pnf 8309  df-mnf 8310  df-ltxr 8312  df-sub 8445  df-neg 8446  df-reap 8848  df-ap 8855  df-2 9295

This theorem is referenced by:  2div2e1  9369  4d2e2  9397  halfre  9450  1mhlfehlf  9455  halfpm6th  9457  2muliap0  9461  halfcl  9463  rehalfcl  9464  half0  9465  2halves  9466  halfaddsub  9471  subhalfhalf  9472  xp1d2m1eqxm1d2  9490  div4p1lem1div2  9491  zneo  9678  nneoor  9679  nneo  9680  zeo  9682  zeo2  9683  halfthird  9850  qbtwnrelemcalc  10614  2tnp1ge0ge0  10660  fldiv4lem1div2  10666  zesq  11019  sqoddm1div8  11054  faclbnd2  11103  crre  11538  addcj  11572  resqrexlemover  11691  resqrexlemcalc1  11695  resqrexlemcvg  11700  maxabslemab  11887  max0addsup  11900  minabs  11917  bdtri  11921  arisum  12180  arisum2  12181  geo2sum  12196  geo2lim  12198  geoihalfsum  12204  ege2le3  12353  efgt0  12366  tanval2ap  12395  tanval3ap  12396  efi4p  12399  efival  12414  cosadd  12419  sinmul  12426  cosmul  12427  sin01bnd  12439  cos01bnd  12440  sin02gt0  12446  odd2np1  12555  mulsucdiv2z  12567  ltoddhalfle  12575  halfleoddlt  12576  nn0enne  12584  nn0o  12589  flodddiv4  12618  flodddiv4t2lthalf  12621  bitsp1e  12634  bitsp1o  12635  bitsinv1lem  12643  6lcm4e12  12780  sqrt2irrlem  12854  sqrt2irr  12855  pythagtriplem12  12969  pythagtriplem14  12971  pythagtriplem15  12972  pythagtriplem16  12973  pythagtriplem17  12974  4sqlem7  13078  4sqlem10  13081  4sqlem19  13103  oddennn  13135  evenennn  13136  maxcncf  15472  mincncf  15473  coscn  15627  sinhalfpilem  15648  cospi  15657  ptolemy  15681  sincosq3sgn  15685  sincosq4sgn  15686  sinq12gt0  15687  cosq23lt0  15690  coseq00topi  15692  tangtx  15695  sincos4thpi  15697  sincos6thpi  15699  sincos3rdpi  15700  pigt3  15701  abssinper  15703  coskpi  15705  logsqrt  15780  mersenne  15857  lgslem1  15865  gausslemma2dlem1a  15923  gausslemma2dlem1f1o  15925  gausslemma2dlem3  15928  lgseisenlem1  15935  lgseisenlem3  15937  lgsquadlem1  15942  lgsquadlem2  15943  lgsquad2lem1  15946  lgsquad2lem2  15947  2lgslem1a1  15951  2lgslem1a2  15952  2lgslem1b  15954  2lgslem1c  15955  2lgslem3a  15958  2lgslem3b  15959  2lgslem3d  15961  apdifflemr  16823  apdiff  16824  qdiff  16825