Step | Hyp | Ref
| Expression |
1 | | ovex 7391 |
. . . . . 6
โข (๐ mod ๐ท) โ V |
2 | 1 | snid 4623 |
. . . . 5
โข (๐ mod ๐ท) โ {(๐ mod ๐ท)} |
3 | | eleq1 2822 |
. . . . 5
โข (๐
= (๐ mod ๐ท) โ (๐
โ {(๐ mod ๐ท)} โ (๐ mod ๐ท) โ {(๐ mod ๐ท)})) |
4 | 2, 3 | mpbiri 258 |
. . . 4
โข (๐
= (๐ mod ๐ท) โ ๐
โ {(๐ mod ๐ท)}) |
5 | | elsni 4604 |
. . . 4
โข (๐
โ {(๐ mod ๐ท)} โ ๐
= (๐ mod ๐ท)) |
6 | 4, 5 | impbii 208 |
. . 3
โข (๐
= (๐ mod ๐ท) โ ๐
โ {(๐ mod ๐ท)}) |
7 | | zre 12508 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
8 | | nnrp 12931 |
. . . . . . . . 9
โข (๐ท โ โ โ ๐ท โ
โ+) |
9 | | modlt 13791 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ท โ โ+)
โ (๐ mod ๐ท) < ๐ท) |
10 | 7, 8, 9 | syl2an 597 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) < ๐ท) |
11 | | nnre 12165 |
. . . . . . . . . . . 12
โข (๐ท โ โ โ ๐ท โ
โ) |
12 | | nnne0 12192 |
. . . . . . . . . . . 12
โข (๐ท โ โ โ ๐ท โ 0) |
13 | | redivcl 11879 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ท โ โ โง ๐ท โ 0) โ (๐ / ๐ท) โ โ) |
14 | 7, 11, 12, 13 | syl3an 1161 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ท โ โ โง ๐ท โ โ) โ (๐ / ๐ท) โ โ) |
15 | 14 | 3anidm23 1422 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ / ๐ท) โ โ) |
16 | 15 | flcld 13709 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ท โ โ) โ
(โโ(๐ / ๐ท)) โ
โค) |
17 | | nnz 12525 |
. . . . . . . . . 10
โข (๐ท โ โ โ ๐ท โ
โค) |
18 | 17 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ท โ
โค) |
19 | | zmodcl 13802 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) โ
โ0) |
20 | 19 | nn0zd 12530 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) โ โค) |
21 | | zsubcl 12550 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ mod ๐ท) โ โค) โ (๐ โ (๐ mod ๐ท)) โ โค) |
22 | 20, 21 | syldan 592 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ โ (๐ mod ๐ท)) โ โค) |
23 | | nncn 12166 |
. . . . . . . . . . . 12
โข (๐ท โ โ โ ๐ท โ
โ) |
24 | 23 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ท โ
โ) |
25 | 16 | zcnd 12613 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ท โ โ) โ
(โโ(๐ / ๐ท)) โ
โ) |
26 | 24, 25 | mulcomd 11181 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ท ยท (โโ(๐ / ๐ท))) = ((โโ(๐ / ๐ท)) ยท ๐ท)) |
27 | | modval 13782 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ท โ โ+)
โ (๐ mod ๐ท) = (๐ โ (๐ท ยท (โโ(๐ / ๐ท))))) |
28 | 7, 8, 27 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) = (๐ โ (๐ท ยท (โโ(๐ / ๐ท))))) |
29 | 19 | nn0cnd 12480 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) โ โ) |
30 | | zmulcl 12557 |
. . . . . . . . . . . . . 14
โข ((๐ท โ โค โง
(โโ(๐ / ๐ท)) โ โค) โ (๐ท ยท (โโ(๐ / ๐ท))) โ โค) |
31 | 17, 16, 30 | syl2an2 685 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ท ยท (โโ(๐ / ๐ท))) โ โค) |
32 | 31 | zcnd 12613 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ท ยท (โโ(๐ / ๐ท))) โ โ) |
33 | | zcn 12509 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
34 | 33 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ โ
โ) |
35 | 29, 32, 34 | subexsub 11578 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ท โ โ) โ ((๐ mod ๐ท) = (๐ โ (๐ท ยท (โโ(๐ / ๐ท)))) โ (๐ท ยท (โโ(๐ / ๐ท))) = (๐ โ (๐ mod ๐ท)))) |
36 | 28, 35 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ท ยท (โโ(๐ / ๐ท))) = (๐ โ (๐ mod ๐ท))) |
37 | 26, 36 | eqtr3d 2775 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ท โ โ) โ
((โโ(๐ / ๐ท)) ยท ๐ท) = (๐ โ (๐ mod ๐ท))) |
38 | | dvds0lem 16154 |
. . . . . . . . 9
โข
((((โโ(๐
/ ๐ท)) โ โค โง
๐ท โ โค โง
(๐ โ (๐ mod ๐ท)) โ โค) โง
((โโ(๐ / ๐ท)) ยท ๐ท) = (๐ โ (๐ mod ๐ท))) โ ๐ท โฅ (๐ โ (๐ mod ๐ท))) |
39 | 16, 18, 22, 37, 38 | syl31anc 1374 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ท โฅ (๐ โ (๐ mod ๐ท))) |
40 | | divalg2 16292 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ท โ โ) โ
โ!๐ง โ
โ0 (๐ง <
๐ท โง ๐ท โฅ (๐ โ ๐ง))) |
41 | | breq1 5109 |
. . . . . . . . . . 11
โข (๐ง = (๐ mod ๐ท) โ (๐ง < ๐ท โ (๐ mod ๐ท) < ๐ท)) |
42 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ง = (๐ mod ๐ท) โ (๐ โ ๐ง) = (๐ โ (๐ mod ๐ท))) |
43 | 42 | breq2d 5118 |
. . . . . . . . . . 11
โข (๐ง = (๐ mod ๐ท) โ (๐ท โฅ (๐ โ ๐ง) โ ๐ท โฅ (๐ โ (๐ mod ๐ท)))) |
44 | 41, 43 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ง = (๐ mod ๐ท) โ ((๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง)) โ ((๐ mod ๐ท) < ๐ท โง ๐ท โฅ (๐ โ (๐ mod ๐ท))))) |
45 | 44 | riota2 7340 |
. . . . . . . . 9
โข (((๐ mod ๐ท) โ โ0 โง
โ!๐ง โ
โ0 (๐ง <
๐ท โง ๐ท โฅ (๐ โ ๐ง))) โ (((๐ mod ๐ท) < ๐ท โง ๐ท โฅ (๐ โ (๐ mod ๐ท))) โ (โฉ๐ง โ โ0 (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง))) = (๐ mod ๐ท))) |
46 | 19, 40, 45 | syl2anc 585 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ท โ โ) โ (((๐ mod ๐ท) < ๐ท โง ๐ท โฅ (๐ โ (๐ mod ๐ท))) โ (โฉ๐ง โ โ0 (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง))) = (๐ mod ๐ท))) |
47 | 10, 39, 46 | mpbi2and 711 |
. . . . . . 7
โข ((๐ โ โค โง ๐ท โ โ) โ
(โฉ๐ง โ
โ0 (๐ง <
๐ท โง ๐ท โฅ (๐ โ ๐ง))) = (๐ mod ๐ท)) |
48 | 47 | eqcomd 2739 |
. . . . . 6
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) = (โฉ๐ง โ โ0 (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง)))) |
49 | 48 | sneqd 4599 |
. . . . 5
โข ((๐ โ โค โง ๐ท โ โ) โ {(๐ mod ๐ท)} = {(โฉ๐ง โ โ0 (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง)))}) |
50 | | snriota 7348 |
. . . . . 6
โข
(โ!๐ง โ
โ0 (๐ง <
๐ท โง ๐ท โฅ (๐ โ ๐ง)) โ {๐ง โ โ0 โฃ (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง))} = {(โฉ๐ง โ โ0 (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง)))}) |
51 | 40, 50 | syl 17 |
. . . . 5
โข ((๐ โ โค โง ๐ท โ โ) โ {๐ง โ โ0
โฃ (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง))} = {(โฉ๐ง โ โ0 (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง)))}) |
52 | 49, 51 | eqtr4d 2776 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ {(๐ mod ๐ท)} = {๐ง โ โ0 โฃ (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง))}) |
53 | 52 | eleq2d 2820 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ) โ (๐
โ {(๐ mod ๐ท)} โ ๐
โ {๐ง โ โ0 โฃ (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง))})) |
54 | 6, 53 | bitrid 283 |
. 2
โข ((๐ โ โค โง ๐ท โ โ) โ (๐
= (๐ mod ๐ท) โ ๐
โ {๐ง โ โ0 โฃ (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง))})) |
55 | | breq1 5109 |
. . . 4
โข (๐ง = ๐
โ (๐ง < ๐ท โ ๐
< ๐ท)) |
56 | | oveq2 7366 |
. . . . 5
โข (๐ง = ๐
โ (๐ โ ๐ง) = (๐ โ ๐
)) |
57 | 56 | breq2d 5118 |
. . . 4
โข (๐ง = ๐
โ (๐ท โฅ (๐ โ ๐ง) โ ๐ท โฅ (๐ โ ๐
))) |
58 | 55, 57 | anbi12d 632 |
. . 3
โข (๐ง = ๐
โ ((๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง)) โ (๐
< ๐ท โง ๐ท โฅ (๐ โ ๐
)))) |
59 | 58 | elrab 3646 |
. 2
โข (๐
โ {๐ง โ โ0 โฃ (๐ง < ๐ท โง ๐ท โฅ (๐ โ ๐ง))} โ (๐
โ โ0 โง (๐
< ๐ท โง ๐ท โฅ (๐ โ ๐
)))) |
60 | 54, 59 | bitrdi 287 |
1
โข ((๐ โ โค โง ๐ท โ โ) โ (๐
= (๐ mod ๐ท) โ (๐
โ โ0 โง (๐
< ๐ท โง ๐ท โฅ (๐ โ ๐
))))) |