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

Theorem smuval2 12689
 Description: The partial sum sequence stabilizes at after the -th element of the sequence; this stable value is the value of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016.)
Hypotheses
Ref Expression
smuval.a
smuval.b
smuval.n
smuval2.m
Assertion
Ref Expression
smuval2 smul
Distinct variable groups:   ,,,   ,   ,   ,,,
Allowed substitution hints:   (,)   (,,)   (,,)   (,)

Proof of Theorem smuval2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smuval2.m . 2
2 fveq2 5541 . . . . . 6
32eleq2d 2363 . . . . 5
43bibi2d 309 . . . 4 smul smul
54imbi2d 307 . . 3 smul smul
6 fveq2 5541 . . . . . 6
76eleq2d 2363 . . . . 5
87bibi2d 309 . . . 4 smul smul
98imbi2d 307 . . 3 smul smul
10 fveq2 5541 . . . . . 6
1110eleq2d 2363 . . . . 5
1211bibi2d 309 . . . 4 smul smul
1312imbi2d 307 . . 3 smul smul
14 fveq2 5541 . . . . . 6
1514eleq2d 2363 . . . . 5
1615bibi2d 309 . . . 4 smul smul
1716imbi2d 307 . . 3 smul smul
18 smuval.a . . . . 5
19 smuval.b . . . . 5
20 smuval.p . . . . 5 sadd
21 smuval.n . . . . 5
2218, 19, 20, 21smuval 12688 . . . 4 smul
2322a1i 10 . . 3 smul
2418adantr 451 . . . . . . . . . 10
2519adantr 451 . . . . . . . . . 10
26 peano2nn0 10020 . . . . . . . . . . . 12
2721, 26syl 15 . . . . . . . . . . 11
28 eluznn0 10304 . . . . . . . . . . 11
2927, 28sylan 457 . . . . . . . . . 10
3024, 25, 20, 29smupp1 12687 . . . . . . . . 9 sadd
3130eleq2d 2363 . . . . . . . 8 sadd
3224, 25, 20smupf 12685 . . . . . . . . . . . . . . 15
33 ffvelrn 5679 . . . . . . . . . . . . . . 15
3432, 29, 33syl2anc 642 . . . . . . . . . . . . . 14
35 elpwi 3646 . . . . . . . . . . . . . 14
3634, 35syl 15 . . . . . . . . . . . . 13
37 ssrab2 3271 . . . . . . . . . . . . . 14
3837a1i 10 . . . . . . . . . . . . 13
3927adantr 451 . . . . . . . . . . . . 13
4036, 38, 39sadeq 12679 . . . . . . . . . . . 12 sadd ..^ ..^ sadd ..^ ..^
41 inrab2 3454 . . . . . . . . . . . . . . . . 17 ..^ ..^
42 inss1 3402 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
43 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
4442, 43sseldi 3191 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
4544nn0red 10035 . . . . . . . . . . . . . . . . . . . . . 22 ..^
4621adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25
4746adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
4847nn0red 10035 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
49 1re 8853 . . . . . . . . . . . . . . . . . . . . . . . 24
5049a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
5148, 50readdcld 8878 . . . . . . . . . . . . . . . . . . . . . 22 ..^
5229adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
5352nn0red 10035 . . . . . . . . . . . . . . . . . . . . . 22 ..^
54 inss2 3403 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
5554, 43sseldi 3191 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
56 elfzolt2 10899 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
5755, 56syl 15 . . . . . . . . . . . . . . . . . . . . . 22 ..^
58 eluzle 10256 . . . . . . . . . . . . . . . . . . . . . . 23
5958ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . 22 ..^
6045, 51, 53, 57, 59ltletrd 8992 . . . . . . . . . . . . . . . . . . . . 21 ..^
6145, 53ltnled 8982 . . . . . . . . . . . . . . . . . . . . 21 ..^
6260, 61mpbid 201 . . . . . . . . . . . . . . . . . . . 20 ..^
6325adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
6463sseld 3192 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
65 nn0ge0 10007 . . . . . . . . . . . . . . . . . . . . . . 23
6664, 65syl6 29 . . . . . . . . . . . . . . . . . . . . . 22 ..^
6745, 53subge0d 9378 . . . . . . . . . . . . . . . . . . . . . 22 ..^
6866, 67sylibd 205 . . . . . . . . . . . . . . . . . . . . 21 ..^
6968adantld 453 . . . . . . . . . . . . . . . . . . . 20 ..^
7062, 69mtod 168 . . . . . . . . . . . . . . . . . . 19 ..^
7170ralrimiva 2639 . . . . . . . . . . . . . . . . . 18 ..^
72 rabeq0 3489 . . . . . . . . . . . . . . . . . 18 ..^ ..^
7371, 72sylibr 203 . . . . . . . . . . . . . . . . 17 ..^
7441, 73syl5eq 2340 . . . . . . . . . . . . . . . 16 ..^
7574oveq2d 5890 . . . . . . . . . . . . . . 15 ..^ sadd ..^ ..^ sadd
76 inss1 3402 . . . . . . . . . . . . . . . . 17 ..^
7776, 36syl5ss 3203 . . . . . . . . . . . . . . . 16 ..^
78 sadid1 12675 . . . . . . . . . . . . . . . 16 ..^ ..^ sadd ..^
7977, 78syl 15 . . . . . . . . . . . . . . 15 ..^ sadd ..^
8075, 79eqtrd 2328 . . . . . . . . . . . . . 14 ..^ sadd ..^ ..^
8180ineq1d 3382 . . . . . . . . . . . . 13 ..^ sadd ..^ ..^ ..^ ..^
82 inass 3392 . . . . . . . . . . . . . 14 ..^ ..^ ..^ ..^
83 inidm 3391 . . . . . . . . . . . . . . 15 ..^ ..^ ..^
8483ineq2i 3380 . . . . . . . . . . . . . 14 ..^ ..^ ..^
8582, 84eqtri 2316 . . . . . . . . . . . . 13 ..^ ..^ ..^
8681, 85syl6eq 2344 . . . . . . . . . . . 12 ..^ sadd ..^ ..^ ..^
8740, 86eqtrd 2328 . . . . . . . . . . 11 sadd ..^ ..^
8887eleq2d 2363 . . . . . . . . . 10 sadd ..^ ..^
89 elin 3371 . . . . . . . . . 10 sadd ..^ sadd ..^
90 elin 3371 . . . . . . . . . 10 ..^ ..^
9188, 89, 903bitr3g 278 . . . . . . . . 9 sadd ..^ ..^
92 nn0uz 10278 . . . . . . . . . . . . 13
9346, 92syl6eleq 2386 . . . . . . . . . . . 12
94 eluzfz2 10820 . . . . . . . . . . . 12
9593, 94syl 15 . . . . . . . . . . 11
9646nn0zd 10131 . . . . . . . . . . . 12
97 fzval3 10927 . . . . . . . . . . . 12 ..^
9896, 97syl 15 . . . . . . . . . . 11 ..^
9995, 98eleqtrd 2372 . . . . . . . . . 10 ..^
10099biantrud 493 . . . . . . . . 9 sadd sadd ..^
10199biantrud 493 . . . . . . . . 9 ..^
10291, 100, 1013bitr4d 276 . . . . . . . 8 sadd
10331, 102bitrd 244 . . . . . . 7
104103bibi2d 309 . . . . . 6 smul smul
105104biimprd 214 . . . . 5 smul smul
106105expcom 424 . . . 4 smul smul
107106a2d 23 . . 3 smul smul
1085, 9, 13, 17, 23, 107uzind4 10292 . 2 smul
1091, 108mpcom 32 1 smul