Step | Hyp | Ref
| Expression |
1 | | nnz 12525 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
2 | | gcddvds 16388 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โค) โ ((๐ง gcd ๐) โฅ ๐ง โง (๐ง gcd ๐) โฅ ๐)) |
3 | 2 | simpld 496 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โค) โ (๐ง gcd ๐) โฅ ๐ง) |
4 | 1, 3 | sylan2 594 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โฅ ๐ง) |
5 | | gcdcl 16391 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โค) โ (๐ง gcd ๐) โ
โ0) |
6 | 1, 5 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ
โ0) |
7 | 6 | nn0zd 12530 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ โค) |
8 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ง โ
โค) |
9 | 1 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ โ
โค) |
10 | | nnne0 12192 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ 0) |
11 | 10 | neneqd 2945 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ยฌ
๐ = 0) |
12 | 11 | intnand 490 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ยฌ
(๐ง = 0 โง ๐ = 0)) |
13 | 12 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ) โ ยฌ
(๐ง = 0 โง ๐ = 0)) |
14 | | gcdn0cl 16387 |
. . . . . . . . . . . 12
โข (((๐ง โ โค โง ๐ โ โค) โง ยฌ
(๐ง = 0 โง ๐ = 0)) โ (๐ง gcd ๐) โ โ) |
15 | 8, 9, 13, 14 | syl21anc 837 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ โ) |
16 | | nnne0 12192 |
. . . . . . . . . . 11
โข ((๐ง gcd ๐) โ โ โ (๐ง gcd ๐) โ 0) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ 0) |
18 | | dvdsval2 16144 |
. . . . . . . . . 10
โข (((๐ง gcd ๐) โ โค โง (๐ง gcd ๐) โ 0 โง ๐ง โ โค) โ ((๐ง gcd ๐) โฅ ๐ง โ (๐ง / (๐ง gcd ๐)) โ โค)) |
19 | 7, 17, 8, 18 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) โฅ ๐ง โ (๐ง / (๐ง gcd ๐)) โ โค)) |
20 | 4, 19 | mpbid 231 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง / (๐ง gcd ๐)) โ โค) |
21 | 20 | 3adant3 1133 |
. . . . . . 7
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (๐ง / (๐ง gcd ๐)) โ โค) |
22 | 2 | simprd 497 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โค) โ (๐ง gcd ๐) โฅ ๐) |
23 | 1, 22 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โฅ ๐) |
24 | | dvdsval2 16144 |
. . . . . . . . . . . 12
โข (((๐ง gcd ๐) โ โค โง (๐ง gcd ๐) โ 0 โง ๐ โ โค) โ ((๐ง gcd ๐) โฅ ๐ โ (๐ / (๐ง gcd ๐)) โ โค)) |
25 | 7, 17, 9, 24 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) โฅ ๐ โ (๐ / (๐ง gcd ๐)) โ โค)) |
26 | 23, 25 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ / (๐ง gcd ๐)) โ โค) |
27 | | nnre 12165 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
28 | 27 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ โ
โ) |
29 | 6 | nn0red 12479 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ โ) |
30 | | nngt0 12189 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 <
๐) |
31 | 30 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ 0 <
๐) |
32 | | nngt0 12189 |
. . . . . . . . . . . 12
โข ((๐ง gcd ๐) โ โ โ 0 < (๐ง gcd ๐)) |
33 | 15, 32 | syl 17 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ 0 <
(๐ง gcd ๐)) |
34 | 28, 29, 31, 33 | divgt0d 12095 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ 0 <
(๐ / (๐ง gcd ๐))) |
35 | 26, 34 | jca 513 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ / (๐ง gcd ๐)) โ โค โง 0 < (๐ / (๐ง gcd ๐)))) |
36 | 35 | 3adant3 1133 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ ((๐ / (๐ง gcd ๐)) โ โค โง 0 < (๐ / (๐ง gcd ๐)))) |
37 | | elnnz 12514 |
. . . . . . . 8
โข ((๐ / (๐ง gcd ๐)) โ โ โ ((๐ / (๐ง gcd ๐)) โ โค โง 0 < (๐ / (๐ง gcd ๐)))) |
38 | 36, 37 | sylibr 233 |
. . . . . . 7
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (๐ / (๐ง gcd ๐)) โ โ) |
39 | 21, 38 | opelxpd 5672 |
. . . . . 6
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (โค ร
โ)) |
40 | 20, 26 | gcdcld 16393 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) โ
โ0) |
41 | 40 | nn0cnd 12480 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) โ โ) |
42 | | 1cnd 11155 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ) โ 1 โ
โ) |
43 | 6 | nn0cnd 12480 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ โ) |
44 | 43 | mulid1d 11177 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) ยท 1) = (๐ง gcd ๐)) |
45 | | zcn 12509 |
. . . . . . . . . . . 12
โข (๐ง โ โค โ ๐ง โ
โ) |
46 | 45 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ง โ
โ) |
47 | 46, 43, 17 | divcan2d 11938 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) ยท (๐ง / (๐ง gcd ๐))) = ๐ง) |
48 | | nncn 12166 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
49 | 48 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ โ
โ) |
50 | 49, 43, 17 | divcan2d 11938 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) ยท (๐ / (๐ง gcd ๐))) = ๐) |
51 | 47, 50 | oveq12d 7376 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ (((๐ง gcd ๐) ยท (๐ง / (๐ง gcd ๐))) gcd ((๐ง gcd ๐) ยท (๐ / (๐ง gcd ๐)))) = (๐ง gcd ๐)) |
52 | | mulgcd 16434 |
. . . . . . . . . 10
โข (((๐ง gcd ๐) โ โ0 โง (๐ง / (๐ง gcd ๐)) โ โค โง (๐ / (๐ง gcd ๐)) โ โค) โ (((๐ง gcd ๐) ยท (๐ง / (๐ง gcd ๐))) gcd ((๐ง gcd ๐) ยท (๐ / (๐ง gcd ๐)))) = ((๐ง gcd ๐) ยท ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))))) |
53 | 6, 20, 26, 52 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ (((๐ง gcd ๐) ยท (๐ง / (๐ง gcd ๐))) gcd ((๐ง gcd ๐) ยท (๐ / (๐ง gcd ๐)))) = ((๐ง gcd ๐) ยท ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))))) |
54 | 44, 51, 53 | 3eqtr2rd 2780 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) ยท ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐)))) = ((๐ง gcd ๐) ยท 1)) |
55 | 41, 42, 43, 17, 54 | mulcanad 11795 |
. . . . . . 7
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1) |
56 | 55 | 3adant3 1133 |
. . . . . 6
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1) |
57 | 10 | adantl 483 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ โ 0) |
58 | 46, 49, 43, 57, 17 | divcan7d 11964 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐))) = (๐ง / ๐)) |
59 | 58 | eqeq2d 2744 |
. . . . . . 7
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐))) โ ๐ด = (๐ง / ๐))) |
60 | 59 | biimp3ar 1471 |
. . . . . 6
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ ๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐)))) |
61 | | ovex 7391 |
. . . . . . . . . . 11
โข (๐ง / (๐ง gcd ๐)) โ V |
62 | | ovex 7391 |
. . . . . . . . . . 11
โข (๐ / (๐ง gcd ๐)) โ V |
63 | 61, 62 | op1std 7932 |
. . . . . . . . . 10
โข (๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (1st โ๐ฅ) = (๐ง / (๐ง gcd ๐))) |
64 | 61, 62 | op2ndd 7933 |
. . . . . . . . . 10
โข (๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (2nd โ๐ฅ) = (๐ / (๐ง gcd ๐))) |
65 | 63, 64 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ ((1st โ๐ฅ) gcd (2nd
โ๐ฅ)) = ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐)))) |
66 | 65 | eqeq1d 2735 |
. . . . . . . 8
โข (๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1)) |
67 | 63, 64 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ ((1st โ๐ฅ) / (2nd โ๐ฅ)) = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐)))) |
68 | 67 | eqeq2d 2744 |
. . . . . . . 8
โข (๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)) โ ๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐))))) |
69 | 66, 68 | anbi12d 632 |
. . . . . . 7
โข (๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โ (((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1 โง ๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐)))))) |
70 | 69 | rspcev 3580 |
. . . . . 6
โข
((โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (โค ร โ)
โง (((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1 โง ๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐))))) โ โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)))) |
71 | 39, 56, 60, 70 | syl12anc 836 |
. . . . 5
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)))) |
72 | | elxp6 7956 |
. . . . . . 7
โข (๐ฅ โ (โค ร
โ) โ (๐ฅ =
โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ โง ((1st โ๐ฅ) โ โค โง
(2nd โ๐ฅ)
โ โ))) |
73 | | elxp6 7956 |
. . . . . . 7
โข (๐ฆ โ (โค ร
โ) โ (๐ฆ =
โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st โ๐ฆ) โ โค โง
(2nd โ๐ฆ)
โ โ))) |
74 | | simprl 770 |
. . . . . . . . . . . 12
โข ((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โ (1st
โ๐ฅ) โ
โค) |
75 | 74 | ad2antrr 725 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ (1st
โ๐ฅ) โ
โค) |
76 | | simprr 772 |
. . . . . . . . . . . 12
โข ((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โ (2nd
โ๐ฅ) โ
โ) |
77 | 76 | ad2antrr 725 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ (2nd
โ๐ฅ) โ
โ) |
78 | | simprll 778 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1) |
79 | | simprl 770 |
. . . . . . . . . . . 12
โข ((๐ฆ = โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ โง
((1st โ๐ฆ)
โ โค โง (2nd โ๐ฆ) โ โ)) โ (1st
โ๐ฆ) โ
โค) |
80 | 79 | ad2antlr 726 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ (1st
โ๐ฆ) โ
โค) |
81 | | simprr 772 |
. . . . . . . . . . . 12
โข ((๐ฆ = โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ โง
((1st โ๐ฆ)
โ โค โง (2nd โ๐ฆ) โ โ)) โ (2nd
โ๐ฆ) โ
โ) |
82 | 81 | ad2antlr 726 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ (2nd
โ๐ฆ) โ
โ) |
83 | | simprrl 780 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1) |
84 | | simprlr 779 |
. . . . . . . . . . . 12
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) |
85 | | simprrr 781 |
. . . . . . . . . . . 12
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))) |
86 | 84, 85 | eqtr3d 2775 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ((1st
โ๐ฅ) / (2nd
โ๐ฅ)) =
((1st โ๐ฆ)
/ (2nd โ๐ฆ))) |
87 | | qredeq 16538 |
. . . . . . . . . . 11
โข
((((1st โ๐ฅ) โ โค โง (2nd
โ๐ฅ) โ โ
โง ((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1) โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ โง ((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1) โง ((1st โ๐ฅ) / (2nd โ๐ฅ)) = ((1st โ๐ฆ) / (2nd โ๐ฆ))) โ ((1st
โ๐ฅ) = (1st
โ๐ฆ) โง
(2nd โ๐ฅ) =
(2nd โ๐ฆ))) |
88 | 75, 77, 78, 80, 82, 83, 86, 87 | syl331anc 1396 |
. . . . . . . . . 10
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ((1st
โ๐ฅ) = (1st
โ๐ฆ) โง
(2nd โ๐ฅ) =
(2nd โ๐ฆ))) |
89 | | fvex 6856 |
. . . . . . . . . . 11
โข
(1st โ๐ฅ) โ V |
90 | | fvex 6856 |
. . . . . . . . . . 11
โข
(2nd โ๐ฅ) โ V |
91 | 89, 90 | opth 5434 |
. . . . . . . . . 10
โข
(โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โ ((1st
โ๐ฅ) = (1st
โ๐ฆ) โง
(2nd โ๐ฅ) =
(2nd โ๐ฆ))) |
92 | 88, 91 | sylibr 233 |
. . . . . . . . 9
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ
โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ) |
93 | | simplll 774 |
. . . . . . . . 9
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ฅ = โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ) |
94 | | simplrl 776 |
. . . . . . . . 9
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ) |
95 | 92, 93, 94 | 3eqtr4d 2783 |
. . . . . . . 8
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ฅ = ๐ฆ) |
96 | 95 | ex 414 |
. . . . . . 7
โข (((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โ
(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ)) |
97 | 72, 73, 96 | syl2anb 599 |
. . . . . 6
โข ((๐ฅ โ (โค ร
โ) โง ๐ฆ โ
(โค ร โ)) โ (((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ)) |
98 | 97 | rgen2 3191 |
. . . . 5
โข
โ๐ฅ โ
(โค ร โ)โ๐ฆ โ (โค ร
โ)(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ) |
99 | 71, 98 | jctir 522 |
. . . 4
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง โ๐ฅ โ (โค ร
โ)โ๐ฆ โ
(โค ร โ)(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ))) |
100 | 99 | 3expia 1122 |
. . 3
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ด = (๐ง / ๐) โ (โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง โ๐ฅ โ (โค ร
โ)โ๐ฆ โ
(โค ร โ)(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ)))) |
101 | 100 | rexlimivv 3193 |
. 2
โข
(โ๐ง โ
โค โ๐ โ
โ ๐ด = (๐ง / ๐) โ (โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง โ๐ฅ โ (โค ร
โ)โ๐ฆ โ
(โค ร โ)(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ))) |
102 | | elq 12880 |
. 2
โข (๐ด โ โ โ
โ๐ง โ โค
โ๐ โ โ
๐ด = (๐ง / ๐)) |
103 | | fveq2 6843 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (1st โ๐ฅ) = (1st โ๐ฆ)) |
104 | | fveq2 6843 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (2nd โ๐ฅ) = (2nd โ๐ฆ)) |
105 | 103, 104 | oveq12d 7376 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((1st โ๐ฅ) gcd (2nd
โ๐ฅ)) =
((1st โ๐ฆ)
gcd (2nd โ๐ฆ))) |
106 | 105 | eqeq1d 2735 |
. . . 4
โข (๐ฅ = ๐ฆ โ (((1st โ๐ฅ) gcd (2nd
โ๐ฅ)) = 1 โ
((1st โ๐ฆ)
gcd (2nd โ๐ฆ)) = 1)) |
107 | 103, 104 | oveq12d 7376 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((1st โ๐ฅ) / (2nd โ๐ฅ)) = ((1st
โ๐ฆ) / (2nd
โ๐ฆ))) |
108 | 107 | eqeq2d 2744 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)) โ ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ)))) |
109 | 106, 108 | anbi12d 632 |
. . 3
โข (๐ฅ = ๐ฆ โ ((((1st โ๐ฅ) gcd (2nd
โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โ (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ))))) |
110 | 109 | reu4 3690 |
. 2
โข
(โ!๐ฅ โ
(โค ร โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โ (โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง โ๐ฅ โ (โค ร
โ)โ๐ฆ โ
(โค ร โ)(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ))) |
111 | 101, 102,
110 | 3imtr4i 292 |
1
โข (๐ด โ โ โ
โ!๐ฅ โ (โค
ร โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)))) |