Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 (class class class)co 7358
ℂcc 11050 0cc0 11052
− cmin 11386 |
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-reu 3355 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-riota 7314 df-ov 7361 df-oprab 7362 df-mpo 7363 df-er 8649 df-en 8885 df-dom 8886 df-sdom 8887 df-pnf 11192 df-mnf 11193 df-ltxr 11195 df-sub 11388 |
This theorem is referenced by: suble0
11670 lesub0
11673 ltm1
11998 nn0sub
12464 max0sub
13116 modid
13802 modeqmodmin
13847 muldivbinom2
14164 bcn0
14211 bcnn
14213 hashfzo0
14331 hashfz0
14333 ccatlid
14475 pfxmpt
14567 pfxfv
14571 swrdpfx
14596 pfxpfx
14597 cshwsublen
14685 remul2
15016 clim0c
15390 rlimrecl
15463 o1rlimmul
15502 rlimno1
15539 incexclem
15722 supcvg
15742 pwdif
15754 geolim
15756 fallfacval3
15896 binomfallfaclem2
15924 bpolydiflem
15938 bpoly3
15942 addmodlteqALT
16208 dvdsmod
16212 ndvdssub
16292 nn0seqcvgd
16447 phiprmpw
16649 pczpre
16720 pcaddlem
16761 pcmpt2
16766 prmreclem4
16792 4sqlem9
16819 4sqlem11
16828 ramcl
16902 oddvdsnn0
19327 odf1o2
19356 srgbinomlem4
19961 zndvds0
20960 psrlidm
21375 coe1sclmul
21656 coe1sclmul2
21658 cply1mul
21668 recld2
24180 i1fadd
25062 mbfi1fseqlem6
25088 itgposval
25163 dveflem
25346 dv11cn
25368 lhop1lem
25380 coemulc
25619 plydivlem3
25658 plyrem
25668 vieta1lem2
25674 aareccl
25689 aalioulem3
25697 aaliou2b
25704 dvntaylp
25733 taylthlem1
25735 psercn
25788 pserdvlem2
25790 abelthlem2
25794 abelthlem3
25795 abelthlem5
25797 abelthlem7
25800 sinmpi
25847 cosppi
25850 sinhalfpim
25853 sincosq2sgn
25859 logcnlem3
26002 logcnlem4
26003 advlog
26012 efopn
26016 logtayl
26018 pythag
26170 chordthmlem5
26189 atanlogsublem
26268 rlimcnp
26318 efrlim
26322 rlimcxp
26326 cxploglim2
26331 emcllem5
26352 zetacvg
26367 lgamgulmlem2
26382 lgamcvg2
26407 0sgmppw
26549 ppiub
26555 chtublem
26562 logfacrlim
26575 logexprlim
26576 chtppilimlem2
26825 rplogsumlem2
26836 dchrisumlem3
26842 dchrvmasumiflem1
26852 dchrisum0lem2
26869 selberg2lem
26901 logdivbnd
26907 pntrsumo1
26916 pntrlog2bndlem4
26931 pntpbnd1
26937 axlowdimlem17
27910 crctcshlem4
28768 clwlkclwwlklem2a1
28939 clwlkclwwlklem2a
28945 clwlkclwwlklem3
28948 clwlkclwwlk
28949 ipidsq
29655 nmcfnexi
30996 freshmansdream
32070 sgnsub
33147 knoppndvlem10
34987 poimirlem19
36100 poimirlem20
36101 ftc1anc
36162 cntotbnd
36258 aks4d1p1p2
40530 aks4d1p1p7
40534 irrapxlem3
41150 irrapxlem4
41151 pell14qrgt0
41185 pell1qrgaplem
41199 acongeq
41310 jm2.18
41315 hashnzfz
42607 hashnzfz2
42608 hashnzfzclim
42609 bccn1
42631 binomcxplemnotnn0
42643 dstregt0
43522 absimlere
43722 ellimcabssub0
43865 0ellimcdiv
43897 clim0cf
43902 fprodsubrecnncnvlem
44155 ioodvbdlimc2lem
44182 dvnxpaek
44190 dvnmul
44191 itgsbtaddcnst
44230 stoweidlem7
44255 stoweidlem11
44259 stoweidlem26
44274 dirkertrigeqlem2
44347 fourierdlem57
44411 fourierdlem60
44414 fourierdlem61
44415 fourierdlem68
44422 fourierdlem104
44458 fourierdlem107
44461 fourierdlem109
44463 etransclem4
44486 etransclem23
44505 etransclem27
44509 etransclem31
44513 etransclem35
44517 sigarexp
45107 sigaradd
45114 m1modmmod
46614 dignn0flhalflem1
46708 ehl2eudisval0
46818 2sphere0
46843 line2
46845 line2x
46847 itschlc0yqe
46853 itschlc0xyqsol1
46859 itschlc0xyqsol
46860 |