Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . . 10
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ 2
โฅ (๐ /
ฯ)) |
2 | | 2z 12542 |
. . . . . . . . . . . 12
โข 2 โ
โค |
3 | 2 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ 2 โ
โค) |
4 | | fourierswlem.x |
. . . . . . . . . . . . . 14
โข ๐ โ โ |
5 | | pirp 25834 |
. . . . . . . . . . . . . 14
โข ฯ
โ โ+ |
6 | | mod0 13788 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ฯ
โ โ+) โ ((๐ mod ฯ) = 0 โ (๐ / ฯ) โ โค)) |
7 | 4, 5, 6 | mp2an 691 |
. . . . . . . . . . . . 13
โข ((๐ mod ฯ) = 0 โ (๐ / ฯ) โ
โค) |
8 | 7 | biimpi 215 |
. . . . . . . . . . . 12
โข ((๐ mod ฯ) = 0 โ (๐ / ฯ) โ
โค) |
9 | 8 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ (๐ / ฯ) โ
โค) |
10 | | divides 16145 |
. . . . . . . . . . 11
โข ((2
โ โค โง (๐ /
ฯ) โ โค) โ (2 โฅ (๐ / ฯ) โ โ๐ โ โค (๐ ยท 2) = (๐ / ฯ))) |
11 | 3, 9, 10 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ (2
โฅ (๐ / ฯ) โ
โ๐ โ โค
(๐ ยท 2) = (๐ / ฯ))) |
12 | 1, 11 | mpbid 231 |
. . . . . . . . 9
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ
โ๐ โ โค
(๐ ยท 2) = (๐ / ฯ)) |
13 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ 2 โ
โ) |
14 | | picn 25832 |
. . . . . . . . . . . . . . . . . . . 20
โข ฯ
โ โ |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ ฯ
โ โ) |
16 | | zcn 12511 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ ๐ โ
โ) |
17 | 13, 15, 16 | mulassd 11185 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ ((2
ยท ฯ) ยท ๐)
= (2 ยท (ฯ ยท ๐))) |
18 | 15, 16 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ (ฯ
ยท ๐) โ
โ) |
19 | 13, 18 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ (2
ยท (ฯ ยท ๐))
= ((ฯ ยท ๐)
ยท 2)) |
20 | 17, 19 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ ((2
ยท ฯ) ยท ๐)
= ((ฯ ยท ๐)
ยท 2)) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ((2 ยท
ฯ) ยท ๐) = ((ฯ
ยท ๐) ยท
2)) |
22 | 15, 16, 13 | mulassd 11185 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ ((ฯ
ยท ๐) ยท 2) =
(ฯ ยท (๐ ยท
2))) |
23 | 22 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ((ฯ ยท
๐) ยท 2) = (ฯ
ยท (๐ ยท
2))) |
24 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ ยท 2) = (๐ / ฯ) โ (๐ ยท 2) = (๐ / ฯ)) |
25 | 24 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ ยท 2) = (๐ / ฯ) โ (๐ / ฯ) = (๐ ยท 2)) |
26 | 25 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ (๐ / ฯ) = (๐ ยท 2)) |
27 | 4 | recni 11176 |
. . . . . . . . . . . . . . . . . . 19
โข ๐ โ โ |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ๐ โ
โ) |
29 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ฯ โ
โ) |
30 | 16 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ๐ โ
โ) |
31 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ 2 โ
โ) |
32 | 30, 31 | mulcld 11182 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ (๐ ยท 2) โ
โ) |
33 | | pire 25831 |
. . . . . . . . . . . . . . . . . . . 20
โข ฯ
โ โ |
34 | | pipos 25833 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 <
ฯ |
35 | 33, 34 | gt0ne0ii 11698 |
. . . . . . . . . . . . . . . . . . 19
โข ฯ โ
0 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ฯ โ
0) |
37 | 28, 29, 32, 36 | divmuld 11960 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ((๐ / ฯ) = (๐ ยท 2) โ (ฯ ยท (๐ ยท 2)) = ๐)) |
38 | 26, 37 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ (ฯ ยท
(๐ ยท 2)) = ๐) |
39 | 21, 23, 38 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ๐ = ((2 ยท ฯ) ยท
๐)) |
40 | | fourierswlem.t |
. . . . . . . . . . . . . . . 16
โข ๐ = (2 ยท
ฯ) |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ๐ = (2 ยท
ฯ)) |
42 | 39, 41 | oveq12d 7380 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ (๐ / ๐) = (((2 ยท ฯ) ยท ๐) / (2 ยท
ฯ))) |
43 | 13, 15 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ (2
ยท ฯ) โ โ) |
44 | | 2ne0 12264 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
0 |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ 2 โ
0) |
46 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ ฯ โ
0) |
47 | 13, 15, 45, 46 | mulne0d 11814 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ (2
ยท ฯ) โ 0) |
48 | 16, 43, 47 | divcan3d 11943 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (((2
ยท ฯ) ยท ๐)
/ (2 ยท ฯ)) = ๐) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ (((2 ยท
ฯ) ยท ๐) / (2
ยท ฯ)) = ๐) |
50 | 42, 49 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ (๐ / ๐) = ๐) |
51 | | simpl 484 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ ๐ โ
โค) |
52 | 50, 51 | eqeltrd 2838 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง (๐ ยท 2) = (๐ / ฯ)) โ (๐ / ๐) โ โค) |
53 | 52 | ex 414 |
. . . . . . . . . . 11
โข (๐ โ โค โ ((๐ ยท 2) = (๐ / ฯ) โ (๐ / ๐) โ โค)) |
54 | 53 | a1i 11 |
. . . . . . . . . 10
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ (๐ โ โค โ ((๐ ยท 2) = (๐ / ฯ) โ (๐ / ๐) โ โค))) |
55 | 54 | rexlimdv 3151 |
. . . . . . . . 9
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ
(โ๐ โ โค
(๐ ยท 2) = (๐ / ฯ) โ (๐ / ๐) โ โค)) |
56 | 12, 55 | mpd 15 |
. . . . . . . 8
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ (๐ / ๐) โ โค) |
57 | | 2re 12234 |
. . . . . . . . . . . 12
โข 2 โ
โ |
58 | 57, 33 | remulcli 11178 |
. . . . . . . . . . 11
โข (2
ยท ฯ) โ โ |
59 | 40, 58 | eqeltri 2834 |
. . . . . . . . . 10
โข ๐ โ โ |
60 | | 2pos 12263 |
. . . . . . . . . . . 12
โข 0 <
2 |
61 | 57, 33, 60, 34 | mulgt0ii 11295 |
. . . . . . . . . . 11
โข 0 < (2
ยท ฯ) |
62 | 61, 40 | breqtrri 5137 |
. . . . . . . . . 10
โข 0 <
๐ |
63 | 59, 62 | elrpii 12925 |
. . . . . . . . 9
โข ๐ โ
โ+ |
64 | | mod0 13788 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ+)
โ ((๐ mod ๐) = 0 โ (๐ / ๐) โ โค)) |
65 | 4, 63, 64 | mp2an 691 |
. . . . . . . 8
โข ((๐ mod ๐) = 0 โ (๐ / ๐) โ โค) |
66 | 56, 65 | sylibr 233 |
. . . . . . 7
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ (๐ mod ๐) = 0) |
67 | 66 | orcd 872 |
. . . . . 6
โข (((๐ mod ฯ) = 0 โง 2 โฅ
(๐ / ฯ)) โ ((๐ mod ๐) = 0 โจ (๐ mod ๐) = ฯ)) |
68 | | odd2np1 16230 |
. . . . . . . . . 10
โข ((๐ / ฯ) โ โค โ
(ยฌ 2 โฅ (๐ / ฯ)
โ โ๐ โ
โค ((2 ยท ๐) +
1) = (๐ /
ฯ))) |
69 | 7, 68 | sylbi 216 |
. . . . . . . . 9
โข ((๐ mod ฯ) = 0 โ (ยฌ 2
โฅ (๐ / ฯ) โ
โ๐ โ โค ((2
ยท ๐) + 1) = (๐ / ฯ))) |
70 | 69 | biimpa 478 |
. . . . . . . 8
โข (((๐ mod ฯ) = 0 โง ยฌ 2
โฅ (๐ / ฯ)) โ
โ๐ โ โค ((2
ยท ๐) + 1) = (๐ / ฯ)) |
71 | 13, 16 | mulcld 11182 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
72 | 71 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (2 ยท
๐) โ
โ) |
73 | | 1cnd 11157 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ 1 โ
โ) |
74 | 14 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ฯ โ
โ) |
75 | 72, 73, 74 | adddird 11187 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (((2 ยท
๐) + 1) ยท ฯ) =
(((2 ยท ๐) ยท
ฯ) + (1 ยท ฯ))) |
76 | 13, 16 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ (2
ยท ๐) = (๐ ยท 2)) |
77 | 76 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ ((2
ยท ๐) ยท ฯ)
= ((๐ ยท 2) ยท
ฯ)) |
78 | 16, 13, 15 | mulassd 11185 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ ((๐ ยท 2) ยท ฯ) =
(๐ ยท (2 ยท
ฯ))) |
79 | 40 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . 20
โข (2
ยท ฯ) = ๐ |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ (2
ยท ฯ) = ๐) |
81 | 80 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ (๐ ยท (2 ยท ฯ)) =
(๐ ยท ๐)) |
82 | 77, 78, 81 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ ((2
ยท ๐) ยท ฯ)
= (๐ ยท ๐)) |
83 | 14 | mulid2i 11167 |
. . . . . . . . . . . . . . . . . 18
โข (1
ยท ฯ) = ฯ |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ (1
ยท ฯ) = ฯ) |
85 | 82, 84 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ (((2
ยท ๐) ยท ฯ)
+ (1 ยท ฯ)) = ((๐
ยท ๐) +
ฯ)) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (((2 ยท
๐) ยท ฯ) + (1
ยท ฯ)) = ((๐
ยท ๐) +
ฯ)) |
87 | 40, 43 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ ๐ โ
โ) |
88 | 16, 87 | mulcld 11182 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ (๐ ยท ๐) โ โ) |
89 | 88, 15 | addcomd 11364 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ ((๐ ยท ๐) + ฯ) = (ฯ + (๐ ยท ๐))) |
90 | 89 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ((๐ ยท ๐) + ฯ) = (ฯ + (๐ ยท ๐))) |
91 | 75, 86, 90 | 3eqtrrd 2782 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (ฯ + (๐ ยท ๐)) = (((2 ยท ๐) + 1) ยท ฯ)) |
92 | | peano2cn 11334 |
. . . . . . . . . . . . . . . . 17
โข ((2
ยท ๐) โ โ
โ ((2 ยท ๐) + 1)
โ โ) |
93 | 71, 92 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ ((2
ยท ๐) + 1) โ
โ) |
94 | 93, 15 | mulcomd 11183 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (((2
ยท ๐) + 1) ยท
ฯ) = (ฯ ยท ((2 ยท ๐) + 1))) |
95 | 94 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (((2 ยท
๐) + 1) ยท ฯ) =
(ฯ ยท ((2 ยท ๐) + 1))) |
96 | | id 22 |
. . . . . . . . . . . . . . . . 17
โข (((2
ยท ๐) + 1) = (๐ / ฯ) โ ((2 ยท
๐) + 1) = (๐ / ฯ)) |
97 | 96 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
โข (((2
ยท ๐) + 1) = (๐ / ฯ) โ (๐ / ฯ) = ((2 ยท ๐) + 1)) |
98 | 97 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (๐ / ฯ) = ((2 ยท ๐) + 1)) |
99 | 27 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ๐ โ
โ) |
100 | 93 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ((2 ยท
๐) + 1) โ
โ) |
101 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ฯ โ
0) |
102 | 99, 74, 100, 101 | divmuld 11960 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ((๐ / ฯ) = ((2 ยท ๐) + 1) โ (ฯ ยท ((2
ยท ๐) + 1)) = ๐)) |
103 | 98, 102 | mpbid 231 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (ฯ ยท
((2 ยท ๐) + 1)) =
๐) |
104 | 91, 95, 103 | 3eqtrrd 2782 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ๐ = (ฯ + (๐ ยท ๐))) |
105 | 104 | oveq1d 7377 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (๐ mod ๐) = ((ฯ + (๐ ยท ๐)) mod ๐)) |
106 | | modcyc 13818 |
. . . . . . . . . . . . . 14
โข ((ฯ
โ โ โง ๐
โ โ+ โง ๐ โ โค) โ ((ฯ + (๐ ยท ๐)) mod ๐) = (ฯ mod ๐)) |
107 | 33, 63, 106 | mp3an12 1452 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ((ฯ +
(๐ ยท ๐)) mod ๐) = (ฯ mod ๐)) |
108 | 107 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ((ฯ + (๐ ยท ๐)) mod ๐) = (ฯ mod ๐)) |
109 | 33 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ฯ โ
โ) |
110 | 63 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ๐ โ
โ+) |
111 | | 0re 11164 |
. . . . . . . . . . . . . . 15
โข 0 โ
โ |
112 | 111, 33, 34 | ltleii 11285 |
. . . . . . . . . . . . . 14
โข 0 โค
ฯ |
113 | 112 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ 0 โค
ฯ) |
114 | | 2timesgt 43596 |
. . . . . . . . . . . . . . . 16
โข (ฯ
โ โ+ โ ฯ < (2 ยท ฯ)) |
115 | 5, 114 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข ฯ <
(2 ยท ฯ) |
116 | 115, 40 | breqtrri 5137 |
. . . . . . . . . . . . . 14
โข ฯ <
๐ |
117 | 116 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ ฯ < ๐) |
118 | | modid 13808 |
. . . . . . . . . . . . 13
โข (((ฯ
โ โ โง ๐
โ โ+) โง (0 โค ฯ โง ฯ < ๐)) โ (ฯ mod ๐) = ฯ) |
119 | 109, 110,
113, 117, 118 | syl22anc 838 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (ฯ mod ๐) = ฯ) |
120 | 105, 108,
119 | 3eqtrd 2781 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = (๐ / ฯ)) โ (๐ mod ๐) = ฯ) |
121 | 120 | ex 414 |
. . . . . . . . . 10
โข (๐ โ โค โ (((2
ยท ๐) + 1) = (๐ / ฯ) โ (๐ mod ๐) = ฯ)) |
122 | 121 | a1i 11 |
. . . . . . . . 9
โข (((๐ mod ฯ) = 0 โง ยฌ 2
โฅ (๐ / ฯ)) โ
(๐ โ โค โ
(((2 ยท ๐) + 1) =
(๐ / ฯ) โ (๐ mod ๐) = ฯ))) |
123 | 122 | rexlimdv 3151 |
. . . . . . . 8
โข (((๐ mod ฯ) = 0 โง ยฌ 2
โฅ (๐ / ฯ)) โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
(๐ / ฯ) โ (๐ mod ๐) = ฯ)) |
124 | 70, 123 | mpd 15 |
. . . . . . 7
โข (((๐ mod ฯ) = 0 โง ยฌ 2
โฅ (๐ / ฯ)) โ
(๐ mod ๐) = ฯ) |
125 | 124 | olcd 873 |
. . . . . 6
โข (((๐ mod ฯ) = 0 โง ยฌ 2
โฅ (๐ / ฯ)) โ
((๐ mod ๐) = 0 โจ (๐ mod ๐) = ฯ)) |
126 | 67, 125 | pm2.61dan 812 |
. . . . 5
โข ((๐ mod ฯ) = 0 โ ((๐ mod ๐) = 0 โจ (๐ mod ๐) = ฯ)) |
127 | | 0xr 11209 |
. . . . . . . 8
โข 0 โ
โ* |
128 | 33 | rexri 11220 |
. . . . . . . 8
โข ฯ
โ โ* |
129 | | iocgtlb 43814 |
. . . . . . . 8
โข ((0
โ โ* โง ฯ โ โ* โง (๐ mod ๐) โ (0(,]ฯ)) โ 0 < (๐ mod ๐)) |
130 | 127, 128,
129 | mp3an12 1452 |
. . . . . . 7
โข ((๐ mod ๐) โ (0(,]ฯ) โ 0 < (๐ mod ๐)) |
131 | 130 | gt0ne0d 11726 |
. . . . . 6
โข ((๐ mod ๐) โ (0(,]ฯ) โ (๐ mod ๐) โ 0) |
132 | 131 | neneqd 2949 |
. . . . 5
โข ((๐ mod ๐) โ (0(,]ฯ) โ ยฌ (๐ mod ๐) = 0) |
133 | | pm2.53 850 |
. . . . . 6
โข (((๐ mod ๐) = 0 โจ (๐ mod ๐) = ฯ) โ (ยฌ (๐ mod ๐) = 0 โ (๐ mod ๐) = ฯ)) |
134 | 133 | imp 408 |
. . . . 5
โข ((((๐ mod ๐) = 0 โจ (๐ mod ๐) = ฯ) โง ยฌ (๐ mod ๐) = 0) โ (๐ mod ๐) = ฯ) |
135 | 126, 132,
134 | syl2anr 598 |
. . . 4
โข (((๐ mod ๐) โ (0(,]ฯ) โง (๐ mod ฯ) = 0) โ (๐ mod ๐) = ฯ) |
136 | 127 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ mod ๐) = ฯ โ 0 โ
โ*) |
137 | 128 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ mod ๐) = ฯ โ ฯ โ
โ*) |
138 | | modcl 13785 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ+)
โ (๐ mod ๐) โ
โ) |
139 | 4, 63, 138 | mp2an 691 |
. . . . . . . . . . . . . 14
โข (๐ mod ๐) โ โ |
140 | 139 | rexri 11220 |
. . . . . . . . . . . . 13
โข (๐ mod ๐) โ
โ* |
141 | 140 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ mod ๐) = ฯ โ (๐ mod ๐) โ
โ*) |
142 | | id 22 |
. . . . . . . . . . . . 13
โข ((๐ mod ๐) = ฯ โ (๐ mod ๐) = ฯ) |
143 | 34, 142 | breqtrrid 5148 |
. . . . . . . . . . . 12
โข ((๐ mod ๐) = ฯ โ 0 < (๐ mod ๐)) |
144 | 33 | eqlei2 11273 |
. . . . . . . . . . . 12
โข ((๐ mod ๐) = ฯ โ (๐ mod ๐) โค ฯ) |
145 | 136, 137,
141, 143, 144 | eliocd 43819 |
. . . . . . . . . . 11
โข ((๐ mod ๐) = ฯ โ (๐ mod ๐) โ (0(,]ฯ)) |
146 | 145 | iftrued 4499 |
. . . . . . . . . 10
โข ((๐ mod ๐) = ฯ โ if((๐ mod ๐) โ (0(,]ฯ), 1, -1) =
1) |
147 | 146 | adantl 483 |
. . . . . . . . 9
โข (((๐ mod ฯ) = 0 โง (๐ mod ๐) = ฯ) โ if((๐ mod ๐) โ (0(,]ฯ), 1, -1) =
1) |
148 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ (๐ฅ mod ๐) = (๐ mod ๐)) |
149 | 148 | breq1d 5120 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ ((๐ฅ mod ๐) < ฯ โ (๐ mod ๐) < ฯ)) |
150 | 149 | ifbid 4514 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ โ if((๐ฅ mod ๐) < ฯ, 1, -1) = if((๐ mod ๐) < ฯ, 1, -1)) |
151 | | fourierswlem.f |
. . . . . . . . . . . . 13
โข ๐น = (๐ฅ โ โ โฆ if((๐ฅ mod ๐) < ฯ, 1, -1)) |
152 | | 1ex 11158 |
. . . . . . . . . . . . . 14
โข 1 โ
V |
153 | | negex 11406 |
. . . . . . . . . . . . . 14
โข -1 โ
V |
154 | 152, 153 | ifex 4541 |
. . . . . . . . . . . . 13
โข if((๐ mod ๐) < ฯ, 1, -1) โ
V |
155 | 150, 151,
154 | fvmpt 6953 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐นโ๐) = if((๐ mod ๐) < ฯ, 1, -1)) |
156 | 4, 155 | ax-mp 5 |
. . . . . . . . . . 11
โข (๐นโ๐) = if((๐ mod ๐) < ฯ, 1, -1) |
157 | 139 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ mod ๐) < ฯ โ (๐ mod ๐) โ โ) |
158 | | id 22 |
. . . . . . . . . . . . . 14
โข ((๐ mod ๐) < ฯ โ (๐ mod ๐) < ฯ) |
159 | 157, 158 | ltned 11298 |
. . . . . . . . . . . . 13
โข ((๐ mod ๐) < ฯ โ (๐ mod ๐) โ ฯ) |
160 | 159 | necon2bi 2975 |
. . . . . . . . . . . 12
โข ((๐ mod ๐) = ฯ โ ยฌ (๐ mod ๐) < ฯ) |
161 | 160 | iffalsed 4502 |
. . . . . . . . . . 11
โข ((๐ mod ๐) = ฯ โ if((๐ mod ๐) < ฯ, 1, -1) = -1) |
162 | 156, 161 | eqtrid 2789 |
. . . . . . . . . 10
โข ((๐ mod ๐) = ฯ โ (๐นโ๐) = -1) |
163 | 162 | adantl 483 |
. . . . . . . . 9
โข (((๐ mod ฯ) = 0 โง (๐ mod ๐) = ฯ) โ (๐นโ๐) = -1) |
164 | 147, 163 | oveq12d 7380 |
. . . . . . . 8
โข (((๐ mod ฯ) = 0 โง (๐ mod ๐) = ฯ) โ (if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) = (1 + -1)) |
165 | | 1pneg1e0 12279 |
. . . . . . . 8
โข (1 + -1)
= 0 |
166 | 164, 165 | eqtrdi 2793 |
. . . . . . 7
โข (((๐ mod ฯ) = 0 โง (๐ mod ๐) = ฯ) โ (if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) = 0) |
167 | 166 | oveq1d 7377 |
. . . . . 6
โข (((๐ mod ฯ) = 0 โง (๐ mod ๐) = ฯ) โ ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2) = (0 / 2)) |
168 | 167 | adantll 713 |
. . . . 5
โข ((((๐ mod ๐) โ (0(,]ฯ) โง (๐ mod ฯ) = 0) โง (๐ mod ๐) = ฯ) โ ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2) = (0 / 2)) |
169 | | 2cn 12235 |
. . . . . . 7
โข 2 โ
โ |
170 | 169, 44 | div0i 11896 |
. . . . . 6
โข (0 / 2) =
0 |
171 | 170 | a1i 11 |
. . . . 5
โข ((((๐ mod ๐) โ (0(,]ฯ) โง (๐ mod ฯ) = 0) โง (๐ mod ๐) = ฯ) โ (0 / 2) =
0) |
172 | | fourierswlem.y |
. . . . . . 7
โข ๐ = if((๐ mod ฯ) = 0, 0, (๐นโ๐)) |
173 | | iftrue 4497 |
. . . . . . 7
โข ((๐ mod ฯ) = 0 โ if((๐ mod ฯ) = 0, 0, (๐นโ๐)) = 0) |
174 | 172, 173 | eqtr2id 2790 |
. . . . . 6
โข ((๐ mod ฯ) = 0 โ 0 = ๐) |
175 | 174 | ad2antlr 726 |
. . . . 5
โข ((((๐ mod ๐) โ (0(,]ฯ) โง (๐ mod ฯ) = 0) โง (๐ mod ๐) = ฯ) โ 0 = ๐) |
176 | 168, 171,
175 | 3eqtrrd 2782 |
. . . 4
โข ((((๐ mod ๐) โ (0(,]ฯ) โง (๐ mod ฯ) = 0) โง (๐ mod ๐) = ฯ) โ ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2)) |
177 | 135, 176 | mpdan 686 |
. . 3
โข (((๐ mod ๐) โ (0(,]ฯ) โง (๐ mod ฯ) = 0) โ ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2)) |
178 | | iftrue 4497 |
. . . . . . 7
โข ((๐ mod ๐) โ (0(,]ฯ) โ if((๐ mod ๐) โ (0(,]ฯ), 1, -1) =
1) |
179 | 178 | adantr 482 |
. . . . . 6
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ if((๐ mod ๐) โ (0(,]ฯ), 1, -1) =
1) |
180 | 139 | a1i 11 |
. . . . . . . 8
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ (๐ mod ๐) โ โ) |
181 | 33 | a1i 11 |
. . . . . . . 8
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ ฯ
โ โ) |
182 | | iocleub 43815 |
. . . . . . . . . 10
โข ((0
โ โ* โง ฯ โ โ* โง (๐ mod ๐) โ (0(,]ฯ)) โ (๐ mod ๐) โค ฯ) |
183 | 127, 128,
182 | mp3an12 1452 |
. . . . . . . . 9
โข ((๐ mod ๐) โ (0(,]ฯ) โ (๐ mod ๐) โค ฯ) |
184 | 183 | adantr 482 |
. . . . . . . 8
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ (๐ mod ๐) โค ฯ) |
185 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . . . . . 20
โข 1 โ
โ |
186 | 185, 14 | mulcomi 11170 |
. . . . . . . . . . . . . . . . . . 19
โข (1
ยท ฯ) = (ฯ ยท 1) |
187 | 83, 186 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . 18
โข ฯ =
(ฯ ยท 1) |
188 | 187 | oveq1i 7372 |
. . . . . . . . . . . . . . . . 17
โข (ฯ +
(ฯ ยท (2 ยท (โโ(๐ / ๐))))) = ((ฯ ยท 1) + (ฯ ยท
(2 ยท (โโ(๐ / ๐))))) |
189 | 169, 14 | mulcomi 11170 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2
ยท ฯ) = (ฯ ยท 2) |
190 | 40, 189 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . 20
โข ๐ = (ฯ ยท
2) |
191 | 190 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ ยท (โโ(๐ / ๐))) = ((ฯ ยท 2) ยท
(โโ(๐ / ๐))) |
192 | 111, 62 | gtneii 11274 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ๐ โ 0 |
193 | 4, 59, 192 | redivcli 11929 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ / ๐) โ โ |
194 | | flcl 13707 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ / ๐) โ โ โ
(โโ(๐ / ๐)) โ
โค) |
195 | 193, 194 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(โโ(๐ /
๐)) โ
โค |
196 | | zcn 12511 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((โโ(๐ /
๐)) โ โค โ
(โโ(๐ / ๐)) โ
โ) |
197 | 195, 196 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
โข
(โโ(๐ /
๐)) โ
โ |
198 | 14, 169, 197 | mulassi 11173 |
. . . . . . . . . . . . . . . . . . 19
โข ((ฯ
ยท 2) ยท (โโ(๐ / ๐))) = (ฯ ยท (2 ยท
(โโ(๐ / ๐)))) |
199 | 191, 198 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
โข (๐ ยท (โโ(๐ / ๐))) = (ฯ ยท (2 ยท
(โโ(๐ / ๐)))) |
200 | 199 | oveq2i 7373 |
. . . . . . . . . . . . . . . . 17
โข (ฯ +
(๐ ยท
(โโ(๐ / ๐)))) = (ฯ + (ฯ ยท (2
ยท (โโ(๐
/ ๐))))) |
201 | 169, 197 | mulcli 11169 |
. . . . . . . . . . . . . . . . . 18
โข (2
ยท (โโ(๐
/ ๐))) โ
โ |
202 | 14, 185, 201 | adddii 11174 |
. . . . . . . . . . . . . . . . 17
โข (ฯ
ยท (1 + (2 ยท (โโ(๐ / ๐))))) = ((ฯ ยท 1) + (ฯ ยท
(2 ยท (โโ(๐ / ๐))))) |
203 | 188, 200,
202 | 3eqtr4ri 2776 |
. . . . . . . . . . . . . . . 16
โข (ฯ
ยท (1 + (2 ยท (โโ(๐ / ๐))))) = (ฯ + (๐ ยท (โโ(๐ / ๐)))) |
204 | 203 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (ฯ =
(๐ mod ๐) โ (ฯ ยท (1 + (2 ยท
(โโ(๐ / ๐))))) = (ฯ + (๐ ยท (โโ(๐ / ๐))))) |
205 | | id 22 |
. . . . . . . . . . . . . . . . 17
โข (ฯ =
(๐ mod ๐) โ ฯ = (๐ mod ๐)) |
206 | | modval 13783 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ+)
โ (๐ mod ๐) = (๐ โ (๐ ยท (โโ(๐ / ๐))))) |
207 | 4, 63, 206 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
โข (๐ mod ๐) = (๐ โ (๐ ยท (โโ(๐ / ๐)))) |
208 | 205, 207 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
โข (ฯ =
(๐ mod ๐) โ ฯ = (๐ โ (๐ ยท (โโ(๐ / ๐))))) |
209 | 208 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (ฯ =
(๐ mod ๐) โ (ฯ + (๐ ยท (โโ(๐ / ๐)))) = ((๐ โ (๐ ยท (โโ(๐ / ๐)))) + (๐ ยท (โโ(๐ / ๐))))) |
210 | 27 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (ฯ =
(๐ mod ๐) โ ๐ โ โ) |
211 | 59 | recni 11176 |
. . . . . . . . . . . . . . . . . 18
โข ๐ โ โ |
212 | 211, 197 | mulcli 11169 |
. . . . . . . . . . . . . . . . 17
โข (๐ ยท (โโ(๐ / ๐))) โ โ |
213 | 212 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (ฯ =
(๐ mod ๐) โ (๐ ยท (โโ(๐ / ๐))) โ โ) |
214 | 210, 213 | npcand 11523 |
. . . . . . . . . . . . . . 15
โข (ฯ =
(๐ mod ๐) โ ((๐ โ (๐ ยท (โโ(๐ / ๐)))) + (๐ ยท (โโ(๐ / ๐)))) = ๐) |
215 | 204, 209,
214 | 3eqtrrd 2782 |
. . . . . . . . . . . . . 14
โข (ฯ =
(๐ mod ๐) โ ๐ = (ฯ ยท (1 + (2 ยท
(โโ(๐ / ๐)))))) |
216 | 215 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (ฯ =
(๐ mod ๐) โ (๐ / ฯ) = ((ฯ ยท (1 + (2 ยท
(โโ(๐ / ๐))))) / ฯ)) |
217 | 185, 201 | addcli 11168 |
. . . . . . . . . . . . . 14
โข (1 + (2
ยท (โโ(๐
/ ๐)))) โ
โ |
218 | 217, 14, 35 | divcan3i 11908 |
. . . . . . . . . . . . 13
โข ((ฯ
ยท (1 + (2 ยท (โโ(๐ / ๐))))) / ฯ) = (1 + (2 ยท
(โโ(๐ / ๐)))) |
219 | 216, 218 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข (ฯ =
(๐ mod ๐) โ (๐ / ฯ) = (1 + (2 ยท
(โโ(๐ / ๐))))) |
220 | | 1z 12540 |
. . . . . . . . . . . . . 14
โข 1 โ
โค |
221 | | zmulcl 12559 |
. . . . . . . . . . . . . . 15
โข ((2
โ โค โง (โโ(๐ / ๐)) โ โค) โ (2 ยท
(โโ(๐ / ๐))) โ
โค) |
222 | 2, 195, 221 | mp2an 691 |
. . . . . . . . . . . . . 14
โข (2
ยท (โโ(๐
/ ๐))) โ
โค |
223 | | zaddcl 12550 |
. . . . . . . . . . . . . 14
โข ((1
โ โค โง (2 ยท (โโ(๐ / ๐))) โ โค) โ (1 + (2 ยท
(โโ(๐ / ๐)))) โ
โค) |
224 | 220, 222,
223 | mp2an 691 |
. . . . . . . . . . . . 13
โข (1 + (2
ยท (โโ(๐
/ ๐)))) โ
โค |
225 | 224 | a1i 11 |
. . . . . . . . . . . 12
โข (ฯ =
(๐ mod ๐) โ (1 + (2 ยท
(โโ(๐ / ๐)))) โ
โค) |
226 | 219, 225 | eqeltrd 2838 |
. . . . . . . . . . 11
โข (ฯ =
(๐ mod ๐) โ (๐ / ฯ) โ โค) |
227 | 226, 7 | sylibr 233 |
. . . . . . . . . 10
โข (ฯ =
(๐ mod ๐) โ (๐ mod ฯ) = 0) |
228 | 227 | necon3bi 2971 |
. . . . . . . . 9
โข (ยฌ
(๐ mod ฯ) = 0 โ
ฯ โ (๐ mod ๐)) |
229 | 228 | adantl 483 |
. . . . . . . 8
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ ฯ โ
(๐ mod ๐)) |
230 | 180, 181,
184, 229 | leneltd 11316 |
. . . . . . 7
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ (๐ mod ๐) < ฯ) |
231 | | iftrue 4497 |
. . . . . . . 8
โข ((๐ mod ๐) < ฯ โ if((๐ mod ๐) < ฯ, 1, -1) = 1) |
232 | 156, 231 | eqtrid 2789 |
. . . . . . 7
โข ((๐ mod ๐) < ฯ โ (๐นโ๐) = 1) |
233 | 230, 232 | syl 17 |
. . . . . 6
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ (๐นโ๐) = 1) |
234 | 179, 233 | oveq12d 7380 |
. . . . 5
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ
(if((๐ mod ๐) โ (0(,]ฯ), 1, -1) +
(๐นโ๐)) = (1 + 1)) |
235 | 234 | oveq1d 7377 |
. . . 4
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ
((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) +
(๐นโ๐)) / 2) = ((1 + 1) / 2)) |
236 | | 1p1e2 12285 |
. . . . . . 7
โข (1 + 1) =
2 |
237 | 236 | oveq1i 7372 |
. . . . . 6
โข ((1 + 1)
/ 2) = (2 / 2) |
238 | | 2div2e1 12301 |
. . . . . 6
โข (2 / 2) =
1 |
239 | 237, 238 | eqtr2i 2766 |
. . . . 5
โข 1 = ((1 +
1) / 2) |
240 | 233, 239 | eqtr2di 2794 |
. . . 4
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ ((1 + 1)
/ 2) = (๐นโ๐)) |
241 | | iffalse 4500 |
. . . . . 6
โข (ยฌ
(๐ mod ฯ) = 0 โ
if((๐ mod ฯ) = 0, 0,
(๐นโ๐)) = (๐นโ๐)) |
242 | 172, 241 | eqtr2id 2790 |
. . . . 5
โข (ยฌ
(๐ mod ฯ) = 0 โ
(๐นโ๐) = ๐) |
243 | 242 | adantl 483 |
. . . 4
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ (๐นโ๐) = ๐) |
244 | 235, 240,
243 | 3eqtrrd 2782 |
. . 3
โข (((๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ฯ) = 0) โ ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2)) |
245 | 177, 244 | pm2.61dan 812 |
. 2
โข ((๐ mod ๐) โ (0(,]ฯ) โ ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2)) |
246 | 131 | necon2bi 2975 |
. . . . . . . 8
โข ((๐ mod ๐) = 0 โ ยฌ (๐ mod ๐) โ (0(,]ฯ)) |
247 | 246 | iffalsed 4502 |
. . . . . . 7
โข ((๐ mod ๐) = 0 โ if((๐ mod ๐) โ (0(,]ฯ), 1, -1) =
-1) |
248 | | id 22 |
. . . . . . . . . 10
โข ((๐ mod ๐) = 0 โ (๐ mod ๐) = 0) |
249 | 248, 34 | eqbrtrdi 5149 |
. . . . . . . . 9
โข ((๐ mod ๐) = 0 โ (๐ mod ๐) < ฯ) |
250 | 249 | iftrued 4499 |
. . . . . . . 8
โข ((๐ mod ๐) = 0 โ if((๐ mod ๐) < ฯ, 1, -1) = 1) |
251 | 156, 250 | eqtrid 2789 |
. . . . . . 7
โข ((๐ mod ๐) = 0 โ (๐นโ๐) = 1) |
252 | 247, 251 | oveq12d 7380 |
. . . . . 6
โข ((๐ mod ๐) = 0 โ (if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) = (-1 + 1)) |
253 | 252 | oveq1d 7377 |
. . . . 5
โข ((๐ mod ๐) = 0 โ ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2) = ((-1 + 1) / 2)) |
254 | | neg1cn 12274 |
. . . . . . . . 9
โข -1 โ
โ |
255 | 185, 254,
165 | addcomli 11354 |
. . . . . . . 8
โข (-1 + 1)
= 0 |
256 | 255 | oveq1i 7372 |
. . . . . . 7
โข ((-1 + 1)
/ 2) = (0 / 2) |
257 | 256, 170 | eqtri 2765 |
. . . . . 6
โข ((-1 + 1)
/ 2) = 0 |
258 | 257 | a1i 11 |
. . . . 5
โข ((๐ mod ๐) = 0 โ ((-1 + 1) / 2) =
0) |
259 | 40 | oveq2i 7373 |
. . . . . . . . . . . . 13
โข (๐ / ๐) = (๐ / (2 ยท ฯ)) |
260 | | 2cnne0 12370 |
. . . . . . . . . . . . . 14
โข (2 โ
โ โง 2 โ 0) |
261 | 14, 35 | pm3.2i 472 |
. . . . . . . . . . . . . 14
โข (ฯ
โ โ โง ฯ โ 0) |
262 | | divdiv1 11873 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง (2 โ
โ โง 2 โ 0) โง (ฯ โ โ โง ฯ โ 0)) โ
((๐ / 2) / ฯ) = (๐ / (2 ยท
ฯ))) |
263 | 27, 260, 261, 262 | mp3an 1462 |
. . . . . . . . . . . . 13
โข ((๐ / 2) / ฯ) = (๐ / (2 ยท
ฯ)) |
264 | 27, 169, 14, 44, 35 | divdiv32i 11917 |
. . . . . . . . . . . . 13
โข ((๐ / 2) / ฯ) = ((๐ / ฯ) / 2) |
265 | 259, 263,
264 | 3eqtr2i 2771 |
. . . . . . . . . . . 12
โข (๐ / ๐) = ((๐ / ฯ) / 2) |
266 | 265 | oveq2i 7373 |
. . . . . . . . . . 11
โข (2
ยท (๐ / ๐)) = (2 ยท ((๐ / ฯ) / 2)) |
267 | 27, 14, 35 | divcli 11904 |
. . . . . . . . . . . 12
โข (๐ / ฯ) โ
โ |
268 | 267, 169,
44 | divcan2i 11905 |
. . . . . . . . . . 11
โข (2
ยท ((๐ / ฯ) / 2))
= (๐ /
ฯ) |
269 | 266, 268 | eqtr2i 2766 |
. . . . . . . . . 10
โข (๐ / ฯ) = (2 ยท (๐ / ๐)) |
270 | 2 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ / ๐) โ โค โ 2 โ
โค) |
271 | | id 22 |
. . . . . . . . . . 11
โข ((๐ / ๐) โ โค โ (๐ / ๐) โ โค) |
272 | 270, 271 | zmulcld 12620 |
. . . . . . . . . 10
โข ((๐ / ๐) โ โค โ (2 ยท (๐ / ๐)) โ โค) |
273 | 269, 272 | eqeltrid 2842 |
. . . . . . . . 9
โข ((๐ / ๐) โ โค โ (๐ / ฯ) โ โค) |
274 | 65, 273 | sylbi 216 |
. . . . . . . 8
โข ((๐ mod ๐) = 0 โ (๐ / ฯ) โ โค) |
275 | 274, 7 | sylibr 233 |
. . . . . . 7
โข ((๐ mod ๐) = 0 โ (๐ mod ฯ) = 0) |
276 | 275 | iftrued 4499 |
. . . . . 6
โข ((๐ mod ๐) = 0 โ if((๐ mod ฯ) = 0, 0, (๐นโ๐)) = 0) |
277 | 172, 276 | eqtr2id 2790 |
. . . . 5
โข ((๐ mod ๐) = 0 โ 0 = ๐) |
278 | 253, 258,
277 | 3eqtrrd 2782 |
. . . 4
โข ((๐ mod ๐) = 0 โ ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2)) |
279 | 278 | adantl 483 |
. . 3
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง (๐ mod ๐) = 0) โ ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2)) |
280 | 128 | a1i 11 |
. . . . 5
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ ฯ โ
โ*) |
281 | 59 | rexri 11220 |
. . . . . 6
โข ๐ โ
โ* |
282 | 281 | a1i 11 |
. . . . 5
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ ๐ โ
โ*) |
283 | 139 | a1i 11 |
. . . . 5
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ (๐ mod ๐) โ โ) |
284 | | pm4.56 988 |
. . . . . . . 8
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ ยฌ ((๐ mod ๐) โ (0(,]ฯ) โจ (๐ mod ๐) = 0)) |
285 | 284 | biimpi 215 |
. . . . . . 7
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ ยฌ ((๐ mod ๐) โ (0(,]ฯ) โจ (๐ mod ๐) = 0)) |
286 | | olc 867 |
. . . . . . . . 9
โข ((๐ mod ๐) = 0 โ ((๐ mod ๐) โ (0(,]ฯ) โจ (๐ mod ๐) = 0)) |
287 | 286 | adantl 483 |
. . . . . . . 8
โข (((๐ mod ๐) โค ฯ โง (๐ mod ๐) = 0) โ ((๐ mod ๐) โ (0(,]ฯ) โจ (๐ mod ๐) = 0)) |
288 | 127 | a1i 11 |
. . . . . . . . . 10
โข (((๐ mod ๐) โค ฯ โง ยฌ (๐ mod ๐) = 0) โ 0 โ
โ*) |
289 | 128 | a1i 11 |
. . . . . . . . . 10
โข (((๐ mod ๐) โค ฯ โง ยฌ (๐ mod ๐) = 0) โ ฯ โ
โ*) |
290 | 140 | a1i 11 |
. . . . . . . . . 10
โข (((๐ mod ๐) โค ฯ โง ยฌ (๐ mod ๐) = 0) โ (๐ mod ๐) โ
โ*) |
291 | | 0red 11165 |
. . . . . . . . . . . 12
โข (ยฌ
(๐ mod ๐) = 0 โ 0 โ
โ) |
292 | 139 | a1i 11 |
. . . . . . . . . . . 12
โข (ยฌ
(๐ mod ๐) = 0 โ (๐ mod ๐) โ โ) |
293 | | modge0 13791 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ+)
โ 0 โค (๐ mod ๐)) |
294 | 4, 63, 293 | mp2an 691 |
. . . . . . . . . . . . 13
โข 0 โค
(๐ mod ๐) |
295 | 294 | a1i 11 |
. . . . . . . . . . . 12
โข (ยฌ
(๐ mod ๐) = 0 โ 0 โค (๐ mod ๐)) |
296 | | neqne 2952 |
. . . . . . . . . . . 12
โข (ยฌ
(๐ mod ๐) = 0 โ (๐ mod ๐) โ 0) |
297 | 291, 292,
295, 296 | leneltd 11316 |
. . . . . . . . . . 11
โข (ยฌ
(๐ mod ๐) = 0 โ 0 < (๐ mod ๐)) |
298 | 297 | adantl 483 |
. . . . . . . . . 10
โข (((๐ mod ๐) โค ฯ โง ยฌ (๐ mod ๐) = 0) โ 0 < (๐ mod ๐)) |
299 | | simpl 484 |
. . . . . . . . . 10
โข (((๐ mod ๐) โค ฯ โง ยฌ (๐ mod ๐) = 0) โ (๐ mod ๐) โค ฯ) |
300 | 288, 289,
290, 298, 299 | eliocd 43819 |
. . . . . . . . 9
โข (((๐ mod ๐) โค ฯ โง ยฌ (๐ mod ๐) = 0) โ (๐ mod ๐) โ (0(,]ฯ)) |
301 | 300 | orcd 872 |
. . . . . . . 8
โข (((๐ mod ๐) โค ฯ โง ยฌ (๐ mod ๐) = 0) โ ((๐ mod ๐) โ (0(,]ฯ) โจ (๐ mod ๐) = 0)) |
302 | 287, 301 | pm2.61dan 812 |
. . . . . . 7
โข ((๐ mod ๐) โค ฯ โ ((๐ mod ๐) โ (0(,]ฯ) โจ (๐ mod ๐) = 0)) |
303 | 285, 302 | nsyl 140 |
. . . . . 6
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ ยฌ (๐ mod ๐) โค ฯ) |
304 | 33 | a1i 11 |
. . . . . . 7
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ ฯ โ
โ) |
305 | 304, 283 | ltnled 11309 |
. . . . . 6
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ (ฯ < (๐ mod ๐) โ ยฌ (๐ mod ๐) โค ฯ)) |
306 | 303, 305 | mpbird 257 |
. . . . 5
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ ฯ < (๐ mod ๐)) |
307 | | modlt 13792 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ+)
โ (๐ mod ๐) < ๐) |
308 | 4, 63, 307 | mp2an 691 |
. . . . . 6
โข (๐ mod ๐) < ๐ |
309 | 308 | a1i 11 |
. . . . 5
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ (๐ mod ๐) < ๐) |
310 | 280, 282,
283, 306, 309 | eliood 43810 |
. . . 4
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ (๐ mod ๐) โ (ฯ(,)๐)) |
311 | 127 | a1i 11 |
. . . . . . . . 9
โข ((๐ mod ๐) โ (ฯ(,)๐) โ 0 โ
โ*) |
312 | 33 | a1i 11 |
. . . . . . . . 9
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ฯ โ
โ) |
313 | 140 | a1i 11 |
. . . . . . . . 9
โข ((๐ mod ๐) โ (ฯ(,)๐) โ (๐ mod ๐) โ
โ*) |
314 | | ioogtlb 43807 |
. . . . . . . . . 10
โข ((ฯ
โ โ* โง ๐ โ โ* โง (๐ mod ๐) โ (ฯ(,)๐)) โ ฯ < (๐ mod ๐)) |
315 | 128, 281,
314 | mp3an12 1452 |
. . . . . . . . 9
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ฯ < (๐ mod ๐)) |
316 | 311, 312,
313, 315 | gtnelioc 43803 |
. . . . . . . 8
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ยฌ (๐ mod ๐) โ (0(,]ฯ)) |
317 | 316 | iffalsed 4502 |
. . . . . . 7
โข ((๐ mod ๐) โ (ฯ(,)๐) โ if((๐ mod ๐) โ (0(,]ฯ), 1, -1) =
-1) |
318 | 139 | a1i 11 |
. . . . . . . . . 10
โข ((๐ mod ๐) โ (ฯ(,)๐) โ (๐ mod ๐) โ โ) |
319 | 312, 318,
315 | ltnsymd 11311 |
. . . . . . . . 9
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ยฌ (๐ mod ๐) < ฯ) |
320 | 319 | iffalsed 4502 |
. . . . . . . 8
โข ((๐ mod ๐) โ (ฯ(,)๐) โ if((๐ mod ๐) < ฯ, 1, -1) = -1) |
321 | 156, 320 | eqtrid 2789 |
. . . . . . 7
โข ((๐ mod ๐) โ (ฯ(,)๐) โ (๐นโ๐) = -1) |
322 | 317, 321 | oveq12d 7380 |
. . . . . 6
โข ((๐ mod ๐) โ (ฯ(,)๐) โ (if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) = (-1 + -1)) |
323 | 322 | oveq1d 7377 |
. . . . 5
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2) = ((-1 + -1) / 2)) |
324 | | df-2 12223 |
. . . . . . . . . 10
โข 2 = (1 +
1) |
325 | 324 | negeqi 11401 |
. . . . . . . . 9
โข -2 = -(1
+ 1) |
326 | 185, 185 | negdii 11492 |
. . . . . . . . 9
โข -(1 + 1)
= (-1 + -1) |
327 | 325, 326 | eqtr2i 2766 |
. . . . . . . 8
โข (-1 + -1)
= -2 |
328 | 327 | oveq1i 7372 |
. . . . . . 7
โข ((-1 +
-1) / 2) = (-2 / 2) |
329 | | divneg 11854 |
. . . . . . . 8
โข ((2
โ โ โง 2 โ โ โง 2 โ 0) โ -(2 / 2) = (-2 /
2)) |
330 | 169, 169,
44, 329 | mp3an 1462 |
. . . . . . 7
โข -(2 / 2)
= (-2 / 2) |
331 | 238 | negeqi 11401 |
. . . . . . 7
โข -(2 / 2)
= -1 |
332 | 328, 330,
331 | 3eqtr2i 2771 |
. . . . . 6
โข ((-1 +
-1) / 2) = -1 |
333 | 332 | a1i 11 |
. . . . 5
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ((-1 + -1) / 2) =
-1) |
334 | 172 | a1i 11 |
. . . . . 6
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ๐ = if((๐ mod ฯ) = 0, 0, (๐นโ๐))) |
335 | 312, 318 | ltnled 11309 |
. . . . . . . . 9
โข ((๐ mod ๐) โ (ฯ(,)๐) โ (ฯ < (๐ mod ๐) โ ยฌ (๐ mod ๐) โค ฯ)) |
336 | 315, 335 | mpbid 231 |
. . . . . . . 8
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ยฌ (๐ mod ๐) โค ฯ) |
337 | 248, 112 | eqbrtrdi 5149 |
. . . . . . . . . 10
โข ((๐ mod ๐) = 0 โ (๐ mod ๐) โค ฯ) |
338 | 337 | adantl 483 |
. . . . . . . . 9
โข (((๐ mod ฯ) = 0 โง (๐ mod ๐) = 0) โ (๐ mod ๐) โค ฯ) |
339 | 126 | orcanai 1002 |
. . . . . . . . . 10
โข (((๐ mod ฯ) = 0 โง ยฌ
(๐ mod ๐) = 0) โ (๐ mod ๐) = ฯ) |
340 | 339, 144 | syl 17 |
. . . . . . . . 9
โข (((๐ mod ฯ) = 0 โง ยฌ
(๐ mod ๐) = 0) โ (๐ mod ๐) โค ฯ) |
341 | 338, 340 | pm2.61dan 812 |
. . . . . . . 8
โข ((๐ mod ฯ) = 0 โ (๐ mod ๐) โค ฯ) |
342 | 336, 341 | nsyl 140 |
. . . . . . 7
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ยฌ (๐ mod ฯ) = 0) |
343 | 342 | iffalsed 4502 |
. . . . . 6
โข ((๐ mod ๐) โ (ฯ(,)๐) โ if((๐ mod ฯ) = 0, 0, (๐นโ๐)) = (๐นโ๐)) |
344 | 334, 343,
321 | 3eqtrrd 2782 |
. . . . 5
โข ((๐ mod ๐) โ (ฯ(,)๐) โ -1 = ๐) |
345 | 323, 333,
344 | 3eqtrrd 2782 |
. . . 4
โข ((๐ mod ๐) โ (ฯ(,)๐) โ ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2)) |
346 | 310, 345 | syl 17 |
. . 3
โข ((ยฌ
(๐ mod ๐) โ (0(,]ฯ) โง ยฌ (๐ mod ๐) = 0) โ ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2)) |
347 | 279, 346 | pm2.61dan 812 |
. 2
โข (ยฌ
(๐ mod ๐) โ (0(,]ฯ) โ ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2)) |
348 | 245, 347 | pm2.61i 182 |
1
โข ๐ = ((if((๐ mod ๐) โ (0(,]ฯ), 1, -1) + (๐นโ๐)) / 2) |