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