Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2106 Vcvv 3474
0cc0 11112 − cmin 11448
-cneg 11449 |
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-ext 2703 ax-nul 5306 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ne 2941 df-v 3476 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-sn 4629 df-pr 4631 df-uni 4909 df-iota 6495 df-fv 6551 df-ov 7414 df-neg 11451 |
This theorem is referenced by: negiso
12198 infrenegsup
12201 xnegex
13191 ceilval
13807 monoord2
14003 m1expcl2
14055 sgnval
15039 infcvgaux1i
15807 infcvgaux2i
15808 cnmsgnsubg
21349 evth2
24700 ivth2
25196 mbfinf
25406 mbfi1flimlem
25464 i1fibl
25549 ditgex
25593 dvrec
25696 dvmptsub
25708 dvexp3
25719 rolle
25731 dvlipcn
25735 dvivth
25751 lhop2
25756 dvfsumge
25763 ftc2
25785 plyremlem
26041 advlogexp
26387 logtayl
26392 logccv
26395 dvatan
26664 amgmlem
26718 emcllem7
26730 basellem9
26817 addsqnreup
27170 axlowdimlem7
28461 axlowdimlem8
28462 axlowdimlem9
28463 axlowdimlem13
28467 sgnsval
32578 sgnsf
32579 xrge0iifcv
33200 xrge0iifiso
33201 xrge0iifhom
33203 sgncl
33823 dvtan
36841 ftc1anclem5
36868 ftc1anclem6
36869 ftc2nc
36873 areacirclem1
36879 monotoddzzfi
41983 monotoddzz
41984 oddcomabszz
41985 rngunsnply
42217 infnsuprnmpt
44253 liminfltlem
44819 dvcosax
44941 itgsin0pilem1
44965 fourierdlem41
45163 fourierdlem48
45169 fourierdlem102
45223 fourierdlem114
45235 fourierswlem
45245 hoicvr
45563 hoicvrrex
45571 smfliminflem
45845 zlmodzxzldeplem3
47271 amgmwlem
47937 |