Step | Hyp | Ref
| Expression |
1 | | iprodmul.1 |
. 2
β’ π =
(β€β₯βπ) |
2 | | iprodmul.2 |
. 2
β’ (π β π β β€) |
3 | | iprodmul.3 |
. . . 4
β’ (π β βπ β π βπ¦(π¦ β 0 β§ seqπ( Β· , πΉ) β π¦)) |
4 | | iprodmul.4 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
5 | | iprodmul.5 |
. . . . 5
β’ ((π β§ π β π) β π΄ β β) |
6 | 4, 5 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) β β) |
7 | | iprodmul.6 |
. . . 4
β’ (π β βπ β π βπ§(π§ β 0 β§ seqπ( Β· , πΊ) β π§)) |
8 | | iprodmul.7 |
. . . . 5
β’ ((π β§ π β π) β (πΊβπ) = π΅) |
9 | | iprodmul.8 |
. . . . 5
β’ ((π β§ π β π) β π΅ β β) |
10 | 8, 9 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β π) β (πΊβπ) β β) |
11 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
12 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (πΊβπ) = (πΊβπ)) |
13 | 11, 12 | oveq12d 7376 |
. . . . . 6
β’ (π = π β ((πΉβπ) Β· (πΊβπ)) = ((πΉβπ) Β· (πΊβπ))) |
14 | | eqid 2733 |
. . . . . 6
β’ (π β π β¦ ((πΉβπ) Β· (πΊβπ))) = (π β π β¦ ((πΉβπ) Β· (πΊβπ))) |
15 | | ovex 7391 |
. . . . . 6
β’ ((πΉβπ) Β· (πΊβπ)) β V |
16 | 13, 14, 15 | fvmpt 6949 |
. . . . 5
β’ (π β π β ((π β π β¦ ((πΉβπ) Β· (πΊβπ)))βπ) = ((πΉβπ) Β· (πΊβπ))) |
17 | 16 | adantl 483 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ ((πΉβπ) Β· (πΊβπ)))βπ) = ((πΉβπ) Β· (πΊβπ))) |
18 | 1, 3, 6, 7, 10, 17 | ntrivcvgmul 15792 |
. . 3
β’ (π β βπ β π βπ€(π€ β 0 β§ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€)) |
19 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
20 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πΊβπ) = (πΊβπ)) |
21 | 19, 20 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) Β· (πΊβπ)) = ((πΉβπ) Β· (πΊβπ))) |
22 | 21 | cbvmptv 5219 |
. . . . . . . 8
β’ (π β π β¦ ((πΉβπ) Β· (πΊβπ))) = (π β π β¦ ((πΉβπ) Β· (πΊβπ))) |
23 | | seqeq3 13917 |
. . . . . . . 8
β’ ((π β π β¦ ((πΉβπ) Β· (πΊβπ))) = (π β π β¦ ((πΉβπ) Β· (πΊβπ))) β seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) = seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ))))) |
24 | 22, 23 | ax-mp 5 |
. . . . . . 7
β’ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) = seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) |
25 | 24 | breq1i 5113 |
. . . . . 6
β’ (seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€ β seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€) |
26 | 25 | anbi2i 624 |
. . . . 5
β’ ((π€ β 0 β§ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€) β (π€ β 0 β§ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€)) |
27 | 26 | exbii 1851 |
. . . 4
β’
(βπ€(π€ β 0 β§ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€) β βπ€(π€ β 0 β§ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€)) |
28 | 27 | rexbii 3094 |
. . 3
β’
(βπ β
π βπ€(π€ β 0 β§ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€) β βπ β π βπ€(π€ β 0 β§ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€)) |
29 | 18, 28 | sylibr 233 |
. 2
β’ (π β βπ β π βπ€(π€ β 0 β§ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β π€)) |
30 | | eqid 2733 |
. . . 4
β’ (π β π β¦ ((πΉβπ) Β· (πΊβπ))) = (π β π β¦ ((πΉβπ) Β· (πΊβπ))) |
31 | | fveq2 6843 |
. . . . 5
β’ (π = π β (πΉβπ) = (πΉβπ)) |
32 | | fveq2 6843 |
. . . . 5
β’ (π = π β (πΊβπ) = (πΊβπ)) |
33 | 31, 32 | oveq12d 7376 |
. . . 4
β’ (π = π β ((πΉβπ) Β· (πΊβπ)) = ((πΉβπ) Β· (πΊβπ))) |
34 | | simpr 486 |
. . . 4
β’ ((π β§ π β π) β π β π) |
35 | 6, 10 | mulcld 11180 |
. . . 4
β’ ((π β§ π β π) β ((πΉβπ) Β· (πΊβπ)) β β) |
36 | 30, 33, 34, 35 | fvmptd3 6972 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ ((πΉβπ) Β· (πΊβπ)))βπ) = ((πΉβπ) Β· (πΊβπ))) |
37 | 4, 8 | oveq12d 7376 |
. . 3
β’ ((π β§ π β π) β ((πΉβπ) Β· (πΊβπ)) = (π΄ Β· π΅)) |
38 | 36, 37 | eqtrd 2773 |
. 2
β’ ((π β§ π β π) β ((π β π β¦ ((πΉβπ) Β· (πΊβπ)))βπ) = (π΄ Β· π΅)) |
39 | 5, 9 | mulcld 11180 |
. 2
β’ ((π β§ π β π) β (π΄ Β· π΅) β β) |
40 | 1, 2, 3, 4, 5 | iprodclim2 15887 |
. . 3
β’ (π β seqπ( Β· , πΉ) β βπ β π π΄) |
41 | | seqex 13914 |
. . . 4
β’ seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β V |
42 | 41 | a1i 11 |
. . 3
β’ (π β seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β V) |
43 | 1, 2, 7, 8, 9 | iprodclim2 15887 |
. . 3
β’ (π β seqπ( Β· , πΊ) β βπ β π π΅) |
44 | 1, 2, 6 | prodf 15777 |
. . . 4
β’ (π β seqπ( Β· , πΉ):πβΆβ) |
45 | 44 | ffvelcdmda 7036 |
. . 3
β’ ((π β§ π β π) β (seqπ( Β· , πΉ)βπ) β β) |
46 | 1, 2, 10 | prodf 15777 |
. . . 4
β’ (π β seqπ( Β· , πΊ):πβΆβ) |
47 | 46 | ffvelcdmda 7036 |
. . 3
β’ ((π β§ π β π) β (seqπ( Β· , πΊ)βπ) β β) |
48 | | simpr 486 |
. . . . 5
β’ ((π β§ π β π) β π β π) |
49 | 48, 1 | eleqtrdi 2844 |
. . . 4
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
50 | | elfzuz 13443 |
. . . . . . 7
β’ (π β (π...π) β π β (β€β₯βπ)) |
51 | 50, 1 | eleqtrrdi 2845 |
. . . . . 6
β’ (π β (π...π) β π β π) |
52 | 51, 6 | sylan2 594 |
. . . . 5
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) |
53 | 52 | adantlr 714 |
. . . 4
β’ (((π β§ π β π) β§ π β (π...π)) β (πΉβπ) β β) |
54 | 51, 10 | sylan2 594 |
. . . . 5
β’ ((π β§ π β (π...π)) β (πΊβπ) β β) |
55 | 54 | adantlr 714 |
. . . 4
β’ (((π β§ π β π) β§ π β (π...π)) β (πΊβπ) β β) |
56 | 36 | adantlr 714 |
. . . . 5
β’ (((π β§ π β π) β§ π β π) β ((π β π β¦ ((πΉβπ) Β· (πΊβπ)))βπ) = ((πΉβπ) Β· (πΊβπ))) |
57 | 51, 56 | sylan2 594 |
. . . 4
β’ (((π β§ π β π) β§ π β (π...π)) β ((π β π β¦ ((πΉβπ) Β· (πΊβπ)))βπ) = ((πΉβπ) Β· (πΊβπ))) |
58 | 49, 53, 55, 57 | prodfmul 15780 |
. . 3
β’ ((π β§ π β π) β (seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ))))βπ) = ((seqπ( Β· , πΉ)βπ) Β· (seqπ( Β· , πΊ)βπ))) |
59 | 1, 2, 40, 42, 43, 45, 47, 58 | climmul 15521 |
. 2
β’ (π β seqπ( Β· , (π β π β¦ ((πΉβπ) Β· (πΊβπ)))) β (βπ β π π΄ Β· βπ β π π΅)) |
60 | 1, 2, 29, 38, 39, 59 | iprodclim 15886 |
1
β’ (π β βπ β π (π΄ Β· π΅) = (βπ β π π΄ Β· βπ β π π΅)) |