Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1541
∈ wcel 2106 (class class class)co 7405
ℂcc 11104 0cc0 11106
− cmin 11440 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-po 5587 df-so 5588 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11246 df-mnf 11247 df-ltxr 11249 df-sub 11442 |
This theorem is referenced by: mulsubaddmulsub
11674 leaddle0
11725 cru
12200 iccf1o
13469 fzocatel
13692 zmod10
13848 hashfzo
14385 hashfzp1
14387 ccatval21sw
14531 ccats1val2
14573 swrd00
14590 ccatpfx
14647 swrdccat3blem
14685 revccat
14712 repswswrd
14730 climconst
15483 rlimconst
15484 telfsumo
15744 fsumparts
15748 incexc
15779 pwdif
15810 cvgrat
15825 binomfallfaclem2
15980 fallfacfac
15985 bpolysum
15993 divalglem5
16336 nn0seqcvgd
16503 pcmpt2
16822 4sqlem15
16888 efgtlen
19588 srgbinomlem3
20044 cayhamlem1
22359 vitalilem1
25116 dvcnp2
25428 dvferm1lem
25492 c1lip1
25505 dv11cn
25509 ftc1lem5
25548 ftc2
25552 plyeq0lem
25715 dgrcolem2
25779 plydivlem4
25800 qaa
25827 aalioulem3
25838 aaliou3lem2
25847 tayl0
25865 dvntaylp
25874 taylthlem1
25876 taylthlem2
25877 abelthlem9
25943 isosctrlem1
26312 birthdaylem2
26446 rlimcnp
26459 lgam1
26557 basellem2
26575 basellem5
26578 chpub
26712 dchrsum2
26760 sumdchr2
26762 2sqmod
26928 rplogsumlem2
26977 dchrisumlem1
26981 pntlemf
27097 colinearalglem4
28156 crctcsh
29067 eucrct2eupth
29487 ipidsq
29950 dip0r
29957 riesz3i
31302 riesz4i
31303 hmopidmpji
31392 pjclem4
31439 pj3si
31447 cycpmco2lem2
32273 cycpmco2lem4
32275 cycpmco2lem6
32277 freshmansdream
32369 fermltlchr
32466 znfermltl
32467 ccfldextdgrr
32734 signsply0
33550 itgexpif
33606 gg-dvcnp2
35162 dnizeq0
35339 unbdqndv2lem2
35374 poimir
36509 itg2addnclem3
36529 ftc1cnnc
36548 ftc2nc
36558 areacirc
36569 sticksstones10
40959 sticksstones12a
40961 metakunt24
40996 lsubcom23d
41188 fltnltalem
41400 3cubeslem2
41408 congid
41695 congabseq
41698 jm2.18
41712 dgrsub2
41862 areaquad
41950 ofsubid
43068 isosctrlem1ALT
43680 supxrgelem
44033 constlimc
44326 ioodvbdlimc1lem1
44633 dvnxpaek
44644 dvnmul
44645 voliooico
44694 voliccico
44701 stoweidlem13
44715 stoweidlem23
44725 stoweidlem26
44728 stirlinglem5
44780 dirkertrigeqlem2
44801 fourierdlem4
44813 fourierdlem42
44851 fourierdlem60
44868 fourierdlem61
44869 fourierdlem74
44882 fourierdlem75
44883 fourierdlem89
44897 fourierdlem90
44898 fourierdlem91
44899 fourierdlem103
44911 fourierdlem104
44912 fourierdlem107
44915 sqwvfoura
44930 etransclem24
44960 etransclem25
44961 hoidmv1lelem1
45293 hoidmv1lelem2
45294 hoidmvlelem1
45297 hoidmvlelem2
45298 volico2
45343 2elfz2melfz
46012 m1mod0mod1
46023 m1modmmod
47160 eenglngeehlnmlem2
47377 rrx2linest
47381 line2x
47393 itscnhlc0yqe
47398 itsclc0yqsollem1
47401 |