Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 396
∈ wcel 2106 class class class wbr 5103
ℝ*cxr 11121
< clt 11122 ≤
cle 11123 |
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 2708 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7662 ax-cnex 11040 ax-resscn 11041 ax-pre-lttri 11058 ax-pre-lttrn 11059 |
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 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5528 df-po 5542 df-so 5543 df-xp 5636 df-rel 5637 df-cnv 5638 df-co 5639 df-dm 5640 df-rn 5641 df-res 5642 df-ima 5643 df-iota 6443 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-er 8581 df-en 8817 df-dom 8818 df-sdom 8819 df-pnf 11124 df-mnf 11125 df-xr 11126 df-ltxr 11127 df-le 11128 |
This theorem is referenced by: xlt2add
13107 xadddi2
13144 supxrre
13174 infxrre
13183 ixxlb
13214 elicore
13244 elico2
13256 elicc2
13257 caucvgrlem
15491 isnzr2hash
20657 xrsdsreclblem
20766 xblss2ps
23676 xblss2
23677 tgioo
24081 xrge0tsms
24119 xrhmeo
24231 ovoliunlem1
24788 ovoliun
24791 ioombl1lem2
24845 vitalilem4
24897 itg2monolem2
25038 itg2gt0
25047 dvferm1lem
25270 dvferm2lem
25272 lhop1lem
25299 pserdvlem2
25709 abelthlem3
25714 logtayl
25937 xrge0tsmsd
31693 esum2d
32465 usgrcyclgt2v
33498 relowlssretop
35729 itg2gt0cn
36028 areacirclem5
36065 xrge0nemnfd
43323 supxrgere
43324 supxrgelem
43328 infrpge
43342 xrralrecnnge
43382 supxrunb3
43391 icoopn
43516 limsupre
43635 limsupre3lem
43726 xlimpnfv
43832 fourierdlem27
44128 fourierdlem87
44187 gsumge0cl
44365 sge0pr
44388 sge0ssre
44391 sge0xaddlem1
44427 meaiuninc3v
44478 pimiooltgt
44704 pimdecfgtioc
44709 preimageiingt
44714 |