Theorem 2ap0 9407

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 9384	. 2 ⊢ 2 ∈ ℝ
2		2pos 9405	. 2 ⊢ 0 < 2
3	1, 2	gt0ap0ii 8965	1 ⊢ 2 # 0

This proof depends on syntax axioms:   class class class wbr 4131  0cc0 8186   # cap 8918  2c2 9365

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8277  ax-resscn 8278  ax-1cn 8279  ax-1re 8280  ax-icn 8281  ax-addcl 8282  ax-addrcl 8283  ax-mulcl 8284  ax-mulrcl 8285  ax-addcom 8286  ax-mulcom 8287  ax-addass 8288  ax-mulass 8289  ax-distr 8290  ax-i2m1 8291  ax-0lt1 8292  ax-1rid 8293  ax-0id 8294  ax-rnegex 8295  ax-precex 8296  ax-cnre 8297  ax-pre-ltirr 8298  ax-pre-lttrn 8300  ax-pre-apti 8301  ax-pre-ltadd 8302  ax-pre-mulgt0 8303

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-pnf 8369  df-mnf 8370  df-ltxr 8372  df-sub 8507  df-neg 8508  df-reap 8912  df-ap 8919  df-2 9373

This theorem is used by:  2div2e1  9447  4d2e2  9477  halfre  9530  1mhlfehlf  9535  halfpm6th  9537  2muliap0  9541  halfcl  9543  rehalfcl  9544  half0  9545  2halves  9546  halfaddsub  9551  subhalfhalf  9552  xp1d2m1eqxm1d2  9570  div4p1lem1div2  9571  zneo  9759  nneoor  9760  nneo  9761  zeo  9763  zeo2  9764  halfthird  9936  qbtwnrelemcalc  10708  2tnp1ge0ge0  10758  fldiv4lem1div2  10764  zesq  11118  sqoddm1div8  11153  faclbnd2  11203  crre  11645  addcj  11679  sq01  11683  resqrexlemover  11799  resqrexlemcalc1  11803  resqrexlemcvg  11808  maxabslemab  11996  max0addsup  12009  minabs  12027  bdtri  12032  arisum  12291  arisum2  12292  geo2sum  12307  geo2lim  12309  geoihalfsum  12315  ege2le3  12464  efgt0  12477  tanval2ap  12506  tanval3ap  12507  efi4p  12510  efival  12525  cosadd  12530  sinmul  12537  cosmul  12538  sin01bnd  12550  cos01bnd  12551  sin02gt0  12557  odd2np1  12666  mulsucdiv2z  12678  ltoddhalfle  12686  halfleoddlt  12687  nn0enne  12695  nn0o  12700  flodddiv4  12729  flodddiv4t2lthalf  12732  bitsp1e  12745  bitsp1o  12746  bitsinv1lem  12754  6lcm4e12  12891  sqrt2irrlem  12966  sqrt2irr  12967  pythagtriplem12  13084  pythagtriplem14  13086  pythagtriplem15  13087  pythagtriplem16  13088  pythagtriplem17  13089  4sqlem7  13193  4sqlem10  13196  4sqlem19  13218  oddennn  13342  evenennn  13343  maxcncf  15853  mincncf  15854  coscn  16008  sinhalfpilem  16030  cospi  16039  ptolemy  16063  sincosq3sgn  16067  sincosq4sgn  16068  sinq12gt0  16069  cosq23lt0  16072  coseq00topi  16074  tangtx  16077  sincos4thpi  16079  sincos6thpi  16081  sincos3rdpi  16082  pigt3  16083  abssinper  16085  coskpi  16087  sineq0re  16088  logsqrt  16170  log2tlbndlog2  16232  birthdaylog2  16240  ppiqub  16305  chtqub  16308  mersenne  16309  bcmax  16317  bclbnd  16319  bposlem9  16331  lgslem1  16336  gausslemma2dlem1a  16394  gausslemma2dlem1f1o  16396  gausslemma2dlem3  16399  lgseisenlem1  16406  lgseisenlem3  16408  lgsquadlem1  16413  lgsquadlem2  16414  lgsquad2lem1  16417  lgsquad2lem2  16418  2lgslem1a1  16422  2lgslem1a2  16423  2lgslem1b  16425  2lgslem1c  16426  2lgslem3a  16429  2lgslem3b  16430  2lgslem3d  16432  apdifflemr  17315  apdiff  17316  qdiff  17317