Step | Hyp | Ref
| Expression |
1 | | ax-mulf 11001 |
. . . . . . 7
β’ Β·
:(β Γ β)βΆβ |
2 | | ffn 6630 |
. . . . . . 7
β’ (
Β· :(β Γ β)βΆβ β Β· Fn (β
Γ β)) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
β’ Β·
Fn (β Γ β) |
4 | | dvdsmulf1o.x |
. . . . . . . . 9
β’ π = {π₯ β β β£ π₯ β₯ π} |
5 | 4 | ssrab3 4021 |
. . . . . . . 8
β’ π β
β |
6 | | nnsscn 12028 |
. . . . . . . 8
β’ β
β β |
7 | 5, 6 | sstri 3935 |
. . . . . . 7
β’ π β
β |
8 | | dvdsmulf1o.y |
. . . . . . . . 9
β’ π = {π₯ β β β£ π₯ β₯ π} |
9 | 8 | ssrab3 4021 |
. . . . . . . 8
β’ π β
β |
10 | 9, 6 | sstri 3935 |
. . . . . . 7
β’ π β
β |
11 | | xpss12 5615 |
. . . . . . 7
β’ ((π β β β§ π β β) β (π Γ π) β (β Γ
β)) |
12 | 7, 10, 11 | mp2an 690 |
. . . . . 6
β’ (π Γ π) β (β Γ
β) |
13 | | fnssres 6586 |
. . . . . 6
β’ ((
Β· Fn (β Γ β) β§ (π Γ π) β (β Γ β)) β
( Β· βΎ (π
Γ π)) Fn (π Γ π)) |
14 | 3, 12, 13 | mp2an 690 |
. . . . 5
β’ (
Β· βΎ (π Γ
π)) Fn (π Γ π) |
15 | 14 | a1i 11 |
. . . 4
β’ (π β ( Β· βΎ (π Γ π)) Fn (π Γ π)) |
16 | | ovres 7470 |
. . . . . . 7
β’ ((π β π β§ π β π) β (π( Β· βΎ (π Γ π))π) = (π Β· π)) |
17 | 16 | adantl 483 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (π( Β· βΎ (π Γ π))π) = (π Β· π)) |
18 | | breq1 5084 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
19 | 18, 4 | elrab2 3632 |
. . . . . . . . . 10
β’ (π β π β (π β β β§ π β₯ π)) |
20 | 19 | simplbi 499 |
. . . . . . . . 9
β’ (π β π β π β β) |
21 | 20 | ad2antrl 726 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π β β) |
22 | | breq1 5084 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
23 | 22, 8 | elrab2 3632 |
. . . . . . . . . 10
β’ (π β π β (π β β β§ π β₯ π)) |
24 | 23 | simplbi 499 |
. . . . . . . . 9
β’ (π β π β π β β) |
25 | 24 | ad2antll 727 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π β β) |
26 | 21, 25 | nnmulcld 12076 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β β) |
27 | 23 | simprbi 498 |
. . . . . . . . 9
β’ (π β π β π β₯ π) |
28 | 27 | ad2antll 727 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π β₯ π) |
29 | 19 | simprbi 498 |
. . . . . . . . 9
β’ (π β π β π β₯ π) |
30 | 29 | ad2antrl 726 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π β₯ π) |
31 | 25 | nnzd 12475 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β π β β€) |
32 | | dvdsmulf1o.2 |
. . . . . . . . . . . 12
β’ (π β π β β) |
33 | 32 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β π β β) |
34 | 33 | nnzd 12475 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β π β β€) |
35 | 21 | nnzd 12475 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β π β β€) |
36 | | dvdscmul 16041 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β€ β§ π β β€) β (π β₯ π β (π Β· π) β₯ (π Β· π))) |
37 | 31, 34, 35, 36 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β (π β₯ π β (π Β· π) β₯ (π Β· π))) |
38 | | dvdsmulf1o.1 |
. . . . . . . . . . . 12
β’ (π β π β β) |
39 | 38 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β π β β) |
40 | 39 | nnzd 12475 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β π β β€) |
41 | | dvdsmulc 16042 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β€ β§ π β β€) β (π β₯ π β (π Β· π) β₯ (π Β· π))) |
42 | 35, 40, 34, 41 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β (π β₯ π β (π Β· π) β₯ (π Β· π))) |
43 | 26 | nnzd 12475 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β β€) |
44 | 35, 34 | zmulcld 12482 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β β€) |
45 | 40, 34 | zmulcld 12482 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β β€) |
46 | | dvdstr 16052 |
. . . . . . . . . 10
β’ (((π Β· π) β β€ β§ (π Β· π) β β€ β§ (π Β· π) β β€) β (((π Β· π) β₯ (π Β· π) β§ (π Β· π) β₯ (π Β· π)) β (π Β· π) β₯ (π Β· π))) |
47 | 43, 44, 45, 46 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β (((π Β· π) β₯ (π Β· π) β§ (π Β· π) β₯ (π Β· π)) β (π Β· π) β₯ (π Β· π))) |
48 | 37, 42, 47 | syl2and 609 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β ((π β₯ π β§ π β₯ π) β (π Β· π) β₯ (π Β· π))) |
49 | 28, 30, 48 | mp2and 697 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β₯ (π Β· π)) |
50 | | breq1 5084 |
. . . . . . . 8
β’ (π₯ = (π Β· π) β (π₯ β₯ (π Β· π) β (π Β· π) β₯ (π Β· π))) |
51 | | dvdsmulf1o.z |
. . . . . . . 8
β’ π = {π₯ β β β£ π₯ β₯ (π Β· π)} |
52 | 50, 51 | elrab2 3632 |
. . . . . . 7
β’ ((π Β· π) β π β ((π Β· π) β β β§ (π Β· π) β₯ (π Β· π))) |
53 | 26, 49, 52 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) |
54 | 17, 53 | eqeltrd 2837 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (π( Β· βΎ (π Γ π))π) β π) |
55 | 54 | ralrimivva 3194 |
. . . 4
β’ (π β βπ β π βπ β π (π( Β· βΎ (π Γ π))π) β π) |
56 | | ffnov 7433 |
. . . 4
β’ ((
Β· βΎ (π Γ
π)):(π Γ π)βΆπ β (( Β· βΎ (π Γ π)) Fn (π Γ π) β§ βπ β π βπ β π (π( Β· βΎ (π Γ π))π) β π)) |
57 | 15, 55, 56 | sylanbrc 584 |
. . 3
β’ (π β ( Β· βΎ (π Γ π)):(π Γ π)βΆπ) |
58 | 21 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
59 | 58 | nnnn0d 12343 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β0) |
60 | | simprll 777 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β π) |
61 | | breq1 5084 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
62 | 61, 4 | elrab2 3632 |
. . . . . . . . . . . 12
β’ (π β π β (π β β β§ π β₯ π)) |
63 | 62 | simplbi 499 |
. . . . . . . . . . 11
β’ (π β π β π β β) |
64 | 60, 63 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
65 | 64 | nnnn0d 12343 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β0) |
66 | 58 | nnzd 12475 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
67 | 25 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
68 | 67 | nnzd 12475 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
69 | | dvdsmul1 16036 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) |
70 | 66, 68, 69 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ (π Β· π)) |
71 | | simprr 771 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
72 | 7, 60 | sselid 3924 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
73 | | simprlr 778 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β π) |
74 | | breq1 5084 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
75 | 74, 8 | elrab2 3632 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (π β β β§ π β₯ π)) |
76 | 75 | simplbi 499 |
. . . . . . . . . . . . . . 15
β’ (π β π β π β β) |
77 | 73, 76 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
78 | 77 | nncnd 12039 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
79 | 72, 78 | mulcomd 11046 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
80 | 71, 79 | eqtrd 2776 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
81 | 70, 80 | breqtrd 5107 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ (π Β· π)) |
82 | 77 | nnzd 12475 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
83 | 34 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
84 | 66, 83 | gcdcomd 16270 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = (π gcd π)) |
85 | 40 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
86 | 32 | nnzd 12475 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β€) |
87 | 38 | nnzd 12475 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β€) |
88 | 86, 87 | gcdcomd 16270 |
. . . . . . . . . . . . . . 15
β’ (π β (π gcd π) = (π gcd π)) |
89 | | dvdsmulf1o.3 |
. . . . . . . . . . . . . . 15
β’ (π β (π gcd π) = 1) |
90 | 88, 89 | eqtrd 2776 |
. . . . . . . . . . . . . 14
β’ (π β (π gcd π) = 1) |
91 | 90 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
92 | 30 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
93 | | rpdvds 16414 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β€ β§ π β β€) β§ ((π gcd π) = 1 β§ π β₯ π)) β (π gcd π) = 1) |
94 | 83, 66, 85, 91, 92, 93 | syl32anc 1378 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
95 | 84, 94 | eqtrd 2776 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
96 | 75 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π β π β π β₯ π) |
97 | 73, 96 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
98 | | rpdvds 16414 |
. . . . . . . . . . 11
β’ (((π β β€ β§ π β β€ β§ π β β€) β§ ((π gcd π) = 1 β§ π β₯ π)) β (π gcd π) = 1) |
99 | 66, 82, 83, 95, 97, 98 | syl32anc 1378 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
100 | 64 | nnzd 12475 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β€) |
101 | | coprmdvds 16407 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β€ β§ π β β€) β ((π β₯ (π Β· π) β§ (π gcd π) = 1) β π β₯ π)) |
102 | 66, 82, 100, 101 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β ((π β₯ (π Β· π) β§ (π gcd π) = 1) β π β₯ π)) |
103 | 81, 99, 102 | mp2and 697 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
104 | | dvdsmul1 16036 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) |
105 | 100, 82, 104 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ (π Β· π)) |
106 | 58 | nncnd 12039 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
107 | 67 | nncnd 12039 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β β) |
108 | 106, 107 | mulcomd 11046 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
109 | 71, 108 | eqtr3d 2778 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
110 | 105, 109 | breqtrd 5107 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ (π Β· π)) |
111 | 100, 83 | gcdcomd 16270 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = (π gcd π)) |
112 | 62 | simprbi 498 |
. . . . . . . . . . . . . 14
β’ (π β π β π β₯ π) |
113 | 60, 112 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
114 | | rpdvds 16414 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ π β β€ β§ π β β€) β§ ((π gcd π) = 1 β§ π β₯ π)) β (π gcd π) = 1) |
115 | 83, 100, 85, 91, 113, 114 | syl32anc 1378 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
116 | 111, 115 | eqtrd 2776 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
117 | 28 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
118 | | rpdvds 16414 |
. . . . . . . . . . 11
β’ (((π β β€ β§ π β β€ β§ π β β€) β§ ((π gcd π) = 1 β§ π β₯ π)) β (π gcd π) = 1) |
119 | 100, 68, 83, 116, 117, 118 | syl32anc 1378 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π gcd π) = 1) |
120 | | coprmdvds 16407 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β€ β§ π β β€) β ((π β₯ (π Β· π) β§ (π gcd π) = 1) β π β₯ π)) |
121 | 100, 68, 66, 120 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β ((π β₯ (π Β· π) β§ (π gcd π) = 1) β π β₯ π)) |
122 | 110, 119,
121 | mp2and 697 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β₯ π) |
123 | | dvdseq 16072 |
. . . . . . . . 9
β’ (((π β β0
β§ π β
β0) β§ (π β₯ π β§ π β₯ π)) β π = π) |
124 | 59, 65, 103, 122, 123 | syl22anc 837 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π = π) |
125 | 58 | nnne0d 12073 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π β 0) |
126 | 124 | oveq1d 7322 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
127 | 71, 126 | eqtr4d 2779 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β (π Β· π) = (π Β· π)) |
128 | 107, 78, 106, 125, 127 | mulcanad 11660 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β π = π) |
129 | 124, 128 | opeq12d 4817 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ (π Β· π) = (π Β· π))) β β¨π, πβ© = β¨π, πβ©) |
130 | 129 | expr 458 |
. . . . . 6
β’ (((π β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β ((π Β· π) = (π Β· π) β β¨π, πβ© = β¨π, πβ©)) |
131 | 130 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β βπ β π βπ β π ((π Β· π) = (π Β· π) β β¨π, πβ© = β¨π, πβ©)) |
132 | 131 | ralrimivva 3194 |
. . . 4
β’ (π β βπ β π βπ β π βπ β π βπ β π ((π Β· π) = (π Β· π) β β¨π, πβ© = β¨π, πβ©)) |
133 | | fvres 6823 |
. . . . . . . . 9
β’ (π’ β (π Γ π) β (( Β· βΎ (π Γ π))βπ’) = ( Β· βπ’)) |
134 | | fvres 6823 |
. . . . . . . . 9
β’ (π£ β (π Γ π) β (( Β· βΎ (π Γ π))βπ£) = ( Β· βπ£)) |
135 | 133, 134 | eqeqan12d 2750 |
. . . . . . . 8
β’ ((π’ β (π Γ π) β§ π£ β (π Γ π)) β ((( Β· βΎ (π Γ π))βπ’) = (( Β· βΎ (π Γ π))βπ£) β ( Β· βπ’) = ( Β· βπ£))) |
136 | 135 | imbi1d 342 |
. . . . . . 7
β’ ((π’ β (π Γ π) β§ π£ β (π Γ π)) β (((( Β· βΎ (π Γ π))βπ’) = (( Β· βΎ (π Γ π))βπ£) β π’ = π£) β (( Β· βπ’) = ( Β· βπ£) β π’ = π£))) |
137 | 136 | ralbidva 3169 |
. . . . . 6
β’ (π’ β (π Γ π) β (βπ£ β (π Γ π)((( Β· βΎ (π Γ π))βπ’) = (( Β· βΎ (π Γ π))βπ£) β π’ = π£) β βπ£ β (π Γ π)(( Β· βπ’) = ( Β· βπ£) β π’ = π£))) |
138 | 137 | ralbiia 3091 |
. . . . 5
β’
(βπ’ β
(π Γ π)βπ£ β (π Γ π)((( Β· βΎ (π Γ π))βπ’) = (( Β· βΎ (π Γ π))βπ£) β π’ = π£) β βπ’ β (π Γ π)βπ£ β (π Γ π)(( Β· βπ’) = ( Β· βπ£) β π’ = π£)) |
139 | | fveq2 6804 |
. . . . . . . . . . 11
β’ (π£ = β¨π, πβ© β ( Β· βπ£) = ( Β·
ββ¨π, πβ©)) |
140 | | df-ov 7310 |
. . . . . . . . . . 11
β’ (π Β· π) = ( Β· ββ¨π, πβ©) |
141 | 139, 140 | eqtr4di 2794 |
. . . . . . . . . 10
β’ (π£ = β¨π, πβ© β ( Β· βπ£) = (π Β· π)) |
142 | 141 | eqeq2d 2747 |
. . . . . . . . 9
β’ (π£ = β¨π, πβ© β (( Β· βπ’) = ( Β· βπ£) β ( Β· βπ’) = (π Β· π))) |
143 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π£ = β¨π, πβ© β (π’ = π£ β π’ = β¨π, πβ©)) |
144 | 142, 143 | imbi12d 345 |
. . . . . . . 8
β’ (π£ = β¨π, πβ© β ((( Β· βπ’) = ( Β· βπ£) β π’ = π£) β (( Β· βπ’) = (π Β· π) β π’ = β¨π, πβ©))) |
145 | 144 | ralxp 5763 |
. . . . . . 7
β’
(βπ£ β
(π Γ π)(( Β· βπ’) = ( Β· βπ£) β π’ = π£) β βπ β π βπ β π (( Β· βπ’) = (π Β· π) β π’ = β¨π, πβ©)) |
146 | | fveq2 6804 |
. . . . . . . . . . 11
β’ (π’ = β¨π, πβ© β ( Β· βπ’) = ( Β·
ββ¨π, πβ©)) |
147 | | df-ov 7310 |
. . . . . . . . . . 11
β’ (π Β· π) = ( Β· ββ¨π, πβ©) |
148 | 146, 147 | eqtr4di 2794 |
. . . . . . . . . 10
β’ (π’ = β¨π, πβ© β ( Β· βπ’) = (π Β· π)) |
149 | 148 | eqeq1d 2738 |
. . . . . . . . 9
β’ (π’ = β¨π, πβ© β (( Β· βπ’) = (π Β· π) β (π Β· π) = (π Β· π))) |
150 | | eqeq1 2740 |
. . . . . . . . 9
β’ (π’ = β¨π, πβ© β (π’ = β¨π, πβ© β β¨π, πβ© = β¨π, πβ©)) |
151 | 149, 150 | imbi12d 345 |
. . . . . . . 8
β’ (π’ = β¨π, πβ© β ((( Β· βπ’) = (π Β· π) β π’ = β¨π, πβ©) β ((π Β· π) = (π Β· π) β β¨π, πβ© = β¨π, πβ©))) |
152 | 151 | 2ralbidv 3209 |
. . . . . . 7
β’ (π’ = β¨π, πβ© β (βπ β π βπ β π (( Β· βπ’) = (π Β· π) β π’ = β¨π, πβ©) β βπ β π βπ β π ((π Β· π) = (π Β· π) β β¨π, πβ© = β¨π, πβ©))) |
153 | 145, 152 | bitrid 283 |
. . . . . 6
β’ (π’ = β¨π, πβ© β (βπ£ β (π Γ π)(( Β· βπ’) = ( Β· βπ£) β π’ = π£) β βπ β π βπ β π ((π Β· π) = (π Β· π) β β¨π, πβ© = β¨π, πβ©))) |
154 | 153 | ralxp 5763 |
. . . . 5
β’
(βπ’ β
(π Γ π)βπ£ β (π Γ π)(( Β· βπ’) = ( Β· βπ£) β π’ = π£) β βπ β π βπ β π βπ β π βπ β π ((π Β· π) = (π Β· π) β β¨π, πβ© = β¨π, πβ©)) |
155 | 138, 154 | bitri 275 |
. . . 4
β’
(βπ’ β
(π Γ π)βπ£ β (π Γ π)((( Β· βΎ (π Γ π))βπ’) = (( Β· βΎ (π Γ π))βπ£) β π’ = π£) β βπ β π βπ β π βπ β π βπ β π ((π Β· π) = (π Β· π) β β¨π, πβ© = β¨π, πβ©)) |
156 | 132, 155 | sylibr 233 |
. . 3
β’ (π β βπ’ β (π Γ π)βπ£ β (π Γ π)((( Β· βΎ (π Γ π))βπ’) = (( Β· βΎ (π Γ π))βπ£) β π’ = π£)) |
157 | | dff13 7160 |
. . 3
β’ ((
Β· βΎ (π Γ
π)):(π Γ π)β1-1βπ β (( Β· βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ’ β (π Γ π)βπ£ β (π Γ π)((( Β· βΎ (π Γ π))βπ’) = (( Β· βΎ (π Γ π))βπ£) β π’ = π£))) |
158 | 57, 156, 157 | sylanbrc 584 |
. 2
β’ (π β ( Β· βΎ (π Γ π)):(π Γ π)β1-1βπ) |
159 | | breq1 5084 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (π₯ β₯ (π Β· π) β π€ β₯ (π Β· π))) |
160 | 159, 51 | elrab2 3632 |
. . . . . . . . . . 11
β’ (π€ β π β (π€ β β β§ π€ β₯ (π Β· π))) |
161 | 160 | simplbi 499 |
. . . . . . . . . 10
β’ (π€ β π β π€ β β) |
162 | 161 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π€ β β) |
163 | 162 | nnzd 12475 |
. . . . . . . 8
β’ ((π β§ π€ β π) β π€ β β€) |
164 | 38 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π β β) |
165 | 164 | nnzd 12475 |
. . . . . . . 8
β’ ((π β§ π€ β π) β π β β€) |
166 | 164 | nnne0d 12073 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π β 0) |
167 | | simpr 486 |
. . . . . . . . . 10
β’ ((π€ = 0 β§ π = 0) β π = 0) |
168 | 167 | necon3ai 2966 |
. . . . . . . . 9
β’ (π β 0 β Β¬ (π€ = 0 β§ π = 0)) |
169 | 166, 168 | syl 17 |
. . . . . . . 8
β’ ((π β§ π€ β π) β Β¬ (π€ = 0 β§ π = 0)) |
170 | | gcdn0cl 16258 |
. . . . . . . 8
β’ (((π€ β β€ β§ π β β€) β§ Β¬
(π€ = 0 β§ π = 0)) β (π€ gcd π) β β) |
171 | 163, 165,
169, 170 | syl21anc 836 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd π) β β) |
172 | | gcddvds 16259 |
. . . . . . . . 9
β’ ((π€ β β€ β§ π β β€) β ((π€ gcd π) β₯ π€ β§ (π€ gcd π) β₯ π)) |
173 | 163, 165,
172 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π€ β π) β ((π€ gcd π) β₯ π€ β§ (π€ gcd π) β₯ π)) |
174 | 173 | simprd 497 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd π) β₯ π) |
175 | | breq1 5084 |
. . . . . . . 8
β’ (π₯ = (π€ gcd π) β (π₯ β₯ π β (π€ gcd π) β₯ π)) |
176 | 175, 4 | elrab2 3632 |
. . . . . . 7
β’ ((π€ gcd π) β π β ((π€ gcd π) β β β§ (π€ gcd π) β₯ π)) |
177 | 171, 174,
176 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ π€ β π) β (π€ gcd π) β π) |
178 | 32 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π β β) |
179 | 178 | nnzd 12475 |
. . . . . . . 8
β’ ((π β§ π€ β π) β π β β€) |
180 | 178 | nnne0d 12073 |
. . . . . . . . 9
β’ ((π β§ π€ β π) β π β 0) |
181 | | simpr 486 |
. . . . . . . . . 10
β’ ((π€ = 0 β§ π = 0) β π = 0) |
182 | 181 | necon3ai 2966 |
. . . . . . . . 9
β’ (π β 0 β Β¬ (π€ = 0 β§ π = 0)) |
183 | 180, 182 | syl 17 |
. . . . . . . 8
β’ ((π β§ π€ β π) β Β¬ (π€ = 0 β§ π = 0)) |
184 | | gcdn0cl 16258 |
. . . . . . . 8
β’ (((π€ β β€ β§ π β β€) β§ Β¬
(π€ = 0 β§ π = 0)) β (π€ gcd π) β β) |
185 | 163, 179,
183, 184 | syl21anc 836 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd π) β β) |
186 | | gcddvds 16259 |
. . . . . . . . 9
β’ ((π€ β β€ β§ π β β€) β ((π€ gcd π) β₯ π€ β§ (π€ gcd π) β₯ π)) |
187 | 163, 179,
186 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π€ β π) β ((π€ gcd π) β₯ π€ β§ (π€ gcd π) β₯ π)) |
188 | 187 | simprd 497 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd π) β₯ π) |
189 | | breq1 5084 |
. . . . . . . 8
β’ (π₯ = (π€ gcd π) β (π₯ β₯ π β (π€ gcd π) β₯ π)) |
190 | 189, 8 | elrab2 3632 |
. . . . . . 7
β’ ((π€ gcd π) β π β ((π€ gcd π) β β β§ (π€ gcd π) β₯ π)) |
191 | 185, 188,
190 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ π€ β π) β (π€ gcd π) β π) |
192 | 177, 191 | opelxpd 5638 |
. . . . 5
β’ ((π β§ π€ β π) β β¨(π€ gcd π), (π€ gcd π)β© β (π Γ π)) |
193 | 192 | fvresd 6824 |
. . . . . 6
β’ ((π β§ π€ β π) β (( Β· βΎ (π Γ π))ββ¨(π€ gcd π), (π€ gcd π)β©) = ( Β· ββ¨(π€ gcd π), (π€ gcd π)β©)) |
194 | 89 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π€ β π) β (π gcd π) = 1) |
195 | | rpmulgcd2 16410 |
. . . . . . . 8
β’ (((π€ β β€ β§ π β β€ β§ π β β€) β§ (π gcd π) = 1) β (π€ gcd (π Β· π)) = ((π€ gcd π) Β· (π€ gcd π))) |
196 | 163, 165,
179, 194, 195 | syl31anc 1373 |
. . . . . . 7
β’ ((π β§ π€ β π) β (π€ gcd (π Β· π)) = ((π€ gcd π) Β· (π€ gcd π))) |
197 | | df-ov 7310 |
. . . . . . 7
β’ ((π€ gcd π) Β· (π€ gcd π)) = ( Β· ββ¨(π€ gcd π), (π€ gcd π)β©) |
198 | 196, 197 | eqtrdi 2792 |
. . . . . 6
β’ ((π β§ π€ β π) β (π€ gcd (π Β· π)) = ( Β· ββ¨(π€ gcd π), (π€ gcd π)β©)) |
199 | 160 | simprbi 498 |
. . . . . . . 8
β’ (π€ β π β π€ β₯ (π Β· π)) |
200 | 199 | adantl 483 |
. . . . . . 7
β’ ((π β§ π€ β π) β π€ β₯ (π Β· π)) |
201 | 38, 32 | nnmulcld 12076 |
. . . . . . . 8
β’ (π β (π Β· π) β β) |
202 | | gcdeq 16312 |
. . . . . . . 8
β’ ((π€ β β β§ (π Β· π) β β) β ((π€ gcd (π Β· π)) = π€ β π€ β₯ (π Β· π))) |
203 | 161, 201,
202 | syl2anr 598 |
. . . . . . 7
β’ ((π β§ π€ β π) β ((π€ gcd (π Β· π)) = π€ β π€ β₯ (π Β· π))) |
204 | 200, 203 | mpbird 257 |
. . . . . 6
β’ ((π β§ π€ β π) β (π€ gcd (π Β· π)) = π€) |
205 | 193, 198,
204 | 3eqtr2rd 2783 |
. . . . 5
β’ ((π β§ π€ β π) β π€ = (( Β· βΎ (π Γ π))ββ¨(π€ gcd π), (π€ gcd π)β©)) |
206 | | fveq2 6804 |
. . . . . 6
β’ (π’ = β¨(π€ gcd π), (π€ gcd π)β© β (( Β· βΎ (π Γ π))βπ’) = (( Β· βΎ (π Γ π))ββ¨(π€ gcd π), (π€ gcd π)β©)) |
207 | 206 | rspceeqv 3580 |
. . . . 5
β’
((β¨(π€ gcd π), (π€ gcd π)β© β (π Γ π) β§ π€ = (( Β· βΎ (π Γ π))ββ¨(π€ gcd π), (π€ gcd π)β©)) β βπ’ β (π Γ π)π€ = (( Β· βΎ (π Γ π))βπ’)) |
208 | 192, 205,
207 | syl2anc 585 |
. . . 4
β’ ((π β§ π€ β π) β βπ’ β (π Γ π)π€ = (( Β· βΎ (π Γ π))βπ’)) |
209 | 208 | ralrimiva 3140 |
. . 3
β’ (π β βπ€ β π βπ’ β (π Γ π)π€ = (( Β· βΎ (π Γ π))βπ’)) |
210 | | dffo3 7010 |
. . 3
β’ ((
Β· βΎ (π Γ
π)):(π Γ π)βontoβπ β (( Β· βΎ (π Γ π)):(π Γ π)βΆπ β§ βπ€ β π βπ’ β (π Γ π)π€ = (( Β· βΎ (π Γ π))βπ’))) |
211 | 57, 209, 210 | sylanbrc 584 |
. 2
β’ (π β ( Β· βΎ (π Γ π)):(π Γ π)βontoβπ) |
212 | | df-f1o 6465 |
. 2
β’ ((
Β· βΎ (π Γ
π)):(π Γ π)β1-1-ontoβπ β (( Β· βΎ
(π Γ π)):(π Γ π)β1-1βπ β§ ( Β· βΎ (π Γ π)):(π Γ π)βontoβπ)) |
213 | 158, 211,
212 | sylanbrc 584 |
1
β’ (π β ( Β· βΎ (π Γ π)):(π Γ π)β1-1-ontoβπ) |