Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 ≠ wne 2941
class class class wbr 5149 ℝcr 11109
< clt 11248 |
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-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-resscn 11167 ax-pre-lttri 11184 ax-pre-lttrn 11185 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 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-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-ltxr 11253 |
This theorem is referenced by: ltneii
11327 fztpval
13563 geo2sum
15819 bpoly4
16003 ene1
16153 3dvds
16274 3lcm2e6
16668 resslemOLD
17187 starvndxnbasendx
17249 starvndxnplusgndx
17250 starvndxnmulrndx
17251 scandxnbasendx
17261 scandxnplusgndx
17262 scandxnmulrndx
17263 vscandxnbasendx
17266 vscandxnplusgndx
17267 vscandxnmulrndx
17268 vscandxnscandx
17269 ipndxnbasendx
17277 ipndxnplusgndx
17278 ipndxnmulrndx
17279 tsetndxnbasendx
17301 tsetndxnplusgndx
17302 tsetndxnmulrndx
17303 tsetndxnstarvndx
17304 slotstnscsi
17305 plendxnbasendx
17315 plendxnplusgndx
17316 plendxnmulrndx
17317 plendxnscandx
17318 plendxnvscandx
17319 dsndxnbasendx
17334 dsndxnplusgndx
17335 dsndxnmulrndx
17336 slotsdnscsi
17337 dsndxntsetndx
17338 unifndxnbasendx
17344 unifndxntsetndx
17345 resccoOLD
17781 oppgtsetOLD
19219 symgvalstructOLD
19265 mgpscaOLD
19996 mgptsetOLD
19998 mgpdsOLD
20001 cnfldfunALTOLD
20958 psgnodpmr
21143 matscaOLD
21916 matvscaOLD
21918 tuslemOLD
23772 setsmsdsOLD
23984 tngdsOLD
24165 logbrec
26287 2logb9irr
26300 2logb3irr
26302 log2le1
26455 2lgsoddprmlem3a
26913 2lgsoddprmlem3b
26914 2lgsoddprmlem3c
26915 2lgsoddprmlem3d
26916 slotsinbpsd
27692 slotslnbpsd
27693 lngndxnitvndx
27694 konigsberglem2
29506 ex-dif
29676 ex-in
29678 ex-pss
29681 ex-res
29694 dp20u
32044 dp20h
32045 dp2clq
32047 dp2lt10
32050 dp2lt
32051 dplti
32071 dpexpp1
32074 oppgleOLD
32131 resvvscaOLD
32452 zlmdsOLD
32943 zlmtsetOLD
32945 ballotlemi1
33501 sgnnbi
33544 sgnpbi
33545 signswch
33572 itgexpif
33618 hgt750lemd
33660 hgt750lem
33663 fdc
36613 areaquad
41965 mnringscadOLD
42982 mnringvscadOLD
42984 stirlinglem4
44793 stirlinglem13
44802 stirlinglem14
44803 stirlingr
44806 dirker2re
44808 dirkerdenne0
44809 dirkerre
44811 dirkertrigeqlem1
44814 dirkercncflem2
44820 dirkercncflem4
44822 fourierdlem16
44839 fourierdlem21
44844 fourierdlem22
44845 fourierdlem66
44888 fourierdlem83
44905 fourierdlem103
44925 fourierdlem104
44926 sqwvfoura
44944 sqwvfourb
44945 fourierswlem
44946 fouriersw
44947 etransclem46
44996 fmtnoprmfac2lem1
46234 zlmodzxzldeplem
47179 |