Metamath Proof Explorer

Theorem eulerpartlems

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 6-Aug-2018) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses eulerpartlems.r 
|- R = { f | ( `' f " NN ) e. Fin }
eulerpartlems.s 
|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
Assertion eulerpartlems 
|- ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) -> ( A ` t ) = 0 )

Proof

Step Hyp Ref Expression
1 eulerpartlems.r 
 |-  R = { f | ( `' f " NN ) e. Fin }
2 eulerpartlems.s 
 |-  S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
3 1 2 eulerpartlemsf 
 |-  S : ( ( NN0 ^m NN ) i^i R ) --> NN0
4 3 ffvelcdmi 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) e. NN0 )
5 nndiffz1 
 |-  ( ( S ` A ) e. NN0 -> ( NN \ ( 1 ... ( S ` A ) ) ) = ( ZZ>= ` ( ( S ` A ) + 1 ) ) )
6 5 eleq2d 
 |-  ( ( S ` A ) e. NN0 -> ( t e. ( NN \ ( 1 ... ( S ` A ) ) ) <-> t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) )
7 4 6 syl 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( t e. ( NN \ ( 1 ... ( S ` A ) ) ) <-> t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) )
8 7 pm5.32i 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) <-> ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) )
9 eldif 
 |-  ( t e. ( NN \ ( 1 ... ( S ` A ) ) ) <-> ( t e. NN /\ -. t e. ( 1 ... ( S ` A ) ) ) )
10 9 bilani 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( t e. NN /\ -. t e. ( 1 ... ( S ` A ) ) ) )
11 10 simpld 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> t e. NN )
12 1 2 eulerpartlemelr 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) )
13 12 simpld 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A : NN --> NN0 )
14 13 ffvelcdmda 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) -> ( A ` t ) e. NN0 )
15 11 14 syldan 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( A ` t ) e. NN0 )
16 simpl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> A e. ( ( NN0 ^m NN ) i^i R ) )
17 4 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( S ` A ) e. NN0 )
18 10 simprd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> -. t e. ( 1 ... ( S ` A ) ) )
19 simpl 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> t e. NN )
20 nnuz 
 |-  NN = ( ZZ>= ` 1 )
21 19 20 eleqtrdi 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> t e. ( ZZ>= ` 1 ) )
22 simpr 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> ( S ` A ) e. NN0 )
23 22 nn0zd 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> ( S ` A ) e. ZZ )
24 elfz5 
 |-  ( ( t e. ( ZZ>= ` 1 ) /\ ( S ` A ) e. ZZ ) -> ( t e. ( 1 ... ( S ` A ) ) <-> t <_ ( S ` A ) ) )
25 21 23 24 syl2anc 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> ( t e. ( 1 ... ( S ` A ) ) <-> t <_ ( S ` A ) ) )
26 25 notbid 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> ( -. t e. ( 1 ... ( S ` A ) ) <-> -. t <_ ( S ` A ) ) )
27 22 nn0red 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> ( S ` A ) e. RR )
28 19 nnred 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> t e. RR )
29 27 28 ltnled 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> ( ( S ` A ) < t <-> -. t <_ ( S ` A ) ) )
30 26 29 bitr4d 
 |-  ( ( t e. NN /\ ( S ` A ) e. NN0 ) -> ( -. t e. ( 1 ... ( S ` A ) ) <-> ( S ` A ) < t ) )
31 30 biimpa 
 |-  ( ( ( t e. NN /\ ( S ` A ) e. NN0 ) /\ -. t e. ( 1 ... ( S ` A ) ) ) -> ( S ` A ) < t )
32 11 17 18 31 syl21anc 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( S ` A ) < t )
33 1 2 eulerpartlemsv1 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. NN ( ( A ` k ) x. k ) )
34 fveq2 
 |-  ( k = t -> ( A ` k ) = ( A ` t ) )
35 id 
 |-  ( k = t -> k = t )
