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 ∈ ℝ
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  11422  addcj  11456  resqrexlemover  11575  resqrexlemcalc1  11579  resqrexlemcvg  11584  maxabslemab  11771  max0addsup  11784  minabs  11801  bdtri  11805  arisum  12064  arisum2  12065  geo2sum  12080  geo2lim  12082  geoihalfsum  12088  ege2le3  12237  efgt0  12250  tanval2ap  12279  tanval3ap  12280  efi4p  12283  efival  12298  cosadd  12303  sinmul  12310  cosmul  12311  sin01bnd  12323  cos01bnd  12324  sin02gt0  12330  odd2np1  12439  mulsucdiv2z  12451  ltoddhalfle  12459  halfleoddlt  12460  nn0enne  12468  nn0o  12473  flodddiv4  12502  flodddiv4t2lthalf  12505  bitsp1e  12518  bitsp1o  12519  bitsinv1lem  12527  6lcm4e12  12664  sqrt2irrlem  12738  sqrt2irr  12739  pythagtriplem12  12853  pythagtriplem14  12855  pythagtriplem15  12856  pythagtriplem16  12857  pythagtriplem17  12858  4sqlem7  12962  4sqlem10  12965  4sqlem19  12987  oddennn  13018  evenennn  13019  maxcncf  15345  mincncf  15346  coscn  15500  sinhalfpilem  15521  cospi  15530  ptolemy  15554  sincosq3sgn  15558  sincosq4sgn  15559  sinq12gt0  15560  cosq23lt0  15563  coseq00topi  15565  tangtx  15568  sincos4thpi  15570  sincos6thpi  15572  sincos3rdpi  15573  pigt3  15574  abssinper  15576  coskpi  15578  logsqrt  15653  mersenne  15727  lgslem1  15735  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  gausslemma2dlem3  15798  lgseisenlem1  15805  lgseisenlem3  15807  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem1  15816  lgsquad2lem2  15817  2lgslem1a1  15821  2lgslem1a2  15822  2lgslem1b  15824  2lgslem1c  15825  2lgslem3a  15828  2lgslem3b  15829  2lgslem3d  15831  apdifflemr  16677  apdiff  16678