Step |
Hyp |
Ref |
Expression |
1 |
|
fsumge0.1 |
|- ( ph -> A e. Fin ) |
2 |
|
fsumge0.2 |
|- ( ( ph /\ k e. A ) -> B e. RR ) |
3 |
|
fsumge0.3 |
|- ( ( ph /\ k e. A ) -> 0 <_ B ) |
4 |
1
|
adantr |
|- ( ( ph /\ m e. A ) -> A e. Fin ) |
5 |
2
|
adantlr |
|- ( ( ( ph /\ m e. A ) /\ k e. A ) -> B e. RR ) |
6 |
3
|
adantlr |
|- ( ( ( ph /\ m e. A ) /\ k e. A ) -> 0 <_ B ) |
7 |
|
snssi |
|- ( m e. A -> { m } C_ A ) |
8 |
7
|
adantl |
|- ( ( ph /\ m e. A ) -> { m } C_ A ) |
9 |
4 5 6 8
|
fsumless |
|- ( ( ph /\ m e. A ) -> sum_ k e. { m } B <_ sum_ k e. A B ) |
10 |
9
|
adantlr |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> sum_ k e. { m } B <_ sum_ k e. A B ) |
11 |
|
simpr |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> m e. A ) |
12 |
2 3
|
jca |
|- ( ( ph /\ k e. A ) -> ( B e. RR /\ 0 <_ B ) ) |
13 |
12
|
ralrimiva |
|- ( ph -> A. k e. A ( B e. RR /\ 0 <_ B ) ) |
14 |
13
|
adantr |
|- ( ( ph /\ sum_ k e. A B = 0 ) -> A. k e. A ( B e. RR /\ 0 <_ B ) ) |
15 |
|
nfcsb1v |
|- F/_ k [_ m / k ]_ B |
16 |
15
|
nfel1 |
|- F/ k [_ m / k ]_ B e. RR |
17 |
|
nfcv |
|- F/_ k 0 |
18 |
|
nfcv |
|- F/_ k <_ |
19 |
17 18 15
|
nfbr |
|- F/ k 0 <_ [_ m / k ]_ B |
20 |
16 19
|
nfan |
|- F/ k ( [_ m / k ]_ B e. RR /\ 0 <_ [_ m / k ]_ B ) |
21 |
|
csbeq1a |
|- ( k = m -> B = [_ m / k ]_ B ) |
22 |
21
|
eleq1d |
|- ( k = m -> ( B e. RR <-> [_ m / k ]_ B e. RR ) ) |
23 |
21
|
breq2d |
|- ( k = m -> ( 0 <_ B <-> 0 <_ [_ m / k ]_ B ) ) |
24 |
22 23
|
anbi12d |
|- ( k = m -> ( ( B e. RR /\ 0 <_ B ) <-> ( [_ m / k ]_ B e. RR /\ 0 <_ [_ m / k ]_ B ) ) ) |
25 |
20 24
|
rspc |
|- ( m e. A -> ( A. k e. A ( B e. RR /\ 0 <_ B ) -> ( [_ m / k ]_ B e. RR /\ 0 <_ [_ m / k ]_ B ) ) ) |
26 |
14 25
|
mpan9 |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> ( [_ m / k ]_ B e. RR /\ 0 <_ [_ m / k ]_ B ) ) |
27 |
26
|
simpld |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> [_ m / k ]_ B e. RR ) |
28 |
27
|
recnd |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> [_ m / k ]_ B e. CC ) |
29 |
|
sumsns |
|- ( ( m e. A /\ [_ m / k ]_ B e. CC ) -> sum_ k e. { m } B = [_ m / k ]_ B ) |
30 |
11 28 29
|
syl2anc |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> sum_ k e. { m } B = [_ m / k ]_ B ) |
31 |
|
simplr |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> sum_ k e. A B = 0 ) |
32 |
10 30 31
|
3brtr3d |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> [_ m / k ]_ B <_ 0 ) |
33 |
26
|
simprd |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> 0 <_ [_ m / k ]_ B ) |
34 |
|
0re |
|- 0 e. RR |
35 |
|
letri3 |
|- ( ( [_ m / k ]_ B e. RR /\ 0 e. RR ) -> ( [_ m / k ]_ B = 0 <-> ( [_ m / k ]_ B <_ 0 /\ 0 <_ [_ m / k ]_ B ) ) ) |
36 |
27 34 35
|
sylancl |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> ( [_ m / k ]_ B = 0 <-> ( [_ m / k ]_ B <_ 0 /\ 0 <_ [_ m / k ]_ B ) ) ) |
37 |
32 33 36
|
mpbir2and |
|- ( ( ( ph /\ sum_ k e. A B = 0 ) /\ m e. A ) -> [_ m / k ]_ B = 0 ) |
38 |
37
|
ralrimiva |
|- ( ( ph /\ sum_ k e. A B = 0 ) -> A. m e. A [_ m / k ]_ B = 0 ) |
39 |
|
nfv |
|- F/ m B = 0 |
40 |
15
|
nfeq1 |
|- F/ k [_ m / k ]_ B = 0 |
41 |
21
|
eqeq1d |
|- ( k = m -> ( B = 0 <-> [_ m / k ]_ B = 0 ) ) |
42 |
39 40 41
|
cbvralw |
|- ( A. k e. A B = 0 <-> A. m e. A [_ m / k ]_ B = 0 ) |
43 |
38 42
|
sylibr |
|- ( ( ph /\ sum_ k e. A B = 0 ) -> A. k e. A B = 0 ) |
44 |
43
|
ex |
|- ( ph -> ( sum_ k e. A B = 0 -> A. k e. A B = 0 ) ) |
45 |
|
sumz |
|- ( ( A C_ ( ZZ>= ` 0 ) \/ A e. Fin ) -> sum_ k e. A 0 = 0 ) |
46 |
45
|
olcs |
|- ( A e. Fin -> sum_ k e. A 0 = 0 ) |
47 |
|
sumeq2 |
|- ( A. k e. A B = 0 -> sum_ k e. A B = sum_ k e. A 0 ) |
48 |
47
|
eqeq1d |
|- ( A. k e. A B = 0 -> ( sum_ k e. A B = 0 <-> sum_ k e. A 0 = 0 ) ) |
49 |
46 48
|
syl5ibrcom |
|- ( A e. Fin -> ( A. k e. A B = 0 -> sum_ k e. A B = 0 ) ) |
50 |
1 49
|
syl |
|- ( ph -> ( A. k e. A B = 0 -> sum_ k e. A B = 0 ) ) |
51 |
44 50
|
impbid |
|- ( ph -> ( sum_ k e. A B = 0 <-> A. k e. A B = 0 ) ) |