Step | Hyp | Ref
| Expression |
1 | | fzssuz 13488 |
. . . 4
โข
(0...๐ต) โ
(โคโฅโ0) |
2 | | uzssz 12789 |
. . . . 5
โข
(โคโฅโ0) โ โค |
3 | | zssre 12511 |
. . . . 5
โข โค
โ โ |
4 | 2, 3 | sstri 3954 |
. . . 4
โข
(โคโฅโ0) โ โ |
5 | 1, 4 | sstri 3954 |
. . 3
โข
(0...๐ต) โ
โ |
6 | 5 | a1i 11 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ (0...๐ต) โ
โ) |
7 | | ovexd 7393 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ (0...(๐ต โ 1))
โ V) |
8 | | nnm1nn0 12459 |
. . . . 5
โข (๐ต โ โ โ (๐ต โ 1) โ
โ0) |
9 | 8 | adantl 483 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ (๐ต โ 1) โ
โ0) |
10 | | nn0uz 12810 |
. . . 4
โข
โ0 = (โคโฅโ0) |
11 | 9, 10 | eleqtrdi 2844 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ (๐ต โ 1) โ
(โคโฅโ0)) |
12 | | nnz 12525 |
. . . 4
โข (๐ต โ โ โ ๐ต โ
โค) |
13 | 12 | adantl 483 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ ๐ต โ
โค) |
14 | | nnre 12165 |
. . . . 5
โข (๐ต โ โ โ ๐ต โ
โ) |
15 | 14 | adantl 483 |
. . . 4
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ ๐ต โ
โ) |
16 | 15 | ltm1d 12092 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ (๐ต โ 1) <
๐ต) |
17 | | fzsdom2 14334 |
. . 3
โข ((((๐ต โ 1) โ
(โคโฅโ0) โง ๐ต โ โค) โง (๐ต โ 1) < ๐ต) โ (0...(๐ต โ 1)) โบ (0...๐ต)) |
18 | 11, 13, 16, 17 | syl21anc 837 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ (0...(๐ต โ 1))
โบ (0...๐ต)) |
19 | 14 | ad2antlr 726 |
. . . . . 6
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ๐ต โ โ) |
20 | | rpre 12928 |
. . . . . . . . 9
โข (๐ด โ โ+
โ ๐ด โ
โ) |
21 | 20 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ๐ด โ โ) |
22 | | elfzelz 13447 |
. . . . . . . . . 10
โข (๐ โ (0...๐ต) โ ๐ โ โค) |
23 | 22 | zred 12612 |
. . . . . . . . 9
โข (๐ โ (0...๐ต) โ ๐ โ โ) |
24 | 23 | adantl 483 |
. . . . . . . 8
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ๐ โ โ) |
25 | 21, 24 | remulcld 11190 |
. . . . . . 7
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (๐ด ยท ๐) โ โ) |
26 | | 1rp 12924 |
. . . . . . 7
โข 1 โ
โ+ |
27 | | modcl 13784 |
. . . . . . 7
โข (((๐ด ยท ๐) โ โ โง 1 โ
โ+) โ ((๐ด ยท ๐) mod 1) โ โ) |
28 | 25, 26, 27 | sylancl 587 |
. . . . . 6
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ((๐ด ยท ๐) mod 1) โ โ) |
29 | 19, 28 | remulcld 11190 |
. . . . 5
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (๐ต ยท ((๐ด ยท ๐) mod 1)) โ โ) |
30 | 29 | flcld 13709 |
. . . 4
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) โ โค) |
31 | 19 | recnd 11188 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ๐ต โ โ) |
32 | 31 | mul01d 11359 |
. . . . . . . 8
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (๐ต ยท 0) = 0) |
33 | | modge0 13790 |
. . . . . . . . . 10
โข (((๐ด ยท ๐) โ โ โง 1 โ
โ+) โ 0 โค ((๐ด ยท ๐) mod 1)) |
34 | 25, 26, 33 | sylancl 587 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ 0 โค ((๐ด ยท ๐) mod 1)) |
35 | | 0red 11163 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ 0 โ
โ) |
36 | | nngt0 12189 |
. . . . . . . . . . 11
โข (๐ต โ โ โ 0 <
๐ต) |
37 | 36 | ad2antlr 726 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ 0 < ๐ต) |
38 | | lemul2 12013 |
. . . . . . . . . 10
โข ((0
โ โ โง ((๐ด
ยท ๐) mod 1) โ
โ โง (๐ต โ
โ โง 0 < ๐ต))
โ (0 โค ((๐ด ยท
๐) mod 1) โ (๐ต ยท 0) โค (๐ต ยท ((๐ด ยท ๐) mod 1)))) |
39 | 35, 28, 19, 37, 38 | syl112anc 1375 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (0 โค ((๐ด ยท ๐) mod 1) โ (๐ต ยท 0) โค (๐ต ยท ((๐ด ยท ๐) mod 1)))) |
40 | 34, 39 | mpbid 231 |
. . . . . . . 8
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (๐ต ยท 0) โค (๐ต ยท ((๐ด ยท ๐) mod 1))) |
41 | 32, 40 | eqbrtrrd 5130 |
. . . . . . 7
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ 0 โค (๐ต ยท ((๐ด ยท ๐) mod 1))) |
42 | 35, 29 | lenltd 11306 |
. . . . . . 7
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (0 โค (๐ต ยท ((๐ด ยท ๐) mod 1)) โ ยฌ (๐ต ยท ((๐ด ยท ๐) mod 1)) < 0)) |
43 | 41, 42 | mpbid 231 |
. . . . . 6
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ยฌ (๐ต ยท ((๐ด ยท ๐) mod 1)) < 0) |
44 | | 0z 12515 |
. . . . . . 7
โข 0 โ
โค |
45 | | fllt 13717 |
. . . . . . 7
โข (((๐ต ยท ((๐ด ยท ๐) mod 1)) โ โ โง 0 โ
โค) โ ((๐ต
ยท ((๐ด ยท ๐) mod 1)) < 0 โ
(โโ(๐ต ยท
((๐ด ยท ๐) mod 1))) <
0)) |
46 | 29, 44, 45 | sylancl 587 |
. . . . . 6
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ((๐ต ยท ((๐ด ยท ๐) mod 1)) < 0 โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) < 0)) |
47 | 43, 46 | mtbid 324 |
. . . . 5
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ยฌ
(โโ(๐ต ยท
((๐ด ยท ๐) mod 1))) <
0) |
48 | 30 | zred 12612 |
. . . . . 6
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) โ โ) |
49 | 35, 48 | lenltd 11306 |
. . . . 5
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (0 โค
(โโ(๐ต ยท
((๐ด ยท ๐) mod 1))) โ ยฌ
(โโ(๐ต ยท
((๐ด ยท ๐) mod 1))) <
0)) |
50 | 47, 49 | mpbird 257 |
. . . 4
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ 0 โค
(โโ(๐ต ยท
((๐ด ยท ๐) mod 1)))) |
51 | | elnn0z 12517 |
. . . 4
โข
((โโ(๐ต
ยท ((๐ด ยท ๐) mod 1))) โ
โ0 โ ((โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) โ โค โง 0 โค
(โโ(๐ต ยท
((๐ด ยท ๐) mod 1))))) |
52 | 30, 50, 51 | sylanbrc 584 |
. . 3
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) โ
โ0) |
53 | 8 | ad2antlr 726 |
. . 3
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (๐ต โ 1) โ
โ0) |
54 | | flle 13710 |
. . . . . . 7
โข ((๐ต ยท ((๐ด ยท ๐) mod 1)) โ โ โ
(โโ(๐ต ยท
((๐ด ยท ๐) mod 1))) โค (๐ต ยท ((๐ด ยท ๐) mod 1))) |
55 | 29, 54 | syl 17 |
. . . . . 6
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) โค (๐ต ยท ((๐ด ยท ๐) mod 1))) |
56 | | modlt 13791 |
. . . . . . . . 9
โข (((๐ด ยท ๐) โ โ โง 1 โ
โ+) โ ((๐ด ยท ๐) mod 1) < 1) |
57 | 25, 26, 56 | sylancl 587 |
. . . . . . . 8
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ((๐ด ยท ๐) mod 1) < 1) |
58 | | 1red 11161 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ 1 โ
โ) |
59 | | ltmul2 12011 |
. . . . . . . . 9
โข ((((๐ด ยท ๐) mod 1) โ โ โง 1 โ
โ โง (๐ต โ
โ โง 0 < ๐ต))
โ (((๐ด ยท ๐) mod 1) < 1 โ (๐ต ยท ((๐ด ยท ๐) mod 1)) < (๐ต ยท 1))) |
60 | 28, 58, 19, 37, 59 | syl112anc 1375 |
. . . . . . . 8
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (((๐ด ยท ๐) mod 1) < 1 โ (๐ต ยท ((๐ด ยท ๐) mod 1)) < (๐ต ยท 1))) |
61 | 57, 60 | mpbid 231 |
. . . . . . 7
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (๐ต ยท ((๐ด ยท ๐) mod 1)) < (๐ต ยท 1)) |
62 | 31 | mulid1d 11177 |
. . . . . . 7
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (๐ต ยท 1) = ๐ต) |
63 | 61, 62 | breqtrd 5132 |
. . . . . 6
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (๐ต ยท ((๐ด ยท ๐) mod 1)) < ๐ต) |
64 | 48, 29, 19, 55, 63 | lelttrd 11318 |
. . . . 5
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) < ๐ต) |
65 | | nncn 12166 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
66 | | ax-1cn 11114 |
. . . . . . 7
โข 1 โ
โ |
67 | | npcan 11415 |
. . . . . . 7
โข ((๐ต โ โ โง 1 โ
โ) โ ((๐ต โ
1) + 1) = ๐ต) |
68 | 65, 66, 67 | sylancl 587 |
. . . . . 6
โข (๐ต โ โ โ ((๐ต โ 1) + 1) = ๐ต) |
69 | 68 | ad2antlr 726 |
. . . . 5
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ((๐ต โ 1) + 1) = ๐ต) |
70 | 64, 69 | breqtrrd 5134 |
. . . 4
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) < ((๐ต โ 1) + 1)) |
71 | 12 | ad2antlr 726 |
. . . . . 6
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ๐ต โ โค) |
72 | | 1z 12538 |
. . . . . 6
โข 1 โ
โค |
73 | | zsubcl 12550 |
. . . . . 6
โข ((๐ต โ โค โง 1 โ
โค) โ (๐ต โ
1) โ โค) |
74 | 71, 72, 73 | sylancl 587 |
. . . . 5
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (๐ต โ 1) โ โค) |
75 | | zleltp1 12559 |
. . . . 5
โข
(((โโ(๐ต
ยท ((๐ด ยท ๐) mod 1))) โ โค โง
(๐ต โ 1) โ
โค) โ ((โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) โค (๐ต โ 1) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) < ((๐ต โ 1) + 1))) |
76 | 30, 74, 75 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ ((โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) โค (๐ต โ 1) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) < ((๐ต โ 1) + 1))) |
77 | 70, 76 | mpbird 257 |
. . 3
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) โค (๐ต โ 1)) |
78 | | elfz2nn0 13538 |
. . 3
โข
((โโ(๐ต
ยท ((๐ด ยท ๐) mod 1))) โ (0...(๐ต โ 1)) โ
((โโ(๐ต ยท
((๐ด ยท ๐) mod 1))) โ
โ0 โง (๐ต โ 1) โ โ0 โง
(โโ(๐ต ยท
((๐ด ยท ๐) mod 1))) โค (๐ต โ 1))) |
79 | 52, 53, 77, 78 | syl3anbrc 1344 |
. 2
โข (((๐ด โ โ+
โง ๐ต โ โ)
โง ๐ โ (0...๐ต)) โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) โ (0...(๐ต โ 1))) |
80 | | oveq2 7366 |
. . . . 5
โข (๐ = ๐ฅ โ (๐ด ยท ๐) = (๐ด ยท ๐ฅ)) |
81 | 80 | oveq1d 7373 |
. . . 4
โข (๐ = ๐ฅ โ ((๐ด ยท ๐) mod 1) = ((๐ด ยท ๐ฅ) mod 1)) |
82 | 81 | oveq2d 7374 |
. . 3
โข (๐ = ๐ฅ โ (๐ต ยท ((๐ด ยท ๐) mod 1)) = (๐ต ยท ((๐ด ยท ๐ฅ) mod 1))) |
83 | 82 | fveq2d 6847 |
. 2
โข (๐ = ๐ฅ โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) = (โโ(๐ต ยท ((๐ด ยท ๐ฅ) mod 1)))) |
84 | | oveq2 7366 |
. . . . 5
โข (๐ = ๐ฆ โ (๐ด ยท ๐) = (๐ด ยท ๐ฆ)) |
85 | 84 | oveq1d 7373 |
. . . 4
โข (๐ = ๐ฆ โ ((๐ด ยท ๐) mod 1) = ((๐ด ยท ๐ฆ) mod 1)) |
86 | 85 | oveq2d 7374 |
. . 3
โข (๐ = ๐ฆ โ (๐ต ยท ((๐ด ยท ๐) mod 1)) = (๐ต ยท ((๐ด ยท ๐ฆ) mod 1))) |
87 | 86 | fveq2d 6847 |
. 2
โข (๐ = ๐ฆ โ (โโ(๐ต ยท ((๐ด ยท ๐) mod 1))) = (โโ(๐ต ยท ((๐ด ยท ๐ฆ) mod 1)))) |
88 | 6, 7, 18, 79, 83, 87 | fphpdo 41183 |
1
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ โ๐ฅ โ
(0...๐ต)โ๐ฆ โ (0...๐ต)(๐ฅ < ๐ฆ โง (โโ(๐ต ยท ((๐ด ยท ๐ฅ) mod 1))) = (โโ(๐ต ยท ((๐ด ยท ๐ฆ) mod 1))))) |