Step | Hyp | Ref
| Expression |
1 | | elfzoelz 10147 |
. . . . . . . 8
โข (๐ผ โ (0..^๐) โ ๐ผ โ โค) |
2 | 1 | 3ad2ant1 1018 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ผ โ โค) |
3 | | zq 9626 |
. . . . . . 7
โข (๐ผ โ โค โ ๐ผ โ
โ) |
4 | 2, 3 | syl 14 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ผ โ โ) |
5 | | simp3 999 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โค) |
6 | | zq 9626 |
. . . . . . 7
โข (๐ โ โค โ ๐ โ
โ) |
7 | 5, 6 | syl 14 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โ) |
8 | | elfzo0 10182 |
. . . . . . . . . 10
โข (๐ผ โ (0..^๐) โ (๐ผ โ โ0 โง ๐ โ โ โง ๐ผ < ๐)) |
9 | 8 | biimpi 120 |
. . . . . . . . 9
โข (๐ผ โ (0..^๐) โ (๐ผ โ โ0 โง ๐ โ โ โง ๐ผ < ๐)) |
10 | 9 | 3ad2ant1 1018 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ โ โ0 โง ๐ โ โ โง ๐ผ < ๐)) |
11 | 10 | simp2d 1010 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โ) |
12 | | nnq 9633 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
13 | 11, 12 | syl 14 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โ) |
14 | 11 | nngt0d 8963 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ 0 < ๐) |
15 | | modqaddmod 10363 |
. . . . . 6
โข (((๐ผ โ โ โง ๐ โ โ) โง (๐ โ โ โง 0 <
๐)) โ (((๐ผ mod ๐) + ๐) mod ๐) = ((๐ผ + ๐) mod ๐)) |
16 | 4, 7, 13, 14, 15 | syl22anc 1239 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ mod ๐) + ๐) mod ๐) = ((๐ผ + ๐) mod ๐)) |
17 | 16 | eqcomd 2183 |
. . . 4
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ผ + ๐) mod ๐) = (((๐ผ mod ๐) + ๐) mod ๐)) |
18 | | elfzoelz 10147 |
. . . . . . . 8
โข (๐ฝ โ (0..^๐) โ ๐ฝ โ โค) |
19 | 18 | 3ad2ant2 1019 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ฝ โ โค) |
20 | | zq 9626 |
. . . . . . 7
โข (๐ฝ โ โค โ ๐ฝ โ
โ) |
21 | 19, 20 | syl 14 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ฝ โ โ) |
22 | | modqaddmod 10363 |
. . . . . 6
โข (((๐ฝ โ โ โง ๐ โ โ) โง (๐ โ โ โง 0 <
๐)) โ (((๐ฝ mod ๐) + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐)) |
23 | 21, 7, 13, 14, 22 | syl22anc 1239 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ฝ mod ๐) + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐)) |
24 | 23 | eqcomd 2183 |
. . . 4
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ฝ + ๐) mod ๐) = (((๐ฝ mod ๐) + ๐) mod ๐)) |
25 | 17, 24 | eqeq12d 2192 |
. . 3
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐) โ (((๐ผ mod ๐) + ๐) mod ๐) = (((๐ฝ mod ๐) + ๐) mod ๐))) |
26 | 2, 11 | zmodcld 10345 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ mod ๐) โ
โ0) |
27 | 26 | nn0zd 9373 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ mod ๐) โ โค) |
28 | 27, 5 | zaddcld 9379 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ผ mod ๐) + ๐) โ โค) |
29 | 28, 11 | zmodcld 10345 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ mod ๐) + ๐) mod ๐) โ
โ0) |
30 | 29 | nn0cnd 9231 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ mod ๐) + ๐) mod ๐) โ โ) |
31 | 19, 11 | zmodcld 10345 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ฝ mod ๐) โ
โ0) |
32 | 31 | nn0zd 9373 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ฝ mod ๐) โ โค) |
33 | 32, 5 | zaddcld 9379 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ฝ mod ๐) + ๐) โ โค) |
34 | 33, 11 | zmodcld 10345 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ฝ mod ๐) + ๐) mod ๐) โ
โ0) |
35 | 34 | nn0cnd 9231 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ฝ mod ๐) + ๐) mod ๐) โ โ) |
36 | 30, 35 | subeq0ad 8278 |
. . . 4
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) = 0 โ (((๐ผ mod ๐) + ๐) mod ๐) = (((๐ฝ mod ๐) + ๐) mod ๐))) |
37 | | oveq1 5882 |
. . . . 5
โข
(((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) = 0 โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = (0 mod ๐)) |
38 | 4, 13, 14 | modqcld 10328 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ mod ๐) โ โ) |
39 | | qaddcl 9635 |
. . . . . . . . . 10
โข (((๐ผ mod ๐) โ โ โง ๐ โ โ) โ ((๐ผ mod ๐) + ๐) โ โ) |
40 | 38, 7, 39 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ผ mod ๐) + ๐) โ โ) |
41 | 21, 13, 14 | modqcld 10328 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ฝ mod ๐) โ โ) |
42 | | qaddcl 9635 |
. . . . . . . . . 10
โข (((๐ฝ mod ๐) โ โ โง ๐ โ โ) โ ((๐ฝ mod ๐) + ๐) โ โ) |
43 | 41, 7, 42 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ฝ mod ๐) + ๐) โ โ) |
44 | | modqsubmodmod 10383 |
. . . . . . . . 9
โข
(((((๐ผ mod ๐) + ๐) โ โ โง ((๐ฝ mod ๐) + ๐) โ โ) โง (๐ โ โ โง 0 < ๐)) โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = ((((๐ผ mod ๐) + ๐) โ ((๐ฝ mod ๐) + ๐)) mod ๐)) |
45 | 40, 43, 13, 14, 44 | syl22anc 1239 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = ((((๐ผ mod ๐) + ๐) โ ((๐ฝ mod ๐) + ๐)) mod ๐)) |
46 | 26 | nn0cnd 9231 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ mod ๐) โ โ) |
47 | 31 | nn0cnd 9231 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ฝ mod ๐) โ โ) |
48 | 5 | zcnd 9376 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โ) |
49 | 46, 47, 48 | pnpcan2d 8306 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ mod ๐) + ๐) โ ((๐ฝ mod ๐) + ๐)) = ((๐ผ mod ๐) โ (๐ฝ mod ๐))) |
50 | 49 | oveq1d 5890 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((๐ผ mod ๐) + ๐) โ ((๐ฝ mod ๐) + ๐)) mod ๐) = (((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐)) |
51 | 45, 50 | eqtrd 2210 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = (((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐)) |
52 | | q0mod 10355 |
. . . . . . . 8
โข ((๐ โ โ โง 0 <
๐) โ (0 mod ๐) = 0) |
53 | 13, 14, 52 | syl2anc 411 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (0 mod ๐) = 0) |
54 | 51, 53 | eqeq12d 2192 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = (0 mod ๐) โ (((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐) = 0)) |
55 | | zmodidfzoimp 10354 |
. . . . . . . . . . 11
โข (๐ผ โ (0..^๐) โ (๐ผ mod ๐) = ๐ผ) |
56 | 55 | 3ad2ant1 1018 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ mod ๐) = ๐ผ) |
57 | | zmodidfzoimp 10354 |
. . . . . . . . . . 11
โข (๐ฝ โ (0..^๐) โ (๐ฝ mod ๐) = ๐ฝ) |
58 | 57 | 3ad2ant2 1019 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ฝ mod ๐) = ๐ฝ) |
59 | 56, 58 | oveq12d 5893 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ผ mod ๐) โ (๐ฝ mod ๐)) = (๐ผ โ ๐ฝ)) |
60 | 59 | oveq1d 5890 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐) = ((๐ผ โ ๐ฝ) mod ๐)) |
61 | 60 | eqeq1d 2186 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐) = 0 โ ((๐ผ โ ๐ฝ) mod ๐) = 0)) |
62 | | qsubcl 9638 |
. . . . . . . . . 10
โข ((๐ผ โ โ โง ๐ฝ โ โ) โ (๐ผ โ ๐ฝ) โ โ) |
63 | 4, 21, 62 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ โ ๐ฝ) โ โ) |
64 | | modq0 10329 |
. . . . . . . . 9
โข (((๐ผ โ ๐ฝ) โ โ โง ๐ โ โ โง 0 < ๐) โ (((๐ผ โ ๐ฝ) mod ๐) = 0 โ ((๐ผ โ ๐ฝ) / ๐) โ โค)) |
65 | 63, 13, 14, 64 | syl3anc 1238 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ โ ๐ฝ) mod ๐) = 0 โ ((๐ผ โ ๐ฝ) / ๐) โ โค)) |
66 | 2, 19 | zsubcld 9380 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ โ ๐ฝ) โ โค) |
67 | | zdiv 9341 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ผ โ ๐ฝ) โ โค) โ (โ๐ โ โค (๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ((๐ผ โ ๐ฝ) / ๐) โ โค)) |
68 | 11, 66, 67 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (โ๐ โ โค (๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ((๐ผ โ ๐ฝ) / ๐) โ โค)) |
69 | | simpr 110 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ ๐ = 0) |
70 | 69 | oveq2d 5891 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ (๐ ยท ๐) = (๐ ยท 0)) |
71 | 11 | nncnd 8933 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โ) |
72 | 71 | mul01d 8350 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ ยท 0) = 0) |
73 | 72 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ (๐ ยท 0) = 0) |
74 | 70, 73 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ (๐ ยท ๐) = 0) |
75 | 74 | eqeq1d 2186 |
. . . . . . . . . . . . . . 15
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ 0 = (๐ผ โ ๐ฝ))) |
76 | | eqcom 2179 |
. . . . . . . . . . . . . . . 16
โข (0 =
(๐ผ โ ๐ฝ) โ (๐ผ โ ๐ฝ) = 0) |
77 | 10 | simp1d 1009 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ผ โ
โ0) |
78 | 77 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ ๐ผ โ
โ0) |
79 | 78 | nn0cnd 9231 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ ๐ผ โ โ) |
80 | | elfzo0 10182 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฝ โ (0..^๐) โ (๐ฝ โ โ0 โง ๐ โ โ โง ๐ฝ < ๐)) |
81 | 80 | biimpi 120 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฝ โ (0..^๐) โ (๐ฝ โ โ0 โง ๐ โ โ โง ๐ฝ < ๐)) |
82 | 81 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ฝ โ โ0 โง ๐ โ โ โง ๐ฝ < ๐)) |
83 | 82 | simp1d 1009 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ฝ โ
โ0) |
84 | 83 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ ๐ฝ โ
โ0) |
85 | 84 | nn0cnd 9231 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ ๐ฝ โ โ) |
86 | 79, 85 | subeq0ad 8278 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ ((๐ผ โ ๐ฝ) = 0 โ ๐ผ = ๐ฝ)) |
87 | 86 | biimpd 144 |
. . . . . . . . . . . . . . . 16
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ ((๐ผ โ ๐ฝ) = 0 โ ๐ผ = ๐ฝ)) |
88 | 76, 87 | biimtrid 152 |
. . . . . . . . . . . . . . 15
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ (0 = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
89 | 75, 88 | sylbid 150 |
. . . . . . . . . . . . . 14
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
90 | 89 | imp 124 |
. . . . . . . . . . . . 13
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง ๐ = 0) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โ ๐ผ = ๐ฝ) |
91 | 90 | an32s 568 |
. . . . . . . . . . . 12
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ = 0) โ ๐ผ = ๐ฝ) |
92 | | subfzo0 10242 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐)) |
93 | 92 | 3adant3 1017 |
. . . . . . . . . . . . . . . . 17
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐)) |
94 | 93 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ (-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐)) |
95 | 94 | simprd 114 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ (๐ผ โ ๐ฝ) < ๐) |
96 | | simplr 528 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ (๐ ยท ๐) = (๐ผ โ ๐ฝ)) |
97 | 71 | mulridd 7974 |
. . . . . . . . . . . . . . . 16
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ ยท 1) = ๐) |
98 | 97 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ (๐ ยท 1) = ๐) |
99 | 95, 96, 98 | 3brtr4d 4036 |
. . . . . . . . . . . . . 14
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ (๐ ยท ๐) < (๐ ยท 1)) |
100 | | simpllr 534 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ ๐ โ โค) |
101 | 100 | zred 9375 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ ๐ โ โ) |
102 | | 1red 7972 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ 1 โ
โ) |
103 | 11 | nnrpd 9694 |
. . . . . . . . . . . . . . . 16
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ
โ+) |
104 | 103 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ ๐ โ
โ+) |
105 | 101, 102,
104 | ltmul2d 9739 |
. . . . . . . . . . . . . 14
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ (๐ < 1 โ (๐ ยท ๐) < (๐ ยท 1))) |
106 | 99, 105 | mpbird 167 |
. . . . . . . . . . . . 13
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ ๐ < 1) |
107 | | simpr 110 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ ๐ โ โ) |
108 | 107 | nnge1d 8962 |
. . . . . . . . . . . . . 14
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ 1 โค ๐) |
109 | 102, 101,
108 | lensymd 8079 |
. . . . . . . . . . . . 13
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ ยฌ ๐ < 1) |
110 | 106, 109 | pm2.21dd 620 |
. . . . . . . . . . . 12
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง ๐ โ โ) โ ๐ผ = ๐ฝ) |
111 | 93 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐)) |
112 | 111 | simpld 112 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ -๐ < (๐ผ โ ๐ฝ)) |
113 | | simplr 528 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (๐ ยท ๐) = (๐ผ โ ๐ฝ)) |
114 | 112, 113 | breqtrrd 4032 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ -๐ < (๐ ยท ๐)) |
115 | 11 | nnzd 9374 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โค) |
116 | 115 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โค) |
117 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โค) |
118 | 116, 117 | zmulcld 9381 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ (๐ ยท ๐) โ โค) |
119 | 118 | zred 9375 |
. . . . . . . . . . . . . . . . 17
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ (๐ ยท ๐) โ โ) |
120 | 119 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (๐ ยท ๐) โ โ) |
121 | 11 | nnred 8932 |
. . . . . . . . . . . . . . . . 17
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โ) |
122 | 121 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ ๐ โ โ) |
123 | 120, 122 | possumd 8526 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (0 < ((๐ ยท ๐) + ๐) โ -๐ < (๐ ยท ๐))) |
124 | 114, 123 | mpbird 167 |
. . . . . . . . . . . . . 14
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ 0 < ((๐ ยท ๐) + ๐)) |
125 | 97 | eqcomd 2183 |
. . . . . . . . . . . . . . . . 17
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ = (๐ ยท 1)) |
126 | 125 | oveq2d 5891 |
. . . . . . . . . . . . . . . 16
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ ยท ๐) + ๐) = ((๐ ยท ๐) + (๐ ยท 1))) |
127 | 126 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ ((๐ ยท ๐) + ๐) = ((๐ ยท ๐) + (๐ ยท 1))) |
128 | 71 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ ๐ โ โ) |
129 | 117 | zcnd 9376 |
. . . . . . . . . . . . . . . . 17
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โ) |
130 | 129 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ ๐ โ โ) |
131 | | 1cnd 7973 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ 1 โ
โ) |
132 | 128, 130,
131 | adddid 7982 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
133 | 127, 132 | eqtr4d 2213 |
. . . . . . . . . . . . . 14
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ ((๐ ยท ๐) + ๐) = (๐ ยท (๐ + 1))) |
134 | 124, 133 | breqtrd 4030 |
. . . . . . . . . . . . 13
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ 0 < (๐ ยท (๐ + 1))) |
135 | 117 | peano2zd 9378 |
. . . . . . . . . . . . . . . . 17
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ (๐ + 1) โ โค) |
136 | 116, 135 | zmulcld 9381 |
. . . . . . . . . . . . . . . 16
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ (๐ ยท (๐ + 1)) โ โค) |
137 | 136 | zred 9375 |
. . . . . . . . . . . . . . 15
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ (๐ ยท (๐ + 1)) โ โ) |
138 | 137 | ad2antrr 488 |
. . . . . . . . . . . . . 14
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (๐ ยท (๐ + 1)) โ โ) |
139 | | 0red 7958 |
. . . . . . . . . . . . . 14
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ 0 โ
โ) |
140 | 71 | adantr 276 |
. . . . . . . . . . . . . . . . 17
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ ๐ โ โ) |
141 | 135 | zcnd 9376 |
. . . . . . . . . . . . . . . . 17
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ (๐ + 1) โ โ) |
142 | 140, 141 | mulcomd 7979 |
. . . . . . . . . . . . . . . 16
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ (๐ ยท (๐ + 1)) = ((๐ + 1) ยท ๐)) |
143 | 142 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ + 1) ยท ๐)) |
144 | 135 | zred 9375 |
. . . . . . . . . . . . . . . . 17
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ (๐ + 1) โ โ) |
145 | 144 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (๐ + 1) โ โ) |
146 | | zcn 9258 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โค โ ๐ โ
โ) |
147 | | 1cnd 7973 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โค โ 1 โ
โ) |
148 | 146, 147 | addcomd 8108 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ (๐ + 1) = (1 + ๐)) |
149 | 147, 146 | subnegd 8275 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ (1
โ -๐) = (1 + ๐)) |
150 | 148, 149 | eqtr4d 2213 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ (๐ + 1) = (1 โ -๐)) |
151 | 150 | ad3antlr 493 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (๐ + 1) = (1 โ -๐)) |
152 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ -๐ โ โ) |
153 | 152 | nnge1d 8962 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ 1 โค -๐) |
154 | | 1red 7972 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ 1 โ
โ) |
155 | 152 | nnred 8932 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ -๐ โ โ) |
156 | 154, 155 | suble0d 8493 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ ((1 โ -๐) โค 0 โ 1 โค -๐)) |
157 | 153, 156 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (1 โ -๐) โค 0) |
158 | 151, 157 | eqbrtrd 4026 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (๐ + 1) โค 0) |
159 | 11 | nnnn0d 9229 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ
โ0) |
160 | 159 | nn0ge0d 9232 |
. . . . . . . . . . . . . . . . 17
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ 0 โค ๐) |
161 | 160 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ 0 โค ๐) |
162 | | mulle0r 8901 |
. . . . . . . . . . . . . . . 16
โข ((((๐ + 1) โ โ โง ๐ โ โ) โง ((๐ + 1) โค 0 โง 0 โค ๐)) โ ((๐ + 1) ยท ๐) โค 0) |
163 | 145, 122,
158, 161, 162 | syl22anc 1239 |
. . . . . . . . . . . . . . 15
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ ((๐ + 1) ยท ๐) โค 0) |
164 | 143, 163 | eqbrtrd 4026 |
. . . . . . . . . . . . . 14
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ (๐ ยท (๐ + 1)) โค 0) |
165 | 138, 139,
164 | lensymd 8079 |
. . . . . . . . . . . . 13
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ ยฌ 0 < (๐ ยท (๐ + 1))) |
166 | 134, 165 | pm2.21dd 620 |
. . . . . . . . . . . 12
โข
(((((๐ผ โ
(0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โง -๐ โ โ) โ ๐ผ = ๐ฝ) |
167 | | elz 9255 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ โ โ โง (๐ = 0 โจ ๐ โ โ โจ -๐ โ โ))) |
168 | 167 | simprbi 275 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (๐ = 0 โจ ๐ โ โ โจ -๐ โ โ)) |
169 | 168 | ad2antlr 489 |
. . . . . . . . . . . 12
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โ (๐ = 0 โจ ๐ โ โ โจ -๐ โ โ)) |
170 | 91, 110, 166, 169 | mpjao3dan 1307 |
. . . . . . . . . . 11
โข ((((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โง (๐ ยท ๐) = (๐ผ โ ๐ฝ)) โ ๐ผ = ๐ฝ) |
171 | 170 | ex 115 |
. . . . . . . . . 10
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โง ๐ โ โค) โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
172 | 171 | rexlimdva 2594 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (โ๐ โ โค (๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
173 | 68, 172 | sylbird 170 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ โ ๐ฝ) / ๐) โ โค โ ๐ผ = ๐ฝ)) |
174 | 65, 173 | sylbid 150 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ โ ๐ฝ) mod ๐) = 0 โ ๐ผ = ๐ฝ)) |
175 | 61, 174 | sylbid 150 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐) = 0 โ ๐ผ = ๐ฝ)) |
176 | 54, 175 | sylbid 150 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = (0 mod ๐) โ ๐ผ = ๐ฝ)) |
177 | 37, 176 | syl5 32 |
. . . 4
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) = 0 โ ๐ผ = ๐ฝ)) |
178 | 36, 177 | sylbird 170 |
. . 3
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((๐ผ mod ๐) + ๐) mod ๐) = (((๐ฝ mod ๐) + ๐) mod ๐) โ ๐ผ = ๐ฝ)) |
179 | 25, 178 | sylbid 150 |
. 2
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐) โ ๐ผ = ๐ฝ)) |
180 | | oveq1 5882 |
. . 3
โข (๐ผ = ๐ฝ โ (๐ผ + ๐) = (๐ฝ + ๐)) |
181 | 180 | oveq1d 5890 |
. 2
โข (๐ผ = ๐ฝ โ ((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐)) |
182 | 179, 181 | impbid1 142 |
1
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐) โ ๐ผ = ๐ฝ)) |