Theorem 2ap0 9229

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 9206	. 2 ⊢ 2 ∈ ℝ
2		2pos 9227	. 2 ⊢ 0 < 2
3	1, 2	gt0ap0ii 8801	1 ⊢ 2 # 0

Syntax hints:   class class class wbr 4086  0cc0 8025   # cap 8754  2c2 9187

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 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8116  ax-resscn 8117  ax-1cn 8118  ax-1re 8119  ax-icn 8120  ax-addcl 8121  ax-addrcl 8122  ax-mulcl 8123  ax-mulrcl 8124  ax-addcom 8125  ax-mulcom 8126  ax-addass 8127  ax-mulass 8128  ax-distr 8129  ax-i2m1 8130  ax-0lt1 8131  ax-1rid 8132  ax-0id 8133  ax-rnegex 8134  ax-precex 8135  ax-cnre 8136  ax-pre-ltirr 8137  ax-pre-lttrn 8139  ax-pre-apti 8140  ax-pre-ltadd 8141  ax-pre-mulgt0 8142

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-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-pnf 8209  df-mnf 8210  df-ltxr 8212  df-sub 8345  df-neg 8346  df-reap 8748  df-ap 8755  df-2 9195

This theorem is referenced by:  2div2e1  9269  4d2e2  9297  halfre  9350  1mhlfehlf  9355  halfpm6th  9357  2muliap0  9361  halfcl  9363  rehalfcl  9364  half0  9365  2halves  9366  halfaddsub  9371  subhalfhalf  9372  xp1d2m1eqxm1d2  9390  div4p1lem1div2  9391  zneo  9574  nneoor  9575  nneo  9576  zeo  9578  zeo2  9579  halfthird  9746  qbtwnrelemcalc  10508  2tnp1ge0ge0  10554  fldiv4lem1div2  10560  zesq  10913  sqoddm1div8  10948  faclbnd2  10997  crre  11411  addcj  11445  resqrexlemover  11564  resqrexlemcalc1  11568  resqrexlemcvg  11573  maxabslemab  11760  max0addsup  11773  minabs  11790  bdtri  11794  arisum  12052  arisum2  12053  geo2sum  12068  geo2lim  12070  geoihalfsum  12076  ege2le3  12225  efgt0  12238  tanval2ap  12267  tanval3ap  12268  efi4p  12271  efival  12286  cosadd  12291  sinmul  12298  cosmul  12299  sin01bnd  12311  cos01bnd  12312  sin02gt0  12318  odd2np1  12427  mulsucdiv2z  12439  ltoddhalfle  12447  halfleoddlt  12448  nn0enne  12456  nn0o  12461  flodddiv4  12490  flodddiv4t2lthalf  12493  bitsp1e  12506  bitsp1o  12507  bitsinv1lem  12515  6lcm4e12  12652  sqrt2irrlem  12726  sqrt2irr  12727  pythagtriplem12  12841  pythagtriplem14  12843  pythagtriplem15  12844  pythagtriplem16  12845  pythagtriplem17  12846  4sqlem7  12950  4sqlem10  12953  4sqlem19  12975  oddennn  13006  evenennn  13007  maxcncf  15332  mincncf  15333  coscn  15487  sinhalfpilem  15508  cospi  15517  ptolemy  15541  sincosq3sgn  15545  sincosq4sgn  15546  sinq12gt0  15547  cosq23lt0  15550  coseq00topi  15552  tangtx  15555  sincos4thpi  15557  sincos6thpi  15559  sincos3rdpi  15560  pigt3  15561  abssinper  15563  coskpi  15565  logsqrt  15640  mersenne  15714  lgslem1  15722  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  gausslemma2dlem3  15785  lgseisenlem1  15792  lgseisenlem3  15794  lgsquadlem1  15799  lgsquadlem2  15800  lgsquad2lem1  15803  lgsquad2lem2  15804  2lgslem1a1  15808  2lgslem1a2  15809  2lgslem1b  15811  2lgslem1c  15812  2lgslem3a  15815  2lgslem3b  15816  2lgslem3d  15818  apdifflemr  16601  apdiff  16602