Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1533
∈ wcel 2098 (class class class)co 7402
ℂcc 11105 0cc0 11107
+ caddc 11110 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5290 ax-nul 5297 ax-pow 5354 ax-pr 5418 ax-un 7719 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4522 df-pw 4597 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-br 5140 df-opab 5202 df-mpt 5223 df-id 5565 df-po 5579 df-so 5580 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-iota 6486 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-ov 7405 df-er 8700 df-en 8937 df-dom 8938 df-sdom 8939 df-pnf 11249 df-mnf 11250 df-ltxr 11252 |
This theorem is referenced by: negeu
11449 subge0
11726 sublt0d
11839 un0addcl
12504 lincmb01cmp
13473 ico01fl0
13785 discr
14204 ccatlid
14538 swrdfv0
14601 swrdpfx
14659 pfxpfx
14660 cats1un
14673 swrdccatin2
14681 cshwidx0mod
14757 cshw1
14774 relexpaddg
15002 rennim
15188 max0add
15259 fsumsplit
15689 sumsplit
15716 isumsplit
15788 arisum2
15809 binomfallfaclem2
15986 efaddlem
16039 eftlub
16055 ef4p
16059 rpnnen2lem11
16170 moddvds
16211 divalglem9
16347 sadadd2lem2
16394 sadcaddlem
16401 gcdmultipled
16479 pcmpt
16830 4sqlem11
16893 vdwlem6
16924 gsumsgrpccat
18761 mulgnn0dir
19027 sylow1lem1
19514 efgsval2
19649 efgsp1
19653 zaddablx
19788 pgpfaclem1
19999 regsumfsum
21318 regsumsupp
21504 mplcoe5
21926 nrmmetd
24427 blcvx
24658 xrsxmet
24669 reparphti
24867 reparphtiOLD
24868 nulmbl
25408 itg2splitlem
25622 itg2split
25623 itg2monolem1
25624 itgsplitioo
25711 ditgsplit
25734 dvcnp2
25793 dvcnp2OLD
25794 dvcmul
25819 dvcmulf
25820 dvmptcmul
25840 dveflem
25855 dvef
25856 dvlipcn
25871 dvlt0
25882 plymullem1
26091 coeeulem
26101 dgradd2
26146 dgrmulc
26149 plydivlem3
26172 aareccl
26203 taylthlem1
26249 sin2kpi
26358 cos2kpi
26359 coshalfpim
26370 sinkpi
26396 chordthmlem3
26706 chordthmlem5
26708 dcubic1lem
26715 dcubic
26718 atancj
26782 atanlogaddlem
26785 atanlogsublem
26787 scvxcvx
26858 zetacvg
26887 ftalem5
26949 ftalem7
26951 basellem3
26955 chtublem
27084 2sqn0
27307 2sqnn
27312 rplogsumlem2
27358 dchrisumlem1
27362 pntrlog2bndlem2
27451 brbtwn2
28656 axlowdimlem16
28708 axeuclidlem
28713 elntg2
28736 eucrct2eupth
29992 2clwwlk2clwwlk
30097 bcm1n
32500 wrdt2ind
32609 esumpfinvallem
33591 signsplypnf
34080 fsum2dsub
34137 logdivsqrle
34180 revpfxsfxrev
34623 cvxpconn
34750 cvxsconn
34751 fwddifnp1
35659 tan2h
36983 poimirlem16
37007 mbfposadd
37038 itg2addnc
37045 ftc1anclem5
37068 bfplem2
37194 aks4d1p1p4
41442 aks4d1p7d1
41453 aks6d1c1
41483 sticksstones10
41504 sticksstones22
41517 dffltz
41926 3cubeslem3r
41975 pellexlem6
42122 jm2.18
42277 sqrtcval
42941 relexpaddss
43018 int-add02d
43486 sub2times
44527 fzisoeu
44555 xralrple2
44609 cosknegpi
45130 dvsinax
45174 dvasinbx
45181 dvnxpaek
45203 dvnmul
45204 stoweidlem1
45262 stoweidlem13
45274 stoweidlem42
45303 stirlinglem5
45339 stirlinglem11
45345 fourierdlem42
45410 fourierdlem51
45418 fourierdlem88
45455 fourierdlem103
45470 fourierdlem104
45471 fourierdlem107
45474 sqwvfoura
45489 sqwvfourb
45490 fouriersw
45492 elaa2lem
45494 hspmbllem1
45887 cnambpcma
46547 readdcnnred
46556 nn0mnd
47102 altgsumbcALT
47278 nn0sumshdiglemA
47553 line2xlem
47687 line2x
47688 itschlc0yqe
47694 itsclc0yqsollem1
47696 itschlc0xyqsol1
47700 itschlc0xyqsol
47701 2itscp
47715 |