Theorem 2ap0 9236

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 9213	. 2 |- 2 e. RR
2		2pos 9234	. 2 |- 0 < 2
3	1, 2	gt0ap0ii 8808	1 |- 2 # 0

Syntax hints:   class class class wbr 4088   0cc0 8032   # cap 8761   2c2 9194

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-mulrcl 8131  ax-addcom 8132  ax-mulcom 8133  ax-addass 8134  ax-mulass 8135  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-1rid 8139  ax-0id 8140  ax-rnegex 8141  ax-precex 8142  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-lttrn 8146  ax-pre-apti 8147  ax-pre-ltadd 8148  ax-pre-mulgt0 8149

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-ltxr 8219  df-sub 8352  df-neg 8353  df-reap 8755  df-ap 8762  df-2 9202

This theorem is referenced by:  2div2e1  9276  4d2e2  9304  halfre  9357  1mhlfehlf  9362  halfpm6th  9364  2muliap0  9368  halfcl  9370  rehalfcl  9371  half0  9372  2halves  9373  halfaddsub  9378  subhalfhalf  9379  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  zneo  9581  nneoor  9582  nneo  9583  zeo  9585  zeo2  9586  halfthird  9753  qbtwnrelemcalc  10516  2tnp1ge0ge0  10562  fldiv4lem1div2  10568  zesq  10921  sqoddm1div8  10956  faclbnd2  11005  crre  11435  addcj  11469  resqrexlemover  11588  resqrexlemcalc1  11592  resqrexlemcvg  11597  maxabslemab  11784  max0addsup  11797  minabs  11814  bdtri  11818  arisum  12077  arisum2  12078  geo2sum  12093  geo2lim  12095  geoihalfsum  12101  ege2le3  12250  efgt0  12263  tanval2ap  12292  tanval3ap  12293  efi4p  12296  efival  12311  cosadd  12316  sinmul  12323  cosmul  12324  sin01bnd  12336  cos01bnd  12337  sin02gt0  12343  odd2np1  12452  mulsucdiv2z  12464  ltoddhalfle  12472  halfleoddlt  12473  nn0enne  12481  nn0o  12486  flodddiv4  12515  flodddiv4t2lthalf  12518  bitsp1e  12531  bitsp1o  12532  bitsinv1lem  12540  6lcm4e12  12677  sqrt2irrlem  12751  sqrt2irr  12752  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem15  12869  pythagtriplem16  12870  pythagtriplem17  12871  4sqlem7  12975  4sqlem10  12978  4sqlem19  13000  oddennn  13031  evenennn  13032  maxcncf  15358  mincncf  15359  coscn  15513  sinhalfpilem  15534  cospi  15543  ptolemy  15567  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  cosq23lt0  15576  coseq00topi  15578  tangtx  15581  sincos4thpi  15583  sincos6thpi  15585  sincos3rdpi  15586  pigt3  15587  abssinper  15589  coskpi  15591  logsqrt  15666  mersenne  15740  lgslem1  15748  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem3  15811  lgseisenlem1  15818  lgseisenlem3  15820  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem1  15829  lgsquad2lem2  15830  2lgslem1a1  15834  2lgslem1a2  15835  2lgslem1b  15837  2lgslem1c  15838  2lgslem3a  15841  2lgslem3b  15842  2lgslem3d  15844  apdifflemr  16702  apdiff  16703  qdiff  16704