| Colors of
variables: wff
setvar class |
| Syntax hints:
= wceq 1539 ∈ wcel 2104
‘cfv 6544 (class class class)co 7413
ℝcr 11113 0cc0 11114
2c2 12273 4c4 12275
(,)cioo 13330 sincsin 16013
πcpi 16016 |
| This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7729 ax-inf2 9640 ax-cnex 11170 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-addrcl 11175 ax-mulcl 11176 ax-mulrcl 11177 ax-mulcom 11178 ax-addass 11179 ax-mulass 11180 ax-distr 11181 ax-i2m1 11182 ax-1ne0 11183 ax-1rid 11184 ax-rnegex 11185 ax-rrecex 11186 ax-cnre 11187 ax-pre-lttri 11188 ax-pre-lttrn 11189 ax-pre-ltadd 11190 ax-pre-mulgt0 11191 ax-pre-sup 11192 ax-addf 11193 ax-mulf 11194 |
| This theorem depends on definitions:
df-bi 206 df-an 395
df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7369 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7674 df-om 7860 df-1st 7979 df-2nd 7980 df-supp 8151 df-frecs 8270 df-wrecs 8301 df-recs 8375 df-rdg 8414 df-1o 8470 df-2o 8471 df-er 8707 df-map 8826 df-pm 8827 df-ixp 8896 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fsupp 9366 df-fi 9410 df-sup 9441 df-inf 9442 df-oi 9509 df-card 9938 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11452 df-neg 11453 df-div 11878 df-nn 12219 df-2 12281
df-3 12282 df-4 12283
df-5 12284 df-6 12285
df-7 12286 df-8 12287
df-9 12288 df-n0 12479 df-z 12565
df-dec 12684 df-uz 12829 df-q 12939
df-rp 12981 df-xneg 13098 df-xadd 13099 df-xmul 13100 df-ioo 13334 df-ioc 13335 df-ico 13336 df-icc 13337 df-fz 13491 df-fzo 13634 df-fl 13763 df-seq 13973 df-exp 14034 df-fac 14240 df-bc 14269 df-hash 14297 df-shft 15020 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-limsup 15421 df-clim 15438 df-rlim 15439 df-sum 15639 df-ef 16017 df-sin 16019 df-cos 16020 df-pi 16022 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17151 df-ress 17180 df-plusg 17216 df-mulr 17217 df-starv 17218 df-sca 17219 df-vsca 17220 df-ip 17221 df-tset 17222 df-ple 17223 df-ds 17225 df-unif 17226 df-hom 17227 df-cco 17228 df-rest 17374 df-topn 17375 df-0g 17393 df-gsum 17394 df-topgen 17395 df-pt 17396 df-prds 17399 df-xrs 17454 df-qtop 17459 df-imas 17460 df-xps 17462 df-mre 17536 df-mrc 17537 df-acs 17539 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18708 df-mulg 18989 df-cntz 19224 df-cmn 19693 df-psmet 21138 df-xmet 21139 df-met 21140 df-bl 21141 df-mopn 21142 df-fbas 21143 df-fg 21144 df-cnfld 21147 df-top 22618 df-topon 22635 df-topsp 22657 df-bases 22671 df-cld 22745 df-ntr 22746 df-cls 22747 df-nei 22824 df-lp 22862 df-perf 22863 df-cn 22953 df-cnp 22954 df-haus 23041 df-tx 23288 df-hmeo 23481 df-fil 23572 df-fm 23664 df-flim 23665 df-flf 23666 df-xms 24048 df-ms 24049 df-tms 24050 df-cncf 24620 df-limc 25617 df-dv 25618 |
| This theorem is referenced by: picn
26203 pipos
26204 pirp
26205 sinhalfpilem
26207 halfpire
26208 sincosq1lem
26241 sincosq2sgn
26243 sincosq3sgn
26244 sincosq4sgn
26245 coseq00topi
26246 coseq0negpitopi
26247 tangtx
26249 sinq12gt0
26251 sinq12ge0
26252 sinq34lt0t
26253 cosq14gt0
26254 cosq14ge0
26255 sincos4thpi
26257 tan4thpi
26258 sincos6thpi
26259 pigt3
26261 pige3
26262 pige3ALT
26263 coskpi
26266 sineq0
26267 coseq1
26268 cos02pilt1
26269 cosq34lt1
26270 efeq1
26271 cosne0
26272 cosordlem
26273 cosord
26274 cos0pilt1
26275 cos11
26276 sinord
26277 recosf1o
26278 resinf1o
26279 tanord1
26280 negpitopissre
26283 efif1olem1
26285 efif1olem2
26286 efif1olem4
26288 efif1o
26289 efifo
26290 eff1o
26292 ellogrn
26302 relogrn
26304 logimclad
26315 abslogimle
26316 logneg
26330 lognegb
26332 eflogeq
26344 logcj
26348 argregt0
26352 argrege0
26353 argimgt0
26354 argimlt0
26355 logimul
26356 logneg2
26357 abslogle
26360 logcnlem3
26386 dvloglem
26390 logf1o2
26392 efopnlem1
26398 efopnlem2
26399 cxpsqrtlem
26444 abscxpbnd
26495 root1eq1
26497 logreclem
26501 ang180lem1
26548 ang180lem2
26549 ang180lem3
26550 ang180lem4
26551 isosctrlem1
26557 1cubrlem
26580 asinneg
26625 asinsin
26631 asin1
26633 acosbnd
26639 atanlogaddlem
26652 atanlogsublem
26654 atanlogsub
26655 atantan
26662 atanbndlem
26664 atan1
26667 o1cxp
26713 lgamgulmlem4
26770 lgamgulmlem5
26771 lgamgulmlem6
26772 lgambdd
26775 basellem1
26819 basellem4
26822 basellem8
26826 basellem9
26827 circum
34955 logi
35006 bj-pinftyccb
36407 bj-minftyccb
36411 bj-pinftynminfty
36413 taupi
36509 sin2h
36783 cos2h
36784 tan2h
36785 acos1half
41719 proot1ex
42247 isosctrlem1ALT
43999 sineq0ALT
44002 negpilt0
44290 coseq0
44880 sinaover2ne0
44884 itgsin0pilem1
44966 itgsinexplem1
44970 itgsinexp
44971 wallispilem1
45081 wallispilem2
45082 wallispi
45086 stirlinglem15
45104 stirlingr
45106 dirker2re
45108 dirkerval2
45110 dirkerre
45111 dirkerper
45112 dirkertrigeqlem2
45115 dirkertrigeqlem3
45116 dirkertrigeq
45117 dirkeritg
45118 dirkercncflem1
45119 dirkercncflem2
45120 dirkercncflem4
45122 fourierdlem5
45128 fourierdlem9
45132 fourierdlem16
45139 fourierdlem18
45141 fourierdlem21
45144 fourierdlem22
45145 fourierdlem24
45147 fourierdlem38
45161 fourierdlem40
45163 fourierdlem43
45166 fourierdlem44
45167 fourierdlem46
45168 fourierdlem50
45172 fourierdlem58
45180 fourierdlem62
45184 fourierdlem66
45188 fourierdlem72
45194 fourierdlem74
45196 fourierdlem75
45197 fourierdlem76
45198 fourierdlem77
45199 fourierdlem78
45200 fourierdlem83
45205 fourierdlem85
45207 fourierdlem87
45209 fourierdlem88
45210 fourierdlem93
45215 fourierdlem94
45216 fourierdlem95
45217 fourierdlem101
45223 fourierdlem102
45224 fourierdlem103
45225 fourierdlem104
45226 fourierdlem111
45233 fourierdlem112
45234 fourierdlem113
45235 fourierdlem114
45236 sqwvfoura
45244 sqwvfourb
45245 fourierswlem
45246 fouriersw
45247 fouriercn
45248 |
