Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  smupvallem Unicode version

Theorem smupvallem 12690
 Description: If only has elements less than , then all elements of the partial sum sequence past already equal the final value. (Contributed by Mario Carneiro, 20-Sep-2016.)
Hypotheses
Ref Expression
smuval.a
smuval.b
smuval.n
smupvallem.a ..^
smupvallem.m
Assertion
Ref Expression
smupvallem smul
Distinct variable groups:   ,,,   ,   ,   ,,,
Allowed substitution hints:   (,)   (,,)   (,,)   (,)

Proof of Theorem smupvallem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smuval.a . . . . . . 7
2 smuval.b . . . . . . 7
3 smuval.p . . . . . . 7 sadd
41, 2, 3smupf 12685 . . . . . 6
5 smuval.n . . . . . . 7
6 smupvallem.m . . . . . . 7
7 eluznn0 10304 . . . . . . 7
85, 6, 7syl2anc 642 . . . . . 6
9 ffvelrn 5679 . . . . . 6
104, 8, 9syl2anc 642 . . . . 5
11 elpwi 3646 . . . . 5
1210, 11syl 15 . . . 4
1312sseld 3192 . . 3
14 ssrab2 3271 . . . . 5
151, 2, 3smufval 12684 . . . . . 6 smul
1615sseq1d 3218 . . . . 5 smul
1714, 16mpbiri 224 . . . 4 smul
1817sseld 3192 . . 3 smul
191ad2antrr 706 . . . . . . 7
202ad2antrr 706 . . . . . . 7
21 simplr 731 . . . . . . 7
226adantr 451 . . . . . . . 8
23 uztrn 10260 . . . . . . . 8
2422, 23sylan 457 . . . . . . 7
2519, 20, 3, 21, 24smuval2 12689 . . . . . 6 smul
2625bicomd 192 . . . . 5 smul
276ad2antrr 706 . . . . . . . . 9
28 simpll 730 . . . . . . . . 9
29 fveq2 5541 . . . . . . . . . . . 12
3029eqeq1d 2304 . . . . . . . . . . 11
3130imbi2d 307 . . . . . . . . . 10
32 fveq2 5541 . . . . . . . . . . . 12
3332eqeq1d 2304 . . . . . . . . . . 11
3433imbi2d 307 . . . . . . . . . 10
35 fveq2 5541 . . . . . . . . . . . 12
3635eqeq1d 2304 . . . . . . . . . . 11
3736imbi2d 307 . . . . . . . . . 10
38 fveq2 5541 . . . . . . . . . . . 12
3938eqeq1d 2304 . . . . . . . . . . 11
4039imbi2d 307 . . . . . . . . . 10
41 eqidd 2297 . . . . . . . . . . 11
4241a1i 10 . . . . . . . . . 10
431adantr 451 . . . . . . . . . . . . . . . 16
442adantr 451 . . . . . . . . . . . . . . . 16
45 eluznn0 10304 . . . . . . . . . . . . . . . . 17
465, 45sylan 457 . . . . . . . . . . . . . . . 16
4743, 44, 3, 46smupp1 12687 . . . . . . . . . . . . . . 15 sadd
48 eluzle 10256 . . . . . . . . . . . . . . . . . . . . 21
4948adantl 452 . . . . . . . . . . . . . . . . . . . 20
505nn0red 10035 . . . . . . . . . . . . . . . . . . . . . 22
5150adantr 451 . . . . . . . . . . . . . . . . . . . . 21
5246nn0red 10035 . . . . . . . . . . . . . . . . . . . . 21
5351, 52lenltd 8981 . . . . . . . . . . . . . . . . . . . 20
5449, 53mpbid 201 . . . . . . . . . . . . . . . . . . 19
55 smupvallem.a . . . . . . . . . . . . . . . . . . . . . . 23 ..^
5655adantr 451 . . . . . . . . . . . . . . . . . . . . . 22 ..^
5756sseld 3192 . . . . . . . . . . . . . . . . . . . . 21 ..^
58 elfzolt2 10899 . . . . . . . . . . . . . . . . . . . . 21 ..^
5957, 58syl6 29 . . . . . . . . . . . . . . . . . . . 20
6059adantrd 454 . . . . . . . . . . . . . . . . . . 19
6154, 60mtod 168 . . . . . . . . . . . . . . . . . 18
6261ralrimivw 2640 . . . . . . . . . . . . . . . . 17
63 rabeq0 3489 . . . . . . . . . . . . . . . . 17
6462, 63sylibr 203 . . . . . . . . . . . . . . . 16
6564oveq2d 5890 . . . . . . . . . . . . . . 15 sadd sadd
664adantr 451 . . . . . . . . . . . . . . . . . 18
67 ffvelrn 5679 . . . . . . . . . . . . . . . . . 18
6866, 46, 67syl2anc 642 . . . . . . . . . . . . . . . . 17
69 elpwi 3646 . . . . . . . . . . . . . . . . 17
7068, 69syl 15 . . . . . . . . . . . . . . . 16
71 sadid1 12675 . . . . . . . . . . . . . . . 16 sadd
7270, 71syl 15 . . . . . . . . . . . . . . 15 sadd
7347, 65, 723eqtrd 2332 . . . . . . . . . . . . . 14
7473eqeq1d 2304 . . . . . . . . . . . . 13
7574biimprd 214 . . . . . . . . . . . 12
7675expcom 424 . . . . . . . . . . 11
7776a2d 23 . . . . . . . . . 10
7831, 34, 37, 40, 42, 77uzind4 10292 . . . . . . . . 9
7927, 28, 78sylc 56 . . . . . . . 8
80 simpr 447 . . . . . . . . 9
8131, 34, 37, 37, 42, 77uzind4 10292 . . . . . . . . 9
8280, 28, 81sylc 56 . . . . . . . 8
8379, 82eqtr4d 2331 . . . . . . 7
8483eleq2d 2363 . . . . . 6
851ad2antrr 706 . . . . . . 7
862ad2antrr 706 . . . . . . 7
87 simplr 731 . . . . . . 7
8885, 86, 3, 87smuval 12688 . . . . . 6 smul
8984, 88bitr4d 247 . . . . 5 smul
90 simpr 447 . . . . . . . 8
9190nn0zd 10131 . . . . . . 7
9291peano2zd 10136 . . . . . 6
935nn0zd 10131 . . . . . . 7
9493adantr 451 . . . . . 6
95 uztric 10265 . . . . . 6
9692, 94, 95syl2anc 642 . . . . 5
9726, 89, 96mpjaodan 761 . . . 4 smul
9897ex 423 . . 3 smul
9913, 18, 98pm5.21ndd 343 . 2 smul
10099eqrdv 2294 1 smul