Step | Hyp | Ref
| Expression |
1 | | qcn 9633 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
2 | 1 | 3ad2ant2 1019 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โ ๐ต โ โ) |
3 | 2 | adantr 276 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ๐ต โ โ) |
4 | 3 | mulridd 7973 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (๐ต ยท 1) = ๐ต) |
5 | 4 | oveq2d 5890 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (๐ด โ (๐ต ยท 1)) = (๐ด โ ๐ต)) |
6 | 5 | oveq1d 5889 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ((๐ด โ (๐ต ยท 1)) mod ๐ต) = ((๐ด โ ๐ต) mod ๐ต)) |
7 | | simpl1 1000 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ๐ด โ โ) |
8 | | 1zzd 9279 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ 1 โ
โค) |
9 | | simpl2 1001 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ๐ต โ โ) |
10 | | simpl3 1002 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ 0 < ๐ต) |
11 | | modqcyc2 10359 |
. . 3
โข (((๐ด โ โ โง 1 โ
โค) โง (๐ต โ
โ โง 0 < ๐ต))
โ ((๐ด โ (๐ต ยท 1)) mod ๐ต) = (๐ด mod ๐ต)) |
12 | 7, 8, 9, 10, 11 | syl22anc 1239 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ((๐ด โ (๐ต ยท 1)) mod ๐ต) = (๐ด mod ๐ต)) |
13 | | qsubcl 9637 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ ๐ต) โ โ) |
14 | 7, 9, 13 | syl2anc 411 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (๐ด โ ๐ต) โ โ) |
15 | | simpr 110 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) |
16 | | qre 9624 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
17 | 7, 16 | syl 14 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ๐ด โ โ) |
18 | | qre 9624 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ
โ) |
19 | 9, 18 | syl 14 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ๐ต โ โ) |
20 | 17, 19 | subge0d 8491 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (0 โค (๐ด โ ๐ต) โ ๐ต โค ๐ด)) |
21 | 20 | bicomd 141 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (๐ต โค ๐ด โ 0 โค (๐ด โ ๐ต))) |
22 | 3 | 2timesd 9160 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (2 ยท ๐ต) = (๐ต + ๐ต)) |
23 | 22 | breq2d 4015 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (๐ด < (2 ยท ๐ต) โ ๐ด < (๐ต + ๐ต))) |
24 | 17, 19, 19 | ltsubaddd 8497 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ((๐ด โ ๐ต) < ๐ต โ ๐ด < (๐ต + ๐ต))) |
25 | 23, 24 | bitr4d 191 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (๐ด < (2 ยท ๐ต) โ (๐ด โ ๐ต) < ๐ต)) |
26 | 21, 25 | anbi12d 473 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ((๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต)) โ (0 โค (๐ด โ ๐ต) โง (๐ด โ ๐ต) < ๐ต))) |
27 | 15, 26 | mpbid 147 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (0 โค (๐ด โ ๐ต) โง (๐ด โ ๐ต) < ๐ต)) |
28 | | modqid 10348 |
. . 3
โข ((((๐ด โ ๐ต) โ โ โง ๐ต โ โ) โง (0 โค (๐ด โ ๐ต) โง (๐ด โ ๐ต) < ๐ต)) โ ((๐ด โ ๐ต) mod ๐ต) = (๐ด โ ๐ต)) |
29 | 14, 9, 27, 28 | syl21anc 1237 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ ((๐ด โ ๐ต) mod ๐ต) = (๐ด โ ๐ต)) |
30 | 6, 12, 29 | 3eqtr3d 2218 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (๐ด mod ๐ต) = (๐ด โ ๐ต)) |