Step | Hyp | Ref
| Expression |
1 | | nnz 12456 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โค) |
2 | 1 | adantl 483 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ๐ โ
โค) |
3 | | zsubcl 12476 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด โ ๐ต) โ โค) |
4 | 3 | 3adant3 1133 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ด โ ๐ต) โ โค) |
5 | 4 | adantr 482 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ (๐ด โ ๐ต) โ โค) |
6 | | nnz 12456 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ
โค) |
7 | | nnne0 12121 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ 0) |
8 | 6, 7 | jca 513 |
. . . . . 6
โข (๐ถ โ โ โ (๐ถ โ โค โง ๐ถ โ 0)) |
9 | 8 | 3ad2ant3 1136 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ถ โ โค โง ๐ถ โ 0)) |
10 | 9 | adantr 482 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ (๐ถ โ โค โง ๐ถ โ 0)) |
11 | | dvdscmulr 16102 |
. . . . 5
โข ((๐ โ โค โง (๐ด โ ๐ต) โ โค โง (๐ถ โ โค โง ๐ถ โ 0)) โ ((๐ถ ยท ๐) โฅ (๐ถ ยท (๐ด โ ๐ต)) โ ๐ โฅ (๐ด โ ๐ต))) |
12 | 11 | bicomd 222 |
. . . 4
โข ((๐ โ โค โง (๐ด โ ๐ต) โ โค โง (๐ถ โ โค โง ๐ถ โ 0)) โ (๐ โฅ (๐ด โ ๐ต) โ (๐ถ ยท ๐) โฅ (๐ถ ยท (๐ด โ ๐ต)))) |
13 | 2, 5, 10, 12 | syl3anc 1372 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ (๐ โฅ (๐ด โ ๐ต) โ (๐ถ ยท ๐) โฅ (๐ถ ยท (๐ด โ ๐ต)))) |
14 | | zcn 12438 |
. . . . . . . 8
โข (๐ด โ โค โ ๐ด โ
โ) |
15 | | zcn 12438 |
. . . . . . . 8
โข (๐ต โ โค โ ๐ต โ
โ) |
16 | | nncn 12095 |
. . . . . . . 8
โข (๐ถ โ โ โ ๐ถ โ
โ) |
17 | 14, 15, 16 | 3anim123i 1152 |
. . . . . . 7
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ
โ)) |
18 | | 3anrot 1101 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ต โ โ) โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ
โ)) |
19 | 17, 18 | sylibr 233 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ถ โ โ โง ๐ด โ โ โง ๐ต โ
โ)) |
20 | | subdi 11522 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ต โ โ) โ (๐ถ ยท (๐ด โ ๐ต)) = ((๐ถ ยท ๐ด) โ (๐ถ ยท ๐ต))) |
21 | 19, 20 | syl 17 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ถ ยท (๐ด โ ๐ต)) = ((๐ถ ยท ๐ด) โ (๐ถ ยท ๐ต))) |
22 | 21 | adantr 482 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ (๐ถ ยท (๐ด โ ๐ต)) = ((๐ถ ยท ๐ด) โ (๐ถ ยท ๐ต))) |
23 | 22 | breq2d 5116 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ((๐ถ ยท ๐) โฅ (๐ถ ยท (๐ด โ ๐ต)) โ (๐ถ ยท ๐) โฅ ((๐ถ ยท ๐ด) โ (๐ถ ยท ๐ต)))) |
24 | 13, 23 | bitrd 279 |
. 2
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ (๐ โฅ (๐ด โ ๐ต) โ (๐ถ ยท ๐) โฅ ((๐ถ ยท ๐ด) โ (๐ถ ยท ๐ต)))) |
25 | | simpr 486 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ๐ โ
โ) |
26 | | simp1 1137 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ๐ด โ
โค) |
27 | 26 | adantr 482 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ๐ด โ
โค) |
28 | | simp2 1138 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ๐ต โ
โค) |
29 | 28 | adantr 482 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ๐ต โ
โค) |
30 | | moddvds 16082 |
. . 3
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ ((๐ด mod ๐) = (๐ต mod ๐) โ ๐ โฅ (๐ด โ ๐ต))) |
31 | 25, 27, 29, 30 | syl3anc 1372 |
. 2
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ((๐ด mod ๐) = (๐ต mod ๐) โ ๐ โฅ (๐ด โ ๐ต))) |
32 | | simpl3 1194 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ๐ถ โ
โ) |
33 | 32, 25 | nnmulcld 12140 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ (๐ถ ยท ๐) โ โ) |
34 | 6 | 3ad2ant3 1136 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ ๐ถ โ
โค) |
35 | 34, 26 | zmulcld 12546 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ถ ยท ๐ด) โ โค) |
36 | 35 | adantr 482 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ (๐ถ ยท ๐ด) โ โค) |
37 | 34, 28 | zmulcld 12546 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โ (๐ถ ยท ๐ต) โ โค) |
38 | 37 | adantr 482 |
. . 3
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ (๐ถ ยท ๐ต) โ โค) |
39 | | moddvds 16082 |
. . 3
โข (((๐ถ ยท ๐) โ โ โง (๐ถ ยท ๐ด) โ โค โง (๐ถ ยท ๐ต) โ โค) โ (((๐ถ ยท ๐ด) mod (๐ถ ยท ๐)) = ((๐ถ ยท ๐ต) mod (๐ถ ยท ๐)) โ (๐ถ ยท ๐) โฅ ((๐ถ ยท ๐ด) โ (๐ถ ยท ๐ต)))) |
40 | 33, 36, 38, 39 | syl3anc 1372 |
. 2
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ (((๐ถ ยท ๐ด) mod (๐ถ ยท ๐)) = ((๐ถ ยท ๐ต) mod (๐ถ ยท ๐)) โ (๐ถ ยท ๐) โฅ ((๐ถ ยท ๐ด) โ (๐ถ ยท ๐ต)))) |
41 | 24, 31, 40 | 3bitr4d 311 |
1
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ((๐ด mod ๐) = (๐ต mod ๐) โ ((๐ถ ยท ๐ด) mod (๐ถ ยท ๐)) = ((๐ถ ยท ๐ต) mod (๐ถ ยท ๐)))) |