Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 (class class class)co 7406
ℂcc 11105 + caddc 11110 − cmin 11441 |
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 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 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 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 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-po 5588 df-so 5589 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-er 8700 df-en 8937 df-dom 8938 df-sdom 8939 df-pnf 11247 df-mnf 11248 df-ltxr 11250 df-sub 11443 |
This theorem is referenced by: xralrple
13181 quoremz
13817 quoremnn0ALT
13819 intfrac2
13820 intfrac
13848 2cshwcshw
14773 isercoll2
15612 iseralt
15628 mertenslem1
15827 fprodser
15890 risefacfac
15976 fallfacfwd
15977 eflt
16057 efival
16092 bitsmod
16374 bitsinv1lem
16379 odzdvds
16725 modprm0
16735 pcaddlem
16818 vdwapun
16904 vdwlem12
16922 odmodnn0
19403 mndodconglem
19404 mhpmulcl
21684 minveclem4
24941 ivthlem2
24961 dvn2bss
25439 ftc2
25553 mdegmullem
25588 plymullem1
25720 dvtaylp
25874 dvntaylp
25875 dvntaylp0
25876 taylthlem1
25877 ulmbdd
25902 affineequiv
26318 mcubic
26342 quart1lem
26350 quart1
26351 asinsin
26387 birthdaylem2
26447 emcllem6
26495 perfectlem2
26723 lgseisenlem4
26871 lgsquadlem1
26873 addsqnreup
26936 dchrisumlem1
26982 dchrvmasum2if
26990 dchrisum0lem1
27009 selberg3
27052 axsegconlem10
28174 smcnlem
29938 swrdrn3
32107 cycpmco2lem6
32278 oddpwdc
33342 revpfxsfxrev
34095 itg2addnclem3
36530 ftc2nc
36559 dvrelogpow2b
40922 sticksstones10
40960 sticksstones12a
40962 metakunt16
40989 metakunt20
40993 frlmvscadiccat
41078 dffltz
41373 fltnltalem
41401 fltnlta
41402 fzisoeu
43997 lptre2pt
44343 0ellimcdiv
44352 climleltrp
44379 ioodvbdlimc1lem2
44635 dvnprodlem1
44649 itgsinexp
44658 itgsbtaddcnst
44685 dirkertrigeqlem2
44802 fourierdlem4
44814 fourierdlem13
44823 fourierdlem26
44836 fourierdlem41
44851 fourierdlem42
44852 fourierdlem50
44859 fourierdlem60
44869 fourierdlem61
44870 fourierdlem74
44883 fourierdlem75
44884 fourierdlem76
44885 fourierdlem84
44893 fourierdlem89
44898 fourierdlem90
44899 fourierdlem91
44900 fourierdlem93
44902 fourierdlem101
44910 fourierdlem107
44916 fourierdlem111
44920 fourierdlem112
44921 fouriersw
44934 smfaddlem1
45466 sigarcol
45567 perfectALTVlem2
46377 nnpw2pmod
47223 rrx2vlinest
47381 itsclc0xyqsolr
47409 |