Step | Hyp | Ref
| Expression |
1 | | elfzoelz 13501 |
. . . . . . . 8
โข (๐ผ โ (0..^๐) โ ๐ผ โ โค) |
2 | 1 | zred 12540 |
. . . . . . 7
โข (๐ผ โ (0..^๐) โ ๐ผ โ โ) |
3 | 2 | 3ad2ant1 1134 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ผ โ โ) |
4 | | simp3 1139 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โค) |
5 | 4 | zred 12540 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โ) |
6 | | elfzo0 13542 |
. . . . . . . . 9
โข (๐ผ โ (0..^๐) โ (๐ผ โ โ0 โง ๐ โ โ โง ๐ผ < ๐)) |
7 | 6 | simp2bi 1147 |
. . . . . . . 8
โข (๐ผ โ (0..^๐) โ ๐ โ โ) |
8 | 7 | nnrpd 12884 |
. . . . . . 7
โข (๐ผ โ (0..^๐) โ ๐ โ
โ+) |
9 | 8 | 3ad2ant1 1134 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ
โ+) |
10 | | modaddmod 13744 |
. . . . . 6
โข ((๐ผ โ โ โง ๐ โ โ โง ๐ โ โ+)
โ (((๐ผ mod ๐) + ๐) mod ๐) = ((๐ผ + ๐) mod ๐)) |
11 | 3, 5, 9, 10 | syl3anc 1372 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ mod ๐) + ๐) mod ๐) = ((๐ผ + ๐) mod ๐)) |
12 | 11 | eqcomd 2744 |
. . . 4
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ผ + ๐) mod ๐) = (((๐ผ mod ๐) + ๐) mod ๐)) |
13 | | elfzoelz 13501 |
. . . . . . . 8
โข (๐ฝ โ (0..^๐) โ ๐ฝ โ โค) |
14 | 13 | zred 12540 |
. . . . . . 7
โข (๐ฝ โ (0..^๐) โ ๐ฝ โ โ) |
15 | 14 | 3ad2ant2 1135 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ฝ โ โ) |
16 | | modaddmod 13744 |
. . . . . 6
โข ((๐ฝ โ โ โง ๐ โ โ โง ๐ โ โ+)
โ (((๐ฝ mod ๐) + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐)) |
17 | 15, 5, 9, 16 | syl3anc 1372 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ฝ mod ๐) + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐)) |
18 | 17 | eqcomd 2744 |
. . . 4
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ฝ + ๐) mod ๐) = (((๐ฝ mod ๐) + ๐) mod ๐)) |
19 | 12, 18 | eqeq12d 2754 |
. . 3
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐) โ (((๐ผ mod ๐) + ๐) mod ๐) = (((๐ฝ mod ๐) + ๐) mod ๐))) |
20 | | nn0re 12356 |
. . . . . . . . . . . 12
โข (๐ผ โ โ0
โ ๐ผ โ
โ) |
21 | | nnrp 12855 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ+) |
22 | 20, 21 | anim12i 614 |
. . . . . . . . . . 11
โข ((๐ผ โ โ0
โง ๐ โ โ)
โ (๐ผ โ โ
โง ๐ โ
โ+)) |
23 | 22 | 3adant3 1133 |
. . . . . . . . . 10
โข ((๐ผ โ โ0
โง ๐ โ โ
โง ๐ผ < ๐) โ (๐ผ โ โ โง ๐ โ
โ+)) |
24 | | modcl 13707 |
. . . . . . . . . 10
โข ((๐ผ โ โ โง ๐ โ โ+)
โ (๐ผ mod ๐) โ
โ) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
โข ((๐ผ โ โ0
โง ๐ โ โ
โง ๐ผ < ๐) โ (๐ผ mod ๐) โ โ) |
26 | 6, 25 | sylbi 216 |
. . . . . . . 8
โข (๐ผ โ (0..^๐) โ (๐ผ mod ๐) โ โ) |
27 | 26 | 3ad2ant1 1134 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ mod ๐) โ โ) |
28 | 27, 5 | readdcld 11118 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ผ mod ๐) + ๐) โ โ) |
29 | | modcl 13707 |
. . . . . . 7
โข ((((๐ผ mod ๐) + ๐) โ โ โง ๐ โ โ+) โ (((๐ผ mod ๐) + ๐) mod ๐) โ โ) |
30 | 29 | recnd 11117 |
. . . . . 6
โข ((((๐ผ mod ๐) + ๐) โ โ โง ๐ โ โ+) โ (((๐ผ mod ๐) + ๐) mod ๐) โ โ) |
31 | 28, 9, 30 | syl2anc 585 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ mod ๐) + ๐) mod ๐) โ โ) |
32 | | elfzo0 13542 |
. . . . . . . . 9
โข (๐ฝ โ (0..^๐) โ (๐ฝ โ โ0 โง ๐ โ โ โง ๐ฝ < ๐)) |
33 | | nn0re 12356 |
. . . . . . . . . . . 12
โข (๐ฝ โ โ0
โ ๐ฝ โ
โ) |
34 | 33, 21 | anim12i 614 |
. . . . . . . . . . 11
โข ((๐ฝ โ โ0
โง ๐ โ โ)
โ (๐ฝ โ โ
โง ๐ โ
โ+)) |
35 | 34 | 3adant3 1133 |
. . . . . . . . . 10
โข ((๐ฝ โ โ0
โง ๐ โ โ
โง ๐ฝ < ๐) โ (๐ฝ โ โ โง ๐ โ
โ+)) |
36 | | modcl 13707 |
. . . . . . . . . 10
โข ((๐ฝ โ โ โง ๐ โ โ+)
โ (๐ฝ mod ๐) โ
โ) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
โข ((๐ฝ โ โ0
โง ๐ โ โ
โง ๐ฝ < ๐) โ (๐ฝ mod ๐) โ โ) |
38 | 32, 37 | sylbi 216 |
. . . . . . . 8
โข (๐ฝ โ (0..^๐) โ (๐ฝ mod ๐) โ โ) |
39 | 38 | 3ad2ant2 1135 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ฝ mod ๐) โ โ) |
40 | 39, 5 | readdcld 11118 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ฝ mod ๐) + ๐) โ โ) |
41 | | modcl 13707 |
. . . . . . 7
โข ((((๐ฝ mod ๐) + ๐) โ โ โง ๐ โ โ+) โ (((๐ฝ mod ๐) + ๐) mod ๐) โ โ) |
42 | 41 | recnd 11117 |
. . . . . 6
โข ((((๐ฝ mod ๐) + ๐) โ โ โง ๐ โ โ+) โ (((๐ฝ mod ๐) + ๐) mod ๐) โ โ) |
43 | 40, 9, 42 | syl2anc 585 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ฝ mod ๐) + ๐) mod ๐) โ โ) |
44 | 31, 43 | subeq0ad 11456 |
. . . 4
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) = 0 โ (((๐ผ mod ๐) + ๐) mod ๐) = (((๐ฝ mod ๐) + ๐) mod ๐))) |
45 | | oveq1 7357 |
. . . . 5
โข
(((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) = 0 โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = (0 mod ๐)) |
46 | | modsubmodmod 13764 |
. . . . . . . . 9
โข ((((๐ผ mod ๐) + ๐) โ โ โง ((๐ฝ mod ๐) + ๐) โ โ โง ๐ โ โ+) โ
(((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = ((((๐ผ mod ๐) + ๐) โ ((๐ฝ mod ๐) + ๐)) mod ๐)) |
47 | 28, 40, 9, 46 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = ((((๐ผ mod ๐) + ๐) โ ((๐ฝ mod ๐) + ๐)) mod ๐)) |
48 | 26 | recnd 11117 |
. . . . . . . . . . 11
โข (๐ผ โ (0..^๐) โ (๐ผ mod ๐) โ โ) |
49 | 48 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ mod ๐) โ โ) |
50 | 38 | recnd 11117 |
. . . . . . . . . . 11
โข (๐ฝ โ (0..^๐) โ (๐ฝ mod ๐) โ โ) |
51 | 50 | 3ad2ant2 1135 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ฝ mod ๐) โ โ) |
52 | 4 | zcnd 12541 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ๐ โ โ) |
53 | 49, 51, 52 | pnpcan2d 11484 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ mod ๐) + ๐) โ ((๐ฝ mod ๐) + ๐)) = ((๐ผ mod ๐) โ (๐ฝ mod ๐))) |
54 | 53 | oveq1d 7365 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((๐ผ mod ๐) + ๐) โ ((๐ฝ mod ๐) + ๐)) mod ๐) = (((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐)) |
55 | 47, 54 | eqtrd 2778 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = (((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐)) |
56 | 32 | simp2bi 1147 |
. . . . . . . . . 10
โข (๐ฝ โ (0..^๐) โ ๐ โ โ) |
57 | 56 | nnrpd 12884 |
. . . . . . . . 9
โข (๐ฝ โ (0..^๐) โ ๐ โ
โ+) |
58 | | 0mod 13736 |
. . . . . . . . 9
โข (๐ โ โ+
โ (0 mod ๐) =
0) |
59 | 57, 58 | syl 17 |
. . . . . . . 8
โข (๐ฝ โ (0..^๐) โ (0 mod ๐) = 0) |
60 | 59 | 3ad2ant2 1135 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (0 mod ๐) = 0) |
61 | 55, 60 | eqeq12d 2754 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = (0 mod ๐) โ (((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐) = 0)) |
62 | | zmodidfzoimp 13735 |
. . . . . . . . . . 11
โข (๐ผ โ (0..^๐) โ (๐ผ mod ๐) = ๐ผ) |
63 | 62 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ผ mod ๐) = ๐ผ) |
64 | | zmodidfzoimp 13735 |
. . . . . . . . . . 11
โข (๐ฝ โ (0..^๐) โ (๐ฝ mod ๐) = ๐ฝ) |
65 | 64 | 3ad2ant2 1135 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (๐ฝ mod ๐) = ๐ฝ) |
66 | 63, 65 | oveq12d 7368 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((๐ผ mod ๐) โ (๐ฝ mod ๐)) = (๐ผ โ ๐ฝ)) |
67 | 66 | oveq1d 7365 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐) = ((๐ผ โ ๐ฝ) mod ๐)) |
68 | 67 | eqeq1d 2740 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐) = 0 โ ((๐ผ โ ๐ฝ) mod ๐) = 0)) |
69 | | zsubcl 12476 |
. . . . . . . . . . . 12
โข ((๐ผ โ โค โง ๐ฝ โ โค) โ (๐ผ โ ๐ฝ) โ โค) |
70 | 1, 13, 69 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (๐ผ โ ๐ฝ) โ โค) |
71 | 70 | zred 12540 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (๐ผ โ ๐ฝ) โ โ) |
72 | 8 | adantr 482 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ๐ โ
โ+) |
73 | | mod0 13710 |
. . . . . . . . . 10
โข (((๐ผ โ ๐ฝ) โ โ โง ๐ โ โ+) โ (((๐ผ โ ๐ฝ) mod ๐) = 0 โ ((๐ผ โ ๐ฝ) / ๐) โ โค)) |
74 | 71, 72, 73 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (((๐ผ โ ๐ฝ) mod ๐) = 0 โ ((๐ผ โ ๐ฝ) / ๐) โ โค)) |
75 | | zdiv 12504 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ผ โ ๐ฝ) โ โค) โ (โ๐ โ โค (๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ((๐ผ โ ๐ฝ) / ๐) โ โค)) |
76 | 7, 70, 75 | syl2an2r 684 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (โ๐ โ โค (๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ((๐ผ โ ๐ฝ) / ๐) โ โค)) |
77 | | oveq2 7358 |
. . . . . . . . . . . . . . . 16
โข (๐ = 0 โ (๐ ยท ๐) = (๐ ยท 0)) |
78 | | elfzoel2 13500 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ผ โ (0..^๐) โ ๐ โ โค) |
79 | 78 | zcnd 12541 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ผ โ (0..^๐) โ ๐ โ โ) |
80 | 79 | mul01d 11288 |
. . . . . . . . . . . . . . . . . 18
โข (๐ผ โ (0..^๐) โ (๐ ยท 0) = 0) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (๐ ยท 0) = 0) |
82 | 81 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค) โ (๐ ยท 0) = 0) |
83 | 77, 82 | sylan9eq 2798 |
. . . . . . . . . . . . . . 15
โข ((๐ = 0 โง ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค)) โ (๐ ยท ๐) = 0) |
84 | 83 | eqeq1d 2740 |
. . . . . . . . . . . . . 14
โข ((๐ = 0 โง ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค)) โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ 0 = (๐ผ โ ๐ฝ))) |
85 | | eqcom 2745 |
. . . . . . . . . . . . . . . . 17
โข (0 =
(๐ผ โ ๐ฝ) โ (๐ผ โ ๐ฝ) = 0) |
86 | 1 | zcnd 12541 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ผ โ (0..^๐) โ ๐ผ โ โ) |
87 | 13 | zcnd 12541 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฝ โ (0..^๐) โ ๐ฝ โ โ) |
88 | | subeq0 11361 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ผ โ โ โง ๐ฝ โ โ) โ ((๐ผ โ ๐ฝ) = 0 โ ๐ผ = ๐ฝ)) |
89 | 86, 87, 88 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((๐ผ โ ๐ฝ) = 0 โ ๐ผ = ๐ฝ)) |
90 | 89 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((๐ผ โ ๐ฝ) = 0 โ ๐ผ = ๐ฝ)) |
91 | 85, 90 | biimtrid 241 |
. . . . . . . . . . . . . . . 16
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (0 = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
92 | 91 | adantr 482 |
. . . . . . . . . . . . . . 15
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค) โ (0 = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
93 | 92 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ = 0 โง ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค)) โ (0 = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
94 | 84, 93 | sylbid 239 |
. . . . . . . . . . . . 13
โข ((๐ = 0 โง ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค)) โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
95 | 94 | ex 414 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค) โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))) |
96 | | subfzo0 13623 |
. . . . . . . . . . . . . . 15
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐)) |
97 | 96 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค) โ (-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐)) |
98 | | elz 12435 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ (๐ โ โ โง (๐ = 0 โจ ๐ โ โ โจ -๐ โ โ))) |
99 | | pm2.24 124 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = 0 โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))) |
100 | 99 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = 0 โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)))) |
101 | 100 | 2a1d 26 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = 0 โ (๐ โ โ โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)))))) |
102 | | breq1 5107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ((๐ ยท ๐) < ๐ โ (๐ผ โ ๐ฝ) < ๐)) |
103 | | nncn 12095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (๐ โ โ โ ๐ โ
โ) |
104 | 103 | mulid1d 11106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
105 | 104 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท 1) = ๐) |
106 | 105 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ โ โง ๐ โ โ) โ ๐ = (๐ ยท 1)) |
107 | 106 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) < ๐ โ (๐ ยท ๐) < (๐ ยท 1))) |
108 | | nnre 12094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ โ โ โ ๐ โ
โ) |
109 | 108 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
110 | | 1red 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ โง ๐ โ โ) โ 1 โ
โ) |
111 | 21 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ+) |
112 | 109, 110,
111 | ltmul2d 12928 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ โ โง ๐ โ โ) โ (๐ < 1 โ (๐ ยท ๐) < (๐ ยท 1))) |
113 | | nnge1 12115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ โ โ โ 1 โค
๐) |
114 | | 1red 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข (๐ โ โ โ 1 โ
โ) |
115 | 114, 108 | lenltd 11235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (๐ โ โ โ (1 โค
๐ โ ยฌ ๐ < 1)) |
116 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข (ยฌ
๐ < 1 โ (๐ < 1 โ ๐ผ = ๐ฝ)) |
117 | 115, 116 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข (๐ โ โ โ (1 โค
๐ โ (๐ < 1 โ ๐ผ = ๐ฝ))) |
118 | 113, 117 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ โ โ โ (๐ < 1 โ ๐ผ = ๐ฝ)) |
119 | 118 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ โ โง ๐ โ โ) โ (๐ < 1 โ ๐ผ = ๐ฝ)) |
120 | 112, 119 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) < (๐ ยท 1) โ ๐ผ = ๐ฝ)) |
121 | 107, 120 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) < ๐ โ ๐ผ = ๐ฝ)) |
122 | 121 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ โ โ โ (๐ โ โ โ ((๐ ยท ๐) < ๐ โ ๐ผ = ๐ฝ))) |
123 | 122 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ฝ โ โ0
โง ๐ โ โ
โง ๐ฝ < ๐) โ (๐ โ โ โ ((๐ ยท ๐) < ๐ โ ๐ผ = ๐ฝ))) |
124 | 32, 123 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฝ โ (0..^๐) โ (๐ โ โ โ ((๐ ยท ๐) < ๐ โ ๐ผ = ๐ฝ))) |
125 | 124 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (๐ โ โ โ ((๐ ยท ๐) < ๐ โ ๐ผ = ๐ฝ))) |
126 | 125 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ ยท ๐) < ๐ โ (๐ โ โ โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ๐ผ = ๐ฝ))) |
127 | 126 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ ยท ๐) < ๐ โ (๐ โ โ โ (ยฌ ๐ = 0 โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ๐ผ = ๐ฝ)))) |
128 | 102, 127 | syl6bir 254 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ((๐ผ โ ๐ฝ) < ๐ โ (๐ โ โ โ (ยฌ ๐ = 0 โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ๐ผ = ๐ฝ))))) |
129 | 128 | com15 101 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((๐ผ โ ๐ฝ) < ๐ โ (๐ โ โ โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
130 | 129 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ผ โ ๐ฝ) < ๐ โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (๐ โ โ โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
131 | 130 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
โข ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (๐ โ โ โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
132 | 131 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
133 | 132 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (๐ โ โ โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)))))) |
134 | | breq2 5108 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ (-๐ < (๐ ยท ๐) โ -๐ < (๐ผ โ ๐ฝ))) |
135 | | nnre 12094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ โ โ โ ๐ โ
โ) |
136 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((-๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
137 | | remulcl 11070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
138 | 135, 136,
137 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (๐ ยท ๐) โ โ) |
139 | 135 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
140 | 138, 139 | possumd 11714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (0 <
((๐ ยท ๐) + ๐) โ -๐ < (๐ ยท ๐))) |
141 | 103 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
142 | 141 | mulid1d 11106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (๐ ยท 1) = ๐) |
143 | 142 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ ๐ = (๐ ยท 1)) |
144 | 143 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ ((๐ ยท ๐) + ๐) = ((๐ ยท ๐) + (๐ ยท 1))) |
145 | | recn 11075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (๐ โ โ โ ๐ โ
โ) |
146 | 145 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((-๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
147 | 146 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
148 | | 1cnd 11084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ 1
โ โ) |
149 | 141, 147,
148 | adddid 11113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
150 | 144, 149 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ ((๐ ยท ๐) + ๐) = (๐ ยท (๐ + 1))) |
151 | 150 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (0 <
((๐ ยท ๐) + ๐) โ 0 < (๐ ยท (๐ + 1)))) |
152 | | peano2re 11262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (๐ โ โ โ (๐ + 1) โ
โ) |
153 | 152 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((-๐ โ โ โง ๐ โ โ) โ (๐ + 1) โ
โ) |
154 | 153 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (๐ + 1) โ
โ) |
155 | 139, 154 | remulcld 11119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (๐ ยท (๐ + 1)) โ โ) |
156 | | 0red 11092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ 0
โ โ) |
157 | | nnnn0 12354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข (๐ โ โ โ ๐ โ
โ0) |
158 | 157 | nn0ge0d 12410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข (๐ โ โ โ 0 โค
๐) |
159 | | nnge1 12115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข (-๐ โ โ โ 1 โค
-๐) |
160 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
โข (๐ โ โ โ ๐ โ
โ) |
161 | | 1cnd 11084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
โข (๐ โ โ โ 1 โ
โ) |
162 | 160, 161 | addcomd 11291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
โข (๐ โ โ โ (๐ + 1) = (1 + ๐)) |
163 | 161, 160 | subnegd 11453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
โข (๐ โ โ โ (1
โ -๐) = (1 + ๐)) |
164 | 162, 163 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
โข (๐ โ โ โ (๐ + 1) = (1 โ -๐)) |
165 | 145, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
โข (๐ โ โ โ (๐ + 1) = (1 โ -๐)) |
166 | 165 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
โข ((1 โค
-๐ โง ๐ โ โ) โ (๐ + 1) = (1 โ -๐)) |
167 | | 1red 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
โข (๐ โ โ โ 1 โ
โ) |
168 | | renegcl 11398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
โข (๐ โ โ โ -๐ โ
โ) |
169 | 167, 168 | suble0d 11680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
โข (๐ โ โ โ ((1
โ -๐) โค 0 โ 1
โค -๐)) |
170 | 169 | biimparc 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
โข ((1 โค
-๐ โง ๐ โ โ) โ (1 โ -๐) โค 0) |
171 | 166, 170 | eqbrtrd 5126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
โข ((1 โค
-๐ โง ๐ โ โ) โ (๐ + 1) โค 0) |
172 | 159, 171 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
โข ((-๐ โ โ โง ๐ โ โ) โ (๐ + 1) โค 0) |
173 | 158, 172 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (0 โค
๐ โง (๐ + 1) โค 0)) |
174 | 173 | olcd 873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ ((๐ โค 0 โง 0 โค (๐ + 1)) โจ (0 โค ๐ โง (๐ + 1) โค 0))) |
175 | | mulle0b 11960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
โข ((๐ โ โ โง (๐ + 1) โ โ) โ
((๐ ยท (๐ + 1)) โค 0 โ ((๐ โค 0 โง 0 โค (๐ + 1)) โจ (0 โค ๐ โง (๐ + 1) โค 0)))) |
176 | 135, 153,
175 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ ((๐ ยท (๐ + 1)) โค 0 โ ((๐ โค 0 โง 0 โค (๐ + 1)) โจ (0 โค ๐ โง (๐ + 1) โค 0)))) |
177 | 174, 176 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (๐ ยท (๐ + 1)) โค 0) |
178 | 155, 156,
177 | lensymd 11240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ ยฌ 0
< (๐ ยท (๐ + 1))) |
179 | 178 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (0 <
(๐ ยท (๐ + 1)) โ ๐ผ = ๐ฝ)) |
180 | 151, 179 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (0 <
((๐ ยท ๐) + ๐) โ ๐ผ = ๐ฝ)) |
181 | 140, 180 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (-๐ < (๐ ยท ๐) โ ๐ผ = ๐ฝ)) |
182 | 181 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โ โ โง (-๐ โ โ โง ๐ โ โ)) โ (ยฌ
๐ = 0 โ (-๐ < (๐ ยท ๐) โ ๐ผ = ๐ฝ))) |
183 | 182 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ โ โ ((-๐ โ โ โง ๐ โ โ) โ (ยฌ
๐ = 0 โ (-๐ < (๐ ยท ๐) โ ๐ผ = ๐ฝ)))) |
184 | 183 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ผ โ โ0
โง ๐ โ โ
โง ๐ผ < ๐) โ ((-๐ โ โ โง ๐ โ โ) โ (ยฌ ๐ = 0 โ (-๐ < (๐ ยท ๐) โ ๐ผ = ๐ฝ)))) |
185 | 6, 184 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ผ โ (0..^๐) โ ((-๐ โ โ โง ๐ โ โ) โ (ยฌ ๐ = 0 โ (-๐ < (๐ ยท ๐) โ ๐ผ = ๐ฝ)))) |
186 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ โ โ โง ๐ โ โ) โ (ยฌ ๐ = 0 โ (-๐ < (๐ ยท ๐) โ ๐ผ = ๐ฝ)))) |
187 | 186 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (-๐ < (๐ ยท ๐) โ ((-๐ โ โ โง ๐ โ โ) โ (ยฌ ๐ = 0 โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ๐ผ = ๐ฝ)))) |
188 | 134, 187 | syl6bir 254 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ (-๐ < (๐ผ โ ๐ฝ) โ ((-๐ โ โ โง ๐ โ โ) โ (ยฌ ๐ = 0 โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ๐ผ = ๐ฝ))))) |
189 | 188 | com15 101 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (-๐ < (๐ผ โ ๐ฝ) โ ((-๐ โ โ โง ๐ โ โ) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
190 | 189 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
โข (-๐ < (๐ผ โ ๐ฝ) โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ โ โ โง ๐ โ โ) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
191 | 190 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ โ โ โง ๐ โ โ) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
192 | 191 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
โข ((-๐ โ โ โง ๐ โ โ) โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
193 | 192 | ex 414 |
. . . . . . . . . . . . . . . . . 18
โข (-๐ โ โ โ (๐ โ โ โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)))))) |
194 | 101, 133,
193 | 3jaoi 1428 |
. . . . . . . . . . . . . . . . 17
โข ((๐ = 0 โจ ๐ โ โ โจ -๐ โ โ) โ (๐ โ โ โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)))))) |
195 | 194 | impcom 409 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง (๐ = 0 โจ ๐ โ โ โจ -๐ โ โ)) โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
196 | 98, 195 | sylbi 216 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))))) |
197 | 196 | impcom 409 |
. . . . . . . . . . . . . 14
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค) โ ((-๐ < (๐ผ โ ๐ฝ) โง (๐ผ โ ๐ฝ) < ๐) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)))) |
198 | 97, 197 | mpd 15 |
. . . . . . . . . . . . 13
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))) |
199 | 198 | com12 32 |
. . . . . . . . . . . 12
โข (ยฌ
๐ = 0 โ (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค) โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ))) |
200 | 95, 199 | pm2.61i 182 |
. . . . . . . . . . 11
โข (((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โง ๐ โ โค) โ ((๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
201 | 200 | rexlimdva 3151 |
. . . . . . . . . 10
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (โ๐ โ โค (๐ ยท ๐) = (๐ผ โ ๐ฝ) โ ๐ผ = ๐ฝ)) |
202 | 76, 201 | sylbird 260 |
. . . . . . . . 9
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (((๐ผ โ ๐ฝ) / ๐) โ โค โ ๐ผ = ๐ฝ)) |
203 | 74, 202 | sylbid 239 |
. . . . . . . 8
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (((๐ผ โ ๐ฝ) mod ๐) = 0 โ ๐ผ = ๐ฝ)) |
204 | 203 | 3adant3 1133 |
. . . . . . 7
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ โ ๐ฝ) mod ๐) = 0 โ ๐ผ = ๐ฝ)) |
205 | 68, 204 | sylbid 239 |
. . . . . 6
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((๐ผ mod ๐) โ (๐ฝ mod ๐)) mod ๐) = 0 โ ๐ผ = ๐ฝ)) |
206 | 61, 205 | sylbid 239 |
. . . . 5
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) mod ๐) = (0 mod ๐) โ ๐ผ = ๐ฝ)) |
207 | 45, 206 | syl5 34 |
. . . 4
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((((๐ผ mod ๐) + ๐) mod ๐) โ (((๐ฝ mod ๐) + ๐) mod ๐)) = 0 โ ๐ผ = ๐ฝ)) |
208 | 44, 207 | sylbird 260 |
. . 3
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ ((((๐ผ mod ๐) + ๐) mod ๐) = (((๐ฝ mod ๐) + ๐) mod ๐) โ ๐ผ = ๐ฝ)) |
209 | 19, 208 | sylbid 239 |
. 2
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐) โ ๐ผ = ๐ฝ)) |
210 | | oveq1 7357 |
. . 3
โข (๐ผ = ๐ฝ โ (๐ผ + ๐) = (๐ฝ + ๐)) |
211 | 210 | oveq1d 7365 |
. 2
โข (๐ผ = ๐ฝ โ ((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐)) |
212 | 209, 211 | impbid1 224 |
1
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐) โ ๐ผ = ๐ฝ)) |