Step | Hyp | Ref
| Expression |
1 | | prod0 11486 |
. . . 4
|
2 | | fprodf1o.3 |
. . . . . . . . 9
|
3 | 2 | adantr 274 |
. . . . . . . 8
|
4 | | f1oeq2 5405 |
. . . . . . . . 9
|
5 | 4 | adantl 275 |
. . . . . . . 8
|
6 | 3, 5 | mpbid 146 |
. . . . . . 7
|
7 | | f1ofo 5422 |
. . . . . . 7
|
8 | 6, 7 | syl 14 |
. . . . . 6
|
9 | | fo00 5451 |
. . . . . . 7
|
10 | 9 | simprbi 273 |
. . . . . 6
|
11 | 8, 10 | syl 14 |
. . . . 5
|
12 | 11 | prodeq1d 11465 |
. . . 4
|
13 | | prodeq1 11454 |
. . . . . 6
|
14 | | prod0 11486 |
. . . . . 6
|
15 | 13, 14 | eqtrdi 2206 |
. . . . 5
|
16 | 15 | adantl 275 |
. . . 4
|
17 | 1, 12, 16 | 3eqtr4a 2216 |
. . 3
|
18 | 17 | ex 114 |
. 2
|
19 | | 2fveq3 5474 |
. . . . . . . 8
|
20 | | simprl 521 |
. . . . . . . 8
♯ ♯ ♯ |
21 | | simprr 522 |
. . . . . . . 8
♯ ♯ ♯ |
22 | | f1of 5415 |
. . . . . . . . . . . 12
|
23 | 2, 22 | syl 14 |
. . . . . . . . . . 11
|
24 | 23 | ffvelrnda 5603 |
. . . . . . . . . 10
|
25 | | fprodf1o.5 |
. . . . . . . . . . . 12
|
26 | 25 | fmpttd 5623 |
. . . . . . . . . . 11
|
27 | 26 | ffvelrnda 5603 |
. . . . . . . . . 10
|
28 | 24, 27 | syldan 280 |
. . . . . . . . 9
|
29 | 28 | adantlr 469 |
. . . . . . . 8
♯ ♯ |
30 | | simpr 109 |
. . . . . . . . . . . 12
♯ ♯ ♯ |
31 | | f1oco 5438 |
. . . . . . . . . . . 12
♯
♯ |
32 | 2, 30, 31 | syl2an 287 |
. . . . . . . . . . 11
♯ ♯ ♯ |
33 | | f1of 5415 |
. . . . . . . . . . 11
♯ ♯ |
34 | 32, 33 | syl 14 |
. . . . . . . . . 10
♯ ♯ ♯ |
35 | | fvco3 5540 |
. . . . . . . . . 10
♯
♯ |
36 | 34, 35 | sylan 281 |
. . . . . . . . 9
♯ ♯ ♯ |
37 | | f1of 5415 |
. . . . . . . . . . . . 13
♯ ♯ |
38 | 37 | adantl 275 |
. . . . . . . . . . . 12
♯ ♯ ♯ |
39 | 38 | adantl 275 |
. . . . . . . . . . 11
♯ ♯ ♯ |
40 | | fvco3 5540 |
. . . . . . . . . . 11
♯
♯ |
41 | 39, 40 | sylan 281 |
. . . . . . . . . 10
♯ ♯ ♯ |
42 | 41 | fveq2d 5473 |
. . . . . . . . 9
♯ ♯ ♯ |
43 | 36, 42 | eqtrd 2190 |
. . . . . . . 8
♯ ♯ ♯ |
44 | 19, 20, 21, 29, 43 | fprodseq 11484 |
. . . . . . 7
♯ ♯ ♯ ♯ |
45 | | eqid 2157 |
. . . . . . . . . . . . 13
|
46 | | fprodf1o.1 |
. . . . . . . . . . . . 13
|
47 | | fprodf1o.4 |
. . . . . . . . . . . . . 14
|
48 | 23 | ffvelrnda 5603 |
. . . . . . . . . . . . . 14
|
49 | 47, 48 | eqeltrrd 2235 |
. . . . . . . . . . . . 13
|
50 | 46 | eleq1d 2226 |
. . . . . . . . . . . . . 14
|
51 | 25 | ralrimiva 2530 |
. . . . . . . . . . . . . . 15
|
52 | 51 | adantr 274 |
. . . . . . . . . . . . . 14
|
53 | 50, 52, 49 | rspcdva 2821 |
. . . . . . . . . . . . 13
|
54 | 45, 46, 49, 53 | fvmptd3 5562 |
. . . . . . . . . . . 12
|
55 | 47 | fveq2d 5473 |
. . . . . . . . . . . 12
|
56 | | simpr 109 |
. . . . . . . . . . . . 13
|
57 | | eqid 2157 |
. . . . . . . . . . . . . 14
|
58 | 57 | fvmpt2 5552 |
. . . . . . . . . . . . 13
|
59 | 56, 53, 58 | syl2anc 409 |
. . . . . . . . . . . 12
|
60 | 54, 55, 59 | 3eqtr4rd 2201 |
. . . . . . . . . . 11
|
61 | 60 | ralrimiva 2530 |
. . . . . . . . . 10
|
62 | | nffvmpt1 5480 |
. . . . . . . . . . . 12
|
63 | 62 | nfeq1 2309 |
. . . . . . . . . . 11
|
64 | | fveq2 5469 |
. . . . . . . . . . . 12
|
65 | | 2fveq3 5474 |
. . . . . . . . . . . 12
|
66 | 64, 65 | eqeq12d 2172 |
. . . . . . . . . . 11
|
67 | 63, 66 | rspc 2810 |
. . . . . . . . . 10
|
68 | 61, 67 | mpan9 279 |
. . . . . . . . 9
|
69 | 68 | adantlr 469 |
. . . . . . . 8
♯ ♯ |
70 | 69 | prodeq2dv 11467 |
. . . . . . 7
♯ ♯
|
71 | | fveq2 5469 |
. . . . . . . 8
|
72 | 26 | adantr 274 |
. . . . . . . . 9
♯ ♯ |
73 | 72 | ffvelrnda 5603 |
. . . . . . . 8
♯ ♯ |
74 | 71, 20, 32, 73, 36 | fprodseq 11484 |
. . . . . . 7
♯ ♯ ♯ ♯ |
75 | 44, 70, 74 | 3eqtr4rd 2201 |
. . . . . 6
♯ ♯
|
76 | 51 | adantr 274 |
. . . . . . 7
♯ ♯
|
77 | | prodfct 11488 |
. . . . . . 7
|
78 | 76, 77 | syl 14 |
. . . . . 6
♯ ♯
|
79 | 53 | ralrimiva 2530 |
. . . . . . . 8
|
80 | 79 | adantr 274 |
. . . . . . 7
♯ ♯
|
81 | | prodfct 11488 |
. . . . . . 7
|
82 | 80, 81 | syl 14 |
. . . . . 6
♯ ♯
|
83 | 75, 78, 82 | 3eqtr3d 2198 |
. . . . 5
♯ ♯ |
84 | 83 | expr 373 |
. . . 4
♯ ♯ |
85 | 84 | exlimdv 1799 |
. . 3
♯ ♯
|
86 | 85 | expimpd 361 |
. 2
♯ ♯
|
87 | | fprodf1o.2 |
. . 3
|
88 | | fz1f1o 11276 |
. . 3
♯ ♯ |
89 | 87, 88 | syl 14 |
. 2
♯ ♯ |
90 | 18, 86, 89 | mpjaod 708 |
1
|