36 34 35 oveq12d 
 |-  ( k = t -> ( ( A ` k ) x. k ) = ( ( A ` t ) x. t ) )
37 36 cbvsumv 
 |-  sum_ k e. NN ( ( A ` k ) x. k ) = sum_ t e. NN ( ( A ` t ) x. t )
38 33 37 eqtr2di 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> sum_ t e. NN ( ( A ` t ) x. t ) = ( S ` A ) )
39 breq2 
 |-  ( t = l -> ( ( S ` A ) < t <-> ( S ` A ) < l ) )
40 fveq2 
 |-  ( t = l -> ( A ` t ) = ( A ` l ) )
41 40 breq2d 
 |-  ( t = l -> ( 0 < ( A ` t ) <-> 0 < ( A ` l ) ) )
42 39 41 anbi12d 
 |-  ( t = l -> ( ( ( S ` A ) < t /\ 0 < ( A ` t ) ) <-> ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) )
43 42 cbvrexvw 
 |-  ( E. t e. NN ( ( S ` A ) < t /\ 0 < ( A ` t ) ) <-> E. l e. NN ( ( S ` A ) < l /\ 0 < ( A ` l ) ) )
44 4 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ E. l e. NN ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( S ` A ) e. NN0 )
45 44 nn0red 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ E. l e. NN ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( S ` A ) e. RR )
46 4 ad2antrr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( S ` A ) e. NN0 )
47 46 nn0red 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( S ` A ) e. RR )
48 simpr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> l e. NN )
49 48 adantr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> l e. NN )
50 49 nnred 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> l e. RR )
51 1zzd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> 1 e. ZZ )
52 13 ad2antrr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ t e. NN ) -> A : NN --> NN0 )
53 simpr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ t e. NN ) -> t e. NN )
54 eqidd 
 |-  ( ( A : NN --> NN0 /\ t e. NN ) -> ( m e. NN |-> ( ( A ` m ) x. m ) ) = ( m e. NN |-> ( ( A ` m ) x. m ) ) )
55 simpr 
 |-  ( ( ( A : NN --> NN0 /\ t e. NN ) /\ m = t ) -> m = t )
56 55 fveq2d 
 |-  ( ( ( A : NN --> NN0 /\ t e. NN ) /\ m = t ) -> ( A ` m ) = ( A ` t ) )
57 56 55 oveq12d 
 |-  ( ( ( A : NN --> NN0 /\ t e. NN ) /\ m = t ) -> ( ( A ` m ) x. m ) = ( ( A ` t ) x. t ) )
58 simpr 
 |-  ( ( A : NN --> NN0 /\ t e. NN ) -> t e. NN )
59 ffvelcdm 
 |-  ( ( A : NN --> NN0 /\ t e. NN ) -> ( A ` t ) e. NN0 )
60 58 nnnn0d 
 |-  ( ( A : NN --> NN0 /\ t e. NN ) -> t e. NN0 )
61 59 60 nn0mulcld 
 |-  ( ( A : NN --> NN0 /\ t e. NN ) -> ( ( A ` t ) x. t ) e. NN0 )
62 54 57 58 61 fvmptd 
 |-  ( ( A : NN --> NN0 /\ t e. NN ) -> ( ( m e. NN |-> ( ( A ` m ) x. m ) ) ` t ) = ( ( A ` t ) x. t ) )
63 52 53 62 syl2anc 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ t e. NN ) -> ( ( m e. NN |-> ( ( A ` m ) x. m ) ) ` t ) = ( ( A ` t ) x. t ) )
64 13 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> A : NN --> NN0 )
65 64 ffvelcdmda 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ t e. NN ) -> ( A ` t ) e. NN0 )
66 53 nnnn0d 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ t e. NN ) -> t e. NN0 )
67 65 66 nn0mulcld 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ t e. NN ) -> ( ( A ` t ) x. t ) e. NN0 )
68 67 nn0red 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ t e. NN ) -> ( ( A ` t ) x. t ) e. RR )
69 fveq2 
 |-  ( m = t -> ( A ` m ) = ( A ` t ) )
70 id 
 |-  ( m = t -> m = t )
71 69 70 oveq12d 
 |-  ( m = t -> ( ( A ` m ) x. m ) = ( ( A ` t ) x. t ) )
72 71 cbvmptv 
 |-  ( m e. NN |-> ( ( A ` m ) x. m ) ) = ( t e. NN |-> ( ( A ` t ) x. t ) )
73 67 72 fmptd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( m e. NN |-> ( ( A ` m ) x. m ) ) : NN --> NN0 )
74 nn0sscn 
 |-  NN0 C_ CC
