Theorem 2ap0 8909

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 8886	. 2 ⊢ 2 ∈ ℝ
2		2pos 8907	. 2 ⊢ 0 < 2
3	1, 2	gt0ap0ii 8486	1 ⊢ 2 # 0

Syntax hints:   class class class wbr 3965  0cc0 7715   # cap 8439  2c2 8867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-cnex 7806  ax-resscn 7807  ax-1cn 7808  ax-1re 7809  ax-icn 7810  ax-addcl 7811  ax-addrcl 7812  ax-mulcl 7813  ax-mulrcl 7814  ax-addcom 7815  ax-mulcom 7816  ax-addass 7817  ax-mulass 7818  ax-distr 7819  ax-i2m1 7820  ax-0lt1 7821  ax-1rid 7822  ax-0id 7823  ax-rnegex 7824  ax-precex 7825  ax-cnre 7826  ax-pre-ltirr 7827  ax-pre-lttrn 7829  ax-pre-apti 7830  ax-pre-ltadd 7831  ax-pre-mulgt0 7832

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-id 4252  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-iota 5132  df-fun 5169  df-fv 5175  df-riota 5774  df-ov 5821  df-oprab 5822  df-mpo 5823  df-pnf 7897  df-mnf 7898  df-ltxr 7900  df-sub 8031  df-neg 8032  df-reap 8433  df-ap 8440  df-2 8875

This theorem is referenced by:  2div2e1  8948  4d2e2  8976  halfre  9029  1mhlfehlf  9034  halfpm6th  9036  2muliap0  9040  halfcl  9042  rehalfcl  9043  half0  9044  2halves  9045  halfaddsub  9050  xp1d2m1eqxm1d2  9068  div4p1lem1div2  9069  zneo  9248  nneoor  9249  nneo  9250  zeo  9252  zeo2  9253  halfthird  9420  qbtwnrelemcalc  10137  2tnp1ge0ge0  10182  zesq  10518  sqoddm1div8  10553  faclbnd2  10598  crre  10739  addcj  10773  resqrexlemover  10892  resqrexlemcalc1  10896  resqrexlemcvg  10901  maxabslemab  11088  max0addsup  11101  minabs  11117  bdtri  11121  arisum  11377  arisum2  11378  geo2sum  11393  geo2lim  11395  geoihalfsum  11401  ege2le3  11550  efgt0  11563  tanval2ap  11592  tanval3ap  11593  efi4p  11596  efival  11611  cosadd  11616  sinmul  11623  cosmul  11624  sin01bnd  11636  cos01bnd  11637  sin02gt0  11642  odd2np1  11745  mulsucdiv2z  11757  ltoddhalfle  11765  halfleoddlt  11766  nn0enne  11774  nn0o  11779  flodddiv4  11806  flodddiv4t2lthalf  11809  6lcm4e12  11944  sqrt2irrlem  12015  sqrt2irr  12016  oddennn  12093  evenennn  12094  coscn  13051  sinhalfpilem  13072  cospi  13081  ptolemy  13105  sincosq3sgn  13109  sincosq4sgn  13110  sinq12gt0  13111  cosq23lt0  13114  coseq00topi  13116  tangtx  13119  sincos4thpi  13121  sincos6thpi  13123  sincos3rdpi  13124  pigt3  13125  abssinper  13127  coskpi  13129  logsqrt  13203  apdifflemr  13580  apdiff  13581