Step | Hyp | Ref
| Expression |
1 | | fprodfvdvdsd.a |
. . . . . . 7
β’ (π β π΄ β Fin) |
2 | 1 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β π΄ β Fin) |
3 | | diffi 9056 |
. . . . . 6
β’ (π΄ β Fin β (π΄ β {π₯}) β Fin) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (π΄ β {π₯}) β Fin) |
5 | | fprodfvdvdsd.f |
. . . . . . . 8
β’ (π β πΉ:π΅βΆβ€) |
6 | 5 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β (π΄ β {π₯})) β πΉ:π΅βΆβ€) |
7 | | fprodfvdvdsd.b |
. . . . . . . . 9
β’ (π β π΄ β π΅) |
8 | 7 | ssdifssd 4100 |
. . . . . . . 8
β’ (π β (π΄ β {π₯}) β π΅) |
9 | 8 | sselda 3942 |
. . . . . . 7
β’ ((π β§ π β (π΄ β {π₯})) β π β π΅) |
10 | 6, 9 | ffvelcdmd 7030 |
. . . . . 6
β’ ((π β§ π β (π΄ β {π₯})) β (πΉβπ) β β€) |
11 | 10 | adantlr 713 |
. . . . 5
β’ (((π β§ π₯ β π΄) β§ π β (π΄ β {π₯})) β (πΉβπ) β β€) |
12 | 4, 11 | fprodzcl 15771 |
. . . 4
β’ ((π β§ π₯ β π΄) β βπ β (π΄ β {π₯})(πΉβπ) β β€) |
13 | 5 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π΄) β πΉ:π΅βΆβ€) |
14 | 7 | sselda 3942 |
. . . . 5
β’ ((π β§ π₯ β π΄) β π₯ β π΅) |
15 | 13, 14 | ffvelcdmd 7030 |
. . . 4
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β€) |
16 | | dvdsmul2 16095 |
. . . 4
β’
((βπ β
(π΄ β {π₯})(πΉβπ) β β€ β§ (πΉβπ₯) β β€) β (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
17 | 12, 15, 16 | syl2anc 584 |
. . 3
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
18 | 17 | ralrimiva 3141 |
. 2
β’ (π β βπ₯ β π΄ (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
19 | | neldifsnd 4751 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β Β¬ π₯ β (π΄ β {π₯})) |
20 | | disjsn 4670 |
. . . . . . 7
β’ (((π΄ β {π₯}) β© {π₯}) = β
β Β¬ π₯ β (π΄ β {π₯})) |
21 | 19, 20 | sylibr 233 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β ((π΄ β {π₯}) β© {π₯}) = β
) |
22 | | difsnid 4768 |
. . . . . . . 8
β’ (π₯ β π΄ β ((π΄ β {π₯}) βͺ {π₯}) = π΄) |
23 | 22 | eqcomd 2743 |
. . . . . . 7
β’ (π₯ β π΄ β π΄ = ((π΄ β {π₯}) βͺ {π₯})) |
24 | 23 | adantl 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β π΄ = ((π΄ β {π₯}) βͺ {π₯})) |
25 | 13 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π΄) β πΉ:π΅βΆβ€) |
26 | 7 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β π΄ β π΅) |
27 | 26 | sselda 3942 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π΄) β π β π΅) |
28 | 25, 27 | ffvelcdmd 7030 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π β π΄) β (πΉβπ) β β€) |
29 | 28 | zcnd 12540 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ π β π΄) β (πΉβπ) β β) |
30 | 21, 24, 2, 29 | fprodsplit 15783 |
. . . . 5
β’ ((π β§ π₯ β π΄) β βπ β π΄ (πΉβπ) = (βπ β (π΄ β {π₯})(πΉβπ) Β· βπ β {π₯} (πΉβπ))) |
31 | | simpr 485 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
32 | 15 | zcnd 12540 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β) |
33 | | fveq2 6837 |
. . . . . . . 8
β’ (π = π₯ β (πΉβπ) = (πΉβπ₯)) |
34 | 33 | prodsn 15779 |
. . . . . . 7
β’ ((π₯ β π΄ β§ (πΉβπ₯) β β) β βπ β {π₯} (πΉβπ) = (πΉβπ₯)) |
35 | 31, 32, 34 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β βπ β {π₯} (πΉβπ) = (πΉβπ₯)) |
36 | 35 | oveq2d 7365 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (βπ β (π΄ β {π₯})(πΉβπ) Β· βπ β {π₯} (πΉβπ)) = (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
37 | 30, 36 | eqtrd 2777 |
. . . 4
β’ ((π β§ π₯ β π΄) β βπ β π΄ (πΉβπ) = (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
38 | 37 | breq2d 5115 |
. . 3
β’ ((π β§ π₯ β π΄) β ((πΉβπ₯) β₯ βπ β π΄ (πΉβπ) β (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯)))) |
39 | 38 | ralbidva 3170 |
. 2
β’ (π β (βπ₯ β π΄ (πΉβπ₯) β₯ βπ β π΄ (πΉβπ) β βπ₯ β π΄ (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯)))) |
40 | 18, 39 | mpbird 256 |
1
β’ (π β βπ₯ β π΄ (πΉβπ₯) β₯ βπ β π΄ (πΉβπ)) |