Step | Hyp | Ref
| Expression |
1 | | simp2 999 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ ๐ด โ
โค) |
2 | | zq 9639 |
. . . . . . 7
โข (๐ด โ โค โ ๐ด โ
โ) |
3 | 1, 2 | syl 14 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ ๐ด โ
โ) |
4 | | simp3 1000 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ ๐ต โ
โค) |
5 | | simp1 998 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ ๐ โ
โ) |
6 | | nnq 9646 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
7 | 5, 6 | syl 14 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ ๐ โ
โ) |
8 | 5 | nngt0d 8976 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ 0 <
๐) |
9 | | modqmulmod 10402 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โค) โง (๐ โ โ โง 0 <
๐)) โ (((๐ด mod ๐) ยท ๐ต) mod ๐) = ((๐ด ยท ๐ต) mod ๐)) |
10 | 3, 4, 7, 8, 9 | syl22anc 1249 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ (((๐ด mod ๐) ยท ๐ต) mod ๐) = ((๐ด ยท ๐ต) mod ๐)) |
11 | 10 | eqcomd 2193 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ ((๐ด ยท ๐ต) mod ๐) = (((๐ด mod ๐) ยท ๐ต) mod ๐)) |
12 | 11 | adantr 276 |
. . 3
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ ((๐ด ยท ๐ต) mod ๐) = (((๐ด mod ๐) ยท ๐ต) mod ๐)) |
13 | | dvdsval3 11811 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โค) โ (๐ โฅ ๐ด โ (๐ด mod ๐) = 0)) |
14 | 13 | 3adant3 1018 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ (๐ โฅ ๐ด โ (๐ด mod ๐) = 0)) |
15 | 14 | biimpa 296 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ (๐ด mod ๐) = 0) |
16 | 15 | oveq1d 5903 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ ((๐ด mod ๐) ยท ๐ต) = (0 ยท ๐ต)) |
17 | 16 | oveq1d 5903 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ (((๐ด mod ๐) ยท ๐ต) mod ๐) = ((0 ยท ๐ต) mod ๐)) |
18 | 4 | adantr 276 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ ๐ต โ โค) |
19 | 18 | zcnd 9389 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ ๐ต โ โ) |
20 | 19 | mul02d 8362 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ (0 ยท ๐ต) = 0) |
21 | 20 | oveq1d 5903 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ ((0 ยท ๐ต) mod ๐) = (0 mod ๐)) |
22 | 7 | adantr 276 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ ๐ โ โ) |
23 | 8 | adantr 276 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ 0 < ๐) |
24 | | q0mod 10368 |
. . . . . 6
โข ((๐ โ โ โง 0 <
๐) โ (0 mod ๐) = 0) |
25 | 22, 23, 24 | syl2anc 411 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ (0 mod ๐) = 0) |
26 | 21, 25 | eqtrd 2220 |
. . . 4
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ ((0 ยท ๐ต) mod ๐) = 0) |
27 | 17, 26 | eqtrd 2220 |
. . 3
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ (((๐ด mod ๐) ยท ๐ต) mod ๐) = 0) |
28 | 12, 27 | eqtrd 2220 |
. 2
โข (((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โง ๐ โฅ ๐ด) โ ((๐ด ยท ๐ต) mod ๐) = 0) |
29 | 28 | ex 115 |
1
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ (๐ โฅ ๐ด โ ((๐ด ยท ๐ต) mod ๐) = 0)) |