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
28173 brbtwn2
28194 colinearalglem1
28195 colinearalglem2
28196 colinearalg
28199 axsegconlem1
28206 ax5seglem1
28217 ax5seglem2
28218 ax5seglem6
28223 ax5seglem9
28226 axlowdimlem17
28247 axcontlem7
28259 axcontlem8
28260 clwlkclwwlk
29286 clwwlknonex2lem1
29391 2clwwlk2clwwlk
29634 numclwwlk3lem1
29666 smcnlem
29981 ipval2
29991 4ipval2
29992 dipcj
29998 pjhthlem1
30675 lt2addrd
31995 bcm1n
32037 cycpmco2lem5
32320 cycpmco2lem6
32321 sqsscirc2
32920 signslema
33604 circlemeth
33683 logdivsqrle
33693 revpfxsfxrev
34137 revwlk
34146 subfaclim
34210 divcnvlin
34733 iprodgam
34743 gg-dvcnp2
35205 gg-dvmulbr
35206 gg-dvcobr
35207 gg-cmvth
35212 gg-dvfsumlem2
35214 dnicld1
35396 dnibndlem2
35403 dnibndlem3
35404 dnibndlem6
35407 dnibndlem9
35410 dnibndlem10
35411 dnibndlem11
35412 unblimceq0
35431 unbdqndv2lem1
35433 unbdqndv2lem2
35434 knoppndvlem11
35446 knoppndvlem15
35450 knoppndvlem17
35452 knoppndvlem21
35456 bj-bary1lem
36239 bj-bary1lem1
36240 bj-bary1
36241 ftc1cnnclem
36607 ftc1anclem7
36615 ftc1anclem8
36616 ftc1anc
36617 ftc2nc
36618 areacirclem1
36624 areacirclem4
36627 areacirc
36629 cntotbnd
36712 lcmineqlem8
40949 lcmineqlem10
40951 lcmineqlem11
40952 lcmineqlem12
40953 lcmineqlem23
40964 aks4d1p1
40989 sticksstones10
41019 sticksstones12a
41021 sticksstones12
41022 sticksstones22
41032 metakunt15
41047 metakunt16
41048 metakunt29
41061 metakunt30
41062 mvrrsubd
41235 lsubrotld
41238 lsubcom23d
41239 nicomachus
41258 sumcubes
41259 dffltz
41424 fltnltalem
41452 rencldnfilem
41606 pellexlem2
41616 pellexlem6
41620 pell1234qrne0
41639 pell1234qrmulcl
41641 rmyluc
41724 jm2.18
41775 jm2.19
41780 areaquad
42013 lhe4.4ex1a
43136 bcc0
43147 bccp1k
43148 bccm1k
43149 binomcxplemwb
43155 binomcxplemnn0
43156 binomcxplemrat
43157 binomcxplemfrat
43158 binomcxplemdvbinom
43160 binomcxplemnotnn0
43163 isosctrlem1ALT
43743 sineq0ALT
43746 oddfl
44035 dstregt0
44039 subadd4b
44040 sub31
44048 fzisoeu
44058 absnpncan2d
44060 absnpncan3d
44065 supxrgelem
44095 absimlere
44238 cvgcaule
44250 mullimc
44380 ellimcabssub0
44381 mullimcf
44387 limcrecl
44393 lptre2pt
44404 limcleqr
44408 neglimc
44411 addlimc
44412 0ellimcdiv
44413 limclner
44415 reclimc
44417 climleltrp
44440 climisp
44510 climxrrelem
44513 climxrre
44514 cnrefiisplem
44593 climxlim2lem
44609 fprodsubrecnncnvlem
44671 fperdvper
44683 dvdivbd
44687 dvbdfbdioolem2
44693 ioodvbdlimc1lem1
44695 volioc
44736 volico
44747 stoweidlem1
44765 stoweidlem11
44775 stoweidlem13
44777 stoweidlem26
44790 stoweid
44827 wallispi
44834 wallispi2lem1
44835 wallispi2lem2
44836 wallispi2
44837 stirlinglem1
44838 stirlinglem4
44841 stirlinglem5
44842 stirlinglem7
44844 stirlinglem11
44848 dirkertrigeqlem2
44863 fourierdlem4
44875 fourierdlem26
44897 fourierdlem30
44901 fourierdlem42
44913 fourierdlem63
44933 fourierdlem65
44935 fourierdlem72
44942 fourierdlem74
44944 fourierdlem75
44945 fourierdlem76
44946 fourierdlem80
44950 fourierdlem81
44951 fourierdlem89
44959 fourierdlem90
44960 fourierdlem91
44961 fourierdlem107
44977 fourierdlem109
44979 fouriersw
44995 etransclem1
44999 etransclem4
45002 etransclem8
45006 etransclem18
45016 etransclem20
45018 etransclem21
45019 etransclem23
45021 etransclem35
45033 etransclem46
45044 rrxtopnfi
45051 rrndistlt
45054 sge0gtfsumgt
45207 hoidmv1lelem2
45356 hoidmvlelem2
45360 smfmullem1
45555 sigarmf
45618 sigarms
45620 sigarexp
45623 sigardiv
45625 sigarcol
45628 sharhght
45629 sigaradd
45630 cevathlem2
45632 cevath
45633 resubcnnred
46060 fmtnorec2lem
46258 fmtnorec3
46264 fmtnorec4
46265 lighneallem3
46323 quad1
46336 requad01
46337 requad2
46339 fppr2odd
46447 fldivmod
47252 dignn0flhalflem2
47350 affinecomb2
47437 1subrec1sub
47439 eenglngeehlnmlem1
47471 eenglngeehlnmlem2
47472 rrx2vlinest
47475 rrx2linest
47476 line2
47486 itsclc0yqsollem1
47496 itsclc0yqsol
47498 itscnhlc0xyqsol
47499 itschlc0xyqsol1
47500 itschlc0xyqsol
47501 itsclc0xyqsolr
47503 2itscplem1
47512 2itscplem2
47513 2itscplem3
47514 itscnhlinecirc02plem1
47516 inlinecirc02plem
47520 sinhpcosh
47833 i2linesd
47874 |