75 fss 
 |-  ( ( ( m e. NN |-> ( ( A ` m ) x. m ) ) : NN --> NN0 /\ NN0 C_ CC ) -> ( m e. NN |-> ( ( A ` m ) x. m ) ) : NN --> CC )
76 73 74 75 sylancl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( m e. NN |-> ( ( A ` m ) x. m ) ) : NN --> CC )
77 nnex 
 |-  NN e. _V
78 0nn0 
 |-  0 e. NN0
79 eqid 
 |-  ( CC \ { 0 } ) = ( CC \ { 0 } )
80 79 ffs2 
 |-  ( ( NN e. _V /\ 0 e. NN0 /\ ( m e. NN |-> ( ( A ` m ) x. m ) ) : NN --> CC ) -> ( ( m e. NN |-> ( ( A ` m ) x. m ) ) supp 0 ) = ( `' ( m e. NN |-> ( ( A ` m ) x. m ) ) " ( CC \ { 0 } ) ) )
81 77 78 80 mp3an12 
 |-  ( ( m e. NN |-> ( ( A ` m ) x. m ) ) : NN --> CC -> ( ( m e. NN |-> ( ( A ` m ) x. m ) ) supp 0 ) = ( `' ( m e. NN |-> ( ( A ` m ) x. m ) ) " ( CC \ { 0 } ) ) )
82 76 81 syl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( ( m e. NN |-> ( ( A ` m ) x. m ) ) supp 0 ) = ( `' ( m e. NN |-> ( ( A ` m ) x. m ) ) " ( CC \ { 0 } ) ) )
83 fcdmnn0supp 
 |-  ( ( NN e. _V /\ A : NN --> NN0 ) -> ( A supp 0 ) = ( `' A " NN ) )
84 77 64 83 sylancr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( A supp 0 ) = ( `' A " NN ) )
85 12 simprd 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( `' A " NN ) e. Fin )
86 85 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( `' A " NN ) e. Fin )
87 84 86 eqeltrd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( A supp 0 ) e. Fin )
88 77 a1i 
 |-  ( A : NN --> NN0 -> NN e. _V )
89 78 a1i 
 |-  ( A : NN --> NN0 -> 0 e. NN0 )
90 ffn 
 |-  ( A : NN --> NN0 -> A Fn NN )
91 simp3 
 |-  ( ( A : NN --> NN0 /\ t e. NN /\ ( A ` t ) = 0 ) -> ( A ` t ) = 0 )
92 91 oveq1d 
 |-  ( ( A : NN --> NN0 /\ t e. NN /\ ( A ` t ) = 0 ) -> ( ( A ` t ) x. t ) = ( 0 x. t ) )
93 simp2 
 |-  ( ( A : NN --> NN0 /\ t e. NN /\ ( A ` t ) = 0 ) -> t e. NN )
94 93 nncnd 
 |-  ( ( A : NN --> NN0 /\ t e. NN /\ ( A ` t ) = 0 ) -> t e. CC )
95 94 mul02d 
 |-  ( ( A : NN --> NN0 /\ t e. NN /\ ( A ` t ) = 0 ) -> ( 0 x. t ) = 0 )
96 92 95 eqtrd 
 |-  ( ( A : NN --> NN0 /\ t e. NN /\ ( A ` t ) = 0 ) -> ( ( A ` t ) x. t ) = 0 )
97 72 88 89 90 96 suppss3 
 |-  ( A : NN --> NN0 -> ( ( m e. NN |-> ( ( A ` m ) x. m ) ) supp 0 ) C_ ( A supp 0 ) )
98 64 97 syl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( ( m e. NN |-> ( ( A ` m ) x. m ) ) supp 0 ) C_ ( A supp 0 ) )
99 ssfi 
 |-  ( ( ( A supp 0 ) e. Fin /\ ( ( m e. NN |-> ( ( A ` m ) x. m ) ) supp 0 ) C_ ( A supp 0 ) ) -> ( ( m e. NN |-> ( ( A ` m ) x. m ) ) supp 0 ) e. Fin )
100 87 98 99 syl2anc 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( ( m e. NN |-> ( ( A ` m ) x. m ) ) supp 0 ) e. Fin )
101 82 100 eqeltrrd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( `' ( m e. NN |-> ( ( A ` m ) x. m ) ) " ( CC \ { 0 } ) ) e. Fin )
102 20 51 76 101 fsumcvg4 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> seq 1 ( + , ( m e. NN |-> ( ( A ` m ) x. m ) ) ) e. dom ~~> )
103 20 51 63 68 102 isumrecl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> sum_ t e. NN ( ( A ` t ) x. t ) e. RR )
104 103 adantr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> sum_ t e. NN ( ( A ` t ) x. t ) e. RR )
105 simprl 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( S ` A ) < l )
106 13 ffvelcdmda 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( A ` l ) e. NN0 )
107 106 adantr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( A ` l ) e. NN0 )
108 107 nn0red 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( A ` l ) e. RR )
109 108 50 remulcld 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( ( A ` l ) x. l ) e. RR )
110 49 nnnn0d 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> l e. NN0 )
111 110 nn0ge0d 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> 0 <_ l )
112 simprr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> 0 < ( A ` l ) )
113 elnnnn0b 
 |-  ( ( A ` l ) e. NN <-> ( ( A ` l ) e. NN0 /\ 0 < ( A ` l ) ) )
