Step | Hyp | Ref
| Expression |
1 | | nnz 9271 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
2 | | gcddvds 11963 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โค) โ ((๐ง gcd ๐) โฅ ๐ง โง (๐ง gcd ๐) โฅ ๐)) |
3 | 2 | simpld 112 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โค) โ (๐ง gcd ๐) โฅ ๐ง) |
4 | 1, 3 | sylan2 286 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โฅ ๐ง) |
5 | | gcdcl 11966 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โค) โ (๐ง gcd ๐) โ
โ0) |
6 | 1, 5 | sylan2 286 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ
โ0) |
7 | 6 | nn0zd 9372 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ โค) |
8 | | simpl 109 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ง โ
โค) |
9 | 1 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ โ
โค) |
10 | | nnne0 8946 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ 0) |
11 | 10 | neneqd 2368 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ยฌ
๐ = 0) |
12 | 11 | intnand 931 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ยฌ
(๐ง = 0 โง ๐ = 0)) |
13 | 12 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ) โ ยฌ
(๐ง = 0 โง ๐ = 0)) |
14 | | gcdn0cl 11962 |
. . . . . . . . . . . 12
โข (((๐ง โ โค โง ๐ โ โค) โง ยฌ
(๐ง = 0 โง ๐ = 0)) โ (๐ง gcd ๐) โ โ) |
15 | 8, 9, 13, 14 | syl21anc 1237 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ โ) |
16 | 15 | nnne0d 8963 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ 0) |
17 | | dvdsval2 11796 |
. . . . . . . . . 10
โข (((๐ง gcd ๐) โ โค โง (๐ง gcd ๐) โ 0 โง ๐ง โ โค) โ ((๐ง gcd ๐) โฅ ๐ง โ (๐ง / (๐ง gcd ๐)) โ โค)) |
18 | 7, 16, 8, 17 | syl3anc 1238 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) โฅ ๐ง โ (๐ง / (๐ง gcd ๐)) โ โค)) |
19 | 4, 18 | mpbid 147 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง / (๐ง gcd ๐)) โ โค) |
20 | 19 | 3adant3 1017 |
. . . . . . 7
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (๐ง / (๐ง gcd ๐)) โ โค) |
21 | 2 | simprd 114 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โค) โ (๐ง gcd ๐) โฅ ๐) |
22 | 1, 21 | sylan2 286 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โฅ ๐) |
23 | | dvdsval2 11796 |
. . . . . . . . . . . 12
โข (((๐ง gcd ๐) โ โค โง (๐ง gcd ๐) โ 0 โง ๐ โ โค) โ ((๐ง gcd ๐) โฅ ๐ โ (๐ / (๐ง gcd ๐)) โ โค)) |
24 | 7, 16, 9, 23 | syl3anc 1238 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) โฅ ๐ โ (๐ / (๐ง gcd ๐)) โ โค)) |
25 | 22, 24 | mpbid 147 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ / (๐ง gcd ๐)) โ โค) |
26 | | nnre 8925 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
27 | 26 | adantl 277 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ โ
โ) |
28 | 6 | nn0red 9229 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ โ) |
29 | | nngt0 8943 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 <
๐) |
30 | 29 | adantl 277 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ 0 <
๐) |
31 | 15 | nngt0d 8962 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ 0 <
(๐ง gcd ๐)) |
32 | 27, 28, 30, 31 | divgt0d 8891 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ 0 <
(๐ / (๐ง gcd ๐))) |
33 | 25, 32 | jca 306 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ / (๐ง gcd ๐)) โ โค โง 0 < (๐ / (๐ง gcd ๐)))) |
34 | 33 | 3adant3 1017 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ ((๐ / (๐ง gcd ๐)) โ โค โง 0 < (๐ / (๐ง gcd ๐)))) |
35 | | elnnz 9262 |
. . . . . . . 8
โข ((๐ / (๐ง gcd ๐)) โ โ โ ((๐ / (๐ง gcd ๐)) โ โค โง 0 < (๐ / (๐ง gcd ๐)))) |
36 | 34, 35 | sylibr 134 |
. . . . . . 7
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (๐ / (๐ง gcd ๐)) โ โ) |
37 | | opelxpi 4658 |
. . . . . . 7
โข (((๐ง / (๐ง gcd ๐)) โ โค โง (๐ / (๐ง gcd ๐)) โ โ) โ โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (โค ร
โ)) |
38 | 20, 36, 37 | syl2anc 411 |
. . . . . 6
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (โค ร
โ)) |
39 | | fveq2 5515 |
. . . . . . . . . 10
โข (๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (1st โ๐ฅ) = (1st
โโจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ)) |
40 | | simp1 997 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ ๐ง โ โค) |
41 | 15 | 3adant3 1017 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (๐ง gcd ๐) โ โ) |
42 | | znq 9623 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง (๐ง gcd ๐) โ โ) โ (๐ง / (๐ง gcd ๐)) โ โ) |
43 | 40, 41, 42 | syl2anc 411 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (๐ง / (๐ง gcd ๐)) โ โ) |
44 | 9 | 3adant3 1017 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ ๐ โ โค) |
45 | | znq 9623 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง (๐ง gcd ๐) โ โ) โ (๐ / (๐ง gcd ๐)) โ โ) |
46 | 44, 41, 45 | syl2anc 411 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (๐ / (๐ง gcd ๐)) โ โ) |
47 | | op1stg 6150 |
. . . . . . . . . . 11
โข (((๐ง / (๐ง gcd ๐)) โ โ โง (๐ / (๐ง gcd ๐)) โ โ) โ (1st
โโจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) = (๐ง / (๐ง gcd ๐))) |
48 | 43, 46, 47 | syl2anc 411 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (1st โโจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) = (๐ง / (๐ง gcd ๐))) |
49 | 39, 48 | sylan9eqr 2232 |
. . . . . . . . 9
โข (((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โง ๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) โ (1st โ๐ฅ) = (๐ง / (๐ง gcd ๐))) |
50 | | fveq2 5515 |
. . . . . . . . . 10
โข (๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ โ (2nd โ๐ฅ) = (2nd
โโจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ)) |
51 | | op2ndg 6151 |
. . . . . . . . . . 11
โข (((๐ง / (๐ง gcd ๐)) โ โ โง (๐ / (๐ง gcd ๐)) โ โ) โ (2nd
โโจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) = (๐ / (๐ง gcd ๐))) |
52 | 43, 46, 51 | syl2anc 411 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (2nd โโจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) = (๐ / (๐ง gcd ๐))) |
53 | 50, 52 | sylan9eqr 2232 |
. . . . . . . . 9
โข (((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โง ๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) โ (2nd โ๐ฅ) = (๐ / (๐ง gcd ๐))) |
54 | 49, 53 | oveq12d 5892 |
. . . . . . . 8
โข (((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โง ๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) โ ((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐)))) |
55 | 54 | eqeq1d 2186 |
. . . . . . 7
โข (((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โง ๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) โ (((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1)) |
56 | 49, 53 | oveq12d 5892 |
. . . . . . . 8
โข (((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โง ๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) โ ((1st
โ๐ฅ) / (2nd
โ๐ฅ)) = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐)))) |
57 | 56 | eqeq2d 2189 |
. . . . . . 7
โข (((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โง ๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) โ (๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)) โ ๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐))))) |
58 | 55, 57 | anbi12d 473 |
. . . . . 6
โข (((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โง ๐ฅ = โจ(๐ง / (๐ง gcd ๐)), (๐ / (๐ง gcd ๐))โฉ) โ ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โ (((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1 โง ๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐)))))) |
59 | 19, 25 | gcdcld 11968 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) โ
โ0) |
60 | 59 | nn0cnd 9230 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) โ โ) |
61 | | 1cnd 7972 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ 1 โ
โ) |
62 | 6 | nn0cnd 9230 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) โ โ) |
63 | 15 | nnap0d 8964 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ง gcd ๐) # 0) |
64 | 62 | mulridd 7973 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) ยท 1) = (๐ง gcd ๐)) |
65 | | zcn 9257 |
. . . . . . . . . . . . 13
โข (๐ง โ โค โ ๐ง โ
โ) |
66 | 65 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ง โ
โ) |
67 | 66, 62, 63 | divcanap2d 8748 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) ยท (๐ง / (๐ง gcd ๐))) = ๐ง) |
68 | | nncn 8926 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
69 | 68 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ โ
โ) |
70 | 69, 62, 63 | divcanap2d 8748 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) ยท (๐ / (๐ง gcd ๐))) = ๐) |
71 | 67, 70 | oveq12d 5892 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ (((๐ง gcd ๐) ยท (๐ง / (๐ง gcd ๐))) gcd ((๐ง gcd ๐) ยท (๐ / (๐ง gcd ๐)))) = (๐ง gcd ๐)) |
72 | | mulgcd 12016 |
. . . . . . . . . . 11
โข (((๐ง gcd ๐) โ โ0 โง (๐ง / (๐ง gcd ๐)) โ โค โง (๐ / (๐ง gcd ๐)) โ โค) โ (((๐ง gcd ๐) ยท (๐ง / (๐ง gcd ๐))) gcd ((๐ง gcd ๐) ยท (๐ / (๐ง gcd ๐)))) = ((๐ง gcd ๐) ยท ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))))) |
73 | 6, 19, 25, 72 | syl3anc 1238 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ (((๐ง gcd ๐) ยท (๐ง / (๐ง gcd ๐))) gcd ((๐ง gcd ๐) ยท (๐ / (๐ง gcd ๐)))) = ((๐ง gcd ๐) ยท ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))))) |
74 | 64, 71, 73 | 3eqtr2rd 2217 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง gcd ๐) ยท ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐)))) = ((๐ง gcd ๐) ยท 1)) |
75 | 60, 61, 62, 63, 74 | mulcanapad 8619 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1) |
76 | 75 | 3adant3 1017 |
. . . . . . 7
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ ((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1) |
77 | | nnap0 8947 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ # 0) |
78 | 77 | adantl 277 |
. . . . . . . . . 10
โข ((๐ง โ โค โง ๐ โ โ) โ ๐ # 0) |
79 | 66, 69, 62, 78, 63 | divcanap7d 8775 |
. . . . . . . . 9
โข ((๐ง โ โค โง ๐ โ โ) โ ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐))) = (๐ง / ๐)) |
80 | 79 | eqeq2d 2189 |
. . . . . . . 8
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐))) โ ๐ด = (๐ง / ๐))) |
81 | 80 | biimp3ar 1346 |
. . . . . . 7
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ ๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐)))) |
82 | 76, 81 | jca 306 |
. . . . . 6
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (((๐ง / (๐ง gcd ๐)) gcd (๐ / (๐ง gcd ๐))) = 1 โง ๐ด = ((๐ง / (๐ง gcd ๐)) / (๐ / (๐ง gcd ๐))))) |
83 | 38, 58, 82 | rspcedvd 2847 |
. . . . 5
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)))) |
84 | | elxp6 6169 |
. . . . . . 7
โข (๐ฅ โ (โค ร
โ) โ (๐ฅ =
โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ โง ((1st โ๐ฅ) โ โค โง
(2nd โ๐ฅ)
โ โ))) |
85 | | elxp6 6169 |
. . . . . . 7
โข (๐ฆ โ (โค ร
โ) โ (๐ฆ =
โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st โ๐ฆ) โ โค โง
(2nd โ๐ฆ)
โ โ))) |
86 | | simprl 529 |
. . . . . . . . . . . 12
โข ((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โ (1st
โ๐ฅ) โ
โค) |
87 | 86 | ad2antrr 488 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ (1st
โ๐ฅ) โ
โค) |
88 | | simprr 531 |
. . . . . . . . . . . 12
โข ((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โ (2nd
โ๐ฅ) โ
โ) |
89 | 88 | ad2antrr 488 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ (2nd
โ๐ฅ) โ
โ) |
90 | | simprll 537 |
. . . . . . . . . . 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) |
91 | | simprl 529 |
. . . . . . . . . . . 12
โข ((๐ฆ = โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ โง
((1st โ๐ฆ)
โ โค โง (2nd โ๐ฆ) โ โ)) โ (1st
โ๐ฆ) โ
โค) |
92 | 91 | ad2antlr 489 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ (1st
โ๐ฆ) โ
โค) |
93 | | simprr 531 |
. . . . . . . . . . . 12
โข ((๐ฆ = โจ(1st
โ๐ฆ), (2nd
โ๐ฆ)โฉ โง
((1st โ๐ฆ)
โ โค โง (2nd โ๐ฆ) โ โ)) โ (2nd
โ๐ฆ) โ
โ) |
94 | 93 | ad2antlr 489 |
. . . . . . . . . . 11
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ (2nd
โ๐ฆ) โ
โ) |
95 | | simprrl 539 |
. . . . . . . . . . 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) |
96 | | simprlr 538 |
. . . . . . . . . . . 12
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) |
97 | | simprrr 540 |
. . . . . . . . . . . 12
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))) |
98 | 96, 97 | eqtr3d 2212 |
. . . . . . . . . . 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 โ๐ฆ))) |
99 | | qredeq 12095 |
. . . . . . . . . . 11
โข
((((1st โ๐ฅ) โ โค โง (2nd
โ๐ฅ) โ โ
โง ((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1) โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ โง ((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1) โง ((1st โ๐ฅ) / (2nd โ๐ฅ)) = ((1st โ๐ฆ) / (2nd โ๐ฆ))) โ ((1st
โ๐ฅ) = (1st
โ๐ฆ) โง
(2nd โ๐ฅ) =
(2nd โ๐ฆ))) |
100 | 87, 89, 90, 92, 94, 95, 98, 99 | syl331anc 1263 |
. . . . . . . . . 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 โ๐ฆ))) |
101 | | vex 2740 |
. . . . . . . . . . . 12
โข ๐ฅ โ V |
102 | | 1stexg 6167 |
. . . . . . . . . . . 12
โข (๐ฅ โ V โ (1st
โ๐ฅ) โ
V) |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . 11
โข
(1st โ๐ฅ) โ V |
104 | | 2ndexg 6168 |
. . . . . . . . . . . 12
โข (๐ฅ โ V โ (2nd
โ๐ฅ) โ
V) |
105 | 101, 104 | ax-mp 5 |
. . . . . . . . . . 11
โข
(2nd โ๐ฅ) โ V |
106 | 103, 105 | opth 4237 |
. . . . . . . . . 10
โข
(โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โ ((1st
โ๐ฅ) = (1st
โ๐ฆ) โง
(2nd โ๐ฅ) =
(2nd โ๐ฆ))) |
107 | 100, 106 | sylibr 134 |
. . . . . . . . 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 โ๐ฆ)โฉ) |
108 | | simplll 533 |
. . . . . . . . 9
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ฅ = โจ(1st โ๐ฅ), (2nd โ๐ฅ)โฉ) |
109 | | simplrl 535 |
. . . . . . . . 9
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ) |
110 | 107, 108,
109 | 3eqtr4d 2220 |
. . . . . . . 8
โข ((((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โง ((((1st
โ๐ฅ) gcd
(2nd โ๐ฅ))
= 1 โง ๐ด =
((1st โ๐ฅ)
/ (2nd โ๐ฅ))) โง (((1st โ๐ฆ) gcd (2nd
โ๐ฆ)) = 1 โง ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ))))) โ ๐ฅ = ๐ฆ) |
111 | 110 | ex 115 |
. . . . . . 7
โข (((๐ฅ = โจ(1st
โ๐ฅ), (2nd
โ๐ฅ)โฉ โง
((1st โ๐ฅ)
โ โค โง (2nd โ๐ฅ) โ โ)) โง (๐ฆ = โจ(1st โ๐ฆ), (2nd โ๐ฆ)โฉ โง ((1st
โ๐ฆ) โ โค
โง (2nd โ๐ฆ) โ โ))) โ
(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ)) |
112 | 84, 85, 111 | syl2anb 291 |
. . . . . 6
โข ((๐ฅ โ (โค ร
โ) โง ๐ฆ โ
(โค ร โ)) โ (((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ)) |
113 | 112 | rgen2a 2531 |
. . . . 5
โข
โ๐ฅ โ
(โค ร โ)โ๐ฆ โ (โค ร
โ)(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ) |
114 | 83, 113 | jctir 313 |
. . . 4
โข ((๐ง โ โค โง ๐ โ โ โง ๐ด = (๐ง / ๐)) โ (โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง โ๐ฅ โ (โค ร
โ)โ๐ฆ โ
(โค ร โ)(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ))) |
115 | 114 | 3expia 1205 |
. . 3
โข ((๐ง โ โค โง ๐ โ โ) โ (๐ด = (๐ง / ๐) โ (โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง โ๐ฅ โ (โค ร
โ)โ๐ฆ โ
(โค ร โ)(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ)))) |
116 | 115 | rexlimivv 2600 |
. 2
โข
(โ๐ง โ
โค โ๐ โ
โ ๐ด = (๐ง / ๐) โ (โ๐ฅ โ (โค ร
โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง โ๐ฅ โ (โค ร
โ)โ๐ฆ โ
(โค ร โ)(((((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โง (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ)))) โ ๐ฅ = ๐ฆ))) |
117 | | elq 9621 |
. 2
โข (๐ด โ โ โ
โ๐ง โ โค
โ๐ โ โ
๐ด = (๐ง / ๐)) |
118 | | fveq2 5515 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (1st โ๐ฅ) = (1st โ๐ฆ)) |
119 | | fveq2 5515 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (2nd โ๐ฅ) = (2nd โ๐ฆ)) |
120 | 118, 119 | oveq12d 5892 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((1st โ๐ฅ) gcd (2nd
โ๐ฅ)) =
((1st โ๐ฆ)
gcd (2nd โ๐ฆ))) |
121 | 120 | eqeq1d 2186 |
. . . 4
โข (๐ฅ = ๐ฆ โ (((1st โ๐ฅ) gcd (2nd
โ๐ฅ)) = 1 โ
((1st โ๐ฆ)
gcd (2nd โ๐ฆ)) = 1)) |
122 | 118, 119 | oveq12d 5892 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((1st โ๐ฅ) / (2nd โ๐ฅ)) = ((1st
โ๐ฆ) / (2nd
โ๐ฆ))) |
123 | 122 | eqeq2d 2189 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)) โ ๐ด = ((1st โ๐ฆ) / (2nd โ๐ฆ)))) |
124 | 121, 123 | anbi12d 473 |
. . 3
โข (๐ฅ = ๐ฆ โ ((((1st โ๐ฅ) gcd (2nd
โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ))) โ (((1st
โ๐ฆ) gcd
(2nd โ๐ฆ))
= 1 โง ๐ด =
((1st โ๐ฆ)
/ (2nd โ๐ฆ))))) |
125 | 124 | reu4 2931 |
. 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 โ๐ฆ)))) โ ๐ฅ = ๐ฆ))) |
126 | 116, 117,
125 | 3imtr4i 201 |
1
โข (๐ด โ โ โ
โ!๐ฅ โ (โค
ร โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)))) |