Step | Hyp | Ref
| Expression |
1 | | nnz 9271 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ
โค) |
2 | 1 | 3ad2ant3 1020 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ๐ถ โ
โค) |
3 | | simp1 997 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ๐ด โ
โค) |
4 | | divides 11795 |
. . . . . 6
โข ((๐ถ โ โค โง ๐ด โ โค) โ (๐ถ โฅ ๐ด โ โ๐ โ โค (๐ ยท ๐ถ) = ๐ด)) |
5 | 2, 3, 4 | syl2anc 411 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ถ โฅ ๐ด โ โ๐ โ โค (๐ ยท ๐ถ) = ๐ด)) |
6 | | simp2 998 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ๐ต โ
โค) |
7 | | divides 11795 |
. . . . . 6
โข ((๐ถ โ โค โง ๐ต โ โค) โ (๐ถ โฅ ๐ต โ โ๐ โ โค (๐ ยท ๐ถ) = ๐ต)) |
8 | 2, 6, 7 | syl2anc 411 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ถ โฅ ๐ต โ โ๐ โ โค (๐ ยท ๐ถ) = ๐ต)) |
9 | 5, 8 | anbi12d 473 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ((๐ถ โฅ ๐ด โง ๐ถ โฅ ๐ต) โ (โ๐ โ โค (๐ ยท ๐ถ) = ๐ด โง โ๐ โ โค (๐ ยท ๐ถ) = ๐ต))) |
10 | | reeanv 2646 |
. . . 4
โข
(โ๐ โ
โค โ๐ โ
โค ((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ (โ๐ โ โค (๐ ยท ๐ถ) = ๐ด โง โ๐ โ โค (๐ ยท ๐ถ) = ๐ต)) |
11 | 9, 10 | bitr4di 198 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ((๐ถ โฅ ๐ด โง ๐ถ โฅ ๐ต) โ โ๐ โ โค โ๐ โ โค ((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต))) |
12 | | gcdcl 11966 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ
โ0) |
13 | 12 | nn0cnd 9230 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ โ) |
14 | 13 | 3adant3 1017 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (๐ gcd ๐) โ โ) |
15 | | nncn 8926 |
. . . . . . . . . . 11
โข (๐ถ โ โ โ ๐ถ โ
โ) |
16 | 15 | 3ad2ant3 1020 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ๐ถ โ
โ) |
17 | | simp3 999 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ๐ถ โ
โ) |
18 | 17 | nnap0d 8964 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ๐ถ # 0) |
19 | 14, 16, 18 | divcanap4d 8752 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ gcd ๐) ยท ๐ถ) / ๐ถ) = (๐ gcd ๐)) |
20 | | nnnn0 9182 |
. . . . . . . . . . 11
โข (๐ถ โ โ โ ๐ถ โ
โ0) |
21 | | mulgcdr 12018 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ0)
โ ((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) = ((๐ gcd ๐) ยท ๐ถ)) |
22 | 20, 21 | syl3an3 1273 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) = ((๐ gcd ๐) ยท ๐ถ)) |
23 | 22 | oveq1d 5889 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) / ๐ถ) = (((๐ gcd ๐) ยท ๐ถ) / ๐ถ)) |
24 | | zcn 9257 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
25 | 24 | 3ad2ant1 1018 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ๐ โ
โ) |
26 | 25, 16, 18 | divcanap4d 8752 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ((๐ ยท ๐ถ) / ๐ถ) = ๐) |
27 | | zcn 9257 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
28 | 27 | 3ad2ant2 1019 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ๐ โ
โ) |
29 | 28, 16, 18 | divcanap4d 8752 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ((๐ ยท ๐ถ) / ๐ถ) = ๐) |
30 | 26, 29 | oveq12d 5892 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) / ๐ถ) gcd ((๐ ยท ๐ถ) / ๐ถ)) = (๐ gcd ๐)) |
31 | 19, 23, 30 | 3eqtr4d 2220 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) / ๐ถ) = (((๐ ยท ๐ถ) / ๐ถ) gcd ((๐ ยท ๐ถ) / ๐ถ))) |
32 | | oveq12 5883 |
. . . . . . . . . 10
โข (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) = (๐ด gcd ๐ต)) |
33 | 32 | oveq1d 5889 |
. . . . . . . . 9
โข (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ (((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) / ๐ถ) = ((๐ด gcd ๐ต) / ๐ถ)) |
34 | | oveq1 5881 |
. . . . . . . . . 10
โข ((๐ ยท ๐ถ) = ๐ด โ ((๐ ยท ๐ถ) / ๐ถ) = (๐ด / ๐ถ)) |
35 | | oveq1 5881 |
. . . . . . . . . 10
โข ((๐ ยท ๐ถ) = ๐ต โ ((๐ ยท ๐ถ) / ๐ถ) = (๐ต / ๐ถ)) |
36 | 34, 35 | oveqan12d 5893 |
. . . . . . . . 9
โข (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ (((๐ ยท ๐ถ) / ๐ถ) gcd ((๐ ยท ๐ถ) / ๐ถ)) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ))) |
37 | 33, 36 | eqeq12d 2192 |
. . . . . . . 8
โข (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) / ๐ถ) = (((๐ ยท ๐ถ) / ๐ถ) gcd ((๐ ยท ๐ถ) / ๐ถ)) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
38 | 31, 37 | syl5ibcom 155 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
39 | 38 | 3expa 1203 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
40 | 39 | expcom 116 |
. . . . 5
โข (๐ถ โ โ โ ((๐ โ โค โง ๐ โ โค) โ (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ))))) |
41 | 40 | rexlimdvv 2601 |
. . . 4
โข (๐ถ โ โ โ
(โ๐ โ โค
โ๐ โ โค
((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
42 | 41 | 3ad2ant3 1020 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ
(โ๐ โ โค
โ๐ โ โค
((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
43 | 11, 42 | sylbid 150 |
. 2
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ((๐ถ โฅ ๐ด โง ๐ถ โฅ ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
44 | 43 | imp 124 |
1
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง (๐ถ โฅ ๐ด โง ๐ถ โฅ ๐ต)) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ))) |