Step | Hyp | Ref
| Expression |
1 | | simpl3 1194 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐พ โ โค) |
2 | 1 | zred 12540 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐พ โ โ) |
3 | | simpl2 1193 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ โ) |
4 | 3 | nnrpd 12884 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ
โ+) |
5 | | modval 13705 |
. . . 4
โข ((๐พ โ โ โง ๐ โ โ+)
โ (๐พ mod ๐) = (๐พ โ (๐ ยท (โโ(๐พ / ๐))))) |
6 | 2, 4, 5 | syl2anc 585 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐พ mod ๐) = (๐พ โ (๐ ยท (โโ(๐พ / ๐))))) |
7 | 6 | breq2d 5116 |
. 2
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ mod ๐) โ ๐ โฅ (๐พ โ (๐ ยท (โโ(๐พ / ๐)))))) |
8 | | simpl1 1192 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ โ) |
9 | 8 | nnzd 12539 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ โค) |
10 | 3 | nnzd 12539 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โ โค) |
11 | 2, 3 | nndivred 12141 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐พ / ๐) โ โ) |
12 | 11 | flcld 13632 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (โโ(๐พ / ๐)) โ โค) |
13 | | simpr 486 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โฅ ๐) |
14 | 9, 10, 12, 13 | dvdsmultr1d 16114 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โฅ (๐ ยท (โโ(๐พ / ๐)))) |
15 | 10, 12 | zmulcld 12546 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ ยท (โโ(๐พ / ๐))) โ โค) |
16 | 15 | zcnd 12541 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ ยท (โโ(๐พ / ๐))) โ โ) |
17 | 16 | subid1d 11435 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐ ยท (โโ(๐พ / ๐))) โ 0) = (๐ ยท (โโ(๐พ / ๐)))) |
18 | 14, 17 | breqtrrd 5132 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐ โฅ ((๐ ยท (โโ(๐พ / ๐))) โ 0)) |
19 | | 0zd 12445 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ 0 โ โค) |
20 | | moddvds 16082 |
. . . . . 6
โข ((๐ โ โ โง (๐ ยท (โโ(๐พ / ๐))) โ โค โง 0 โ โค)
โ (((๐ ยท
(โโ(๐พ / ๐))) mod ๐) = (0 mod ๐) โ ๐ โฅ ((๐ ยท (โโ(๐พ / ๐))) โ 0))) |
21 | 8, 15, 19, 20 | syl3anc 1372 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (((๐ ยท (โโ(๐พ / ๐))) mod ๐) = (0 mod ๐) โ ๐ โฅ ((๐ ยท (โโ(๐พ / ๐))) โ 0))) |
22 | 18, 21 | mpbird 257 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐ ยท (โโ(๐พ / ๐))) mod ๐) = (0 mod ๐)) |
23 | 22 | eqeq2d 2749 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐พ mod ๐) = ((๐ ยท (โโ(๐พ / ๐))) mod ๐) โ (๐พ mod ๐) = (0 mod ๐))) |
24 | | moddvds 16082 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค โง (๐ ยท (โโ(๐พ / ๐))) โ โค) โ ((๐พ mod ๐) = ((๐ ยท (โโ(๐พ / ๐))) mod ๐) โ ๐ โฅ (๐พ โ (๐ ยท (โโ(๐พ / ๐)))))) |
25 | 8, 1, 15, 24 | syl3anc 1372 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐พ mod ๐) = ((๐ ยท (โโ(๐พ / ๐))) mod ๐) โ ๐ โฅ (๐พ โ (๐ ยท (โโ(๐พ / ๐)))))) |
26 | | moddvds 16082 |
. . . 4
โข ((๐ โ โ โง ๐พ โ โค โง 0 โ
โค) โ ((๐พ mod
๐) = (0 mod ๐) โ ๐ โฅ (๐พ โ 0))) |
27 | 8, 1, 19, 26 | syl3anc 1372 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ((๐พ mod ๐) = (0 mod ๐) โ ๐ โฅ (๐พ โ 0))) |
28 | 23, 25, 27 | 3bitr3d 309 |
. 2
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ โ (๐ ยท (โโ(๐พ / ๐)))) โ ๐ โฅ (๐พ โ 0))) |
29 | 1 | zcnd 12541 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ ๐พ โ โ) |
30 | 29 | subid1d 11435 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐พ โ 0) = ๐พ) |
31 | 30 | breq2d 5116 |
. 2
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ โ 0) โ ๐ โฅ ๐พ)) |
32 | 7, 28, 31 | 3bitrd 305 |
1
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ mod ๐) โ ๐ โฅ ๐พ)) |