Step | Hyp | Ref
| Expression |
1 | | 1t1e1 11175 |
. . . . 5
|
2 | | prod0 14673 |
. . . . . 6
|
3 | | prod0 14673 |
. . . . . 6
|
4 | 2, 3 | oveq12i 6662 |
. . . . 5
|
5 | | prod0 14673 |
. . . . 5
|
6 | 1, 4, 5 | 3eqtr4ri 2655 |
. . . 4
|
7 | | prodeq1 14639 |
. . . 4
|
8 | | prodeq1 14639 |
. . . . 5
|
9 | | prodeq1 14639 |
. . . . 5
|
10 | 8, 9 | oveq12d 6668 |
. . . 4
|
11 | 6, 7, 10 | 3eqtr4a 2682 |
. . 3
|
12 | 11 | a1i 11 |
. 2
|
13 | | simprl 794 |
. . . . . . . . 9
|
14 | | nnuz 11723 |
. . . . . . . . 9
|
15 | 13, 14 | syl6eleq 2711 |
. . . . . . . 8
|
16 | | fprodmul.2 |
. . . . . . . . . . . 12
|
17 | | eqid 2622 |
. . . . . . . . . . . 12
|
18 | 16, 17 | fmptd 6385 |
. . . . . . . . . . 11
|
19 | 18 | adantr 481 |
. . . . . . . . . 10
|
20 | | f1of 6137 |
. . . . . . . . . . 11
|
21 | 20 | ad2antll 765 |
. . . . . . . . . 10
|
22 | | fco 6058 |
. . . . . . . . . 10
|
23 | 19, 21, 22 | syl2anc 693 |
. . . . . . . . 9
|
24 | 23 | ffvelrnda 6359 |
. . . . . . . 8
|
25 | | fprodmul.3 |
. . . . . . . . . . . 12
|
26 | | eqid 2622 |
. . . . . . . . . . . 12
|
27 | 25, 26 | fmptd 6385 |
. . . . . . . . . . 11
|
28 | 27 | adantr 481 |
. . . . . . . . . 10
|
29 | | fco 6058 |
. . . . . . . . . 10
|
30 | 28, 21, 29 | syl2anc 693 |
. . . . . . . . 9
|
31 | 30 | ffvelrnda 6359 |
. . . . . . . 8
|
32 | 21 | ffvelrnda 6359 |
. . . . . . . . . 10
|
33 | | simpr 477 |
. . . . . . . . . . . . . 14
|
34 | 16, 25 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
35 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
36 | 35 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
37 | 33, 34, 36 | syl2anc 693 |
. . . . . . . . . . . . 13
|
38 | 17 | fvmpt2 6291 |
. . . . . . . . . . . . . . 15
|
39 | 33, 16, 38 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
40 | 26 | fvmpt2 6291 |
. . . . . . . . . . . . . . 15
|
41 | 33, 25, 40 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
42 | 39, 41 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
43 | 37, 42 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
44 | 43 | ralrimiva 2966 |
. . . . . . . . . . 11
|
45 | 44 | ad2antrr 762 |
. . . . . . . . . 10
|
46 | | nffvmpt1 6199 |
. . . . . . . . . . . 12
|
47 | | nffvmpt1 6199 |
. . . . . . . . . . . . 13
|
48 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
49 | | nffvmpt1 6199 |
. . . . . . . . . . . . 13
|
50 | 47, 48, 49 | nfov 6676 |
. . . . . . . . . . . 12
|
51 | 46, 50 | nfeq 2776 |
. . . . . . . . . . 11
|
52 | | fveq2 6191 |
. . . . . . . . . . . 12
|
53 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
54 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
55 | 53, 54 | oveq12d 6668 |
. . . . . . . . . . . 12
|
56 | 52, 55 | eqeq12d 2637 |
. . . . . . . . . . 11
|
57 | 51, 56 | rspc 3303 |
. . . . . . . . . 10
|
58 | 32, 45, 57 | sylc 65 |
. . . . . . . . 9
|
59 | | fvco3 6275 |
. . . . . . . . . 10
|
60 | 21, 59 | sylan 488 |
. . . . . . . . 9
|
61 | | fvco3 6275 |
. . . . . . . . . . 11
|
62 | 21, 61 | sylan 488 |
. . . . . . . . . 10
|
63 | | fvco3 6275 |
. . . . . . . . . . 11
|
64 | 21, 63 | sylan 488 |
. . . . . . . . . 10
|
65 | 62, 64 | oveq12d 6668 |
. . . . . . . . 9
|
66 | 58, 60, 65 | 3eqtr4d 2666 |
. . . . . . . 8
|
67 | 15, 24, 31, 66 | prodfmul 14622 |
. . . . . . 7
|
68 | | fveq2 6191 |
. . . . . . . 8
|
69 | | simprr 796 |
. . . . . . . 8
|
70 | 34, 35 | fmptd 6385 |
. . . . . . . . . 10
|
71 | 70 | adantr 481 |
. . . . . . . . 9
|
72 | 71 | ffvelrnda 6359 |
. . . . . . . 8
|
73 | 68, 13, 69, 72, 60 | fprod 14671 |
. . . . . . 7
|
74 | | fveq2 6191 |
. . . . . . . . 9
|
75 | 19 | ffvelrnda 6359 |
. . . . . . . . 9
|
76 | 74, 13, 69, 75, 62 | fprod 14671 |
. . . . . . . 8
|
77 | | fveq2 6191 |
. . . . . . . . 9
|
78 | 28 | ffvelrnda 6359 |
. . . . . . . . 9
|
79 | 77, 13, 69, 78, 64 | fprod 14671 |
. . . . . . . 8
|
80 | 76, 79 | oveq12d 6668 |
. . . . . . 7
|
81 | 67, 73, 80 | 3eqtr4d 2666 |
. . . . . 6
|
82 | | prodfc 14675 |
. . . . . 6
|
83 | | prodfc 14675 |
. . . . . . 7
|
84 | | prodfc 14675 |
. . . . . . 7
|
85 | 83, 84 | oveq12i 6662 |
. . . . . 6
|
86 | 81, 82, 85 | 3eqtr3g 2679 |
. . . . 5
|
87 | 86 | expr 643 |
. . . 4
|
88 | 87 | exlimdv 1861 |
. . 3
|
89 | 88 | expimpd 629 |
. 2
|
90 | | fprodmul.1 |
. . 3
|
91 | | fz1f1o 14441 |
. . 3
|
92 | 90, 91 | syl 17 |
. 2
|
93 | 12, 89, 92 | mpjaod 396 |
1
|