Theorem 2ap0 9226

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 9203	. 2 |- 2 e. RR
2		2pos 9224	. 2 |- 0 < 2
3	1, 2	gt0ap0ii 8798	1 |- 2 # 0

Syntax hints:   class class class wbr 4086   0cc0 8022   # cap 8751   2c2 9184

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8113  ax-resscn 8114  ax-1cn 8115  ax-1re 8116  ax-icn 8117  ax-addcl 8118  ax-addrcl 8119  ax-mulcl 8120  ax-mulrcl 8121  ax-addcom 8122  ax-mulcom 8123  ax-addass 8124  ax-mulass 8125  ax-distr 8126  ax-i2m1 8127  ax-0lt1 8128  ax-1rid 8129  ax-0id 8130  ax-rnegex 8131  ax-precex 8132  ax-cnre 8133  ax-pre-ltirr 8134  ax-pre-lttrn 8136  ax-pre-apti 8137  ax-pre-ltadd 8138  ax-pre-mulgt0 8139

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-pnf 8206  df-mnf 8207  df-ltxr 8209  df-sub 8342  df-neg 8343  df-reap 8745  df-ap 8752  df-2 9192

This theorem is referenced by:  2div2e1  9266  4d2e2  9294  halfre  9347  1mhlfehlf  9352  halfpm6th  9354  2muliap0  9358  halfcl  9360  rehalfcl  9361  half0  9362  2halves  9363  halfaddsub  9368  subhalfhalf  9369  xp1d2m1eqxm1d2  9387  div4p1lem1div2  9388  zneo  9571  nneoor  9572  nneo  9573  zeo  9575  zeo2  9576  halfthird  9743  qbtwnrelemcalc  10505  2tnp1ge0ge0  10551  fldiv4lem1div2  10557  zesq  10910  sqoddm1div8  10945  faclbnd2  10994  crre  11408  addcj  11442  resqrexlemover  11561  resqrexlemcalc1  11565  resqrexlemcvg  11570  maxabslemab  11757  max0addsup  11770  minabs  11787  bdtri  11791  arisum  12049  arisum2  12050  geo2sum  12065  geo2lim  12067  geoihalfsum  12073  ege2le3  12222  efgt0  12235  tanval2ap  12264  tanval3ap  12265  efi4p  12268  efival  12283  cosadd  12288  sinmul  12295  cosmul  12296  sin01bnd  12308  cos01bnd  12309  sin02gt0  12315  odd2np1  12424  mulsucdiv2z  12436  ltoddhalfle  12444  halfleoddlt  12445  nn0enne  12453  nn0o  12458  flodddiv4  12487  flodddiv4t2lthalf  12490  bitsp1e  12503  bitsp1o  12504  bitsinv1lem  12512  6lcm4e12  12649  sqrt2irrlem  12723  sqrt2irr  12724  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem15  12841  pythagtriplem16  12842  pythagtriplem17  12843  4sqlem7  12947  4sqlem10  12950  4sqlem19  12972  oddennn  13003  evenennn  13004  maxcncf  15329  mincncf  15330  coscn  15484  sinhalfpilem  15505  cospi  15514  ptolemy  15538  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  cosq23lt0  15547  coseq00topi  15549  tangtx  15552  sincos4thpi  15554  sincos6thpi  15556  sincos3rdpi  15557  pigt3  15558  abssinper  15560  coskpi  15562  logsqrt  15637  mersenne  15711  lgslem1  15719  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem3  15782  lgseisenlem1  15789  lgseisenlem3  15791  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem1  15800  lgsquad2lem2  15801  2lgslem1a1  15805  2lgslem1a2  15806  2lgslem1b  15808  2lgslem1c  15809  2lgslem3a  15812  2lgslem3b  15813  2lgslem3d  15815  apdifflemr  16587  apdiff  16588