Theorem 2ap0 9077

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 9054	. 2 |- 2 e. RR
2		2pos 9075	. 2 |- 0 < 2
3	1, 2	gt0ap0ii 8649	1 |- 2 # 0

Syntax hints:   class class class wbr 4030   0cc0 7874   # cap 8602   2c2 9035

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-mulrcl 7973  ax-addcom 7974  ax-mulcom 7975  ax-addass 7976  ax-mulass 7977  ax-distr 7978  ax-i2m1 7979  ax-0lt1 7980  ax-1rid 7981  ax-0id 7982  ax-rnegex 7983  ax-precex 7984  ax-cnre 7985  ax-pre-ltirr 7986  ax-pre-lttrn 7988  ax-pre-apti 7989  ax-pre-ltadd 7990  ax-pre-mulgt0 7991

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-pnf 8058  df-mnf 8059  df-ltxr 8061  df-sub 8194  df-neg 8195  df-reap 8596  df-ap 8603  df-2 9043

This theorem is referenced by:  2div2e1  9117  4d2e2  9145  halfre  9198  1mhlfehlf  9203  halfpm6th  9205  2muliap0  9209  halfcl  9211  rehalfcl  9212  half0  9213  2halves  9214  halfaddsub  9219  subhalfhalf  9220  xp1d2m1eqxm1d2  9238  div4p1lem1div2  9239  zneo  9421  nneoor  9422  nneo  9423  zeo  9425  zeo2  9426  halfthird  9593  qbtwnrelemcalc  10327  2tnp1ge0ge0  10373  fldiv4lem1div2  10379  zesq  10732  sqoddm1div8  10767  faclbnd2  10816  crre  11004  addcj  11038  resqrexlemover  11157  resqrexlemcalc1  11161  resqrexlemcvg  11166  maxabslemab  11353  max0addsup  11366  minabs  11382  bdtri  11386  arisum  11644  arisum2  11645  geo2sum  11660  geo2lim  11662  geoihalfsum  11668  ege2le3  11817  efgt0  11830  tanval2ap  11859  tanval3ap  11860  efi4p  11863  efival  11878  cosadd  11883  sinmul  11890  cosmul  11891  sin01bnd  11903  cos01bnd  11904  sin02gt0  11910  odd2np1  12017  mulsucdiv2z  12029  ltoddhalfle  12037  halfleoddlt  12038  nn0enne  12046  nn0o  12051  flodddiv4  12078  flodddiv4t2lthalf  12081  6lcm4e12  12228  sqrt2irrlem  12302  sqrt2irr  12303  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem15  12419  pythagtriplem16  12420  pythagtriplem17  12421  4sqlem7  12525  4sqlem10  12528  4sqlem19  12550  oddennn  12552  evenennn  12553  maxcncf  14794  mincncf  14795  coscn  14946  sinhalfpilem  14967  cospi  14976  ptolemy  15000  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  cosq23lt0  15009  coseq00topi  15011  tangtx  15014  sincos4thpi  15016  sincos6thpi  15018  sincos3rdpi  15019  pigt3  15020  abssinper  15022  coskpi  15024  logsqrt  15098  lgslem1  15157  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem3  15220  lgseisenlem1  15227  lgseisenlem3  15229  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem1  15238  lgsquad2lem2  15239  2lgslem1a1  15243  2lgslem1a2  15244  2lgslem1b  15246  2lgslem1c  15247  2lgslem3a  15250  2lgslem3b  15251  2lgslem3d  15253  apdifflemr  15607  apdiff  15608