Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 (class class class)co 7409
ℂcc 11108 + caddc 11113 − 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: mvlraddd
11624 mvlladdd
11625 mvrraddd
11626 addlsub
11630 pnpncand
11635 pncan1
11638 eluzmn
12829 icoshftf1o
13451 xov1plusxeqvd
13475 zesq
14189 hashdifsnp1
14457 ccatval3
14529 fsump1
15702 fsumrev2
15728 fprodp1
15913 risefacp1
15973 fallfacp1
15974 sadcp1
16396 smupp1
16421 hashdvds
16708 pythagtriplem4
16752 pythagtriplem6
16754 pythagtriplem7
16755 pythagtriplem12
16759 pythagtriplem14
16761 pcqdiv
16790 mulgdirlem
18985 cayhamlem1
22368 pjthlem1
24954 ovolicopnf
25041 i1faddlem
25210 itg1addlem4
25216 itg1addlem4OLD
25217 itgpowd
25567 taylthlem2
25886 ulmshft
25902 efif1olem2
26052 efif1olem4
26054 logdiflbnd
26499 lgamgulmlem2
26534 lgamcvg2
26559 relgamcl
26566 ftalem2
26578 mulog2sumlem1
27037 mulog2sumlem3
27039 pntrlog2bndlem2
27081 pntrlog2bndlem4
27083 pntrlog2bndlem5
27084 colinearalglem4
28167 axpaschlem
28198 wwlksnred
29146 wwlksnext
29147 wwlksnredwwlkn
29149 wwlksnextproplem2
29164 clwlkclwwlklem2
29253 clwlkclwwlklem3
29254 clwwlkf
29300 wwlksext2clwwlk
29310 eucrct2eupth
29498 numclwwlk2lem1
29629 numclwlk2lem2f
29630 pjhthlem1
30644 fzm1ne1
32000 fzom1ne1
32012 wrdt2ind
32117 cshwrnid
32125 psgnfzto1stlem
32259 cycpmco2lem4
32288 cycpmco2lem5
32289 cycpmco2lem7
32291 madjusmdetlem2
32808 dya2icoseg
33276 fibp1
33400 ballotlemfc0
33491 ballotlemfcc
33492 ballotlemsgt1
33509 ballotlemsel1i
33511 ballotlemsima
33514 ballotlem1ri
33533 signstfvn
33580 reprsuc
33627 bcprod
34708 bccolsum
34709 unblimceq0
35383 knoppndvlem6
35393 bj-bary1lem1
36192 sin2h
36478 itg2addnclem
36539 itg2addnclem3
36541 areacirclem4
36579 ssbnd
36656 lcmineqlem10
40903 lcmineqlem11
40904 lcmineqlem18
40911 lcmineqlem19
40912 sticksstones12a
40973 sticksstones12
40974 metakunt12
40996 mvrrsubd
41187 fz1sump1
41208 oddnumth
41209 dffltz
41376 jm2.19lem4
41731 jm2.23
41735 int-eqmvtd
42941 hashnzfzclim
43081 dvradcnv2
43106 binomcxplemnn0
43108 binomcxplemnotnn0
43115 nnsplit
44068 iccshift
44231 iooshift
44235 climinf
44322 limcperiod
44344 0ellimcdiv
44365 cncfshift
44590 cncfperiod
44595 dvdsn1add
44655 dvnmul
44659 dvnprodlem1
44662 itgiccshift
44696 itgperiod
44697 stoweidlem17
44733 wallispilem4
44784 wallispilem5
44785 stirlinglem1
44790 stirlinglem5
44794 stirlinglem6
44795 stirlinglem10
44799 dirkertrigeqlem2
44815 fourierdlem14
44837 fourierdlem19
44842 fourierdlem41
44864 fourierdlem42
44865 fourierdlem48
44870 fourierdlem49
44871 fourierdlem50
44872 fourierdlem64
44886 fourierdlem74
44896 fourierdlem75
44897 fourierdlem81
44903 fourierdlem92
44914 fourierdlem97
44919 fourierdlem103
44925 fourierdlem104
44926 fourierdlem107
44929 etransclem9
44959 nnfoctbdjlem
45171 fldivmod
47204 |