Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ ๐ด โ
โ0) |
2 | | nn0z 9273 |
. . . . . . 7
โข (๐ด โ โ0
โ ๐ด โ
โค) |
3 | | zq 9626 |
. . . . . . 7
โข (๐ด โ โค โ ๐ด โ
โ) |
4 | 2, 3 | syl 14 |
. . . . . 6
โข (๐ด โ โ0
โ ๐ด โ
โ) |
5 | 1, 4 | syl 14 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ ๐ด โ
โ) |
6 | 5 | adantr 276 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ๐ด < ๐ต) โ ๐ด โ โ) |
7 | | nnq 9633 |
. . . . . 6
โข (๐ต โ โ โ ๐ต โ
โ) |
8 | 7 | 3ad2ant2 1019 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ ๐ต โ
โ) |
9 | 8 | adantr 276 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ๐ด < ๐ต) โ ๐ต โ โ) |
10 | 1 | nn0ge0d 9232 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ 0 โค ๐ด) |
11 | 10 | adantr 276 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ๐ด < ๐ต) โ 0 โค ๐ด) |
12 | | simpr 110 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ๐ด < ๐ต) โ ๐ด < ๐ต) |
13 | | modqid 10349 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง ๐ด < ๐ต)) โ (๐ด mod ๐ต) = ๐ด) |
14 | 6, 9, 11, 12, 13 | syl22anc 1239 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ๐ด < ๐ต) โ (๐ด mod ๐ต) = ๐ด) |
15 | | iftrue 3540 |
. . . . 5
โข (๐ด < ๐ต โ if(๐ด < ๐ต, ๐ด, (๐ด โ ๐ต)) = ๐ด) |
16 | 15 | eqcomd 2183 |
. . . 4
โข (๐ด < ๐ต โ ๐ด = if(๐ด < ๐ต, ๐ด, (๐ด โ ๐ต))) |
17 | 16 | adantl 277 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ๐ด < ๐ต) โ ๐ด = if(๐ด < ๐ต, ๐ด, (๐ด โ ๐ต))) |
18 | 14, 17 | eqtrd 2210 |
. 2
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ๐ด < ๐ต) โ (๐ด mod ๐ต) = if(๐ด < ๐ต, ๐ด, (๐ด โ ๐ต))) |
19 | 5 | adantr 276 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ ๐ด โ โ) |
20 | 8 | adantr 276 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ ๐ต โ โ) |
21 | | simp2 998 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ ๐ต โ
โ) |
22 | 21 | adantr 276 |
. . . . 5
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ ๐ต โ โ) |
23 | 22 | nngt0d 8963 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ 0 < ๐ต) |
24 | 21 | nnred 8932 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ ๐ต โ
โ) |
25 | 1 | nn0red 9230 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ ๐ด โ
โ) |
26 | 24, 25 | lenltd 8075 |
. . . . 5
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ (๐ต โค ๐ด โ ยฌ ๐ด < ๐ต)) |
27 | 26 | biimpar 297 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ ๐ต โค ๐ด) |
28 | | simpl3 1002 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ ๐ด < (2 ยท ๐ต)) |
29 | | q2submod 10385 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ต) โง (๐ต โค ๐ด โง ๐ด < (2 ยท ๐ต))) โ (๐ด mod ๐ต) = (๐ด โ ๐ต)) |
30 | 19, 20, 23, 27, 28, 29 | syl32anc 1246 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ (๐ด mod ๐ต) = (๐ด โ ๐ต)) |
31 | | iffalse 3543 |
. . . . 5
โข (ยฌ
๐ด < ๐ต โ if(๐ด < ๐ต, ๐ด, (๐ด โ ๐ต)) = (๐ด โ ๐ต)) |
32 | 31 | adantl 277 |
. . . 4
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ if(๐ด < ๐ต, ๐ด, (๐ด โ ๐ต)) = (๐ด โ ๐ต)) |
33 | 32 | eqcomd 2183 |
. . 3
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ (๐ด โ ๐ต) = if(๐ด < ๐ต, ๐ด, (๐ด โ ๐ต))) |
34 | 30, 33 | eqtrd 2210 |
. 2
โข (((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โง ยฌ ๐ด < ๐ต) โ (๐ด mod ๐ต) = if(๐ด < ๐ต, ๐ด, (๐ด โ ๐ต))) |
35 | 1, 2 | syl 14 |
. . 3
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ ๐ด โ
โค) |
36 | 21 | nnzd 9374 |
. . 3
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ ๐ต โ
โค) |
37 | | zdclt 9330 |
. . . 4
โข ((๐ด โ โค โง ๐ต โ โค) โ
DECID ๐ด <
๐ต) |
38 | | exmiddc 836 |
. . . 4
โข
(DECID ๐ด < ๐ต โ (๐ด < ๐ต โจ ยฌ ๐ด < ๐ต)) |
39 | 37, 38 | syl 14 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด < ๐ต โจ ยฌ ๐ด < ๐ต)) |
40 | 35, 36, 39 | syl2anc 411 |
. 2
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ (๐ด < ๐ต โจ ยฌ ๐ด < ๐ต)) |
41 | 18, 34, 40 | mpjaodan 798 |
1
โข ((๐ด โ โ0
โง ๐ต โ โ
โง ๐ด < (2 ยท
๐ต)) โ (๐ด mod ๐ต) = if(๐ด < ๐ต, ๐ด, (๐ด โ ๐ต))) |