Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
class class class wbr 5109 ℝcr 11058
0cc0 11059 < clt 11197
ℝ+crp 12923 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-br 5110 df-rp 12924 |
This theorem is referenced by: rpge0
12936 rpgecl
12951 0nrp
12958 rpgt0d
12968 addlelt
13037 0mod
13816 sgnrrp
14985 01sqrexlem2
15137 01sqrexlem4
15139 01sqrexlem6
15141 resqrex
15144 rpsqrtcl
15158 climconst
15434 rlimconst
15435 divrcnv
15745 rprisefaccl
15914 blcntrps
23788 blcntr
23789 stdbdmet
23895 stdbdmopn
23897 prdsxmslem2
23908 metustid
23933 nmoix
24116 metdseq0
24240 lebnumii
24352 itgulm
25790 pilem2
25834 cos02pilt1
25905 tanregt0
25918 logdmnrp
26019 cxple2
26075 asinneg
26259 asin1
26267 reasinsin
26269 atanbndlem
26298 atanbnd
26299 atan1
26301 rlimcnp
26338 chtrpcl
26547 ppiltx
26549 bposlem8
26662 pntlem3
26980 padicabvcxp
27003 0cnop
30970 0cnfn
30971 rpdp2cl
31794 xdivpnfrp
31845 pnfinf
32075 hgt750lem2
33329 taupilem1
35842 itg2gt0cn
36183 areacirclem1
36216 areacirclem4
36219 prdstotbnd
36303 prdsbnd2
36304 aks4d1p1p6
40580 irrapxlem3
41194 neglt
43609 xralrple2
43679 constlimc
43955 0cnv
44073 ioodvbdlimc1lem1
44262 fourierdlem103
44540 fourierdlem104
44541 etransclem18
44583 etransclem46
44611 hoidmvlelem3
44928 |