Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โค) |
2 | 1 | adantr 482 |
. . . . 5
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โค) |
3 | | eqcom 2740 |
. . . . . . . . 9
โข (๐ด = ((๐ ยท ๐) + ๐ต) โ ((๐ ยท ๐) + ๐ต) = ๐ด) |
4 | | nn0cn 12482 |
. . . . . . . . . . . 12
โข (๐ด โ โ0
โ ๐ด โ
โ) |
5 | 4 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ด โ โ) |
6 | 5 | ad2antrr 725 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ด โ โ) |
7 | | nn0re 12481 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ0
โ ๐ด โ
โ) |
8 | | modcl 13838 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ โ โ+)
โ (๐ด mod ๐) โ
โ) |
9 | 7, 8 | sylan 581 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ด mod ๐) โ โ) |
10 | 9 | recnd 11242 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ด mod ๐) โ โ) |
11 | 10 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ (๐ด mod ๐) โ โ) |
12 | | eleq1 2822 |
. . . . . . . . . . . . 13
โข ((๐ด mod ๐) = ๐ต โ ((๐ด mod ๐) โ โ โ ๐ต โ โ)) |
13 | 12 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ((๐ด mod ๐) โ โ โ ๐ต โ โ)) |
14 | 11, 13 | mpbid 231 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ๐ต โ โ) |
15 | 14 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ต โ โ) |
16 | | zcn 12563 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
17 | 16 | adantl 483 |
. . . . . . . . . . 11
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
18 | | rpcn 12984 |
. . . . . . . . . . . . 13
โข (๐ โ โ+
โ ๐ โ
โ) |
19 | 18 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ โ โ) |
20 | 19 | ad2antrr 725 |
. . . . . . . . . . 11
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
21 | 17, 20 | mulcld 11234 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ ยท ๐) โ โ) |
22 | 6, 15, 21 | subadd2d 11590 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) = (๐ ยท ๐) โ ((๐ ยท ๐) + ๐ต) = ๐ด)) |
23 | 3, 22 | bitr4id 290 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
24 | 4 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ๐ด โ โ) |
25 | 24, 14 | subcld 11571 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ (๐ด โ ๐ต) โ โ) |
26 | 25 | adantr 482 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด โ ๐ต) โ โ) |
27 | | rpcnne0 12992 |
. . . . . . . . . . 11
โข (๐ โ โ+
โ (๐ โ โ
โง ๐ โ
0)) |
28 | 27 | adantl 483 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ โ โ โง ๐ โ 0)) |
29 | 28 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ โ โ โง ๐ โ 0)) |
30 | | divmul3 11877 |
. . . . . . . . 9
โข (((๐ด โ ๐ต) โ โ โง ๐ โ โ โง (๐ โ โ โง ๐ โ 0)) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
31 | 26, 17, 29, 30 | syl3anc 1372 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
32 | | oveq2 7417 |
. . . . . . . . . . . . . 14
โข (๐ต = (๐ด mod ๐) โ (๐ด โ ๐ต) = (๐ด โ (๐ด mod ๐))) |
33 | 32 | oveq1d 7424 |
. . . . . . . . . . . . 13
โข (๐ต = (๐ด mod ๐) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
34 | 33 | eqcoms 2741 |
. . . . . . . . . . . 12
โข ((๐ด mod ๐) = ๐ต โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
35 | 34 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
36 | 35 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
37 | | moddiffl 13847 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ+)
โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
38 | 7, 37 | sylan 581 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
40 | 36, 39 | eqtrd 2773 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) / ๐) = (โโ(๐ด / ๐))) |
41 | 40 | eqeq1d 2735 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (โโ(๐ด / ๐)) = ๐)) |
42 | 23, 31, 41 | 3bitr2d 307 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ (โโ(๐ด / ๐)) = ๐)) |
43 | | nn0ge0 12497 |
. . . . . . . . . . . 12
โข (๐ด โ โ0
โ 0 โค ๐ด) |
44 | 7, 43 | jca 513 |
. . . . . . . . . . 11
โข (๐ด โ โ0
โ (๐ด โ โ
โง 0 โค ๐ด)) |
45 | | rpregt0 12988 |
. . . . . . . . . . 11
โข (๐ โ โ+
โ (๐ โ โ
โง 0 < ๐)) |
46 | | divge0 12083 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ โ โ โง 0 < ๐)) โ 0 โค (๐ด / ๐)) |
47 | 44, 45, 46 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ 0 โค (๐ด / ๐)) |
48 | 7 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ด โ โ) |
49 | | rpre 12982 |
. . . . . . . . . . . . 13
โข (๐ โ โ+
โ ๐ โ
โ) |
50 | 49 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ โ โ) |
51 | | rpne0 12990 |
. . . . . . . . . . . . 13
โข (๐ โ โ+
โ ๐ โ
0) |
52 | 51 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ๐ โ 0) |
53 | 48, 50, 52 | redivcld 12042 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (๐ด / ๐) โ โ) |
54 | | 0z 12569 |
. . . . . . . . . . 11
โข 0 โ
โค |
55 | | flge 13770 |
. . . . . . . . . . 11
โข (((๐ด / ๐) โ โ โง 0 โ โค)
โ (0 โค (๐ด / ๐) โ 0 โค
(โโ(๐ด / ๐)))) |
56 | 53, 54, 55 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ (0 โค (๐ด / ๐) โ 0 โค (โโ(๐ด / ๐)))) |
57 | 47, 56 | mpbid 231 |
. . . . . . . . 9
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ 0 โค (โโ(๐ด / ๐))) |
58 | | breq2 5153 |
. . . . . . . . 9
โข
((โโ(๐ด /
๐)) = ๐ โ (0 โค (โโ(๐ด / ๐)) โ 0 โค ๐)) |
59 | 57, 58 | syl5ibcom 244 |
. . . . . . . 8
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((โโ(๐ด / ๐)) = ๐ โ 0 โค ๐)) |
60 | 59 | ad2antrr 725 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ
((โโ(๐ด / ๐)) = ๐ โ 0 โค ๐)) |
61 | 42, 60 | sylbid 239 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ 0 โค ๐)) |
62 | 61 | imp 408 |
. . . . 5
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ 0 โค ๐) |
63 | | elnn0z 12571 |
. . . . 5
โข (๐ โ โ0
โ (๐ โ โค
โง 0 โค ๐)) |
64 | 2, 62, 63 | sylanbrc 584 |
. . . 4
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โ0) |
65 | | oveq1 7416 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
66 | 65 | oveq1d 7424 |
. . . . . 6
โข (๐ = ๐ โ ((๐ ยท ๐) + ๐ต) = ((๐ ยท ๐) + ๐ต)) |
67 | 66 | eqeq2d 2744 |
. . . . 5
โข (๐ = ๐ โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + ๐ต))) |
68 | 67 | adantl 483 |
. . . 4
โข
((((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โง ๐ = ๐) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + ๐ต))) |
69 | | simpr 486 |
. . . 4
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ด = ((๐ ยท ๐) + ๐ต)) |
70 | 64, 68, 69 | rspcedvd 3615 |
. . 3
โข
(((((๐ด โ
โ0 โง ๐
โ โ+) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต)) |
71 | | nn0z 12583 |
. . . . 5
โข (๐ด โ โ0
โ ๐ด โ
โค) |
72 | | modmuladdim 13879 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ โ+)
โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |
73 | 71, 72 | sylan 581 |
. . . 4
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |
74 | 73 | imp 408 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต)) |
75 | 70, 74 | r19.29a 3163 |
. 2
โข (((๐ด โ โ0
โง ๐ โ
โ+) โง (๐ด mod ๐) = ๐ต) โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต)) |
76 | 75 | ex 414 |
1
โข ((๐ด โ โ0
โง ๐ โ
โ+) โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต))) |