Step | Hyp | Ref
| Expression |
1 | | eqcom 2740 |
. 2
โข ((๐ mod ๐ท) = ๐
โ ๐
= (๐ mod ๐ท)) |
2 | | divalgmodcl 16294 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ โง ๐
โ โ0)
โ (๐
= (๐ mod ๐ท) โ (๐
< ๐ท โง ๐ท โฅ (๐ โ ๐
)))) |
3 | 2 | 3adant3r 1182 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ (๐
= (๐ mod ๐ท) โ (๐
< ๐ท โง ๐ท โฅ (๐ โ ๐
)))) |
4 | | ibar 530 |
. . . . 5
โข (๐
< ๐ท โ (๐ท โฅ (๐ โ ๐
) โ (๐
< ๐ท โง ๐ท โฅ (๐ โ ๐
)))) |
5 | 4 | adantl 483 |
. . . 4
โข ((๐
โ โ0
โง ๐
< ๐ท) โ (๐ท โฅ (๐ โ ๐
) โ (๐
< ๐ท โง ๐ท โฅ (๐ โ ๐
)))) |
6 | 5 | 3ad2ant3 1136 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ (๐ท โฅ (๐ โ ๐
) โ (๐
< ๐ท โง ๐ท โฅ (๐ โ ๐
)))) |
7 | | nnz 12525 |
. . . . . 6
โข (๐ท โ โ โ ๐ท โ
โค) |
8 | 7 | 3ad2ant2 1135 |
. . . . 5
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ ๐ท โ โค) |
9 | | simp1 1137 |
. . . . . 6
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ ๐ โ โค) |
10 | | nn0z 12529 |
. . . . . . . 8
โข (๐
โ โ0
โ ๐
โ
โค) |
11 | 10 | adantr 482 |
. . . . . . 7
โข ((๐
โ โ0
โง ๐
< ๐ท) โ ๐
โ โค) |
12 | 11 | 3ad2ant3 1136 |
. . . . . 6
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ ๐
โ โค) |
13 | 9, 12 | zsubcld 12617 |
. . . . 5
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ (๐ โ ๐
) โ โค) |
14 | | divides 16143 |
. . . . 5
โข ((๐ท โ โค โง (๐ โ ๐
) โ โค) โ (๐ท โฅ (๐ โ ๐
) โ โ๐ง โ โค (๐ง ยท ๐ท) = (๐ โ ๐
))) |
15 | 8, 13, 14 | syl2anc 585 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ (๐ท โฅ (๐ โ ๐
) โ โ๐ง โ โค (๐ง ยท ๐ท) = (๐ โ ๐
))) |
16 | | eqcom 2740 |
. . . . . 6
โข ((๐ง ยท ๐ท) = (๐ โ ๐
) โ (๐ โ ๐
) = (๐ง ยท ๐ท)) |
17 | | zcn 12509 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
โ) |
18 | 17 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ ๐ โ โ) |
19 | 18 | adantr 482 |
. . . . . . 7
โข (((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โง ๐ง โ โค) โ ๐ โ โ) |
20 | | nn0cn 12428 |
. . . . . . . . . 10
โข (๐
โ โ0
โ ๐
โ
โ) |
21 | 20 | adantr 482 |
. . . . . . . . 9
โข ((๐
โ โ0
โง ๐
< ๐ท) โ ๐
โ โ) |
22 | 21 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ ๐
โ โ) |
23 | 22 | adantr 482 |
. . . . . . 7
โข (((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โง ๐ง โ โค) โ ๐
โ โ) |
24 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โง ๐ง โ โค) โ ๐ง โ โค) |
25 | 8 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โง ๐ง โ โค) โ ๐ท โ โค) |
26 | 24, 25 | zmulcld 12618 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โง ๐ง โ โค) โ (๐ง ยท ๐ท) โ โค) |
27 | 26 | zcnd 12613 |
. . . . . . 7
โข (((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โง ๐ง โ โค) โ (๐ง ยท ๐ท) โ โ) |
28 | 19, 23, 27 | subadd2d 11536 |
. . . . . 6
โข (((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โง ๐ง โ โค) โ ((๐ โ ๐
) = (๐ง ยท ๐ท) โ ((๐ง ยท ๐ท) + ๐
) = ๐)) |
29 | 16, 28 | bitrid 283 |
. . . . 5
โข (((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โง ๐ง โ โค) โ ((๐ง ยท ๐ท) = (๐ โ ๐
) โ ((๐ง ยท ๐ท) + ๐
) = ๐)) |
30 | 29 | rexbidva 3170 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ (โ๐ง โ โค (๐ง ยท ๐ท) = (๐ โ ๐
) โ โ๐ง โ โค ((๐ง ยท ๐ท) + ๐
) = ๐)) |
31 | 15, 30 | bitrd 279 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ (๐ท โฅ (๐ โ ๐
) โ โ๐ง โ โค ((๐ง ยท ๐ท) + ๐
) = ๐)) |
32 | 3, 6, 31 | 3bitr2d 307 |
. 2
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ (๐
= (๐ mod ๐ท) โ โ๐ง โ โค ((๐ง ยท ๐ท) + ๐
) = ๐)) |
33 | 1, 32 | bitrid 283 |
1
โข ((๐ โ โค โง ๐ท โ โ โง (๐
โ โ0
โง ๐
< ๐ท)) โ ((๐ mod ๐ท) = ๐
โ โ๐ง โ โค ((๐ง ยท ๐ท) + ๐
) = ๐)) |