Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โค) |
2 | 1 | adantr 481 |
. . . . 5
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โค) |
3 | | eqcom 2739 |
. . . . . . . . 9
โข (๐ด = ((๐ ยท ๐) + ๐ต) โ ((๐ ยท ๐) + ๐ต) = ๐ด) |
4 | | nn0cn 12481 |
. . . . . . . . . . . 12
โข (๐ด โ โ0
โ ๐ด โ
โ) |
5 | 4 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ด โ โ) |
6 | 5 | ad2antrr 724 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ด โ โ) |
7 | | nn0re 12480 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ0
โ ๐ด โ
โ) |
8 | | modcl 13837 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ โ โ+)
โ (๐ด mod ๐) โ
โ) |
9 | 7, 8 | sylan 580 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ด mod ๐) โ โ) |
10 | 9 | recnd 11241 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ด mod ๐) โ โ) |
11 | 10 | adantr 481 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ (๐ด mod ๐) โ โ) |
12 | | eleq1 2821 |
. . . . . . . . . . . . 13
โข ((๐ด mod ๐) = ๐ต โ ((๐ด mod ๐) โ โ โ ๐ต โ โ)) |
13 | 12 | adantl 482 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ((๐ด mod ๐) โ โ โ ๐ต โ โ)) |
14 | 11, 13 | mpbid 231 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ๐ต โ โ) |
15 | 14 | adantr 481 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ต โ โ) |
16 | | zcn 12562 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
17 | 16 | adantl 482 |
. . . . . . . . . . 11
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
18 | | rpcn 12983 |
. . . . . . . . . . . . 13
โข (๐ โ โ+
โ ๐ โ
โ) |
19 | 18 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ โ โ) |
20 | 19 | ad2antrr 724 |
. . . . . . . . . . 11
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
21 | 17, 20 | mulcld 11233 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ ยท ๐) โ โ) |
22 | 6, 15, 21 | subadd2d 11589 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) = (๐ ยท ๐) โ ((๐ ยท ๐) + ๐ต) = ๐ด)) |
23 | 3, 22 | bitr4id 289 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
24 | 4 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ๐ด โ โ) |
25 | 24, 14 | subcld 11570 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ (๐ด โ ๐ต) โ โ) |
26 | 25 | adantr 481 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด โ ๐ต) โ โ) |
27 | | rpcnne0 12991 |
. . . . . . . . . . 11
โข (๐ โ โ+
โ (๐ โ โ
โง ๐ โ
0)) |
28 | 27 | adantl 482 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ โ โ โง ๐ โ 0)) |
29 | 28 | ad2antrr 724 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ โ โ โง ๐ โ 0)) |
30 | | divmul3 11876 |
. . . . . . . . 9
โข (((๐ด โ ๐ต) โ โ โง ๐ โ โ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
31 | 26, 17, 29, 30 | syl3anc 1371 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
32 | | oveq2 7416 |
. . . . . . . . . . . . . 14
โข (๐ต = (๐ด mod ๐) โ (๐ด โ ๐ต) = (๐ด โ (๐ด mod ๐))) |
33 | 32 | oveq1d 7423 |
. . . . . . . . . . . . 13
โข (๐ต = (๐ด mod ๐) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
34 | 33 | eqcoms 2740 |
. . . . . . . . . . . 12
โข ((๐ด mod ๐) = ๐ต โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
35 | 34 | adantl 482 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
36 | 35 | adantr 481 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
37 | | moddiffl 13846 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ+)
โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
38 | 7, 37 | sylan 580 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
39 | 38 | ad2antrr 724 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
40 | 36, 39 | eqtrd 2772 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) / ๐) = (โโ(๐ด / ๐))) |
41 | 40 | eqeq1d 2734 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (โโ(๐ด / ๐)) = ๐)) |
42 | 23, 31, 41 | 3bitr2d 306 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ (โโ(๐ด / ๐)) = ๐)) |
43 | | nn0ge0 12496 |
. . . . . . . . . . . 12
โข (๐ด โ โ0
โ 0 โค ๐ด) |
44 | 7, 43 | jca 512 |
. . . . . . . . . . 11
โข (๐ด โ โ0
โ (๐ด โ โ
โง 0 โค ๐ด)) |
45 | | rpregt0 12987 |
. . . . . . . . . . 11
โข (๐ โ โ+
โ (๐ โ โ
โง 0 < ๐)) |
46 | | divge0 12082 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ โ โ โง 0 < ๐)) โ 0 โค (๐ด / ๐)) |
47 | 44, 45, 46 | syl2an 596 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ 0 โค (๐ด / ๐)) |
48 | 7 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ด โ โ) |
49 | | rpre 12981 |
. . . . . . . . . . . . 13
โข (๐ โ โ+
โ ๐ โ
โ) |
50 | 49 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ โ โ) |
51 | | rpne0 12989 |
. . . . . . . . . . . . 13
โข (๐ โ โ+
โ ๐ โ
0) |
52 | 51 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ โ 0) |
53 | 48, 50, 52 | redivcld 12041 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ด / ๐) โ โ) |
54 | | 0z 12568 |
. . . . . . . . . . 11
โข 0 โ
โค |
55 | | flge 13769 |
. . . . . . . . . . 11
โข (((๐ด / ๐) โ โ โง 0 โ โค)
โ (0 โค (๐ด / ๐) โ 0 โค
(โโ(๐ด / ๐)))) |
56 | 53, 54, 55 | sylancl 586 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (0 โค (๐ด / ๐) โ 0 โค (โโ(๐ด / ๐)))) |
57 | 47, 56 | mpbid 231 |
. . . . . . . . 9
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ 0 โค (โโ(๐ด / ๐))) |
58 | | breq2 5152 |
. . . . . . . . 9
โข
((โโ(๐ด /
๐)) = ๐ โ (0 โค (โโ(๐ด / ๐)) โ 0 โค ๐)) |
59 | 57, 58 | syl5ibcom 244 |
. . . . . . . 8
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((โโ(๐ด / ๐)) = ๐ โ 0 โค ๐)) |
60 | 59 | ad2antrr 724 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ
((โโ(๐ด / ๐)) = ๐ โ 0 โค ๐)) |
61 | 42, 60 | sylbid 239 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ 0 โค ๐)) |
62 | 61 | imp 407 |
. . . . 5
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ 0 โค ๐) |
63 | | elnn0z 12570 |
. . . . 5
โข (๐ โ โ0
โ (๐ โ โค
โง 0 โค ๐)) |
64 | 2, 62, 63 | sylanbrc 583 |
. . . 4
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โ0) |
65 | | oveq1 7415 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
66 | 65 | oveq1d 7423 |
. . . . . 6
โข (๐ = ๐ โ ((๐ ยท ๐) + ๐ต) = ((๐ ยท ๐) + ๐ต)) |
67 | 66 | eqeq2d 2743 |
. . . . 5
โข (๐ = ๐ โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + ๐ต))) |
68 | 67 | adantl 482 |
. . . 4
โข
((((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โง ๐ = ๐) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + ๐ต))) |
69 | | simpr 485 |
. . . 4
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ด = ((๐ ยท ๐) + ๐ต)) |
70 | 64, 68, 69 | rspcedvd 3614 |
. . 3
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต)) |
71 | | nn0z 12582 |
. . . . 5
โข (๐ด โ โ0
โ ๐ด โ
โค) |
72 | | modmuladdim 13878 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ โ+)
โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |
73 | 71, 72 | sylan 580 |
. . . 4
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |
74 | 73 | imp 407 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต)) |
75 | 70, 74 | r19.29a 3162 |
. 2
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต)) |
76 | 75 | ex 413 |
1
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต))) |