Step | Hyp | Ref
| Expression |
1 | | nnq 9635 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
2 | 1 | 3ad2ant1 1018 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
3 | | flqcl 10275 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โค) |
4 | | zq 9628 |
. . . . . . 7
โข
((โโ๐ด)
โ โค โ (โโ๐ด) โ โ) |
5 | 3, 4 | syl 14 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
6 | 5 | 3ad2ant2 1019 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ๐ด) โ
โ) |
7 | | qmulcl 9639 |
. . . . 5
โข ((๐ โ โ โง
(โโ๐ด) โ
โ) โ (๐ ยท
(โโ๐ด)) โ
โ) |
8 | 2, 6, 7 | syl2anc 411 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ (๐ ยท (โโ๐ด)) โ
โ) |
9 | | qre 9627 |
. . . 4
โข ((๐ ยท (โโ๐ด)) โ โ โ (๐ ยท (โโ๐ด)) โ
โ) |
10 | 8, 9 | syl 14 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ (๐ ยท (โโ๐ด)) โ
โ) |
11 | | simp2 998 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ด โ
โ) |
12 | | qmulcl 9639 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ ยท ๐ด) โ โ) |
13 | 2, 11, 12 | syl2anc 411 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ (๐ ยท ๐ด) โ โ) |
14 | 13 | flqcld 10279 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ(๐ ยท
๐ด)) โ
โค) |
15 | 14 | zred 9377 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ(๐ ยท
๐ด)) โ
โ) |
16 | | nnmulcl 8942 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
17 | | nnq 9635 |
. . . . . . 7
โข ((๐ ยท ๐) โ โ โ (๐ ยท ๐) โ โ) |
18 | 16, 17 | syl 14 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
19 | 18 | 3adant2 1016 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
20 | | qre 9627 |
. . . . 5
โข ((๐ ยท ๐) โ โ โ (๐ ยท ๐) โ โ) |
21 | 19, 20 | syl 14 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
22 | | simp1 997 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
23 | 22 | nncnd 8935 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
24 | | simp3 999 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
25 | 24 | nncnd 8935 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
26 | 22 | nnap0d 8967 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ # 0) |
27 | 24 | nnap0d 8967 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ # 0) |
28 | 23, 25, 26, 27 | mulap0d 8617 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ (๐ ยท ๐) # 0) |
29 | | 0z 9266 |
. . . . . . . . . 10
โข 0 โ
โค |
30 | | zq 9628 |
. . . . . . . . . 10
โข (0 โ
โค โ 0 โ โ) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
โข 0 โ
โ |
32 | | qapne 9641 |
. . . . . . . . 9
โข (((๐ ยท ๐) โ โ โง 0 โ โ)
โ ((๐ ยท ๐) # 0 โ (๐ ยท ๐) โ 0)) |
33 | 19, 31, 32 | sylancl 413 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ ยท ๐) # 0 โ (๐ ยท ๐) โ 0)) |
34 | 28, 33 | mpbid 147 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ 0) |
35 | | qdivcl 9645 |
. . . . . . 7
โข (((๐ ยท (โโ๐ด)) โ โ โง (๐ ยท ๐) โ โ โง (๐ ยท ๐) โ 0) โ ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)) โ โ) |
36 | 8, 19, 34, 35 | syl3anc 1238 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)) โ โ) |
37 | 36 | flqcld 10279 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ((๐ ยท
(โโ๐ด)) / (๐ ยท ๐))) โ โค) |
38 | 37 | zred 9377 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ((๐ ยท
(โโ๐ด)) / (๐ ยท ๐))) โ โ) |
39 | 21, 38 | remulcld 7990 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ ยท ๐) ยท (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)))) โ โ) |
40 | | nnnn0 9185 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ0) |
41 | | flqmulnn0 10301 |
. . . . 5
โข ((๐ โ โ0
โง ๐ด โ โ)
โ (๐ ยท
(โโ๐ด)) โค
(โโ(๐ ยท
๐ด))) |
42 | 40, 41 | sylan 283 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ ยท (โโ๐ด)) โค (โโ(๐ ยท ๐ด))) |
43 | 22, 11, 42 | syl2anc 411 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ (๐ ยท (โโ๐ด)) โค (โโ(๐ ยท ๐ด))) |
44 | 10, 15, 39, 43 | lesub1dd 8520 |
. 2
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ ยท (โโ๐ด)) โ ((๐ ยท ๐) ยท (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐))))) โค ((โโ(๐ ยท ๐ด)) โ ((๐ ยท ๐) ยท (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)))))) |
45 | 22 | nnred 8934 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
46 | 24 | nnred 8934 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
47 | 22 | nngt0d 8965 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ 0 <
๐) |
48 | 24 | nngt0d 8965 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ 0 <
๐) |
49 | 45, 46, 47, 48 | mulgt0d 8082 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ 0 <
(๐ ยท ๐)) |
50 | | modqval 10326 |
. . 3
โข (((๐ ยท (โโ๐ด)) โ โ โง (๐ ยท ๐) โ โ โง 0 < (๐ ยท ๐)) โ ((๐ ยท (โโ๐ด)) mod (๐ ยท ๐)) = ((๐ ยท (โโ๐ด)) โ ((๐ ยท ๐) ยท (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)))))) |
51 | 8, 19, 49, 50 | syl3anc 1238 |
. 2
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ ยท (โโ๐ด)) mod (๐ ยท ๐)) = ((๐ ยท (โโ๐ด)) โ ((๐ ยท ๐) ยท (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)))))) |
52 | | zq 9628 |
. . . . 5
โข
((โโ(๐
ยท ๐ด)) โ โค
โ (โโ(๐
ยท ๐ด)) โ
โ) |
53 | 14, 52 | syl 14 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ(๐ ยท
๐ด)) โ
โ) |
54 | | modqval 10326 |
. . . 4
โข
(((โโ(๐
ยท ๐ด)) โ โ
โง (๐ ยท ๐) โ โ โง 0 <
(๐ ยท ๐)) โ ((โโ(๐ ยท ๐ด)) mod (๐ ยท ๐)) = ((โโ(๐ ยท ๐ด)) โ ((๐ ยท ๐) ยท
(โโ((โโ(๐ ยท ๐ด)) / (๐ ยท ๐)))))) |
55 | 53, 19, 49, 54 | syl3anc 1238 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
((โโ(๐ ยท
๐ด)) mod (๐ ยท ๐)) = ((โโ(๐ ยท ๐ด)) โ ((๐ ยท ๐) ยท
(โโ((โโ(๐ ยท ๐ด)) / (๐ ยท ๐)))))) |
56 | 16 | 3adant2 1016 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
57 | | flqdiv 10323 |
. . . . . . 7
โข (((๐ ยท ๐ด) โ โ โง (๐ ยท ๐) โ โ) โ
(โโ((โโ(๐ ยท ๐ด)) / (๐ ยท ๐))) = (โโ((๐ ยท ๐ด) / (๐ ยท ๐)))) |
58 | 13, 56, 57 | syl2anc 411 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ((โโ(๐ ยท ๐ด)) / (๐ ยท ๐))) = (โโ((๐ ยท ๐ด) / (๐ ยท ๐)))) |
59 | | flqdiv 10323 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ
(โโ((โโ๐ด) / ๐)) = (โโ(๐ด / ๐))) |
60 | 59 | 3adant1 1015 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ((โโ๐ด) / ๐)) = (โโ(๐ด / ๐))) |
61 | 3 | zcnd 9378 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
62 | 11, 61 | syl 14 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ๐ด) โ
โ) |
63 | 62, 25, 23, 27, 26 | divcanap5d 8776 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)) = ((โโ๐ด) / ๐)) |
64 | 63 | fveq2d 5521 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ((๐ ยท
(โโ๐ด)) / (๐ ยท ๐))) = (โโ((โโ๐ด) / ๐))) |
65 | | qcn 9636 |
. . . . . . . . . 10
โข (๐ด โ โ โ ๐ด โ
โ) |
66 | 11, 65 | syl 14 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ๐ด โ
โ) |
67 | 66, 25, 23, 27, 26 | divcanap5d 8776 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ ยท ๐ด) / (๐ ยท ๐)) = (๐ด / ๐)) |
68 | 67 | fveq2d 5521 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ((๐ ยท
๐ด) / (๐ ยท ๐))) = (โโ(๐ด / ๐))) |
69 | 60, 64, 68 | 3eqtr4rd 2221 |
. . . . . 6
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ((๐ ยท
๐ด) / (๐ ยท ๐))) = (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)))) |
70 | 58, 69 | eqtrd 2210 |
. . . . 5
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
(โโ((โโ(๐ ยท ๐ด)) / (๐ ยท ๐))) = (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)))) |
71 | 70 | oveq2d 5893 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ ยท ๐) ยท
(โโ((โโ(๐ ยท ๐ด)) / (๐ ยท ๐)))) = ((๐ ยท ๐) ยท (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐))))) |
72 | 71 | oveq2d 5893 |
. . 3
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
((โโ(๐ ยท
๐ด)) โ ((๐ ยท ๐) ยท
(โโ((โโ(๐ ยท ๐ด)) / (๐ ยท ๐))))) = ((โโ(๐ ยท ๐ด)) โ ((๐ ยท ๐) ยท (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)))))) |
73 | 55, 72 | eqtrd 2210 |
. 2
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ
((โโ(๐ ยท
๐ด)) mod (๐ ยท ๐)) = ((โโ(๐ ยท ๐ด)) โ ((๐ ยท ๐) ยท (โโ((๐ ยท (โโ๐ด)) / (๐ ยท ๐)))))) |
74 | 44, 51, 73 | 3brtr4d 4037 |
1
โข ((๐ โ โ โง ๐ด โ โ โง ๐ โ โ) โ ((๐ ยท (โโ๐ด)) mod (๐ ยท ๐)) โค ((โโ(๐ ยท ๐ด)) mod (๐ ยท ๐))) |