114 nnge1 
 |-  ( ( A ` l ) e. NN -> 1 <_ ( A ` l ) )
115 113 114 sylbir 
 |-  ( ( ( A ` l ) e. NN0 /\ 0 < ( A ` l ) ) -> 1 <_ ( A ` l ) )
116 107 112 115 syl2anc 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> 1 <_ ( A ` l ) )
117 50 108 111 116 lemulge12d 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> l <_ ( ( A ` l ) x. l ) )
118 106 nn0cnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( A ` l ) e. CC )
119 48 nncnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> l e. CC )
120 118 119 mulcld 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( ( A ` l ) x. l ) e. CC )
121 id 
 |-  ( t = l -> t = l )
122 40 121 oveq12d 
 |-  ( t = l -> ( ( A ` t ) x. t ) = ( ( A ` l ) x. l ) )
123 122 sumsn 
 |-  ( ( l e. NN /\ ( ( A ` l ) x. l ) e. CC ) -> sum_ t e. { l } ( ( A ` t ) x. t ) = ( ( A ` l ) x. l ) )
124 48 120 123 syl2anc 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> sum_ t e. { l } ( ( A ` t ) x. t ) = ( ( A ` l ) x. l ) )
125 snfi 
 |-  { l } e. Fin
126 125 a1i 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> { l } e. Fin )
127 48 snssd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> { l } C_ NN )
128 67 nn0ge0d 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ t e. NN ) -> 0 <_ ( ( A ` t ) x. t ) )
129 20 51 126 127 63 68 128 102 isumless 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> sum_ t e. { l } ( ( A ` t ) x. t ) <_ sum_ t e. NN ( ( A ` t ) x. t ) )
130 124 129 eqbrtrrd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) -> ( ( A ` l ) x. l ) <_ sum_ t e. NN ( ( A ` t ) x. t ) )
131 130 adantr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( ( A ` l ) x. l ) <_ sum_ t e. NN ( ( A ` t ) x. t ) )
132 50 109 104 117 131 letrd 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> l <_ sum_ t e. NN ( ( A ` t ) x. t ) )
133 47 50 104 105 132 ltletrd 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ l e. NN ) /\ ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( S ` A ) < sum_ t e. NN ( ( A ` t ) x. t ) )
134 133 r19.29an 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ E. l e. NN ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> ( S ` A ) < sum_ t e. NN ( ( A ` t ) x. t ) )
135 45 134 gtned 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ E. l e. NN ( ( S ` A ) < l /\ 0 < ( A ` l ) ) ) -> sum_ t e. NN ( ( A ` t ) x. t ) =/= ( S ` A ) )
136 135 ex 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( E. l e. NN ( ( S ` A ) < l /\ 0 < ( A ` l ) ) -> sum_ t e. NN ( ( A ` t ) x. t ) =/= ( S ` A ) ) )
137 43 136 biimtrid 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( E. t e. NN ( ( S ` A ) < t /\ 0 < ( A ` t ) ) -> sum_ t e. NN ( ( A ` t ) x. t ) =/= ( S ` A ) ) )
138 137 necon2bd 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( sum_ t e. NN ( ( A ` t ) x. t ) = ( S ` A ) -> -. E. t e. NN ( ( S ` A ) < t /\ 0 < ( A ` t ) ) ) )
139 38 138 mpd 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> -. E. t e. NN ( ( S ` A ) < t /\ 0 < ( A ` t ) ) )
140 ralnex 
 |-  ( A. t e. NN -. ( ( S ` A ) < t /\ 0 < ( A ` t ) ) <-> -. E. t e. NN ( ( S ` A ) < t /\ 0 < ( A ` t ) ) )
