| Colors of
variables: wff
setvar class |
| Syntax hints:
→ wi 4 ∧ w3a 1087
∈ wcel 2106 class class class wbr 5142
(class class class)co 7394 ℝcr 11093
≤ cle 11233 [,]cicc 13311 |
| This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5293 ax-nul 5300 ax-pow 5357 ax-pr 5421 ax-un 7709 ax-cnex 11150 ax-resscn 11151 ax-pre-lttri 11168 ax-pre-lttrn 11169 |
| This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4320 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5143 df-opab 5205 df-mpt 5226 df-id 5568 df-po 5582 df-so 5583 df-xp 5676 df-rel 5677 df-cnv 5678 df-co 5679 df-dm 5680 df-rn 5681 df-res 5682 df-ima 5683 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7397 df-oprab 7398 df-mpo 7399 df-er 8688 df-en 8925 df-dom 8926 df-sdom 8927 df-pnf 11234 df-mnf 11235 df-xr 11236 df-ltxr 11237 df-le 11238 df-icc 13315 |
| This theorem is referenced by: iccshift
44068 iccsuble
44069 cncfiooiccre
44448 itgioocnicc
44530 iblcncfioo
44531 itgspltprt
44532 itgiccshift
44533 itgperiod
44534 fourierdlem43
44703 fourierdlem44
44704 fourierdlem73
44732 fourierdlem81
44740 fourierdlem82
44741 fourierdlem83
44742 fourierdlem84
44743 fourierdlem92
44751 fourierdlem93
44752 fourierdlem101
44760 fourierdlem103
44762 fourierdlem104
44763 fourierdlem107
44766 fourierdlem111
44770 |
