Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . . . . . 8
|
2 | 1 | mptex 6486 |
. . . . . . 7
|
3 | | fmuldfeqlem1.6 |
. . . . . . . 8
|
4 | 3 | fvmpt2 6291 |
. . . . . . 7
|
5 | 2, 4 | mpan2 707 |
. . . . . 6
|
6 | | fveq2 6191 |
. . . . . . . 8
|
7 | 6 | fveq1d 6193 |
. . . . . . 7
|
8 | 7 | cbvmptv 4750 |
. . . . . 6
|
9 | 5, 8 | syl6eq 2672 |
. . . . 5
|
10 | 9 | adantl 482 |
. . . 4
|
11 | | fveq2 6191 |
. . . . . 6
|
12 | 11 | fveq1d 6193 |
. . . . 5
|
13 | 12 | adantl 482 |
. . . 4
|
14 | | fmuldfeqlem1.11 |
. . . . 5
|
15 | 14 | adantr 481 |
. . . 4
|
16 | | fmuldfeqlem1.8 |
. . . . . . 7
|
17 | 16, 14 | ffvelrnd 6360 |
. . . . . 6
|
18 | 17 | ancli 574 |
. . . . . 6
|
19 | | nfcv 2764 |
. . . . . . 7
|
20 | | fmuldfeqlem1.1 |
. . . . . . . . 9
|
21 | | nfv 1843 |
. . . . . . . . 9
|
22 | 20, 21 | nfan 1828 |
. . . . . . . 8
|
23 | | nfv 1843 |
. . . . . . . 8
|
24 | 22, 23 | nfim 1825 |
. . . . . . 7
|
25 | | eleq1 2689 |
. . . . . . . . 9
|
26 | 25 | anbi2d 740 |
. . . . . . . 8
|
27 | | feq1 6026 |
. . . . . . . 8
|
28 | 26, 27 | imbi12d 334 |
. . . . . . 7
|
29 | | fmuldfeqlem1.13 |
. . . . . . 7
|
30 | 19, 24, 28, 29 | vtoclgf 3264 |
. . . . . 6
|
31 | 17, 18, 30 | sylc 65 |
. . . . 5
|
32 | 31 | ffvelrnda 6359 |
. . . 4
|
33 | 10, 13, 15, 32 | fvmptd 6288 |
. . 3
|
34 | 33 | oveq2d 6666 |
. 2
|
35 | | fmuldfeqlem1.10 |
. . . . 5
|
36 | | elfzuz 12338 |
. . . . 5
|
37 | 35, 36 | syl 17 |
. . . 4
|
38 | | seqp1 12816 |
. . . 4
|
39 | 37, 38 | syl 17 |
. . 3
|
40 | 39 | adantr 481 |
. 2
|
41 | | seqp1 12816 |
. . . . . 6
|
42 | 37, 41 | syl 17 |
. . . . 5
|
43 | | fmuldfeqlem1.5 |
. . . . . . . 8
|
44 | | nfcv 2764 |
. . . . . . . . 9
|
45 | | nfcv 2764 |
. . . . . . . . 9
|
46 | | nfcv 2764 |
. . . . . . . . 9
|
47 | | nfcv 2764 |
. . . . . . . . 9
|
48 | | fveq1 6190 |
. . . . . . . . . . 11
|
49 | | fveq1 6190 |
. . . . . . . . . . 11
|
50 | 48, 49 | oveqan12d 6669 |
. . . . . . . . . 10
|
51 | 50 | mpteq2dv 4745 |
. . . . . . . . 9
|
52 | 44, 45, 46, 47, 51 | cbvmpt2 6734 |
. . . . . . . 8
|
53 | 43, 52 | eqtri 2644 |
. . . . . . 7
|
54 | 53 | a1i 11 |
. . . . . 6
|
55 | | nfcv 2764 |
. . . . . . . . . . . 12
|
56 | | fmuldfeqlem1.3 |
. . . . . . . . . . . . . 14
|
57 | | nfmpt1 4747 |
. . . . . . . . . . . . . 14
|
58 | 56, 56, 57 | nfmpt2 6724 |
. . . . . . . . . . . . 13
|
59 | 43, 58 | nfcxfr 2762 |
. . . . . . . . . . . 12
|
60 | | nfcv 2764 |
. . . . . . . . . . . 12
|
61 | 55, 59, 60 | nfseq 12811 |
. . . . . . . . . . 11
|
62 | | nfcv 2764 |
. . . . . . . . . . 11
|
63 | 61, 62 | nffv 6198 |
. . . . . . . . . 10
|
64 | 63 | nfeq2 2780 |
. . . . . . . . 9
|
65 | | nfv 1843 |
. . . . . . . . 9
|
66 | 64, 65 | nfan 1828 |
. . . . . . . 8
|
67 | | fveq1 6190 |
. . . . . . . . . 10
|
68 | 67 | ad2antrr 762 |
. . . . . . . . 9
|
69 | | fveq1 6190 |
. . . . . . . . . 10
|
70 | 69 | ad2antlr 763 |
. . . . . . . . 9
|
71 | 68, 70 | oveq12d 6668 |
. . . . . . . 8
|
72 | 66, 71 | mpteq2da 4743 |
. . . . . . 7
|
73 | 72 | adantl 482 |
. . . . . 6
|
74 | | eqid 2622 |
. . . . . . 7
|
75 | | 3simpc 1060 |
. . . . . . . 8
|
76 | | nfcv 2764 |
. . . . . . . . 9
|
77 | | nfcv 2764 |
. . . . . . . . 9
|
78 | | nfcv 2764 |
. . . . . . . . 9
|
79 | | nfv 1843 |
. . . . . . . . . . 11
|
80 | | nfv 1843 |
. . . . . . . . . . 11
|
81 | 20, 79, 80 | nf3an 1831 |
. . . . . . . . . 10
|
82 | | nfv 1843 |
. . . . . . . . . 10
|
83 | 81, 82 | nfim 1825 |
. . . . . . . . 9
|
84 | | fmuldfeqlem1.2 |
. . . . . . . . . . 11
|
85 | | nfv 1843 |
. . . . . . . . . . 11
|
86 | | nfv 1843 |
. . . . . . . . . . 11
|
87 | 84, 85, 86 | nf3an 1831 |
. . . . . . . . . 10
|
88 | | nfv 1843 |
. . . . . . . . . 10
|
89 | 87, 88 | nfim 1825 |
. . . . . . . . 9
|
90 | | eleq1 2689 |
. . . . . . . . . . 11
|
91 | 90 | 3anbi2d 1404 |
. . . . . . . . . 10
|
92 | 48 | oveq1d 6665 |
. . . . . . . . . . . 12
|
93 | 92 | mpteq2dv 4745 |
. . . . . . . . . . 11
|
94 | 93 | eleq1d 2686 |
. . . . . . . . . 10
|
95 | 91, 94 | imbi12d 334 |
. . . . . . . . 9
|
96 | | eleq1 2689 |
. . . . . . . . . . 11
|
97 | 96 | 3anbi3d 1405 |
. . . . . . . . . 10
|
98 | 49 | oveq2d 6666 |
. . . . . . . . . . . 12
|
99 | 98 | mpteq2dv 4745 |
. . . . . . . . . . 11
|
100 | 99 | eleq1d 2686 |
. . . . . . . . . 10
|
101 | 97, 100 | imbi12d 334 |
. . . . . . . . 9
|
102 | | fmuldfeqlem1.9 |
. . . . . . . . 9
|
103 | 76, 77, 78, 83, 89, 95, 101, 102 | vtocl2gf 3268 |
. . . . . . . 8
|
104 | 75, 103 | mpcom 38 |
. . . . . . 7
|
105 | | fmuldfeqlem1.7 |
. . . . . . 7
|
106 | 53, 74, 35, 16, 104, 105 | fmulcl 39813 |
. . . . . 6
|
107 | | mptexg 6484 |
. . . . . . 7
|
108 | 105, 107 | syl 17 |
. . . . . 6
|
109 | 54, 73, 106, 17, 108 | ovmpt2d 6788 |
. . . . 5
|
110 | 42, 109 | eqtrd 2656 |
. . . 4
|
111 | 106 | ancli 574 |
. . . . . . 7
|
112 | | nfcv 2764 |
. . . . . . . . . 10
|
113 | | nfmpt21 6722 |
. . . . . . . . . . 11
|
114 | 43, 113 | nfcxfr 2762 |
. . . . . . . . . 10
|
115 | | nfcv 2764 |
. . . . . . . . . 10
|
116 | 112, 114,
115 | nfseq 12811 |
. . . . . . . . 9
|
117 | | nfcv 2764 |
. . . . . . . . 9
|
118 | 116, 117 | nffv 6198 |
. . . . . . . 8
|
119 | 118 | nfel1 2779 |
. . . . . . . . . 10
|
120 | 20, 119 | nfan 1828 |
. . . . . . . . 9
|
121 | | nfcv 2764 |
. . . . . . . . . 10
|
122 | | nfcv 2764 |
. . . . . . . . . 10
|
123 | 118, 121,
122 | nff 6041 |
. . . . . . . . 9
|
124 | 120, 123 | nfim 1825 |
. . . . . . . 8
|
125 | | eleq1 2689 |
. . . . . . . . . 10
|
126 | 125 | anbi2d 740 |
. . . . . . . . 9
|
127 | | feq1 6026 |
. . . . . . . . 9
|
128 | 126, 127 | imbi12d 334 |
. . . . . . . 8
|
129 | 118, 124,
128, 29 | vtoclgf 3264 |
. . . . . . 7
|
130 | 106, 111,
129 | sylc 65 |
. . . . . 6
|
131 | 130 | ffvelrnda 6359 |
. . . . 5
|
132 | 131, 32 | remulcld 10070 |
. . . 4
|
133 | 110, 132 | fvmpt2d 6293 |
. . 3
|
134 | | fmuldfeqlem1.12 |
. . . . 5
|
135 | 134 | oveq1d 6665 |
. . . 4
|
136 | 135 | adantr 481 |
. . 3
|
137 | 133, 136 | eqtrd 2656 |
. 2
|
138 | 34, 40, 137 | 3eqtr4rd 2667 |
1
|