141 139 140 sylibr 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A. t e. NN -. ( ( S ` A ) < t /\ 0 < ( A ` t ) ) )
142 imnan 
 |-  ( ( ( S ` A ) < t -> -. 0 < ( A ` t ) ) <-> -. ( ( S ` A ) < t /\ 0 < ( A ` t ) ) )
143 142 ralbii 
 |-  ( A. t e. NN ( ( S ` A ) < t -> -. 0 < ( A ` t ) ) <-> A. t e. NN -. ( ( S ` A ) < t /\ 0 < ( A ` t ) ) )
144 141 143 sylibr 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A. t e. NN ( ( S ` A ) < t -> -. 0 < ( A ` t ) ) )
145 144 r19.21bi 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) -> ( ( S ` A ) < t -> -. 0 < ( A ` t ) ) )
146 145 imp 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) /\ ( S ` A ) < t ) -> -. 0 < ( A ` t ) )
147 16 11 32 146 syl21anc 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> -. 0 < ( A ` t ) )
148 nn0re 
 |-  ( ( A ` t ) e. NN0 -> ( A ` t ) e. RR )
149 0red 
 |-  ( ( A ` t ) e. NN0 -> 0 e. RR )
150 148 149 lenltd 
 |-  ( ( A ` t ) e. NN0 -> ( ( A ` t ) <_ 0 <-> -. 0 < ( A ` t ) ) )
151 nn0le0eq0 
 |-  ( ( A ` t ) e. NN0 -> ( ( A ` t ) <_ 0 <-> ( A ` t ) = 0 ) )
152 150 151 bitr3d 
 |-  ( ( A ` t ) e. NN0 -> ( -. 0 < ( A ` t ) <-> ( A ` t ) = 0 ) )
153 152 biimpa 
 |-  ( ( ( A ` t ) e. NN0 /\ -. 0 < ( A ` t ) ) -> ( A ` t ) = 0 )
154 15 147 153 syl2anc 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( A ` t ) = 0 )
155 8 154 sylbir 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) -> ( A ` t ) = 0 )