Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
(class class class)co 7409 ℂcc 11108
− cmin 11444 |
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-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 |
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-reu 3378 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-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-ltxr 11253 df-sub 11446 |
This theorem is referenced by: pnpncand
11635 muleqadd
11858 lineq
12051 modmuladdnn0
13880 hashfz
14387 hashfzo
14389 hashf1lem2
14417 hashf1
14418 ccatswrd
14618 pfxccatin12lem2
14681 crre
15061 remim
15064 remullem
15075 abs3lem
15285 caubnd2
15304 bhmafibid1cn
15410 bhmafibid2cn
15411 bhmafibid2
15413 rlimuni
15494 climuni
15496 rlimcld2
15522 rlimrege0
15523 rlimrecl
15524 mulcn2
15540 reccn2
15541 cn1lem
15542 o1sub
15560 rlimo1
15561 o1dif
15574 rlimsqzlem
15595 caucvgrlem2
15621 iseralt
15631 fsumparts
15752 cvgcmpce
15764 incexclem
15782 arisum2
15807 geoserg
15812 pwdif
15814 geo2sum2
15820 fallfacfwd
15980 binomfallfaclem2
15984 bpolycl
15996 bpoly3
16002 bpoly4
16003 fsumcube
16004 sinf
16067 tanval2
16076 tanval3
16077 sinneg
16089 efival
16095 sinhval
16097 bitsinv1lem
16382 bitsres
16414 pythagtriplem1
16749 pythagtriplem14
16761 pythagtriplem17
16764 dvdsprmpweqle
16819 4sqlem5
16875 mul4sqlem
16886 4sqlem17
16894 vdwlem5
16918 vdwlem6
16919 vdwlem8
16921 blcvx
24314 recld2
24330 addcnlem
24380 cnllycmp
24472 cphipval2
24758 4cphipval2
24759 cphipval
24760 ipcnlem2
24761 rrxmval
24922 rrxmetlem
24924 pjthlem1
24954 ovollb2lem
25005 itgcnlem
25307 dvlem
25413 dvconst
25434 dvid
25435 dvcnp2
25437 dvaddbr
25455 dvmulbr
25456 dvcobr
25463 dvcjbr
25466 dvrec
25472 dvmptim
25487 dvcnvlem
25493 dveflem
25496 dvsincos
25498 cmvth
25508 dvlip
25510 dvlipcn
25511 c1liplem1
25513 dveq0
25517 dv11cn
25518 dvle
25524 lhop1lem
25530 dvfsumabs
25540 dvfsumlem1
25543 dvfsumlem2
25544 dvfsumrlim
25548 dvfsumrlim2
25549 ftc1lem4
25556 ftc1lem5
25557 ftc2
25561 dgrcolem2
25788 plydiveu
25811 aaliou2b
25854 taylfvallem1
25869 taylply2
25880 dvtaylp
25882 dvntaylp
25883 taylthlem1
25885 taylthlem2
25886 ulmbdd
25910 ulmcn
25911 ulmdvlem1
25912 mtest
25916 iblulm
25919 itgulm
25920 abelthlem9
25952 ptolemy
26006 tangtx
26015 sineq0
26033 efeq1
26037 efif1olem4
26054 tanarg
26127 logcnlem3
26152 logcnlem4
26153 advlogexp
26163 efopn
26166 cxpcn3lem
26255 cxpeq
26265 ang180lem4
26317 ang180lem5
26318 ang180
26319 isosctrlem2
26324 isosctrlem3
26325 isosctr
26326 ssscongptld
26327 affineequiv
26328 affineequiv2
26329 affineequiv3
26330 affineequiv4
26331 affineequivne
26332 angpieqvdlem
26333 angpieqvdlem2
26334 angpined
26335 angpieqvd
26336 chordthmlem
26337 chordthmlem2
26338 chordthmlem3
26339 chordthmlem4
26340 chordthmlem5
26341 heron
26343 quad2
26344 quad
26345 dcubic1lem
26348 dcubic
26351 mcubic
26352 cubic2
26353 cubic
26354 dquartlem1
26356 dquartlem2
26357 dquart
26358 quart1cl
26359 quart1lem
26360 quart1
26361 quartlem2
26363 quartlem4
26365 quart
26366 atanf
26385 sinasin
26394 asinsin
26397 atanneg
26412 atancj
26415 efiatan
26417 atanlogsub
26421 efiatan2
26422 2efiatan
26423 atanbndlem
26430 dvatan
26440 atantayl
26442 lgamgulmlem2
26534 lgamgulmlem3
26535 lgamgulmlem5
26537 lgamgulmlem6
26538 lgamgulm2
26540 lgamucov
26542 lgamcvg2
26559 gamcvg
26560 gamcvg2lem
26563 ftalem2
26578 logfacrlim
26727 logexprlim
26728 lgsdirprm
26834 gausslemma2dlem1a
26868 gausslemma2dlem4
26872 2sqmod
26939 addsq2nreurex
26947 vmadivsum
26985 rpvmasumlem
26990 dchrisumlem2
26993 dchrisumlem3
26994 dchrmusum2
26997 dchrvmasumlem2
27001 dchrvmasumlem3
27002 dchrvmasumiflem1
27004 rpvmasum2
27015 dchrisum0lem1b
27018 dchrisum0lem1
27019 dchrisum0lem2a
27020 rplogsum
27030 mudivsum
27033 mulogsumlem
27034 mulogsum
27035 mulog2sumlem1
27037 mulog2sumlem2
27038 mulog2sumlem3
27039 vmalogdivsum2
27041 vmalogdivsum
27042 2vmadivsumlem
27043 selberglem1
27048 selberglem2
27049 selberg2lem
27053 selberg2
27054 selberg3lem1
27060 selberg4lem1
27063 selberg4
27064 pntrsumo1
27068 selberg3r
27072 selberg34r
27074 pntrlog2bndlem1
27080 pntrlog2bndlem2
27081 pntrlog2bndlem3
27082 pntrlog2bndlem4
27083 pntrlog2bndlem5
27084 pntibndlem2
27094 pntlemf
27108 pntlemo
27110 ttgcontlem1
28142 brbtwn2
28163 colinearalglem1
28164 colinearalglem2
28165 colinearalg
28168 axsegconlem1
28175 ax5seglem1
28186 ax5seglem2
28187 ax5seglem6
28192 ax5seglem9
28195 axlowdimlem17
28216 axcontlem7
28228 axcontlem8
28229 clwlkclwwlk
29255 clwwlknonex2lem1
29360 2clwwlk2clwwlk
29603 numclwwlk3lem1
29635 smcnlem
29950 ipval2
29960 4ipval2
29961 dipcj
29967 pjhthlem1
30644 lt2addrd
31964 bcm1n
32006 cycpmco2lem5
32289 cycpmco2lem6
32290 sqsscirc2
32889 signslema
33573 circlemeth
33652 logdivsqrle
33662 revpfxsfxrev
34106 revwlk
34115 subfaclim
34179 divcnvlin
34702 iprodgam
34712 gg-dvcnp2
35174 gg-dvmulbr
35175 gg-dvcobr
35176 gg-cmvth
35181 gg-dvfsumlem2
35183 dnicld1
35348 dnibndlem2
35355 dnibndlem3
35356 dnibndlem6
35359 dnibndlem9
35362 dnibndlem10
35363 dnibndlem11
35364 unblimceq0
35383 unbdqndv2lem1
35385 unbdqndv2lem2
35386 knoppndvlem11
35398 knoppndvlem15
35402 knoppndvlem17
35404 knoppndvlem21
35408 bj-bary1lem
36191 bj-bary1lem1
36192 bj-bary1
36193 ftc1cnnclem
36559 ftc1anclem7
36567 ftc1anclem8
36568 ftc1anc
36569 ftc2nc
36570 areacirclem1
36576 areacirclem4
36579 areacirc
36581 cntotbnd
36664 lcmineqlem8
40901 lcmineqlem10
40903 lcmineqlem11
40904 lcmineqlem12
40905 lcmineqlem23
40916 aks4d1p1
40941 sticksstones10
40971 sticksstones12a
40973 sticksstones12
40974 sticksstones22
40984 metakunt15
40999 metakunt16
41000 metakunt29
41013 metakunt30
41014 mvrrsubd
41187 lsubrotld
41190 lsubcom23d
41191 nicomachus
41210 sumcubes
41211 dffltz
41376 fltnltalem
41404 rencldnfilem
41558 pellexlem2
41568 pellexlem6
41572 pell1234qrne0
41591 pell1234qrmulcl
41593 rmyluc
41676 jm2.18
41727 jm2.19
41732 areaquad
41965 lhe4.4ex1a
43088 bcc0
43099 bccp1k
43100 bccm1k
43101 binomcxplemwb
43107 binomcxplemnn0
43108 binomcxplemrat
43109 binomcxplemfrat
43110 binomcxplemdvbinom
43112 binomcxplemnotnn0
43115 isosctrlem1ALT
43695 sineq0ALT
43698 oddfl
43987 dstregt0
43991 subadd4b
43992 sub31
44000 fzisoeu
44010 absnpncan2d
44012 absnpncan3d
44017 supxrgelem
44047 absimlere
44190 cvgcaule
44202 mullimc
44332 ellimcabssub0
44333 mullimcf
44339 limcrecl
44345 lptre2pt
44356 limcleqr
44360 neglimc
44363 addlimc
44364 0ellimcdiv
44365 limclner
44367 reclimc
44369 climleltrp
44392 climisp
44462 climxrrelem
44465 climxrre
44466 cnrefiisplem
44545 climxlim2lem
44561 fprodsubrecnncnvlem
44623 fperdvper
44635 dvdivbd
44639 dvbdfbdioolem2
44645 ioodvbdlimc1lem1
44647 volioc
44688 volico
44699 stoweidlem1
44717 stoweidlem11
44727 stoweidlem13
44729 stoweidlem26
44742 stoweid
44779 wallispi
44786 wallispi2lem1
44787 wallispi2lem2
44788 wallispi2
44789 stirlinglem1
44790 stirlinglem4
44793 stirlinglem5
44794 stirlinglem7
44796 stirlinglem11
44800 dirkertrigeqlem2
44815 fourierdlem4
44827 fourierdlem26
44849 fourierdlem30
44853 fourierdlem42
44865 fourierdlem63
44885 fourierdlem65
44887 fourierdlem72
44894 fourierdlem74
44896 fourierdlem75
44897 fourierdlem76
44898 fourierdlem80
44902 fourierdlem81
44903 fourierdlem89
44911 fourierdlem90
44912 fourierdlem91
44913 fourierdlem107
44929 fourierdlem109
44931 fouriersw
44947 etransclem1
44951 etransclem4
44954 etransclem8
44958 etransclem18
44968 etransclem20
44970 etransclem21
44971 etransclem23
44973 etransclem35
44985 etransclem46
44996 rrxtopnfi
45003 rrndistlt
45006 sge0gtfsumgt
45159 hoidmv1lelem2
45308 hoidmvlelem2
45312 smfmullem1
45507 sigarmf
45570 sigarms
45572 sigarexp
45575 sigardiv
45577 sigarcol
45580 sharhght
45581 sigaradd
45582 cevathlem2
45584 cevath
45585 resubcnnred
46012 fmtnorec2lem
46210 fmtnorec3
46216 fmtnorec4
46217 lighneallem3
46275 quad1
46288 requad01
46289 requad2
46291 fppr2odd
46399 fldivmod
47204 dignn0flhalflem2
47302 affinecomb2
47389 1subrec1sub
47391 eenglngeehlnmlem1
47423 eenglngeehlnmlem2
47424 rrx2vlinest
47427 rrx2linest
47428 line2
47438 itsclc0yqsollem1
47448 itsclc0yqsol
47450 itscnhlc0xyqsol
47451 itschlc0xyqsol1
47452 itschlc0xyqsol
47453 itsclc0xyqsolr
47455 2itscplem1
47464 2itscplem2
47465 2itscplem3
47466 itscnhlinecirc02plem1
47468 inlinecirc02plem
47472 sinhpcosh
47785 i2linesd
47826 |