Step | Hyp | Ref
| Expression |
1 | | prodfdiv.1 |
. . . 4
β’ (π β π β (β€β₯βπ)) |
2 | | prodfdivap.3 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) β β) |
3 | | elfzuz 10021 |
. . . . 5
β’ (π β (π...π) β π β (β€β₯βπ)) |
4 | | prodfdivap.4 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) # 0) |
5 | 3, 4 | sylan2 286 |
. . . 4
β’ ((π β§ π β (π...π)) β (πΊβπ) # 0) |
6 | | eqid 2177 |
. . . . . 6
β’ (π β
(β€β₯βπ) β¦ (1 / (πΊβπ))) = (π β (β€β₯βπ) β¦ (1 / (πΊβπ))) |
7 | | fveq2 5516 |
. . . . . . 7
β’ (π = π β (πΊβπ) = (πΊβπ)) |
8 | 7 | oveq2d 5891 |
. . . . . 6
β’ (π = π β (1 / (πΊβπ)) = (1 / (πΊβπ))) |
9 | | simpr 110 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
10 | 2, 4 | recclapd 8738 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β (1 / (πΊβπ)) β β) |
11 | 6, 8, 9, 10 | fvmptd3 5610 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (1 / (πΊβπ)))βπ) = (1 / (πΊβπ))) |
12 | 3, 11 | sylan2 286 |
. . . 4
β’ ((π β§ π β (π...π)) β ((π β (β€β₯βπ) β¦ (1 / (πΊβπ)))βπ) = (1 / (πΊβπ))) |
13 | 11, 10 | eqeltrd 2254 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (1 / (πΊβπ)))βπ) β β) |
14 | 1, 2, 5, 12, 13 | prodfrecap 11554 |
. . 3
β’ (π β (seqπ( Β· , (π β (β€β₯βπ) β¦ (1 / (πΊβπ))))βπ) = (1 / (seqπ( Β· , πΊ)βπ))) |
15 | 14 | oveq2d 5891 |
. 2
β’ (π β ((seqπ( Β· , πΉ)βπ) Β· (seqπ( Β· , (π β (β€β₯βπ) β¦ (1 / (πΊβπ))))βπ)) = ((seqπ( Β· , πΉ)βπ) Β· (1 / (seqπ( Β· , πΊ)βπ)))) |
16 | | prodfdivap.2 |
. . 3
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
17 | | eleq1w 2238 |
. . . . . . . . 9
β’ (π = π β (π β (β€β₯βπ) β π β (β€β₯βπ))) |
18 | 17 | anbi2d 464 |
. . . . . . . 8
β’ (π = π β ((π β§ π β (β€β₯βπ)) β (π β§ π β (β€β₯βπ)))) |
19 | | fveq2 5516 |
. . . . . . . . 9
β’ (π = π β (πΊβπ) = (πΊβπ)) |
20 | 19 | eleq1d 2246 |
. . . . . . . 8
β’ (π = π β ((πΊβπ) β β β (πΊβπ) β β)) |
21 | 18, 20 | imbi12d 234 |
. . . . . . 7
β’ (π = π β (((π β§ π β (β€β₯βπ)) β (πΊβπ) β β) β ((π β§ π β (β€β₯βπ)) β (πΊβπ) β β))) |
22 | 21, 2 | chvarvv 1908 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) β β) |
23 | 19 | breq1d 4014 |
. . . . . . . 8
β’ (π = π β ((πΊβπ) # 0 β (πΊβπ) # 0)) |
24 | 18, 23 | imbi12d 234 |
. . . . . . 7
β’ (π = π β (((π β§ π β (β€β₯βπ)) β (πΊβπ) # 0) β ((π β§ π β (β€β₯βπ)) β (πΊβπ) # 0))) |
25 | 24, 4 | chvarvv 1908 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) # 0) |
26 | 22, 25 | recclapd 8738 |
. . . . 5
β’ ((π β§ π β (β€β₯βπ)) β (1 / (πΊβπ)) β β) |
27 | 26 | fmpttd 5672 |
. . . 4
β’ (π β (π β (β€β₯βπ) β¦ (1 / (πΊβπ))):(β€β₯βπ)βΆβ) |
28 | 27 | ffvelcdmda 5652 |
. . 3
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (1 / (πΊβπ)))βπ) β β) |
29 | 16, 2, 4 | divrecapd 8750 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((πΉβπ) / (πΊβπ)) = ((πΉβπ) Β· (1 / (πΊβπ)))) |
30 | | prodfdivap.5 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β (π»βπ) = ((πΉβπ) / (πΊβπ))) |
31 | 11 | oveq2d 5891 |
. . . 4
β’ ((π β§ π β (β€β₯βπ)) β ((πΉβπ) Β· ((π β (β€β₯βπ) β¦ (1 / (πΊβπ)))βπ)) = ((πΉβπ) Β· (1 / (πΊβπ)))) |
32 | 29, 30, 31 | 3eqtr4d 2220 |
. . 3
β’ ((π β§ π β (β€β₯βπ)) β (π»βπ) = ((πΉβπ) Β· ((π β (β€β₯βπ) β¦ (1 / (πΊβπ)))βπ))) |
33 | 1, 16, 28, 32 | prod3fmul 11549 |
. 2
β’ (π β (seqπ( Β· , π»)βπ) = ((seqπ( Β· , πΉ)βπ) Β· (seqπ( Β· , (π β (β€β₯βπ) β¦ (1 / (πΊβπ))))βπ))) |
34 | | eqid 2177 |
. . . . 5
β’
(β€β₯βπ) = (β€β₯βπ) |
35 | | eluzel2 9533 |
. . . . . 6
β’ (π β
(β€β₯βπ) β π β β€) |
36 | 1, 35 | syl 14 |
. . . . 5
β’ (π β π β β€) |
37 | 34, 36, 16 | prodf 11546 |
. . . 4
β’ (π β seqπ( Β· , πΉ):(β€β₯βπ)βΆβ) |
38 | 37, 1 | ffvelcdmd 5653 |
. . 3
β’ (π β (seqπ( Β· , πΉ)βπ) β β) |
39 | 34, 36, 2 | prodf 11546 |
. . . 4
β’ (π β seqπ( Β· , πΊ):(β€β₯βπ)βΆβ) |
40 | 39, 1 | ffvelcdmd 5653 |
. . 3
β’ (π β (seqπ( Β· , πΊ)βπ) β β) |
41 | 1, 2, 5 | prodfap0 11553 |
. . 3
β’ (π β (seqπ( Β· , πΊ)βπ) # 0) |
42 | 38, 40, 41 | divrecapd 8750 |
. 2
β’ (π β ((seqπ( Β· , πΉ)βπ) / (seqπ( Β· , πΊ)βπ)) = ((seqπ( Β· , πΉ)βπ) Β· (1 / (seqπ( Β· , πΊ)βπ)))) |
43 | 15, 33, 42 | 3eqtr4d 2220 |
1
β’ (π β (seqπ( Β· , π»)βπ) = ((seqπ( Β· , πΉ)βπ) / (seqπ( Β· , πΊ)βπ))) |