Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2105 ≠ wne 2939
class class class wbr 5148 ℝcr 11115
< clt 11255 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-resscn 11173 ax-pre-lttri 11190 ax-pre-lttrn 11191 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-po 5588 df-so 5589 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-er 8709 df-en 8946 df-dom 8947 df-sdom 8948 df-pnf 11257 df-mnf 11258 df-ltxr 11260 |
This theorem is referenced by: ltneii
11334 fztpval
13570 geo2sum
15826 bpoly4
16010 ene1
16160 3dvds
16281 3lcm2e6
16675 resslemOLD
17194 starvndxnbasendx
17256 starvndxnplusgndx
17257 starvndxnmulrndx
17258 scandxnbasendx
17268 scandxnplusgndx
17269 scandxnmulrndx
17270 vscandxnbasendx
17273 vscandxnplusgndx
17274 vscandxnmulrndx
17275 vscandxnscandx
17276 ipndxnbasendx
17284 ipndxnplusgndx
17285 ipndxnmulrndx
17286 tsetndxnbasendx
17308 tsetndxnplusgndx
17309 tsetndxnmulrndx
17310 tsetndxnstarvndx
17311 slotstnscsi
17312 plendxnbasendx
17322 plendxnplusgndx
17323 plendxnmulrndx
17324 plendxnscandx
17325 plendxnvscandx
17326 dsndxnbasendx
17341 dsndxnplusgndx
17342 dsndxnmulrndx
17343 slotsdnscsi
17344 dsndxntsetndx
17345 unifndxnbasendx
17351 unifndxntsetndx
17352 resccoOLD
17788 oppgtsetOLD
19267 symgvalstructOLD
19313 mgpscaOLD
20044 mgptsetOLD
20046 mgpdsOLD
20049 cnfldfunALTOLD
21247 psgnodpmr
21453 matscaOLD
22236 matvscaOLD
22238 tuslemOLD
24092 setsmsdsOLD
24304 tngdsOLD
24485 logbrec
26628 2logb9irr
26641 2logb3irr
26643 log2le1
26796 2lgsoddprmlem3a
27256 2lgsoddprmlem3b
27257 2lgsoddprmlem3c
27258 2lgsoddprmlem3d
27259 slotsinbpsd
28125 slotslnbpsd
28126 lngndxnitvndx
28127 konigsberglem2
29939 ex-dif
30109 ex-in
30111 ex-pss
30114 ex-res
30127 dp20u
32477 dp20h
32478 dp2clq
32480 dp2lt10
32483 dp2lt
32484 dplti
32504 dpexpp1
32507 oppgleOLD
32564 resvvscaOLD
32888 zlmdsOLD
33407 zlmtsetOLD
33409 ballotlemi1
33965 sgnnbi
34008 sgnpbi
34009 signswch
34036 itgexpif
34082 hgt750lemd
34124 hgt750lem
34127 fdc
37077 areaquad
42428 mnringscadOLD
43445 mnringvscadOLD
43447 stirlinglem4
45252 stirlinglem13
45261 stirlinglem14
45262 stirlingr
45265 dirker2re
45267 dirkerdenne0
45268 dirkerre
45270 dirkertrigeqlem1
45273 dirkercncflem2
45279 dirkercncflem4
45281 fourierdlem16
45298 fourierdlem21
45303 fourierdlem22
45304 fourierdlem66
45347 fourierdlem83
45364 fourierdlem103
45384 fourierdlem104
45385 sqwvfoura
45403 sqwvfourb
45404 fourierswlem
45405 fouriersw
45406 etransclem46
45455 fmtnoprmfac2lem1
46693 zlmodzxzldeplem
47341 |