Step | Hyp | Ref
| Expression |
1 | | zmodcl 10344 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) โ
โ0) |
2 | 1 | nn0zd 9373 |
. 2
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) โ โค) |
3 | | znq 9624 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ / ๐ท) โ โ) |
4 | 3 | flqcld 10277 |
. 2
โข ((๐ โ โค โง ๐ท โ โ) โ
(โโ(๐ / ๐ท)) โ
โค) |
5 | 1 | nn0ge0d 9232 |
. 2
โข ((๐ โ โค โง ๐ท โ โ) โ 0 โค
(๐ mod ๐ท)) |
6 | | zq 9626 |
. . . . 5
โข (๐ โ โค โ ๐ โ
โ) |
7 | 6 | adantr 276 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ โ
โ) |
8 | | nnq 9633 |
. . . . 5
โข (๐ท โ โ โ ๐ท โ
โ) |
9 | 8 | adantl 277 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ท โ
โ) |
10 | | nngt0 8944 |
. . . . 5
โข (๐ท โ โ โ 0 <
๐ท) |
11 | 10 | adantl 277 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ 0 <
๐ท) |
12 | | modqlt 10333 |
. . . 4
โข ((๐ โ โ โง ๐ท โ โ โง 0 <
๐ท) โ (๐ mod ๐ท) < ๐ท) |
13 | 7, 9, 11, 12 | syl3anc 1238 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) < ๐ท) |
14 | | nnre 8926 |
. . . . 5
โข (๐ท โ โ โ ๐ท โ
โ) |
15 | 14 | adantl 277 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ท โ
โ) |
16 | | 0red 7958 |
. . . . 5
โข ((๐ โ โค โง ๐ท โ โ) โ 0 โ
โ) |
17 | 16, 15, 11 | ltled 8076 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ 0 โค
๐ท) |
18 | 15, 17 | absidd 11176 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ) โ
(absโ๐ท) = ๐ท) |
19 | 13, 18 | breqtrrd 4032 |
. 2
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) < (absโ๐ท)) |
20 | 1 | nn0cnd 9231 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) โ โ) |
21 | 4 | zcnd 9376 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ
(โโ(๐ / ๐ท)) โ
โ) |
22 | | simpr 110 |
. . . . 5
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ท โ
โ) |
23 | 22 | nncnd 8933 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ท โ
โ) |
24 | 21, 23 | mulcld 7978 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ) โ
((โโ(๐ / ๐ท)) ยท ๐ท) โ โ) |
25 | | modqvalr 10325 |
. . . . . 6
โข ((๐ โ โ โง ๐ท โ โ โง 0 <
๐ท) โ (๐ mod ๐ท) = (๐ โ ((โโ(๐ / ๐ท)) ยท ๐ท))) |
26 | 7, 9, 11, 25 | syl3anc 1238 |
. . . . 5
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ mod ๐ท) = (๐ โ ((โโ(๐ / ๐ท)) ยท ๐ท))) |
27 | 26 | oveq1d 5890 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ ((๐ mod ๐ท) + ((โโ(๐ / ๐ท)) ยท ๐ท)) = ((๐ โ ((โโ(๐ / ๐ท)) ยท ๐ท)) + ((โโ(๐ / ๐ท)) ยท ๐ท))) |
28 | | simpl 109 |
. . . . . 6
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ โ
โค) |
29 | 28 | zcnd 9376 |
. . . . 5
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ โ
โ) |
30 | 29, 24 | npcand 8272 |
. . . 4
โข ((๐ โ โค โง ๐ท โ โ) โ ((๐ โ ((โโ(๐ / ๐ท)) ยท ๐ท)) + ((โโ(๐ / ๐ท)) ยท ๐ท)) = ๐) |
31 | 27, 30 | eqtr2d 2211 |
. . 3
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ = ((๐ mod ๐ท) + ((โโ(๐ / ๐ท)) ยท ๐ท))) |
32 | 20, 24, 31 | comraddd 8114 |
. 2
โข ((๐ โ โค โง ๐ท โ โ) โ ๐ = (((โโ(๐ / ๐ท)) ยท ๐ท) + (๐ mod ๐ท))) |
33 | | breq2 4008 |
. . . 4
โข (๐ = (๐ mod ๐ท) โ (0 โค ๐ โ 0 โค (๐ mod ๐ท))) |
34 | | breq1 4007 |
. . . 4
โข (๐ = (๐ mod ๐ท) โ (๐ < (absโ๐ท) โ (๐ mod ๐ท) < (absโ๐ท))) |
35 | | oveq2 5883 |
. . . . 5
โข (๐ = (๐ mod ๐ท) โ ((๐ ยท ๐ท) + ๐) = ((๐ ยท ๐ท) + (๐ mod ๐ท))) |
36 | 35 | eqeq2d 2189 |
. . . 4
โข (๐ = (๐ mod ๐ท) โ (๐ = ((๐ ยท ๐ท) + ๐) โ ๐ = ((๐ ยท ๐ท) + (๐ mod ๐ท)))) |
37 | 33, 34, 36 | 3anbi123d 1312 |
. . 3
โข (๐ = (๐ mod ๐ท) โ ((0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ (0 โค (๐ mod ๐ท) โง (๐ mod ๐ท) < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + (๐ mod ๐ท))))) |
38 | | oveq1 5882 |
. . . . . 6
โข (๐ = (โโ(๐ / ๐ท)) โ (๐ ยท ๐ท) = ((โโ(๐ / ๐ท)) ยท ๐ท)) |
39 | 38 | oveq1d 5890 |
. . . . 5
โข (๐ = (โโ(๐ / ๐ท)) โ ((๐ ยท ๐ท) + (๐ mod ๐ท)) = (((โโ(๐ / ๐ท)) ยท ๐ท) + (๐ mod ๐ท))) |
40 | 39 | eqeq2d 2189 |
. . . 4
โข (๐ = (โโ(๐ / ๐ท)) โ (๐ = ((๐ ยท ๐ท) + (๐ mod ๐ท)) โ ๐ = (((โโ(๐ / ๐ท)) ยท ๐ท) + (๐ mod ๐ท)))) |
41 | 40 | 3anbi3d 1318 |
. . 3
โข (๐ = (โโ(๐ / ๐ท)) โ ((0 โค (๐ mod ๐ท) โง (๐ mod ๐ท) < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + (๐ mod ๐ท))) โ (0 โค (๐ mod ๐ท) โง (๐ mod ๐ท) < (absโ๐ท) โง ๐ = (((โโ(๐ / ๐ท)) ยท ๐ท) + (๐ mod ๐ท))))) |
42 | 37, 41 | rspc2ev 2857 |
. 2
โข (((๐ mod ๐ท) โ โค โง (โโ(๐ / ๐ท)) โ โค โง (0 โค (๐ mod ๐ท) โง (๐ mod ๐ท) < (absโ๐ท) โง ๐ = (((โโ(๐ / ๐ท)) ยท ๐ท) + (๐ mod ๐ท)))) โ โ๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐))) |
43 | 2, 4, 5, 19, 32, 42 | syl113anc 1250 |
1
โข ((๐ โ โค โง ๐ท โ โ) โ
โ๐ โ โค
โ๐ โ โค (0
โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐))) |