Step | Hyp | Ref
| Expression |
1 | | simpl3 1002 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐พ โ โค) |
2 | | zq 9628 |
. . . . 5
โข (๐พ โ โค โ ๐พ โ
โ) |
3 | 1, 2 | syl 14 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐พ โ โ) |
4 | | simpl2 1001 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ โ) |
5 | | nnq 9635 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
6 | 4, 5 | syl 14 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ โ) |
7 | 4 | nngt0d 8965 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ 0 < ๐) |
8 | | modqval 10326 |
. . . 4
โข ((๐พ โ โ โง ๐ โ โ โง 0 <
๐) โ (๐พ mod ๐) = (๐พ โ (๐ ยท (โโ(๐พ / ๐))))) |
9 | 3, 6, 7, 8 | syl3anc 1238 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐พ mod ๐) = (๐พ โ (๐ ยท (โโ(๐พ / ๐))))) |
10 | 9 | breq2d 4017 |
. 2
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ mod ๐) โ ๐ โฅ (๐พ โ (๐ ยท (โโ(๐พ / ๐)))))) |
11 | | simpl1 1000 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ โ) |
12 | 11 | nnzd 9376 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ โค) |
13 | 4 | nnzd 9376 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ โค) |
14 | | znq 9626 |
. . . . . . . . 9
โข ((๐พ โ โค โง ๐ โ โ) โ (๐พ / ๐) โ โ) |
15 | 1, 4, 14 | syl2anc 411 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐พ / ๐) โ โ) |
16 | 15 | flqcld 10279 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (โโ(๐พ / ๐)) โ โค) |
17 | | simpr 110 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โฅ ๐) |
18 | 12, 13, 16, 17 | dvdsmultr1d 11841 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โฅ (๐ ยท (โโ(๐พ / ๐)))) |
19 | 13, 16 | zmulcld 9383 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ ยท (โโ(๐พ / ๐))) โ โค) |
20 | 19 | zcnd 9378 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ ยท (โโ(๐พ / ๐))) โ โ) |
21 | 20 | subid1d 8259 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐ ยท (โโ(๐พ / ๐))) โ 0) = (๐ ยท (โโ(๐พ / ๐)))) |
22 | 18, 21 | breqtrrd 4033 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โฅ ((๐ ยท (โโ(๐พ / ๐))) โ 0)) |
23 | | 0zd 9267 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ 0 โ โค) |
24 | | moddvds 11808 |
. . . . . 6
โข ((๐ โ โ โง (๐ ยท (โโ(๐พ / ๐))) โ โค โง 0 โ โค)
โ (((๐ ยท
(โโ(๐พ / ๐))) mod ๐) = (0 mod ๐) โ ๐ โฅ ((๐ ยท (โโ(๐พ / ๐))) โ 0))) |
25 | 11, 19, 23, 24 | syl3anc 1238 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (((๐ ยท (โโ(๐พ / ๐))) mod ๐) = (0 mod ๐) โ ๐ โฅ ((๐ ยท (โโ(๐พ / ๐))) โ 0))) |
26 | 22, 25 | mpbird 167 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐ ยท (โโ(๐พ / ๐))) mod ๐) = (0 mod ๐)) |
27 | 26 | eqeq2d 2189 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐พ mod ๐) = ((๐ ยท (โโ(๐พ / ๐))) mod ๐) โ (๐พ mod ๐) = (0 mod ๐))) |
28 | | moddvds 11808 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค โง (๐ ยท (โโ(๐พ / ๐))) โ โค) โ ((๐พ mod ๐) = ((๐ ยท (โโ(๐พ / ๐))) mod ๐) โ ๐ โฅ (๐พ โ (๐ ยท (โโ(๐พ / ๐)))))) |
29 | 11, 1, 19, 28 | syl3anc 1238 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐พ mod ๐) = ((๐ ยท (โโ(๐พ / ๐))) mod ๐) โ ๐ โฅ (๐พ โ (๐ ยท (โโ(๐พ / ๐)))))) |
30 | | moddvds 11808 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค โง 0 โ
โค) โ ((๐พ mod
๐) = (0 mod ๐) โ ๐ โฅ (๐พ โ 0))) |
31 | 11, 1, 23, 30 | syl3anc 1238 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐พ mod ๐) = (0 mod ๐) โ ๐ โฅ (๐พ โ 0))) |
32 | 27, 29, 31 | 3bitr3d 218 |
. 2
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ โ (๐ ยท (โโ(๐พ / ๐)))) โ ๐ โฅ (๐พ โ 0))) |
33 | 1 | zcnd 9378 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐พ โ โ) |
34 | 33 | subid1d 8259 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐พ โ 0) = ๐พ) |
35 | 34 | breq2d 4017 |
. 2
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ โ 0) โ ๐ โฅ ๐พ)) |
36 | 10, 32, 35 | 3bitrd 214 |
1
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ mod ๐) โ ๐ โฅ ๐พ)) |