Step | Hyp | Ref
| Expression |
1 | | nnz 12583 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ
โค) |
2 | 1 | 3ad2ant3 1133 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ๐ถ โ
โค) |
3 | | simp1 1134 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ๐ด โ
โค) |
4 | | divides 16203 |
. . . . . 6
โข ((๐ถ โ โค โง ๐ด โ โค) โ (๐ถ โฅ ๐ด โ โ๐ โ โค (๐ ยท ๐ถ) = ๐ด)) |
5 | 2, 3, 4 | syl2anc 582 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ถ โฅ ๐ด โ โ๐ โ โค (๐ ยท ๐ถ) = ๐ด)) |
6 | | simp2 1135 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ๐ต โ
โค) |
7 | | divides 16203 |
. . . . . 6
โข ((๐ถ โ โค โง ๐ต โ โค) โ (๐ถ โฅ ๐ต โ โ๐ โ โค (๐ ยท ๐ถ) = ๐ต)) |
8 | 2, 6, 7 | syl2anc 582 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ถ โฅ ๐ต โ โ๐ โ โค (๐ ยท ๐ถ) = ๐ต)) |
9 | 5, 8 | anbi12d 629 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ((๐ถ โฅ ๐ด โง ๐ถ โฅ ๐ต) โ (โ๐ โ โค (๐ ยท ๐ถ) = ๐ด โง โ๐ โ โค (๐ ยท ๐ถ) = ๐ต))) |
10 | | reeanv 3224 |
. . . 4
โข
(โ๐ โ
โค โ๐ โ
โค ((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ (โ๐ โ โค (๐ ยท ๐ถ) = ๐ด โง โ๐ โ โค (๐ ยท ๐ถ) = ๐ต)) |
11 | 9, 10 | bitr4di 288 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ((๐ถ โฅ ๐ด โง ๐ถ โฅ ๐ต) โ โ๐ โ โค โ๐ โ โค ((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต))) |
12 | | gcdcl 16451 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ
โ0) |
13 | 12 | nn0cnd 12538 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โ โ) |
14 | 13 | 3adant3 1130 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (๐ gcd ๐) โ โ) |
15 | | nncn 12224 |
. . . . . . . . . . 11
โข (๐ถ โ โ โ ๐ถ โ
โ) |
16 | 15 | 3ad2ant3 1133 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ๐ถ โ
โ) |
17 | | nnne0 12250 |
. . . . . . . . . . 11
โข (๐ถ โ โ โ ๐ถ โ 0) |
18 | 17 | 3ad2ant3 1133 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ๐ถ โ 0) |
19 | 14, 16, 18 | divcan4d 12000 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ gcd ๐) ยท ๐ถ) / ๐ถ) = (๐ gcd ๐)) |
20 | | nnnn0 12483 |
. . . . . . . . . . 11
โข (๐ถ โ โ โ ๐ถ โ
โ0) |
21 | | mulgcdr 16496 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ0)
โ ((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) = ((๐ gcd ๐) ยท ๐ถ)) |
22 | 20, 21 | syl3an3 1163 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) = ((๐ gcd ๐) ยท ๐ถ)) |
23 | 22 | oveq1d 7426 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) / ๐ถ) = (((๐ gcd ๐) ยท ๐ถ) / ๐ถ)) |
24 | | zcn 12567 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
25 | 24 | 3ad2ant1 1131 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ๐ โ
โ) |
26 | 25, 16, 18 | divcan4d 12000 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ((๐ ยท ๐ถ) / ๐ถ) = ๐) |
27 | | zcn 12567 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
28 | 27 | 3ad2ant2 1132 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ๐ โ
โ) |
29 | 28, 16, 18 | divcan4d 12000 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ ((๐ ยท ๐ถ) / ๐ถ) = ๐) |
30 | 26, 29 | oveq12d 7429 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) / ๐ถ) gcd ((๐ ยท ๐ถ) / ๐ถ)) = (๐ gcd ๐)) |
31 | 19, 23, 30 | 3eqtr4d 2780 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) / ๐ถ) = (((๐ ยท ๐ถ) / ๐ถ) gcd ((๐ ยท ๐ถ) / ๐ถ))) |
32 | | oveq12 7420 |
. . . . . . . . . 10
โข (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) = (๐ด gcd ๐ต)) |
33 | 32 | oveq1d 7426 |
. . . . . . . . 9
โข (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ (((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) / ๐ถ) = ((๐ด gcd ๐ต) / ๐ถ)) |
34 | | oveq1 7418 |
. . . . . . . . . 10
โข ((๐ ยท ๐ถ) = ๐ด โ ((๐ ยท ๐ถ) / ๐ถ) = (๐ด / ๐ถ)) |
35 | | oveq1 7418 |
. . . . . . . . . 10
โข ((๐ ยท ๐ถ) = ๐ต โ ((๐ ยท ๐ถ) / ๐ถ) = (๐ต / ๐ถ)) |
36 | 34, 35 | oveqan12d 7430 |
. . . . . . . . 9
โข (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ (((๐ ยท ๐ถ) / ๐ถ) gcd ((๐ ยท ๐ถ) / ๐ถ)) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ))) |
37 | 33, 36 | eqeq12d 2746 |
. . . . . . . 8
โข (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((((๐ ยท ๐ถ) gcd (๐ ยท ๐ถ)) / ๐ถ) = (((๐ ยท ๐ถ) / ๐ถ) gcd ((๐ ยท ๐ถ) / ๐ถ)) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
38 | 31, 37 | syl5ibcom 244 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
39 | 38 | 3expa 1116 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง ๐ถ โ โ) โ (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
40 | 39 | expcom 412 |
. . . . 5
โข (๐ถ โ โ โ ((๐ โ โค โง ๐ โ โค) โ (((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ))))) |
41 | 40 | rexlimdvv 3208 |
. . . 4
โข (๐ถ โ โ โ
(โ๐ โ โค
โ๐ โ โค
((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
42 | 41 | 3ad2ant3 1133 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ
(โ๐ โ โค
โ๐ โ โค
((๐ ยท ๐ถ) = ๐ด โง (๐ ยท ๐ถ) = ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
43 | 11, 42 | sylbid 239 |
. 2
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ((๐ถ โฅ ๐ด โง ๐ถ โฅ ๐ต) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ)))) |
44 | 43 | imp 405 |
1
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง (๐ถ โฅ ๐ด โง ๐ถ โฅ ๐ต)) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ))) |