Theorem 2ap0 9191

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 9168	. 2 ⊢ 2 ∈ ℝ
2		2pos 9189	. 2 ⊢ 0 < 2
3	1, 2	gt0ap0ii 8763	1 ⊢ 2 # 0

Syntax hints:   class class class wbr 4082  0cc0 7987   # cap 8716  2c2 9149

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 4201  ax-pow 4257  ax-pr 4292  ax-un 4521  ax-setind 4626  ax-cnex 8078  ax-resscn 8079  ax-1cn 8080  ax-1re 8081  ax-icn 8082  ax-addcl 8083  ax-addrcl 8084  ax-mulcl 8085  ax-mulrcl 8086  ax-addcom 8087  ax-mulcom 8088  ax-addass 8089  ax-mulass 8090  ax-distr 8091  ax-i2m1 8092  ax-0lt1 8093  ax-1rid 8094  ax-0id 8095  ax-rnegex 8096  ax-precex 8097  ax-cnre 8098  ax-pre-ltirr 8099  ax-pre-lttrn 8101  ax-pre-apti 8102  ax-pre-ltadd 8103  ax-pre-mulgt0 8104

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 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-id 4381  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-iota 5274  df-fun 5316  df-fv 5322  df-riota 5947  df-ov 5997  df-oprab 5998  df-mpo 5999  df-pnf 8171  df-mnf 8172  df-ltxr 8174  df-sub 8307  df-neg 8308  df-reap 8710  df-ap 8717  df-2 9157

This theorem is referenced by:  2div2e1  9231  4d2e2  9259  halfre  9312  1mhlfehlf  9317  halfpm6th  9319  2muliap0  9323  halfcl  9325  rehalfcl  9326  half0  9327  2halves  9328  halfaddsub  9333  subhalfhalf  9334  xp1d2m1eqxm1d2  9352  div4p1lem1div2  9353  zneo  9536  nneoor  9537  nneo  9538  zeo  9540  zeo2  9541  halfthird  9708  qbtwnrelemcalc  10462  2tnp1ge0ge0  10508  fldiv4lem1div2  10514  zesq  10867  sqoddm1div8  10902  faclbnd2  10951  crre  11354  addcj  11388  resqrexlemover  11507  resqrexlemcalc1  11511  resqrexlemcvg  11516  maxabslemab  11703  max0addsup  11716  minabs  11733  bdtri  11737  arisum  11995  arisum2  11996  geo2sum  12011  geo2lim  12013  geoihalfsum  12019  ege2le3  12168  efgt0  12181  tanval2ap  12210  tanval3ap  12211  efi4p  12214  efival  12229  cosadd  12234  sinmul  12241  cosmul  12242  sin01bnd  12254  cos01bnd  12255  sin02gt0  12261  odd2np1  12370  mulsucdiv2z  12382  ltoddhalfle  12390  halfleoddlt  12391  nn0enne  12399  nn0o  12404  flodddiv4  12433  flodddiv4t2lthalf  12436  bitsp1e  12449  bitsp1o  12450  bitsinv1lem  12458  6lcm4e12  12595  sqrt2irrlem  12669  sqrt2irr  12670  pythagtriplem12  12784  pythagtriplem14  12786  pythagtriplem15  12787  pythagtriplem16  12788  pythagtriplem17  12789  4sqlem7  12893  4sqlem10  12896  4sqlem19  12918  oddennn  12949  evenennn  12950  maxcncf  15274  mincncf  15275  coscn  15429  sinhalfpilem  15450  cospi  15459  ptolemy  15483  sincosq3sgn  15487  sincosq4sgn  15488  sinq12gt0  15489  cosq23lt0  15492  coseq00topi  15494  tangtx  15497  sincos4thpi  15499  sincos6thpi  15501  sincos3rdpi  15502  pigt3  15503  abssinper  15505  coskpi  15507  logsqrt  15582  mersenne  15656  lgslem1  15664  gausslemma2dlem1a  15722  gausslemma2dlem1f1o  15724  gausslemma2dlem3  15727  lgseisenlem1  15734  lgseisenlem3  15736  lgsquadlem1  15741  lgsquadlem2  15742  lgsquad2lem1  15745  lgsquad2lem2  15746  2lgslem1a1  15750  2lgslem1a2  15751  2lgslem1b  15753  2lgslem1c  15754  2lgslem3a  15757  2lgslem3b  15758  2lgslem3d  15760  apdifflemr  16346  apdiff  16347