Step | Hyp | Ref
| Expression |
1 | | mpomulf 11207 |
. . . . . . 7
β’ (π₯ β β, π¦ β β β¦ (π₯ Β· π¦)):(β Γ
β)βΆβ |
2 | | ffn 6711 |
. . . . . . 7
β’ ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)):(β Γ β)βΆβ
β (π₯ β β,
π¦ β β β¦
(π₯ Β· π¦)) Fn (β Γ
β)) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
β’ (π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) Fn (β Γ
β) |
4 | | mpodvdsmulf1o.x |
. . . . . . . . 9
β’ π = {π₯ β β β£ π₯ β₯ π} |
5 | 4 | ssrab3 4075 |
. . . . . . . 8
β’ π β
β |
6 | | nnsscn 12221 |
. . . . . . . 8
β’ β
β β |
7 | 5, 6 | sstri 3986 |
. . . . . . 7
β’ π β
β |
8 | | mpodvdsmulf1o.y |
. . . . . . . . 9
β’ π = {π₯ β β β£ π₯ β₯ π} |
9 | 8 | ssrab3 4075 |
. . . . . . . 8
β’ π β
β |
10 | 9, 6 | sstri 3986 |
. . . . . . 7
β’ π β
β |
11 | | xpss12 5684 |
. . . . . . 7
β’ ((π β β β§ π β β) β (π Γ π) β (β Γ
β)) |
12 | 7, 10, 11 | mp2an 689 |
. . . . . 6
β’ (π Γ π) β (β Γ
β) |
13 | | fnssres 6667 |
. . . . . 6
β’ (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) Fn (β Γ β) β§ (π Γ π) β (β Γ β)) β
((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)) Fn (π Γ π)) |
14 | 3, 12, 13 | mp2an 689 |
. . . . 5
β’ ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)) Fn (π Γ π) |
15 | 14 | a1i 11 |
. . . 4
β’ (π β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)) Fn (π Γ π)) |
16 | | ovres 7570 |
. . . . . . 7
β’ ((π β π β§ π β π) β (π((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π)) |
17 | 16 | adantl 481 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (π((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π)) |
18 | 7 | sseli 3973 |
. . . . . . . . . 10
β’ (π β π β π β β) |
19 | 18 | adantr 480 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β π β β) |
20 | 10 | sseli 3973 |
. . . . . . . . . 10
β’ (π β π β π β β) |
21 | 20 | adantl 481 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β π β β) |
22 | | ovmpot 7565 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π Β· π)) |
23 | 22 | eqcomd 2732 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π Β· π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π)) |
24 | 19, 21, 23 | syl2anc 583 |
. . . . . . . 8
β’ ((π β π β§ π β π) β (π Β· π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π)) |
25 | 24 | adantl 481 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π)) |
26 | 5 | sseli 3973 |
. . . . . . . . . 10
β’ (π β π β π β β) |
27 | 26 | ad2antrl 725 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β π β β) |
28 | 9 | sseli 3973 |
. . . . . . . . . 10
β’ (π β π β π β β) |
29 | 28 | ad2antll 726 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β π β β) |
30 | 27, 29 | nnmulcld 12269 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β β) |
31 | | breq1 5144 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
32 | 31, 8 | elrab2 3681 |
. . . . . . . . . . 11
β’ (π β π β (π β β β§ π β₯ π)) |
33 | 32 | simprbi 496 |
. . . . . . . . . 10
β’ (π β π β π β₯ π) |
34 | 33 | ad2antll 726 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β π β₯ π) |
35 | | breq1 5144 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
36 | 35, 4 | elrab2 3681 |
. . . . . . . . . . 11
β’ (π β π β (π β β β§ π β₯ π)) |
37 | 36 | simprbi 496 |
. . . . . . . . . 10
β’ (π β π β π β₯ π) |
38 | 37 | ad2antrl 725 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β π β₯ π) |
39 | 29 | nnzd 12589 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β π β β€) |
40 | | mpodvdsmulf1o.2 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
41 | 40 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π β π)) β π β β) |
42 | 41 | nnzd 12589 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β π β β€) |
43 | 27 | nnzd 12589 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β π β β€) |
44 | | dvdscmul 16233 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β€ β§ π β β€) β (π β₯ π β (π Β· π) β₯ (π Β· π))) |
45 | 39, 42, 43, 44 | syl3anc 1368 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β (π β₯ π β (π Β· π) β₯ (π Β· π))) |
46 | | mpodvdsmulf1o.1 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
47 | 46 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ π β π)) β π β β) |
48 | 47 | nnzd 12589 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β π β β€) |
49 | | dvdsmulc 16234 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β€ β§ π β β€) β (π β₯ π β (π Β· π) β₯ (π Β· π))) |
50 | 43, 48, 42, 49 | syl3anc 1368 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β (π β₯ π β (π Β· π) β₯ (π Β· π))) |
51 | 30 | nnzd 12589 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β β€) |
52 | 43, 42 | zmulcld 12676 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β β€) |
53 | 48, 42 | zmulcld 12676 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β β€) |
54 | | dvdstr 16244 |
. . . . . . . . . . 11
β’ (((π Β· π) β β€ β§ (π Β· π) β β€ β§ (π Β· π) β β€) β (((π Β· π) β₯ (π Β· π) β§ (π Β· π) β₯ (π Β· π)) β (π Β· π) β₯ (π Β· π))) |
55 | 51, 52, 53, 54 | syl3anc 1368 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β (((π Β· π) β₯ (π Β· π) β§ (π Β· π) β₯ (π Β· π)) β (π Β· π) β₯ (π Β· π))) |
56 | 45, 50, 55 | syl2and 607 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β ((π β₯ π β§ π β₯ π) β (π Β· π) β₯ (π Β· π))) |
57 | 34, 38, 56 | mp2and 696 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β₯ (π Β· π)) |
58 | | breq1 5144 |
. . . . . . . . 9
β’ (π₯ = (π Β· π) β (π₯ β₯ (π Β· π) β (π Β· π) β₯ (π Β· π))) |
59 | | mpodvdsmulf1o.z |
. . . . . . . . 9
β’ π = {π₯ β β β£ π₯ β₯ (π Β· π)} |
60 | 58, 59 | elrab2 3681 |
. . . . . . . 8
β’ ((π Β· π) β π β ((π Β· π) β β β§ (π Β· π) β₯ (π Β· π))) |
61 | 30, 57, 60 | sylanbrc 582 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) |
62 | 25, 61 | eqeltrrd 2828 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β π) |
63 | 17, 62 | eqeltrd 2827 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (π((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))π) β π) |
64 | 63 | ralrimivva 3194 |
. . . 4
β’ (π β βπ β π βπ β π (π((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))π) β π) |
65 | | ffnov 7531 |
. . . 4
β’ (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)βΆπ β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)) Fn (π Γ π) β§ βπ β π βπ β π (π((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))π) β π)) |
66 | 15, 64, 65 | sylanbrc 582 |
. . 3
β’ (π β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)βΆπ) |
67 | 19 | ad2antlr 724 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β π β β) |
68 | 21 | ad2antlr 724 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β π β β) |
69 | 67, 68, 22 | syl2anc 583 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π Β· π)) |
70 | 7 | sseli 3973 |
. . . . . . . . . 10
β’ (π β π β π β β) |
71 | 70 | ad2antrl 725 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β π β β) |
72 | 10 | sseli 3973 |
. . . . . . . . . 10
β’ (π β π β π β β) |
73 | 72 | ad2antll 726 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β π β β) |
74 | | ovmpot 7565 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π Β· π)) |
75 | 71, 73, 74 | syl2anc 583 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π Β· π)) |
76 | 69, 75 | eqeq12d 2742 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β ((π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β (π Β· π) = (π Β· π))) |
77 | 27 | adantr 480 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
78 | 77 | nnnn0d 12536 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β0) |
79 | | simprll 776 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β π) |
80 | 5, 79 | sselid 3975 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
81 | 80 | nnnn0d 12536 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β0) |
82 | 77 | nnzd 12589 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
83 | 29 | adantr 480 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
84 | 83 | nnzd 12589 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
85 | | dvdsmul1 16228 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) |
86 | 82, 84, 85 | syl2anc 583 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ (π Β· π)) |
87 | | simprr 770 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
88 | 7, 79 | sselid 3975 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
89 | | simprlr 777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β π) |
90 | 10, 89 | sselid 3975 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
91 | 88, 90 | mulcomd 11239 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
92 | 87, 91 | eqtrd 2766 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
93 | 86, 92 | breqtrd 5167 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ (π Β· π)) |
94 | 9, 89 | sselid 3975 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
95 | 94 | nnzd 12589 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
96 | 42 | adantr 480 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
97 | 82, 96 | gcdcomd 16462 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = (π gcd π)) |
98 | 48 | adantr 480 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
99 | 40 | nnzd 12589 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β€) |
100 | 46 | nnzd 12589 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β€) |
101 | 99, 100 | gcdcomd 16462 |
. . . . . . . . . . . . . . . 16
β’ (π β (π gcd π) = (π gcd π)) |
102 | | mpodvdsmulf1o.3 |
. . . . . . . . . . . . . . . 16
β’ (π β (π gcd π) = 1) |
103 | 101, 102 | eqtrd 2766 |
. . . . . . . . . . . . . . 15
β’ (π β (π gcd π) = 1) |
104 | 103 | ad2antrr 723 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
105 | 38 | adantr 480 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
106 | | rpdvds 16604 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β€ β§ π β β€) β§ ((π gcd π) = 1 β§ π β₯ π)) β (π gcd π) = 1) |
107 | 96, 82, 98, 104, 105, 106 | syl32anc 1375 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
108 | 97, 107 | eqtrd 2766 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
109 | | breq1 5144 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
110 | 109, 8 | elrab2 3681 |
. . . . . . . . . . . . . 14
β’ (π β π β (π β β β§ π β₯ π)) |
111 | 110 | simprbi 496 |
. . . . . . . . . . . . 13
β’ (π β π β π β₯ π) |
112 | 89, 111 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
113 | | rpdvds 16604 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ π β β€ β§ π β β€) β§ ((π gcd π) = 1 β§ π β₯ π)) β (π gcd π) = 1) |
114 | 82, 95, 96, 108, 112, 113 | syl32anc 1375 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
115 | 80 | nnzd 12589 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
116 | | coprmdvds 16597 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€ β§ π β β€) β ((π β₯ (π Β· π) β§ (π gcd π) = 1) β π β₯ π)) |
117 | 82, 95, 115, 116 | syl3anc 1368 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β ((π β₯ (π Β· π) β§ (π gcd π) = 1) β π β₯ π)) |
118 | 93, 114, 117 | mp2and 696 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
119 | | dvdsmul1 16228 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) |
120 | 115, 95, 119 | syl2anc 583 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ (π Β· π)) |
121 | 77 | nncnd 12232 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
122 | 83 | nncnd 12232 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
123 | 121, 122 | mulcomd 11239 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
124 | 87, 123 | eqtr3d 2768 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
125 | 120, 124 | breqtrd 5167 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ (π Β· π)) |
126 | 115, 96 | gcdcomd 16462 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = (π gcd π)) |
127 | | breq1 5144 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
128 | 127, 4 | elrab2 3681 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (π β β β§ π β₯ π)) |
129 | 128 | simprbi 496 |
. . . . . . . . . . . . . . 15
β’ (π β π β π β₯ π) |
130 | 79, 129 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
131 | | rpdvds 16604 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β β€ β§ π β β€) β§ ((π gcd π) = 1 β§ π β₯ π)) β (π gcd π) = 1) |
132 | 96, 115, 98, 104, 130, 131 | syl32anc 1375 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
133 | 126, 132 | eqtrd 2766 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
134 | 34 | adantr 480 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
135 | | rpdvds 16604 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ π β β€ β§ π β β€) β§ ((π gcd π) = 1 β§ π β₯ π)) β (π gcd π) = 1) |
136 | 115, 84, 96, 133, 134, 135 | syl32anc 1375 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
137 | | coprmdvds 16597 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€ β§ π β β€) β ((π β₯ (π Β· π) β§ (π gcd π) = 1) β π β₯ π)) |
138 | 115, 84, 82, 137 | syl3anc 1368 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β ((π β₯ (π Β· π) β§ (π gcd π) = 1) β π β₯ π)) |
139 | 125, 136,
138 | mp2and 696 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
140 | | dvdseq 16264 |
. . . . . . . . . 10
β’ (((π β β0
β§ π β
β0) β§ (π β₯ π β§ π β₯ π)) β π = π) |
141 | 78, 81, 118, 139, 140 | syl22anc 836 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π = π) |
142 | 77 | nnne0d 12266 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β 0) |
143 | 141 | oveq1d 7420 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
144 | 87, 143 | eqtr4d 2769 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
145 | 122, 90, 121, 142, 144 | mulcanad 11853 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π = π) |
146 | 141, 145 | opeq12d 4876 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β β¨π, πβ© = β¨π, πβ©) |
147 | 146 | expr 456 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β ((π Β· π) = (π Β· π) β β¨π, πβ© = β¨π, πβ©)) |
148 | 76, 147 | sylbid 239 |
. . . . . 6
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β ((π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β β¨π, πβ© = β¨π, πβ©)) |
149 | 148 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β βπ β π βπ β π ((π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β β¨π, πβ© = β¨π, πβ©)) |
150 | 149 | ralrimivva 3194 |
. . . 4
β’ (π β βπ β π βπ β π βπ β π βπ β π ((π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β β¨π, πβ© = β¨π, πβ©)) |
151 | | fvres 6904 |
. . . . . . . . 9
β’ (π’ β (π Γ π) β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’)) |
152 | | fvres 6904 |
. . . . . . . . 9
β’ (π£ β (π Γ π) β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ£) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£)) |
153 | 151, 152 | eqeqan12d 2740 |
. . . . . . . 8
β’ ((π’ β (π Γ π) β§ π£ β (π Γ π)) β ((((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’) = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ£) β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£))) |
154 | 153 | imbi1d 341 |
. . . . . . 7
β’ ((π’ β (π Γ π) β§ π£ β (π Γ π)) β (((((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’) = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ£) β π’ = π£) β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) β π’ = π£))) |
155 | 154 | ralbidva 3169 |
. . . . . 6
β’ (π’ β (π Γ π) β (βπ£ β (π Γ π)((((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’) = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ£) β π’ = π£) β βπ£ β (π Γ π)(((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) β π’ = π£))) |
156 | 155 | ralbiia 3085 |
. . . . 5
β’
(βπ’ β
(π Γ π)βπ£ β (π Γ π)((((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’) = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ£) β π’ = π£) β βπ’ β (π Γ π)βπ£ β (π Γ π)(((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) β π’ = π£)) |
157 | | fveq2 6885 |
. . . . . . . . . . 11
β’ (π£ = β¨π, πβ© β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))ββ¨π, πβ©)) |
158 | | df-ov 7408 |
. . . . . . . . . . 11
β’ (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))ββ¨π, πβ©) |
159 | 157, 158 | eqtr4di 2784 |
. . . . . . . . . 10
β’ (π£ = β¨π, πβ© β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π)) |
160 | 159 | eqeq2d 2737 |
. . . . . . . . 9
β’ (π£ = β¨π, πβ© β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π))) |
161 | | eqeq2 2738 |
. . . . . . . . 9
β’ (π£ = β¨π, πβ© β (π’ = π£ β π’ = β¨π, πβ©)) |
162 | 160, 161 | imbi12d 344 |
. . . . . . . 8
β’ (π£ = β¨π, πβ© β ((((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) β π’ = π£) β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β π’ = β¨π, πβ©))) |
163 | 162 | ralxp 5835 |
. . . . . . 7
β’
(βπ£ β
(π Γ π)(((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) β π’ = π£) β βπ β π βπ β π (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β π’ = β¨π, πβ©)) |
164 | | fveq2 6885 |
. . . . . . . . . . 11
β’ (π’ = β¨π, πβ© β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))ββ¨π, πβ©)) |
165 | | df-ov 7408 |
. . . . . . . . . . 11
β’ (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))ββ¨π, πβ©) |
166 | 164, 165 | eqtr4di 2784 |
. . . . . . . . . 10
β’ (π’ = β¨π, πβ© β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π)) |
167 | 166 | eqeq1d 2728 |
. . . . . . . . 9
β’ (π’ = β¨π, πβ© β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π))) |
168 | | eqeq1 2730 |
. . . . . . . . 9
β’ (π’ = β¨π, πβ© β (π’ = β¨π, πβ© β β¨π, πβ© = β¨π, πβ©)) |
169 | 167, 168 | imbi12d 344 |
. . . . . . . 8
β’ (π’ = β¨π, πβ© β ((((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β π’ = β¨π, πβ©) β ((π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β β¨π, πβ© = β¨π, πβ©))) |
170 | 169 | 2ralbidv 3212 |
. . . . . . 7
β’ (π’ = β¨π, πβ© β (βπ β π βπ β π (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β π’ = β¨π, πβ©) β βπ β π βπ β π ((π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β β¨π, πβ© = β¨π, πβ©))) |
171 | 163, 170 | bitrid 283 |
. . . . . 6
β’ (π’ = β¨π, πβ© β (βπ£ β (π Γ π)(((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) β π’ = π£) β βπ β π βπ β π ((π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β β¨π, πβ© = β¨π, πβ©))) |
172 | 171 | ralxp 5835 |
. . . . 5
β’
(βπ’ β
(π Γ π)βπ£ β (π Γ π)(((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ’) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))βπ£) β π’ = π£) β βπ β π βπ β π βπ β π βπ β π ((π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β β¨π, πβ© = β¨π, πβ©)) |
173 | 156, 172 | bitri 275 |
. . . 4
β’
(βπ’ β
(π Γ π)βπ£ β (π Γ π)((((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’) = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ£) β π’ = π£) β βπ β π βπ β π βπ β π βπ β π ((π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) = (π(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))π) β β¨π, πβ© = β¨π, πβ©)) |
174 | 150, 173 | sylibr 233 |
. . 3
β’ (π β βπ’ β (π Γ π)βπ£ β (π Γ π)((((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’) = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ£) β π’ = π£)) |
175 | | dff13 7250 |
. . 3
β’ (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)β1-1βπ β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ’ β (π Γ π)βπ£ β (π Γ π)((((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’) = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ£) β π’ = π£))) |
176 | 66, 174, 175 | sylanbrc 582 |
. 2
β’ (π β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)β1-1βπ) |
177 | | breq1 5144 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (π₯ β₯ (π Β· π) β π€ β₯ (π Β· π))) |
178 | 177, 59 | elrab2 3681 |
. . . . . . . . . . 11
β’ (π€ β π β (π€ β β β§ π€ β₯ (π Β· π))) |
179 | 178 | simplbi 497 |
. . . . . . . . . 10
β’ (π€ β π β π€ β β) |
180 | 179 | adantl 481 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π€ β β) |
181 | 180 | nnzd 12589 |
. . . . . . . 8
β’ ((π β§ π€ β π) β π€ β β€) |
182 | 46 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π β β) |
183 | 182 | nnzd 12589 |
. . . . . . . 8
β’ ((π β§ π€ β π) β π β β€) |
184 | 182 | nnne0d 12266 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π β 0) |
185 | | simpr 484 |
. . . . . . . . . 10
β’ ((π€ = 0 β§ π = 0) β π = 0) |
186 | 185 | necon3ai 2959 |
. . . . . . . . 9
β’ (π β 0 β Β¬ (π€ = 0 β§ π = 0)) |
187 | 184, 186 | syl 17 |
. . . . . . . 8
β’ ((π β§ π€ β π) β Β¬ (π€ = 0 β§ π = 0)) |
188 | | gcdn0cl 16450 |
. . . . . . . 8
β’ (((π€ β β€ β§ π β β€) β§ Β¬
(π€ = 0 β§ π = 0)) β (π€ gcd π) β β) |
189 | 181, 183,
187, 188 | syl21anc 835 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd π) β β) |
190 | | gcddvds 16451 |
. . . . . . . . 9
β’ ((π€ β β€ β§ π β β€) β ((π€ gcd π) β₯ π€ β§ (π€ gcd π) β₯ π)) |
191 | 181, 183,
190 | syl2anc 583 |
. . . . . . . 8
β’ ((π β§ π€ β π) β ((π€ gcd π) β₯ π€ β§ (π€ gcd π) β₯ π)) |
192 | 191 | simprd 495 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd π) β₯ π) |
193 | | breq1 5144 |
. . . . . . . 8
β’ (π₯ = (π€ gcd π) β (π₯ β₯ π β (π€ gcd π) β₯ π)) |
194 | 193, 4 | elrab2 3681 |
. . . . . . 7
β’ ((π€ gcd π) β π β ((π€ gcd π) β β β§ (π€ gcd π) β₯ π)) |
195 | 189, 192,
194 | sylanbrc 582 |
. . . . . 6
β’ ((π β§ π€ β π) β (π€ gcd π) β π) |
196 | 40 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π β β) |
197 | 196 | nnzd 12589 |
. . . . . . . 8
β’ ((π β§ π€ β π) β π β β€) |
198 | 196 | nnne0d 12266 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π β 0) |
199 | | simpr 484 |
. . . . . . . . . 10
β’ ((π€ = 0 β§ π = 0) β π = 0) |
200 | 199 | necon3ai 2959 |
. . . . . . . . 9
β’ (π β 0 β Β¬ (π€ = 0 β§ π = 0)) |
201 | 198, 200 | syl 17 |
. . . . . . . 8
β’ ((π β§ π€ β π) β Β¬ (π€ = 0 β§ π = 0)) |
202 | | gcdn0cl 16450 |
. . . . . . . 8
β’ (((π€ β β€ β§ π β β€) β§ Β¬
(π€ = 0 β§ π = 0)) β (π€ gcd π) β β) |
203 | 181, 197,
201, 202 | syl21anc 835 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd π) β β) |
204 | | gcddvds 16451 |
. . . . . . . . 9
β’ ((π€ β β€ β§ π β β€) β ((π€ gcd π) β₯ π€ β§ (π€ gcd π) β₯ π)) |
205 | 181, 197,
204 | syl2anc 583 |
. . . . . . . 8
β’ ((π β§ π€ β π) β ((π€ gcd π) β₯ π€ β§ (π€ gcd π) β₯ π)) |
206 | 205 | simprd 495 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd π) β₯ π) |
207 | | breq1 5144 |
. . . . . . . 8
β’ (π₯ = (π€ gcd π) β (π₯ β₯ π β (π€ gcd π) β₯ π)) |
208 | 207, 8 | elrab2 3681 |
. . . . . . 7
β’ ((π€ gcd π) β π β ((π€ gcd π) β β β§ (π€ gcd π) β₯ π)) |
209 | 203, 206,
208 | sylanbrc 582 |
. . . . . 6
β’ ((π β§ π€ β π) β (π€ gcd π) β π) |
210 | 195, 209 | opelxpd 5708 |
. . . . 5
β’ ((π β§ π€ β π) β β¨(π€ gcd π), (π€ gcd π)β© β (π Γ π)) |
211 | 210 | fvresd 6905 |
. . . . . . 7
β’ ((π β§ π€ β π) β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))ββ¨(π€ gcd π), (π€ gcd π)β©) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))ββ¨(π€ gcd π), (π€ gcd π)β©)) |
212 | | df-ov 7408 |
. . . . . . . 8
β’ ((π€ gcd π)(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))(π€ gcd π)) = ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))ββ¨(π€ gcd π), (π€ gcd π)β©) |
213 | 189 | nncnd 12232 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β (π€ gcd π) β β) |
214 | 203 | nncnd 12232 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β (π€ gcd π) β β) |
215 | | ovmpot 7565 |
. . . . . . . . 9
β’ (((π€ gcd π) β β β§ (π€ gcd π) β β) β ((π€ gcd π)(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))(π€ gcd π)) = ((π€ gcd π) Β· (π€ gcd π))) |
216 | 213, 214,
215 | syl2anc 583 |
. . . . . . . 8
β’ ((π β§ π€ β π) β ((π€ gcd π)(π₯ β β, π¦ β β β¦ (π₯ Β· π¦))(π€ gcd π)) = ((π€ gcd π) Β· (π€ gcd π))) |
217 | 212, 216 | eqtr3id 2780 |
. . . . . . 7
β’ ((π β§ π€ β π) β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦))ββ¨(π€ gcd π), (π€ gcd π)β©) = ((π€ gcd π) Β· (π€ gcd π))) |
218 | | df-ov 7408 |
. . . . . . . 8
β’ ((π€ gcd π) Β· (π€ gcd π)) = ( Β· ββ¨(π€ gcd π), (π€ gcd π)β©) |
219 | 218 | a1i 11 |
. . . . . . 7
β’ ((π β§ π€ β π) β ((π€ gcd π) Β· (π€ gcd π)) = ( Β· ββ¨(π€ gcd π), (π€ gcd π)β©)) |
220 | 211, 217,
219 | 3eqtrd 2770 |
. . . . . 6
β’ ((π β§ π€ β π) β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))ββ¨(π€ gcd π), (π€ gcd π)β©) = ( Β· ββ¨(π€ gcd π), (π€ gcd π)β©)) |
221 | 102 | adantr 480 |
. . . . . . . 8
β’ ((π β§ π€ β π) β (π gcd π) = 1) |
222 | | rpmulgcd2 16600 |
. . . . . . . 8
β’ (((π€ β β€ β§ π β β€ β§ π β β€) β§ (π gcd π) = 1) β (π€ gcd (π Β· π)) = ((π€ gcd π) Β· (π€ gcd π))) |
223 | 181, 183,
197, 221, 222 | syl31anc 1370 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd (π Β· π)) = ((π€ gcd π) Β· (π€ gcd π))) |
224 | 223, 218 | eqtrdi 2782 |
. . . . . 6
β’ ((π β§ π€ β π) β (π€ gcd (π Β· π)) = ( Β· ββ¨(π€ gcd π), (π€ gcd π)β©)) |
225 | 178 | simprbi 496 |
. . . . . . . 8
β’ (π€ β π β π€ β₯ (π Β· π)) |
226 | 225 | adantl 481 |
. . . . . . 7
β’ ((π β§ π€ β π) β π€ β₯ (π Β· π)) |
227 | 46, 40 | nnmulcld 12269 |
. . . . . . . 8
β’ (π β (π Β· π) β β) |
228 | | gcdeq 16502 |
. . . . . . . 8
β’ ((π€ β β β§ (π Β· π) β β) β ((π€ gcd (π Β· π)) = π€ β π€ β₯ (π Β· π))) |
229 | 179, 227,
228 | syl2anr 596 |
. . . . . . 7
β’ ((π β§ π€ β π) β ((π€ gcd (π Β· π)) = π€ β π€ β₯ (π Β· π))) |
230 | 226, 229 | mpbird 257 |
. . . . . 6
β’ ((π β§ π€ β π) β (π€ gcd (π Β· π)) = π€) |
231 | 220, 224,
230 | 3eqtr2rd 2773 |
. . . . 5
β’ ((π β§ π€ β π) β π€ = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))ββ¨(π€ gcd π), (π€ gcd π)β©)) |
232 | | fveq2 6885 |
. . . . . 6
β’ (π’ = β¨(π€ gcd π), (π€ gcd π)β© β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’) = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))ββ¨(π€ gcd π), (π€ gcd π)β©)) |
233 | 232 | rspceeqv 3628 |
. . . . 5
β’
((β¨(π€ gcd π), (π€ gcd π)β© β (π Γ π) β§ π€ = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))ββ¨(π€ gcd π), (π€ gcd π)β©)) β βπ’ β (π Γ π)π€ = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’)) |
234 | 210, 231,
233 | syl2anc 583 |
. . . 4
β’ ((π β§ π€ β π) β βπ’ β (π Γ π)π€ = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’)) |
235 | 234 | ralrimiva 3140 |
. . 3
β’ (π β βπ€ β π βπ’ β (π Γ π)π€ = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’)) |
236 | | dffo3 7097 |
. . 3
β’ (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)βontoβπ β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π βπ’ β (π Γ π)π€ = (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π))βπ’))) |
237 | 66, 235, 236 | sylanbrc 582 |
. 2
β’ (π β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)βontoβπ) |
238 | | df-f1o 6544 |
. 2
β’ (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)β1-1-ontoβπ β (((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)β1-1βπ β§ ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)βontoβπ)) |
239 | 176, 237,
238 | sylanbrc 582 |
1
β’ (π β ((π₯ β β, π¦ β β β¦ (π₯ Β· π¦)) βΎ (π Γ π)):(π Γ π)β1-1-ontoβπ) |