Step | Hyp | Ref
| Expression |
1 | | ovex 7391 |
. . . . . . . 8
β’
(1...π) β
V |
2 | 1 | mptex 7174 |
. . . . . . 7
β’ (π β (1...π) β¦ ((πβπ)βπ‘)) β V |
3 | | fmuldfeqlem1.6 |
. . . . . . . 8
β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) |
4 | 3 | fvmpt2 6960 |
. . . . . . 7
β’ ((π‘ β π β§ (π β (1...π) β¦ ((πβπ)βπ‘)) β V) β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
5 | 2, 4 | mpan2 690 |
. . . . . 6
β’ (π‘ β π β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
6 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
7 | 6 | fveq1d 6845 |
. . . . . . 7
β’ (π = π β ((πβπ)βπ‘) = ((πβπ)βπ‘)) |
8 | 7 | cbvmptv 5219 |
. . . . . 6
β’ (π β (1...π) β¦ ((πβπ)βπ‘)) = (π β (1...π) β¦ ((πβπ)βπ‘)) |
9 | 5, 8 | eqtrdi 2793 |
. . . . 5
β’ (π‘ β π β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
10 | 9 | adantl 483 |
. . . 4
β’ ((π β§ π‘ β π) β (πΉβπ‘) = (π β (1...π) β¦ ((πβπ)βπ‘))) |
11 | | fveq2 6843 |
. . . . . 6
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
12 | 11 | fveq1d 6845 |
. . . . 5
β’ (π = (π + 1) β ((πβπ)βπ‘) = ((πβ(π + 1))βπ‘)) |
13 | 12 | adantl 483 |
. . . 4
β’ (((π β§ π‘ β π) β§ π = (π + 1)) β ((πβπ)βπ‘) = ((πβ(π + 1))βπ‘)) |
14 | | fmuldfeqlem1.11 |
. . . . 5
β’ (π β (π + 1) β (1...π)) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π β§ π‘ β π) β (π + 1) β (1...π)) |
16 | | fmuldfeqlem1.8 |
. . . . . . 7
β’ (π β π:(1...π)βΆπ) |
17 | 16, 14 | ffvelcdmd 7037 |
. . . . . 6
β’ (π β (πβ(π + 1)) β π) |
18 | 17 | ancli 550 |
. . . . . 6
β’ (π β (π β§ (πβ(π + 1)) β π)) |
19 | | nfcv 2908 |
. . . . . . 7
β’
β²π(πβ(π + 1)) |
20 | | fmuldfeqlem1.1 |
. . . . . . . . 9
β’
β²ππ |
21 | | nfv 1918 |
. . . . . . . . 9
β’
β²π(πβ(π + 1)) β π |
22 | 20, 21 | nfan 1903 |
. . . . . . . 8
β’
β²π(π β§ (πβ(π + 1)) β π) |
23 | | nfv 1918 |
. . . . . . . 8
β’
β²π(πβ(π + 1)):πβΆβ |
24 | 22, 23 | nfim 1900 |
. . . . . . 7
β’
β²π((π β§ (πβ(π + 1)) β π) β (πβ(π + 1)):πβΆβ) |
25 | | eleq1 2826 |
. . . . . . . . 9
β’ (π = (πβ(π + 1)) β (π β π β (πβ(π + 1)) β π)) |
26 | 25 | anbi2d 630 |
. . . . . . . 8
β’ (π = (πβ(π + 1)) β ((π β§ π β π) β (π β§ (πβ(π + 1)) β π))) |
27 | | feq1 6650 |
. . . . . . . 8
β’ (π = (πβ(π + 1)) β (π:πβΆβ β (πβ(π + 1)):πβΆβ)) |
28 | 26, 27 | imbi12d 345 |
. . . . . . 7
β’ (π = (πβ(π + 1)) β (((π β§ π β π) β π:πβΆβ) β ((π β§ (πβ(π + 1)) β π) β (πβ(π + 1)):πβΆβ))) |
29 | | fmuldfeqlem1.13 |
. . . . . . 7
β’ ((π β§ π β π) β π:πβΆβ) |
30 | 19, 24, 28, 29 | vtoclgf 3524 |
. . . . . 6
β’ ((πβ(π + 1)) β π β ((π β§ (πβ(π + 1)) β π) β (πβ(π + 1)):πβΆβ)) |
31 | 17, 18, 30 | sylc 65 |
. . . . 5
β’ (π β (πβ(π + 1)):πβΆβ) |
32 | 31 | ffvelcdmda 7036 |
. . . 4
β’ ((π β§ π‘ β π) β ((πβ(π + 1))βπ‘) β β) |
33 | 10, 13, 15, 32 | fvmptd 6956 |
. . 3
β’ ((π β§ π‘ β π) β ((πΉβπ‘)β(π + 1)) = ((πβ(π + 1))βπ‘)) |
34 | 33 | oveq2d 7374 |
. 2
β’ ((π β§ π‘ β π) β ((seq1( Β· , (πΉβπ‘))βπ) Β· ((πΉβπ‘)β(π + 1))) = ((seq1( Β· , (πΉβπ‘))βπ) Β· ((πβ(π + 1))βπ‘))) |
35 | | fmuldfeqlem1.10 |
. . . . 5
β’ (π β π β (1...π)) |
36 | | elfzuz 13438 |
. . . . 5
β’ (π β (1...π) β π β
(β€β₯β1)) |
37 | 35, 36 | syl 17 |
. . . 4
β’ (π β π β
(β€β₯β1)) |
38 | | seqp1 13922 |
. . . 4
β’ (π β
(β€β₯β1) β (seq1( Β· , (πΉβπ‘))β(π + 1)) = ((seq1( Β· , (πΉβπ‘))βπ) Β· ((πΉβπ‘)β(π + 1)))) |
39 | 37, 38 | syl 17 |
. . 3
β’ (π β (seq1( Β· , (πΉβπ‘))β(π + 1)) = ((seq1( Β· , (πΉβπ‘))βπ) Β· ((πΉβπ‘)β(π + 1)))) |
40 | 39 | adantr 482 |
. 2
β’ ((π β§ π‘ β π) β (seq1( Β· , (πΉβπ‘))β(π + 1)) = ((seq1( Β· , (πΉβπ‘))βπ) Β· ((πΉβπ‘)β(π + 1)))) |
41 | | seqp1 13922 |
. . . . . 6
β’ (π β
(β€β₯β1) β (seq1(π, π)β(π + 1)) = ((seq1(π, π)βπ)π(πβ(π + 1)))) |
42 | 37, 41 | syl 17 |
. . . . 5
β’ (π β (seq1(π, π)β(π + 1)) = ((seq1(π, π)βπ)π(πβ(π + 1)))) |
43 | | fmuldfeqlem1.5 |
. . . . . . . 8
β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
44 | | nfcv 2908 |
. . . . . . . . 9
β’
β²β(π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) |
45 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π(π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) |
46 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π(π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) |
47 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π(π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) |
48 | | fveq1 6842 |
. . . . . . . . . . 11
β’ (π = β β (πβπ‘) = (ββπ‘)) |
49 | | fveq1 6842 |
. . . . . . . . . . 11
β’ (π = π β (πβπ‘) = (πβπ‘)) |
50 | 48, 49 | oveqan12d 7377 |
. . . . . . . . . 10
β’ ((π = β β§ π = π) β ((πβπ‘) Β· (πβπ‘)) = ((ββπ‘) Β· (πβπ‘))) |
51 | 50 | mpteq2dv 5208 |
. . . . . . . . 9
β’ ((π = β β§ π = π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) = (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘)))) |
52 | 44, 45, 46, 47, 51 | cbvmpo 7452 |
. . . . . . . 8
β’ (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) = (β β π, π β π β¦ (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘)))) |
53 | 43, 52 | eqtri 2765 |
. . . . . . 7
β’ π = (β β π, π β π β¦ (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘)))) |
54 | 53 | a1i 11 |
. . . . . 6
β’ (π β π = (β β π, π β π β¦ (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))))) |
55 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π‘1 |
56 | | fmuldfeqlem1.3 |
. . . . . . . . . . . . . 14
β’
β²π‘π |
57 | | nfmpt1 5214 |
. . . . . . . . . . . . . 14
β’
β²π‘(π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) |
58 | 56, 56, 57 | nfmpo 7440 |
. . . . . . . . . . . . 13
β’
β²π‘(π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
59 | 43, 58 | nfcxfr 2906 |
. . . . . . . . . . . 12
β’
β²π‘π |
60 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π‘π |
61 | 55, 59, 60 | nfseq 13917 |
. . . . . . . . . . 11
β’
β²π‘seq1(π, π) |
62 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π‘π |
63 | 61, 62 | nffv 6853 |
. . . . . . . . . 10
β’
β²π‘(seq1(π, π)βπ) |
64 | 63 | nfeq2 2925 |
. . . . . . . . 9
β’
β²π‘ β = (seq1(π, π)βπ) |
65 | | nfv 1918 |
. . . . . . . . 9
β’
β²π‘ π = (πβ(π + 1)) |
66 | 64, 65 | nfan 1903 |
. . . . . . . 8
β’
β²π‘(β = (seq1(π, π)βπ) β§ π = (πβ(π + 1))) |
67 | | fveq1 6842 |
. . . . . . . . . 10
β’ (β = (seq1(π, π)βπ) β (ββπ‘) = ((seq1(π, π)βπ)βπ‘)) |
68 | 67 | ad2antrr 725 |
. . . . . . . . 9
β’ (((β = (seq1(π, π)βπ) β§ π = (πβ(π + 1))) β§ π‘ β π) β (ββπ‘) = ((seq1(π, π)βπ)βπ‘)) |
69 | | fveq1 6842 |
. . . . . . . . . 10
β’ (π = (πβ(π + 1)) β (πβπ‘) = ((πβ(π + 1))βπ‘)) |
70 | 69 | ad2antlr 726 |
. . . . . . . . 9
β’ (((β = (seq1(π, π)βπ) β§ π = (πβ(π + 1))) β§ π‘ β π) β (πβπ‘) = ((πβ(π + 1))βπ‘)) |
71 | 68, 70 | oveq12d 7376 |
. . . . . . . 8
β’ (((β = (seq1(π, π)βπ) β§ π = (πβ(π + 1))) β§ π‘ β π) β ((ββπ‘) Β· (πβπ‘)) = (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘))) |
72 | 66, 71 | mpteq2da 5204 |
. . . . . . 7
β’ ((β = (seq1(π, π)βπ) β§ π = (πβ(π + 1))) β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) = (π‘ β π β¦ (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘)))) |
73 | 72 | adantl 483 |
. . . . . 6
β’ ((π β§ (β = (seq1(π, π)βπ) β§ π = (πβ(π + 1)))) β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) = (π‘ β π β¦ (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘)))) |
74 | | eqid 2737 |
. . . . . . 7
β’
(seq1(π, π)βπ) = (seq1(π, π)βπ) |
75 | | 3simpc 1151 |
. . . . . . . 8
β’ ((π β§ β β π β§ π β π) β (β β π β§ π β π)) |
76 | | nfcv 2908 |
. . . . . . . . 9
β’
β²πβ |
77 | | nfcv 2908 |
. . . . . . . . 9
β’
β²πβ |
78 | | nfcv 2908 |
. . . . . . . . 9
β’
β²ππ |
79 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π β β π |
80 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π π β π |
81 | 20, 79, 80 | nf3an 1905 |
. . . . . . . . . 10
β’
β²π(π β§ β β π β§ π β π) |
82 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π |
83 | 81, 82 | nfim 1900 |
. . . . . . . . 9
β’
β²π((π β§ β β π β§ π β π) β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π) |
84 | | fmuldfeqlem1.2 |
. . . . . . . . . . 11
β’
β²ππ |
85 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π β β π |
86 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π π β π |
87 | 84, 85, 86 | nf3an 1905 |
. . . . . . . . . 10
β’
β²π(π β§ β β π β§ π β π) |
88 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π |
89 | 87, 88 | nfim 1900 |
. . . . . . . . 9
β’
β²π((π β§ β β π β§ π β π) β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π) |
90 | | eleq1 2826 |
. . . . . . . . . . 11
β’ (π = β β (π β π β β β π)) |
91 | 90 | 3anbi2d 1442 |
. . . . . . . . . 10
β’ (π = β β ((π β§ π β π β§ π β π) β (π β§ β β π β§ π β π))) |
92 | 48 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π = β β ((πβπ‘) Β· (πβπ‘)) = ((ββπ‘) Β· (πβπ‘))) |
93 | 92 | mpteq2dv 5208 |
. . . . . . . . . . 11
β’ (π = β β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) = (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘)))) |
94 | 93 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π = β β ((π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π)) |
95 | 91, 94 | imbi12d 345 |
. . . . . . . . 9
β’ (π = β β (((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) β ((π β§ β β π β§ π β π) β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π))) |
96 | | eleq1 2826 |
. . . . . . . . . . 11
β’ (π = π β (π β π β π β π)) |
97 | 96 | 3anbi3d 1443 |
. . . . . . . . . 10
β’ (π = π β ((π β§ β β π β§ π β π) β (π β§ β β π β§ π β π))) |
98 | 49 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π = π β ((ββπ‘) Β· (πβπ‘)) = ((ββπ‘) Β· (πβπ‘))) |
99 | 98 | mpteq2dv 5208 |
. . . . . . . . . . 11
β’ (π = π β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) = (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘)))) |
100 | 99 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π = π β ((π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π)) |
101 | 97, 100 | imbi12d 345 |
. . . . . . . . 9
β’ (π = π β (((π β§ β β π β§ π β π) β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π) β ((π β§ β β π β§ π β π) β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π))) |
102 | | fmuldfeqlem1.9 |
. . . . . . . . 9
β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) |
103 | 76, 77, 78, 83, 89, 95, 101, 102 | vtocl2gf 3530 |
. . . . . . . 8
β’ ((β β π β§ π β π) β ((π β§ β β π β§ π β π) β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π)) |
104 | 75, 103 | mpcom 38 |
. . . . . . 7
β’ ((π β§ β β π β§ π β π) β (π‘ β π β¦ ((ββπ‘) Β· (πβπ‘))) β π) |
105 | | fmuldfeqlem1.7 |
. . . . . . 7
β’ (π β π β V) |
106 | 53, 74, 35, 16, 104, 105 | fmulcl 43829 |
. . . . . 6
β’ (π β (seq1(π, π)βπ) β π) |
107 | | mptexg 7172 |
. . . . . . 7
β’ (π β V β (π‘ β π β¦ (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘))) β V) |
108 | 105, 107 | syl 17 |
. . . . . 6
β’ (π β (π‘ β π β¦ (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘))) β V) |
109 | 54, 73, 106, 17, 108 | ovmpod 7508 |
. . . . 5
β’ (π β ((seq1(π, π)βπ)π(πβ(π + 1))) = (π‘ β π β¦ (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘)))) |
110 | 42, 109 | eqtrd 2777 |
. . . 4
β’ (π β (seq1(π, π)β(π + 1)) = (π‘ β π β¦ (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘)))) |
111 | 106 | ancli 550 |
. . . . . . 7
β’ (π β (π β§ (seq1(π, π)βπ) β π)) |
112 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π1 |
113 | | nfmpo1 7438 |
. . . . . . . . . . 11
β’
β²π(π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
114 | 43, 113 | nfcxfr 2906 |
. . . . . . . . . 10
β’
β²ππ |
115 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²ππ |
116 | 112, 114,
115 | nfseq 13917 |
. . . . . . . . 9
β’
β²πseq1(π, π) |
117 | | nfcv 2908 |
. . . . . . . . 9
β’
β²ππ |
118 | 116, 117 | nffv 6853 |
. . . . . . . 8
β’
β²π(seq1(π, π)βπ) |
119 | 118 | nfel1 2924 |
. . . . . . . . . 10
β’
β²π(seq1(π, π)βπ) β π |
120 | 20, 119 | nfan 1903 |
. . . . . . . . 9
β’
β²π(π β§ (seq1(π, π)βπ) β π) |
121 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²ππ |
122 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²πβ |
123 | 118, 121,
122 | nff 6665 |
. . . . . . . . 9
β’
β²π(seq1(π, π)βπ):πβΆβ |
124 | 120, 123 | nfim 1900 |
. . . . . . . 8
β’
β²π((π β§ (seq1(π, π)βπ) β π) β (seq1(π, π)βπ):πβΆβ) |
125 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π = (seq1(π, π)βπ) β (π β π β (seq1(π, π)βπ) β π)) |
126 | 125 | anbi2d 630 |
. . . . . . . . 9
β’ (π = (seq1(π, π)βπ) β ((π β§ π β π) β (π β§ (seq1(π, π)βπ) β π))) |
127 | | feq1 6650 |
. . . . . . . . 9
β’ (π = (seq1(π, π)βπ) β (π:πβΆβ β (seq1(π, π)βπ):πβΆβ)) |
128 | 126, 127 | imbi12d 345 |
. . . . . . . 8
β’ (π = (seq1(π, π)βπ) β (((π β§ π β π) β π:πβΆβ) β ((π β§ (seq1(π, π)βπ) β π) β (seq1(π, π)βπ):πβΆβ))) |
129 | 118, 124,
128, 29 | vtoclgf 3524 |
. . . . . . 7
β’
((seq1(π, π)βπ) β π β ((π β§ (seq1(π, π)βπ) β π) β (seq1(π, π)βπ):πβΆβ)) |
130 | 106, 111,
129 | sylc 65 |
. . . . . 6
β’ (π β (seq1(π, π)βπ):πβΆβ) |
131 | 130 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π‘ β π) β ((seq1(π, π)βπ)βπ‘) β β) |
132 | 131, 32 | remulcld 11186 |
. . . 4
β’ ((π β§ π‘ β π) β (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘)) β β) |
133 | 110, 132 | fvmpt2d 6962 |
. . 3
β’ ((π β§ π‘ β π) β ((seq1(π, π)β(π + 1))βπ‘) = (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘))) |
134 | | fmuldfeqlem1.12 |
. . . . 5
β’ (π β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) |
135 | 134 | oveq1d 7373 |
. . . 4
β’ (π β (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘)) = ((seq1( Β· , (πΉβπ‘))βπ) Β· ((πβ(π + 1))βπ‘))) |
136 | 135 | adantr 482 |
. . 3
β’ ((π β§ π‘ β π) β (((seq1(π, π)βπ)βπ‘) Β· ((πβ(π + 1))βπ‘)) = ((seq1( Β· , (πΉβπ‘))βπ) Β· ((πβ(π + 1))βπ‘))) |
137 | 133, 136 | eqtrd 2777 |
. 2
β’ ((π β§ π‘ β π) β ((seq1(π, π)β(π + 1))βπ‘) = ((seq1( Β· , (πΉβπ‘))βπ) Β· ((πβ(π + 1))βπ‘))) |
138 | 34, 40, 137 | 3eqtr4rd 2788 |
1
β’ ((π β§ π‘ β π) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1))) |