Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โค) |
2 | 1 | adantr 276 |
. . . . 5
โข
(((((๐ด โ
โ0 โง ๐
โ โ โง 0 < ๐) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โค) |
3 | | eqcom 2179 |
. . . . . . . . 9
โข (๐ด = ((๐ ยท ๐) + ๐ต) โ ((๐ ยท ๐) + ๐ต) = ๐ด) |
4 | | nn0cn 9185 |
. . . . . . . . . . . 12
โข (๐ด โ โ0
โ ๐ด โ
โ) |
5 | 4 | 3ad2ant1 1018 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
๐ด โ
โ) |
6 | 5 | ad2antrr 488 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ด โ โ) |
7 | | nn0z 9272 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โ0
โ ๐ด โ
โค) |
8 | | zq 9625 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โค โ ๐ด โ
โ) |
9 | 7, 8 | syl 14 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โ0
โ ๐ด โ
โ) |
10 | 9 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
๐ด โ
โ) |
11 | 10 | adantr 276 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ ๐ด โ โ) |
12 | | simpl2 1001 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ ๐ โ โ) |
13 | | simpl3 1002 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ 0 < ๐) |
14 | 11, 12, 13 | modqcld 10327 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ (๐ด mod ๐) โ โ) |
15 | | qcn 9633 |
. . . . . . . . . . . . 13
โข ((๐ด mod ๐) โ โ โ (๐ด mod ๐) โ โ) |
16 | 14, 15 | syl 14 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ (๐ด mod ๐) โ โ) |
17 | | eleq1 2240 |
. . . . . . . . . . . . 13
โข ((๐ด mod ๐) = ๐ต โ ((๐ด mod ๐) โ โ โ ๐ต โ โ)) |
18 | 17 | adantl 277 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ ((๐ด mod ๐) โ โ โ ๐ต โ โ)) |
19 | 16, 18 | mpbid 147 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ ๐ต โ โ) |
20 | 19 | adantr 276 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ต โ โ) |
21 | | zcn 9257 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
22 | 21 | adantl 277 |
. . . . . . . . . . 11
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
23 | | qcn 9633 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
24 | 12, 23 | syl 14 |
. . . . . . . . . . . 12
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ ๐ โ โ) |
25 | 24 | adantr 276 |
. . . . . . . . . . 11
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
26 | 22, 25 | mulcld 7977 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ ยท ๐) โ โ) |
27 | 6, 20, 26 | subadd2d 8286 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) = (๐ ยท ๐) โ ((๐ ยท ๐) + ๐ต) = ๐ด)) |
28 | 3, 27 | bitr4id 199 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
29 | 5 | adantr 276 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ ๐ด โ โ) |
30 | 29, 19 | subcld 8267 |
. . . . . . . . . 10
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ (๐ด โ ๐ต) โ โ) |
31 | 30 | adantr 276 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด โ ๐ต) โ โ) |
32 | | qre 9624 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
33 | 32 | 3ad2ant2 1019 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
๐ โ
โ) |
34 | 33 | ad2antrr 488 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ โ โ) |
35 | 13 | adantr 276 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ 0 < ๐) |
36 | 34, 35 | gt0ap0d 8585 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ๐ # 0) |
37 | 31, 22, 25, 36 | divmulap3d 8781 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (๐ด โ ๐ต) = (๐ ยท ๐))) |
38 | | oveq2 5882 |
. . . . . . . . . . . . . 14
โข (๐ต = (๐ด mod ๐) โ (๐ด โ ๐ต) = (๐ด โ (๐ด mod ๐))) |
39 | 38 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข (๐ต = (๐ด mod ๐) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
40 | 39 | eqcoms 2180 |
. . . . . . . . . . . 12
โข ((๐ด mod ๐) = ๐ต โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
41 | 40 | adantl 277 |
. . . . . . . . . . 11
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
42 | 41 | adantr 276 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) / ๐) = ((๐ด โ (๐ด mod ๐)) / ๐)) |
43 | | modqdiffl 10334 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ โง 0 <
๐) โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
44 | 9, 43 | syl3an1 1271 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
45 | 44 | ad2antrr 488 |
. . . . . . . . . 10
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ (๐ด mod ๐)) / ๐) = (โโ(๐ด / ๐))) |
46 | 42, 45 | eqtrd 2210 |
. . . . . . . . 9
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ ((๐ด โ ๐ต) / ๐) = (โโ(๐ด / ๐))) |
47 | 46 | eqeq1d 2186 |
. . . . . . . 8
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (((๐ด โ ๐ต) / ๐) = ๐ โ (โโ(๐ด / ๐)) = ๐)) |
48 | 28, 37, 47 | 3bitr2d 216 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ (โโ(๐ด / ๐)) = ๐)) |
49 | | qre 9624 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด โ
โ) |
50 | 10, 49 | syl 14 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
๐ด โ
โ) |
51 | | nn0ge0 9200 |
. . . . . . . . . . . 12
โข (๐ด โ โ0
โ 0 โค ๐ด) |
52 | 51 | 3ad2ant1 1018 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ 0
โค ๐ด) |
53 | | simp3 999 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ 0
< ๐) |
54 | | divge0 8829 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ โ โ โง 0 < ๐)) โ 0 โค (๐ด / ๐)) |
55 | 50, 52, 33, 53, 54 | syl22anc 1239 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ 0
โค (๐ด / ๐)) |
56 | | simp2 998 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
๐ โ
โ) |
57 | 53 | gt0ne0d 8468 |
. . . . . . . . . . . 12
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
๐ โ 0) |
58 | | qdivcl 9642 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ โ โ โง ๐ โ 0) โ (๐ด / ๐) โ โ) |
59 | 10, 56, 57, 58 | syl3anc 1238 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
(๐ด / ๐) โ โ) |
60 | | 0z 9263 |
. . . . . . . . . . 11
โข 0 โ
โค |
61 | | flqge 10281 |
. . . . . . . . . . 11
โข (((๐ด / ๐) โ โ โง 0 โ โค)
โ (0 โค (๐ด / ๐) โ 0 โค
(โโ(๐ด / ๐)))) |
62 | 59, 60, 61 | sylancl 413 |
. . . . . . . . . 10
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ (0
โค (๐ด / ๐) โ 0 โค (โโ(๐ด / ๐)))) |
63 | 55, 62 | mpbid 147 |
. . . . . . . . 9
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ 0
โค (โโ(๐ด /
๐))) |
64 | | breq2 4007 |
. . . . . . . . 9
โข
((โโ(๐ด /
๐)) = ๐ โ (0 โค (โโ(๐ด / ๐)) โ 0 โค ๐)) |
65 | 63, 64 | syl5ibcom 155 |
. . . . . . . 8
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
((โโ(๐ด / ๐)) = ๐ โ 0 โค ๐)) |
66 | 65 | ad2antrr 488 |
. . . . . . 7
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ
((โโ(๐ด / ๐)) = ๐ โ 0 โค ๐)) |
67 | 48, 66 | sylbid 150 |
. . . . . 6
โข ((((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โง ๐ โ โค) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ 0 โค ๐)) |
68 | 67 | imp 124 |
. . . . 5
โข
(((((๐ด โ
โ0 โง ๐
โ โ โง 0 < ๐) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ 0 โค ๐) |
69 | | elnn0z 9265 |
. . . . 5
โข (๐ โ โ0
โ (๐ โ โค
โง 0 โค ๐)) |
70 | 2, 68, 69 | sylanbrc 417 |
. . . 4
โข
(((((๐ด โ
โ0 โง ๐
โ โ โง 0 < ๐) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ โ โ0) |
71 | | oveq1 5881 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
72 | 71 | oveq1d 5889 |
. . . . . 6
โข (๐ = ๐ โ ((๐ ยท ๐) + ๐ต) = ((๐ ยท ๐) + ๐ต)) |
73 | 72 | eqeq2d 2189 |
. . . . 5
โข (๐ = ๐ โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + ๐ต))) |
74 | 73 | adantl 277 |
. . . 4
โข
((((((๐ด โ
โ0 โง ๐
โ โ โง 0 < ๐) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โง ๐ = ๐) โ (๐ด = ((๐ ยท ๐) + ๐ต) โ ๐ด = ((๐ ยท ๐) + ๐ต))) |
75 | | simpr 110 |
. . . 4
โข
(((((๐ด โ
โ0 โง ๐
โ โ โง 0 < ๐) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ ๐ด = ((๐ ยท ๐) + ๐ต)) |
76 | 70, 74, 75 | rspcedvd 2847 |
. . 3
โข
(((((๐ด โ
โ0 โง ๐
โ โ โง 0 < ๐) โง (๐ด mod ๐) = ๐ต) โง ๐ โ โค) โง ๐ด = ((๐ ยท ๐) + ๐ต)) โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต)) |
77 | | modqmuladdim 10366 |
. . . . 5
โข ((๐ด โ โค โง ๐ โ โ โง 0 <
๐) โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |
78 | 7, 77 | syl3an1 1271 |
. . . 4
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) |
79 | 78 | imp 124 |
. . 3
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต)) |
80 | 76, 79 | r19.29a 2620 |
. 2
โข (((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โง
(๐ด mod ๐) = ๐ต) โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต)) |
81 | 80 | ex 115 |
1
โข ((๐ด โ โ0
โง ๐ โ โ
โง 0 < ๐) โ
((๐ด mod ๐) = ๐ต โ โ๐ โ โ0 ๐ด = ((๐ ยท ๐) + ๐ต))) |