Theorem gt0ap0d 8811

Description: Positive implies apart from zero. Because of the way we define #, A must be an element of RR, not just RR*. (Contributed by Jim Kingdon, 27-Feb-2020.)

Hypotheses

Ref	Expression
gt0ap0d.1	|- ( ph -> A e. RR )
gt0ap0d.2	|- ( ph -> 0 < A )

Assertion

Ref	Expression
gt0ap0d	|- ( ph -> A # 0 )

Proof of Theorem gt0ap0d

Step	Hyp	Ref	Expression
1		gt0ap0d.1	. 2 |- ( ph -> A e. RR )
2		gt0ap0d.2	. 2 |- ( ph -> 0 < A )
3		gt0ap0 8808	. 2 |- ( ( A e. RR /\ 0 < A ) -> A # 0 )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> A # 0 )

Syntax hints:   -> wi 4   e. wcel 2201   class class class wbr 4087   RRcr 8033   0cc0 8034   < clt 8216   # cap 8763

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 2203  ax-14 2204  ax-ext 2212  ax-sep 4206  ax-pow 4263  ax-pr 4298  ax-un 4529  ax-setind 4634  ax-cnex 8125  ax-resscn 8126  ax-1cn 8127  ax-1re 8128  ax-icn 8129  ax-addcl 8130  ax-addrcl 8131  ax-mulcl 8132  ax-mulrcl 8133  ax-addcom 8134  ax-mulcom 8135  ax-addass 8136  ax-mulass 8137  ax-distr 8138  ax-i2m1 8139  ax-0lt1 8140  ax-1rid 8141  ax-0id 8142  ax-rnegex 8143  ax-precex 8144  ax-cnre 8145  ax-pre-ltirr 8146  ax-pre-lttrn 8148  ax-pre-apti 8149  ax-pre-ltadd 8150  ax-pre-mulgt0 8151

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-nel 2497  df-ral 2514  df-rex 2515  df-reu 2516  df-rab 2518  df-v 2803  df-sbc 3031  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3653  df-sn 3674  df-pr 3675  df-op 3677  df-uni 3893  df-br 4088  df-opab 4150  df-id 4389  df-xp 4730  df-rel 4731  df-cnv 4732  df-co 4733  df-dm 4734  df-iota 5285  df-fun 5327  df-fv 5333  df-riota 5973  df-ov 6023  df-oprab 6024  df-mpo 6025  df-pnf 8218  df-mnf 8219  df-ltxr 8221  df-sub 8354  df-neg 8355  df-reap 8757  df-ap 8764

This theorem is referenced by:  prodgt0gt0  9033  prodgt0  9034  ltdiv1  9050  ltmuldiv  9056  ledivmul  9059  lt2mul2div  9061  lemuldiv  9063  ltrec  9065  lerec  9066  ltrec1  9070  lerec2  9071  ledivdiv  9072  lediv2  9073  ltdiv23  9074  lediv23  9075  lediv12a  9076  recp1lt1  9081  ledivp1  9085  nnap0  9174  rpap0  9907  modq0  10594  mulqmod0  10595  negqmod0  10596  modqlt  10598  modqdiffl  10600  modqid0  10615  modqcyc  10624  modqmuladdnn0  10633  q2txmodxeq0  10649  modqdi  10657  ltexp2a  10856  leexp2a  10857  expnbnd  10928  expcanlem  10980  expcan  10981  resqrexlemover  11590  resqrexlemcalc1  11594  resqrexlemcalc2  11595  ltabs  11667  divcnv  12078  expcnvre  12084  georeclim  12094  geoisumr  12099  cvgratnnlembern  12104  cvgratnnlemfm  12110  cvgratz  12113  cnopnap  15361  reeff1oleme  15522  tangtx  15588  mersenne  15747  perfectlem2  15750  lgsquadlem1  15832  lgsquadlem2  15833  trirec0  16710  ltlenmkv  16737