Step | Hyp | Ref
| Expression |
1 | | simpr 483 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โค) |
2 | 1 | adantr 479 |
. . . . 5
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โค) |
3 | | eqcom 2737 |
. . . . . . . . 9
โข (๐ด = ((๐ ยท ๐) + ๐ต) โ ((๐ ยท ๐) + ๐ต) = ๐ด) |
4 | | nn0cn 12486 |
. . . . . . . . . . . 12
โข (๐ด โ โ0
โ ๐ด โ
โ) |
5 | 4 | adantr 479 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ด โ โ) |
6 | 5 | ad2antrr 722 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ด โ โ) |
7 | | nn0re 12485 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ0
โ ๐ด โ
โ) |
8 | | modcl 13842 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ โ โ+)
โ (๐ด mod ๐) โ
โ) |
9 | 7, 8 | sylan 578 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ด mod ๐) โ โ) |
10 | 9 | recnd 11246 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ด mod ๐) โ โ) |
11 | 10 | adantr 479 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ (๐ด mod ๐) โ โ) |
12 | | eleq1 2819 |
. . . . . . . . . . . . 13
โข ((๐ด mod ๐) = ๐ต โ ((๐ด mod ๐) โ โ โ ๐ต โ โ)) |
13 | 12 | adantl 480 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ((๐ด mod ๐) โ โ โ ๐ต โ โ)) |
14 | 11, 13 | mpbid 231 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ๐ต โ โ) |
15 | 14 | adantr 479 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ต โ โ) |
16 | | zcn 12567 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
17 | 16 | adantl 480 |
. . . . . . . . . . 11
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
18 | | rpcn 12988 |
. . . . . . . . . . . . 13
โข (๐ โ โ+
โ ๐ โ
โ) |
19 | 18 | adantl 480 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ โ โ) |
20 | 19 | ad2antrr 722 |
. . . . . . . . . . 11
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
21 | 17, 20 | mulcld 11238 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ ยท ๐) โ โ) |
22 | 6, 15, 21 | subadd2d 11594 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) = (๐ ยท ๐) โ ((๐ ยท ๐) + ๐ต) = ๐ด)) |
23 | 3, 22 | bitr4id 289 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
24 | 4 | ad2antrr 722 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ๐ด โ โ) |
25 | 24, 14 | subcld 11575 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ (๐ด โ ๐ต) โ โ) |
26 | 25 | adantr 479 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด โ ๐ต) โ โ) |
27 | | rpcnne0 12996 |
. . . . . . . . . . 11
โข (๐ โ โ+
โ (๐ โ โ
โง ๐ โ
0)) |
28 | 27 | adantl 480 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ โ โ โง ๐ โ 0)) |
29 | 28 | ad2antrr 722 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ โ โ โง ๐ โ 0)) |
30 | | divmul3 11881 |
. . . . . . . . 9
โข (((๐ด โ ๐ต) โ โ โง ๐ โ โ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
31 | 26, 17, 29, 30 | syl3anc 1369 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
32 | | oveq2 7419 |
. . . . . . . . . . . . . 14
โข (๐ต = (๐ด mod ๐) โ (๐ด โ ๐ต) = (๐ด โ (๐ด mod ๐))) |
33 | 32 | oveq1d 7426 |
. . . . . . . . . . . . 13
โข (๐ต = (๐ด mod ๐) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
34 | 33 | eqcoms 2738 |
. . . . . . . . . . . 12
โข ((๐ด mod ๐) = ๐ต โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
35 | 34 | adantl 480 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
36 | 35 | adantr 479 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
37 | | moddiffl 13851 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ+)
โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
38 | 7, 37 | sylan 578 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
39 | 38 | ad2antrr 722 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
40 | 36, 39 | eqtrd 2770 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) / ๐) = (โโ(๐ด / ๐))) |
41 | 40 | eqeq1d 2732 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (โโ(๐ด / ๐)) = ๐)) |
42 | 23, 31, 41 | 3bitr2d 306 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ (โโ(๐ด / ๐)) = ๐)) |
43 | | nn0ge0 12501 |
. . . . . . . . . . . 12
โข (๐ด โ โ0
โ 0 โค ๐ด) |
44 | 7, 43 | jca 510 |
. . . . . . . . . . 11
โข (๐ด โ โ0
โ (๐ด โ โ
โง 0 โค ๐ด)) |
45 | | rpregt0 12992 |
. . . . . . . . . . 11
โข (๐ โ โ+
โ (๐ โ โ
โง 0 < ๐)) |
46 | | divge0 12087 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ โ โ โง 0 < ๐)) โ 0 โค (๐ด / ๐)) |
47 | 44, 45, 46 | syl2an 594 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ 0 โค (๐ด / ๐)) |
48 | 7 | adantr 479 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ด โ โ) |
49 | | rpre 12986 |
. . . . . . . . . . . . 13
โข (๐ โ โ+
โ ๐ โ
โ) |
50 | 49 | adantl 480 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ โ โ) |
51 | | rpne0 12994 |
. . . . . . . . . . . . 13
โข (๐ โ โ+
โ ๐ โ
0) |
52 | 51 | adantl 480 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ โ 0) |
53 | 48, 50, 52 | redivcld 12046 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ด / ๐) โ โ) |
54 | | 0z 12573 |
. . . . . . . . . . 11
โข 0 โ
โค |
55 | | flge 13774 |
. . . . . . . . . . 11
โข (((๐ด / ๐) โ โ โง 0 โ โค)
โ (0 โค (๐ด / ๐) โ 0 โค
(โโ(๐ด / ๐)))) |
56 | 53, 54, 55 | sylancl 584 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (0 โค (๐ด / ๐) โ 0 โค (โโ(๐ด / ๐)))) |
57 | 47, 56 | mpbid 231 |
. . . . . . . . 9
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ 0 โค (โโ(๐ด / ๐))) |
58 | | breq2 5151 |
. . . . . . . . 9
โข
((โโ(๐ด /
๐)) = ๐ โ (0 โค (โโ(๐ด / ๐)) โ 0 โค ๐)) |
59 | 57, 58 | syl5ibcom 244 |
. . . . . . . 8
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((โโ(๐ด / ๐)) = ๐ โ 0 โค ๐)) |
60 | 59 | ad2antrr 722 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ
((โโ(๐ด / ๐)) = ๐ โ 0 โค ๐)) |
61 | 42, 60 | sylbid 239 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ 0 โค ๐)) |
62 | 61 | imp 405 |
. . . . 5
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ 0 โค ๐) |
63 | | elnn0z 12575 |
. . . . 5
โข (๐ โ โ0
โ (๐ โ โค
โง 0 โค ๐)) |
64 | 2, 62, 63 | sylanbrc 581 |
. . . 4
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โ0) |
65 | | oveq1 7418 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
66 | 65 | oveq1d 7426 |
. . . . . 6
โข (๐ = ๐ โ ((๐ ยท ๐) + ๐ต) = ((๐ ยท ๐) + ๐ต)) |
67 | 66 | eqeq2d 2741 |
. . . . 5
โข (๐ = ๐ โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + ๐ต))) |
68 | 67 | adantl 480 |
. . . 4
โข
((((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โง ๐ = ๐) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + ๐ต))) |
69 | | simpr 483 |
. . . 4
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ด = ((๐ ยท ๐) + ๐ต)) |
70 | 64, 68, 69 | rspcedvd 3613 |
. . 3
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต)) |
71 | | nn0z 12587 |
. . . . 5
โข (๐ด โ โ0
โ ๐ด โ
โค) |
72 | | modmuladdim 13883 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ โ+)
โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |
73 | 71, 72 | sylan 578 |
. . . 4
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |
74 | 73 | imp 405 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต)) |
75 | 70, 74 | r19.29a 3160 |
. 2
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต)) |
76 | 75 | ex 411 |
1
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต))) |