Step | Hyp | Ref
| Expression |
1 | | fprodfvdvdsd.a |
. . . . . . 7
β’ (π β π΄ β Fin) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β π΄ β Fin) |
3 | | diffi 9057 |
. . . . . 6
β’ (π΄ β Fin β (π΄ β {π₯}) β Fin) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (π΄ β {π₯}) β Fin) |
5 | | fprodfvdvdsd.f |
. . . . . . . 8
β’ (π β πΉ:π΅βΆβ€) |
6 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (π΄ β {π₯})) β πΉ:π΅βΆβ€) |
7 | | fprodfvdvdsd.b |
. . . . . . . . 9
β’ (π β π΄ β π΅) |
8 | 7 | ssdifssd 4101 |
. . . . . . . 8
β’ (π β (π΄ β {π₯}) β π΅) |
9 | 8 | sselda 3943 |
. . . . . . 7
β’ ((π β§ π β (π΄ β {π₯})) β π β π΅) |
10 | 6, 9 | ffvelcdmd 7031 |
. . . . . 6
β’ ((π β§ π β (π΄ β {π₯})) β (πΉβπ) β β€) |
11 | 10 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β π΄) β§ π β (π΄ β {π₯})) β (πΉβπ) β β€) |
12 | 4, 11 | fprodzcl 15772 |
. . . 4
β’ ((π β§ π₯ β π΄) β βπ β (π΄ β {π₯})(πΉβπ) β β€) |
13 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΄) β πΉ:π΅βΆβ€) |
14 | 7 | sselda 3943 |
. . . . 5
β’ ((π β§ π₯ β π΄) β π₯ β π΅) |
15 | 13, 14 | ffvelcdmd 7031 |
. . . 4
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β€) |
16 | | dvdsmul2 16096 |
. . . 4
β’
((βπ β
(π΄ β {π₯})(πΉβπ) β β€ β§ (πΉβπ₯) β β€) β (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
17 | 12, 15, 16 | syl2anc 585 |
. . 3
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
18 | 17 | ralrimiva 3142 |
. 2
β’ (π β βπ₯ β π΄ (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
19 | | neldifsnd 4752 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β Β¬ π₯ β (π΄ β {π₯})) |
20 | | disjsn 4671 |
. . . . . . 7
β’ (((π΄ β {π₯}) β© {π₯}) = β
β Β¬ π₯ β (π΄ β {π₯})) |
21 | 19, 20 | sylibr 233 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β ((π΄ β {π₯}) β© {π₯}) = β
) |
22 | | difsnid 4769 |
. . . . . . . 8
β’ (π₯ β π΄ β ((π΄ β {π₯}) βͺ {π₯}) = π΄) |
23 | 22 | eqcomd 2744 |
. . . . . . 7
β’ (π₯ β π΄ β π΄ = ((π΄ β {π₯}) βͺ {π₯})) |
24 | 23 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β π΄ = ((π΄ β {π₯}) βͺ {π₯})) |
25 | 13 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π΄) β πΉ:π΅βΆβ€) |
26 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β π΄ β π΅) |
27 | 26 | sselda 3943 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π΄) β π β π΅) |
28 | 25, 27 | ffvelcdmd 7031 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π β π΄) β (πΉβπ) β β€) |
29 | 28 | zcnd 12541 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ π β π΄) β (πΉβπ) β β) |
30 | 21, 24, 2, 29 | fprodsplit 15784 |
. . . . 5
β’ ((π β§ π₯ β π΄) β βπ β π΄ (πΉβπ) = (βπ β (π΄ β {π₯})(πΉβπ) Β· βπ β {π₯} (πΉβπ))) |
31 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
32 | 15 | zcnd 12541 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β) |
33 | | fveq2 6838 |
. . . . . . . 8
β’ (π = π₯ β (πΉβπ) = (πΉβπ₯)) |
34 | 33 | prodsn 15780 |
. . . . . . 7
β’ ((π₯ β π΄ β§ (πΉβπ₯) β β) β βπ β {π₯} (πΉβπ) = (πΉβπ₯)) |
35 | 31, 32, 34 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β βπ β {π₯} (πΉβπ) = (πΉβπ₯)) |
36 | 35 | oveq2d 7366 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (βπ β (π΄ β {π₯})(πΉβπ) Β· βπ β {π₯} (πΉβπ)) = (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
37 | 30, 36 | eqtrd 2778 |
. . . 4
β’ ((π β§ π₯ β π΄) β βπ β π΄ (πΉβπ) = (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯))) |
38 | 37 | breq2d 5116 |
. . 3
β’ ((π β§ π₯ β π΄) β ((πΉβπ₯) β₯ βπ β π΄ (πΉβπ) β (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯)))) |
39 | 38 | ralbidva 3171 |
. 2
β’ (π β (βπ₯ β π΄ (πΉβπ₯) β₯ βπ β π΄ (πΉβπ) β βπ₯ β π΄ (πΉβπ₯) β₯ (βπ β (π΄ β {π₯})(πΉβπ) Β· (πΉβπ₯)))) |
40 | 18, 39 | mpbird 257 |
1
β’ (π β βπ₯ β π΄ (πΉβπ₯) β₯ βπ β π΄ (πΉβπ)) |