Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1533
∈ wcel 2098 (class class class)co 7404
ℂcc 11107 0cc0 11109
+ caddc 11112 |
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 2697 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7721 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 |
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 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5142 df-opab 5204 df-mpt 5225 df-id 5567 df-po 5581 df-so 5582 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-iota 6488 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7407 df-er 8702 df-en 8939 df-dom 8940 df-sdom 8941 df-pnf 11251 df-mnf 11252 df-ltxr 11254 |
This theorem is referenced by: ltaddneg
11430 subsub2
11489 negsub
11509 ltaddpos
11705 addge01
11725 add20
11727 nnge1
12241 nnnn0addcl
12503 un0addcl
12506 uzaddcl
12889 xaddrid
13223 fzosubel3
13696 expadd
14073 faclbnd4lem4
14259 faclbnd6
14262 hashgadd
14340 ccatrid
14541 pfxmpt
14632 pfxfv
14636 pfxswrd
14660 pfxccatin12lem1
14682 pfxccatin12lem2
14685 swrdccat3blem
14693 cshweqrep
14775 relexpaddg
15004 reim0b
15070 rereb
15071 immul2
15088 max0add
15261 iseraltlem2
15633 fsumsplit
15691 sumsplit
15718 binomfallfaclem2
15988 pwp1fsum
16339 bitsinv1lem
16387 sadadd2lem2
16396 sadcaddlem
16403 bezoutlem1
16486 pcadd
16829 pcadd2
16830 pcmpt
16832 vdwapun
16914 vdwlem1
16921 mulgnn0dir
19029 psgnunilem2
19413 sylow1lem1
19516 efginvrel2
19645 efgredleme
19661 efgcpbllemb
19673 frgpnabllem1
19791 regsumfsum
21325 pzriprnglem10
21373 regsumsupp
21511 mplcoe5
21933 xrsxmet
24676 reparphti
24874 reparphtiOLD
24875 cphpyth
25095 minveclem6
25313 ovolunnul
25380 voliunlem3
25432 ovolioo
25448 itg2splitlem
25629 itg2split
25630 itgrevallem1
25675 itgsplitioo
25718 ditgsplit
25741 dvnadd
25810 dvlipcn
25878 ply1divex
26023 dvntaylp
26257 ulmshft
26277 abelthlem6
26324 cosmpi
26374 sinppi
26375 sinhalfpip
26378 logrnaddcl
26459 affineequiv
26706 chordthmlem3
26717 atanlogaddlem
26796 atanlogsublem
26798 leibpi
26825 scvxcvx
26869 dmgmn0
26909 lgamgulmlem2
26913 lgambdd
26920 logexprlim
27109 2sqblem
27315 2sq2
27317 2sqnn
27323 dchrvmasum2if
27381 dchrvmasumlem
27407 axcontlem8
28733 elntg2
28747 crctcshlem4
29579 eupth2lem3lem6
29991 ipidsq
30468 minvecolem6
30640 normpyc
30904 pjspansn
31335 lnfnmuli
31802 hstoh
31990 archirngz
32839 indsumin
33550 esumpfinvallem
33602 signsvtp
34124 signlem0
34128 fsum2dsub
34148 cvxpconn
34761 cvxsconn
34762 elmrsubrn
35039 faclim2
35251 fwddifn0
35669 fwddifnp1
35670 dnizeq0
35859 knoppndvlem6
35901 bj-bary1lem
36698 poimirlem1
37000 poimirlem5
37004 poimirlem6
37005 poimirlem7
37006 poimirlem11
37010 poimirlem12
37011 poimirlem17
37016 poimirlem20
37019 poimirlem22
37021 poimirlem24
37023 poimirlem25
37024 poimirlem29
37028 poimirlem31
37030 mblfinlem2
37037 mbfposadd
37046 itg2addnc
37053 itgaddnclem2
37058 ftc1anclem5
37076 ftc1anclem8
37079 areacirc
37092 lcmineqlem4
41411 lcmineqlem18
41425 aks4d1p1p7
41453 aks4d1p3
41457 posbezout
41478 sticksstones10
41513 sticksstones12a
41515 metakunt29
41555 metakunt30
41556 3cubeslem2
41982 3cubeslem3r
41984 pell1qrgaplem
42170 jm2.19lem3
42289 jm2.25
42297 relexpaddss
43026 int-add01d
43493 binomcxplemnn0
43665 fperiodmullem
44566 xralrple3
44637 sumnnodd
44899 fprodaddrecnncnvlem
45178 ioodvbdlimc1lem2
45201 volioc
45241 volico
45252 stoweidlem11
45280 stoweidlem26
45295 stirlinglem12
45354 fourierdlem4
45380 fourierdlem42
45418 fourierdlem60
45435 fourierdlem61
45436 fourierdlem92
45467 fourierdlem107
45482 fouriersw
45500 etransclem24
45527 etransclem35
45538 hoidmvlelem2
45865 hspmbllem1
45895 sharhght
46134 deccarry
46572 nn0mnd
47110 altgsumbcALT
47286 itcovalpclem1
47612 eenglngeehlnmlem2
47680 line2y
47697 itschlc0xyqsol1
47708 itschlc0xyqsol
47709 2itscp
47723 |