Theorem 2ap0 9083

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 9060	. 2 |- 2 e. RR
2		2pos 9081	. 2 |- 0 < 2
3	1, 2	gt0ap0ii 8655	1 |- 2 # 0

Syntax hints:   class class class wbr 4033   0cc0 7879   # cap 8608   2c2 9041

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-mulrcl 7978  ax-addcom 7979  ax-mulcom 7980  ax-addass 7981  ax-mulass 7982  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-1rid 7986  ax-0id 7987  ax-rnegex 7988  ax-precex 7989  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-lttrn 7993  ax-pre-apti 7994  ax-pre-ltadd 7995  ax-pre-mulgt0 7996

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-opab 4095  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-iota 5219  df-fun 5260  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-pnf 8063  df-mnf 8064  df-ltxr 8066  df-sub 8199  df-neg 8200  df-reap 8602  df-ap 8609  df-2 9049

This theorem is referenced by:  2div2e1  9123  4d2e2  9151  halfre  9204  1mhlfehlf  9209  halfpm6th  9211  2muliap0  9215  halfcl  9217  rehalfcl  9218  half0  9219  2halves  9220  halfaddsub  9225  subhalfhalf  9226  xp1d2m1eqxm1d2  9244  div4p1lem1div2  9245  zneo  9427  nneoor  9428  nneo  9429  zeo  9431  zeo2  9432  halfthird  9599  qbtwnrelemcalc  10345  2tnp1ge0ge0  10391  fldiv4lem1div2  10397  zesq  10750  sqoddm1div8  10785  faclbnd2  10834  crre  11022  addcj  11056  resqrexlemover  11175  resqrexlemcalc1  11179  resqrexlemcvg  11184  maxabslemab  11371  max0addsup  11384  minabs  11401  bdtri  11405  arisum  11663  arisum2  11664  geo2sum  11679  geo2lim  11681  geoihalfsum  11687  ege2le3  11836  efgt0  11849  tanval2ap  11878  tanval3ap  11879  efi4p  11882  efival  11897  cosadd  11902  sinmul  11909  cosmul  11910  sin01bnd  11922  cos01bnd  11923  sin02gt0  11929  odd2np1  12038  mulsucdiv2z  12050  ltoddhalfle  12058  halfleoddlt  12059  nn0enne  12067  nn0o  12072  flodddiv4  12101  flodddiv4t2lthalf  12104  bitsp1e  12116  bitsp1o  12117  6lcm4e12  12255  sqrt2irrlem  12329  sqrt2irr  12330  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem15  12447  pythagtriplem16  12448  pythagtriplem17  12449  4sqlem7  12553  4sqlem10  12556  4sqlem19  12578  oddennn  12609  evenennn  12610  maxcncf  14851  mincncf  14852  coscn  15006  sinhalfpilem  15027  cospi  15036  ptolemy  15060  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  cosq23lt0  15069  coseq00topi  15071  tangtx  15074  sincos4thpi  15076  sincos6thpi  15078  sincos3rdpi  15079  pigt3  15080  abssinper  15082  coskpi  15084  logsqrt  15159  mersenne  15233  lgslem1  15241  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem3  15304  lgseisenlem1  15311  lgseisenlem3  15313  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem1  15322  lgsquad2lem2  15323  2lgslem1a1  15327  2lgslem1a2  15328  2lgslem1b  15330  2lgslem1c  15331  2lgslem3a  15334  2lgslem3b  15335  2lgslem3d  15337  apdifflemr  15691  apdiff  15692