Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 (class class class)co 7358
ℂcc 11050 0cc0 11052
+ caddc 11055 |
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 2708 ax-sep 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 ax-resscn 11109 ax-1cn 11110 ax-icn 11111 ax-addcl 11112 ax-addrcl 11113 ax-mulcl 11114 ax-mulrcl 11115 ax-mulcom 11116 ax-addass 11117 ax-mulass 11118 ax-distr 11119 ax-i2m1 11120 ax-1ne0 11121 ax-1rid 11122 ax-rnegex 11123 ax-rrecex 11124 ax-cnre 11125 ax-pre-lttri 11126 ax-pre-lttrn 11127 ax-pre-ltadd 11128 |
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 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3066 df-rex 3075 df-rab 3409 df-v 3448 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-po 5546 df-so 5547 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 df-ov 7361 df-er 8649 df-en 8885 df-dom 8886 df-sdom 8887 df-pnf 11192 df-mnf 11193 df-ltxr 11195 |
This theorem is referenced by: ltaddneg
11371 subsub2
11430 negsub
11450 ltaddpos
11646 addge01
11666 add20
11668 nnge1
12182 nnnn0addcl
12444 un0addcl
12447 uzaddcl
12830 xaddid1
13161 fzosubel3
13634 expadd
14011 faclbnd4lem4
14197 faclbnd6
14200 hashgadd
14278 ccatrid
14476 pfxmpt
14567 pfxfv
14571 pfxswrd
14595 pfxccatin12lem1
14617 pfxccatin12lem2
14620 swrdccat3blem
14628 cshweqrep
14710 relexpaddg
14939 reim0b
15005 rereb
15006 immul2
15023 max0add
15196 iseraltlem2
15568 fsumsplit
15627 sumsplit
15654 binomfallfaclem2
15924 pwp1fsum
16274 bitsinv1lem
16322 sadadd2lem2
16331 sadcaddlem
16338 bezoutlem1
16421 pcadd
16762 pcadd2
16763 pcmpt
16765 vdwapun
16847 vdwlem1
16854 mulgnn0dir
18907 psgnunilem2
19278 sylow1lem1
19381 efginvrel2
19510 efgredleme
19526 efgcpbllemb
19538 frgpnabllem1
19652 regsumfsum
20868 regsumsupp
21029 mplcoe5
21444 xrsxmet
24175 reparphti
24363 cphpyth
24583 minveclem6
24801 ovolunnul
24867 voliunlem3
24919 ovolioo
24935 itg2splitlem
25116 itg2split
25117 itgrevallem1
25162 itgsplitioo
25205 ditgsplit
25228 dvnadd
25296 dvlipcn
25361 ply1divex
25504 dvntaylp
25733 ulmshft
25752 abelthlem6
25798 cosmpi
25848 sinppi
25849 sinhalfpip
25852 logrnaddcl
25933 affineequiv
26176 chordthmlem3
26187 atanlogaddlem
26266 atanlogsublem
26268 leibpi
26295 scvxcvx
26338 dmgmn0
26378 lgamgulmlem2
26382 lgambdd
26389 logexprlim
26576 2sqblem
26782 2sq2
26784 2sqnn
26790 dchrvmasum2if
26848 dchrvmasumlem
26874 axcontlem8
27923 elntg2
27937 crctcshlem4
28768 eupth2lem3lem6
29180 ipidsq
29655 minvecolem6
29827 normpyc
30091 pjspansn
30522 lnfnmuli
30989 hstoh
31177 archirngz
32028 indsumin
32624 esumpfinvallem
32676 signsvtp
33198 signlem0
33202 fsum2dsub
33223 cvxpconn
33839 cvxsconn
33840 elmrsubrn
34117 faclim2
34324 fwddifn0
34752 fwddifnp1
34753 dnizeq0
34941 knoppndvlem6
34983 bj-bary1lem
35784 poimirlem1
36082 poimirlem5
36086 poimirlem6
36087 poimirlem7
36088 poimirlem11
36092 poimirlem12
36093 poimirlem17
36098 poimirlem20
36101 poimirlem22
36103 poimirlem24
36105 poimirlem25
36106 poimirlem29
36110 poimirlem31
36112 mblfinlem2
36119 mbfposadd
36128 itg2addnc
36135 itgaddnclem2
36140 ftc1anclem5
36158 ftc1anclem8
36161 areacirc
36174 lcmineqlem4
40492 lcmineqlem18
40506 aks4d1p1p7
40534 aks4d1p3
40538 sticksstones10
40566 sticksstones12a
40568 metakunt29
40608 metakunt30
40609 3cubeslem2
41011 3cubeslem3r
41013 pell1qrgaplem
41199 jm2.19lem3
41318 jm2.25
41326 relexpaddss
41997 int-add01d
42464 binomcxplemnn0
42636 fperiodmullem
43544 xralrple3
43615 sumnnodd
43878 fprodaddrecnncnvlem
44157 ioodvbdlimc1lem2
44180 volioc
44220 volico
44231 stoweidlem11
44259 stoweidlem26
44274 stirlinglem12
44333 fourierdlem4
44359 fourierdlem42
44397 fourierdlem60
44414 fourierdlem61
44415 fourierdlem92
44446 fourierdlem107
44461 fouriersw
44479 etransclem24
44506 etransclem35
44517 hoidmvlelem2
44844 hspmbllem1
44874 sharhght
45113 deccarry
45550 nn0mnd
46120 altgsumbcALT
46436 itcovalpclem1
46763 eenglngeehlnmlem2
46831 line2y
46848 itschlc0xyqsol1
46859 itschlc0xyqsol
46860 2itscp
46874 |