Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . 3
โข ๐
= (๐ฅ โ (1...๐ป) โฆ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))) |
2 | | oveq1 7365 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ฅ ยท 2) = (๐ ยท 2)) |
3 | 2 | breq1d 5116 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ฅ ยท 2) < (๐ / 2) โ (๐ ยท 2) < (๐ / 2))) |
4 | 2 | oveq2d 7374 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ โ (๐ฅ ยท 2)) = (๐ โ (๐ ยท 2))) |
5 | 3, 2, 4 | ifbieq12d 4515 |
. . . . 5
โข (๐ฅ = ๐ โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = if((๐ ยท 2) < (๐ / 2), (๐ ยท 2), (๐ โ (๐ ยท 2)))) |
6 | 5 | adantl 483 |
. . . 4
โข (((๐ โง ๐ โ ((๐ + 1)...๐ป)) โง ๐ฅ = ๐) โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = if((๐ ยท 2) < (๐ / 2), (๐ ยท 2), (๐ โ (๐ ยท 2)))) |
7 | | gausslemma2d.p |
. . . . . . . 8
โข (๐ โ ๐ โ (โ โ
{2})) |
8 | 7 | gausslemma2dlem0a 26707 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
9 | | elfz2 13432 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1)...๐ป) โ (((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โง ((๐ + 1) โค ๐ โง ๐ โค ๐ป))) |
10 | | gausslemma2d.m |
. . . . . . . . . . . . . . . . 17
โข ๐ = (โโ(๐ / 4)) |
11 | 10 | oveq1i 7368 |
. . . . . . . . . . . . . . . 16
โข (๐ + 1) = ((โโ(๐ / 4)) + 1) |
12 | 11 | breq1i 5113 |
. . . . . . . . . . . . . . 15
โข ((๐ + 1) โค ๐ โ ((โโ(๐ / 4)) + 1) โค ๐) |
13 | | nnre 12161 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
14 | | 4re 12238 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 4 โ
โ |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ 4 โ
โ) |
16 | | 4ne0 12262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 4 โ
0 |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ 4 โ
0) |
18 | 13, 15, 17 | redivcld 11984 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐ / 4) โ
โ) |
19 | 18 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / 4) โ
โ) |
20 | | fllelt 13703 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ / 4) โ โ โ
((โโ(๐ / 4))
โค (๐ / 4) โง (๐ / 4) <
((โโ(๐ / 4)) +
1))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ๐ โ โ) โ
((โโ(๐ / 4))
โค (๐ / 4) โง (๐ / 4) <
((โโ(๐ / 4)) +
1))) |
22 | 18 | flcld 13704 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ
(โโ(๐ / 4))
โ โค) |
23 | 22 | zred 12608 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ
(โโ(๐ / 4))
โ โ) |
24 | | peano2re 11329 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((โโ(๐ /
4)) โ โ โ ((โโ(๐ / 4)) + 1) โ โ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ
((โโ(๐ / 4)) +
1) โ โ) |
26 | 25 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โค โง ๐ โ โ) โ
((โโ(๐ / 4)) +
1) โ โ) |
27 | | zre 12504 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โค โ ๐ โ
โ) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
29 | | ltleletr 11249 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ / 4) โ โ โง
((โโ(๐ / 4)) +
1) โ โ โง ๐
โ โ) โ (((๐
/ 4) < ((โโ(๐ / 4)) + 1) โง ((โโ(๐ / 4)) + 1) โค ๐) โ (๐ / 4) โค ๐)) |
30 | 19, 26, 28, 29 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ / 4) <
((โโ(๐ / 4)) +
1) โง ((โโ(๐
/ 4)) + 1) โค ๐) โ
(๐ / 4) โค ๐)) |
31 | 30 | expd 417 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / 4) <
((โโ(๐ / 4)) +
1) โ (((โโ(๐ / 4)) + 1) โค ๐ โ (๐ / 4) โค ๐))) |
32 | 31 | adantld 492 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ๐ โ โ) โ
(((โโ(๐ / 4))
โค (๐ / 4) โง (๐ / 4) <
((โโ(๐ / 4)) +
1)) โ (((โโ(๐ / 4)) + 1) โค ๐ โ (๐ / 4) โค ๐))) |
33 | 21, 32 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐ โ โ) โ
(((โโ(๐ / 4)) +
1) โค ๐ โ (๐ / 4) โค ๐)) |
34 | 33 | imp 408 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โค โง ๐ โ โ) โง
((โโ(๐ / 4)) +
1) โค ๐) โ (๐ / 4) โค ๐) |
35 | 13 | rehalfcld 12401 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐ / 2) โ
โ) |
36 | 35 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / 2) โ
โ) |
37 | | 2re 12228 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 2 โ
โ |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โค โ 2 โ
โ) |
39 | 27, 38 | remulcld 11186 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ (๐ ยท 2) โ
โ) |
40 | 39 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท 2) โ
โ) |
41 | | 2pos 12257 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 0 <
2 |
42 | 37, 41 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (2 โ
โ โง 0 < 2) |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ (2
โ โ โง 0 < 2)) |
44 | | lediv1 12021 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ / 2) โ โ โง
(๐ ยท 2) โ
โ โง (2 โ โ โง 0 < 2)) โ ((๐ / 2) โค (๐ ยท 2) โ ((๐ / 2) / 2) โค ((๐ ยท 2) / 2))) |
45 | 36, 40, 43, 44 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / 2) โค (๐ ยท 2) โ ((๐ / 2) / 2) โค ((๐ ยท 2) / 2))) |
46 | | nncn 12162 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
47 | | 2cnne0 12364 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (2 โ
โ โง 2 โ 0) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ (2 โ
โ โง 2 โ 0)) |
49 | | divdiv1 11867 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ โง (2 โ
โ โง 2 โ 0) โง (2 โ โ โง 2 โ 0)) โ ((๐ / 2) / 2) = (๐ / (2 ยท 2))) |
50 | 46, 48, 48, 49 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ((๐ / 2) / 2) = (๐ / (2 ยท 2))) |
51 | | 2t2e4 12318 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (2
ยท 2) = 4 |
52 | 51 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ / (2 ยท 2)) = (๐ / 4) |
53 | 50, 52 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ((๐ / 2) / 2) = (๐ / 4)) |
54 | | zcn 12505 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ ๐ โ
โ) |
55 | | 2cnd 12232 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ 2 โ
โ) |
56 | | 2ne0 12258 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 2 โ
0 |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ 2 โ
0) |
58 | 54, 55, 57 | divcan4d 11938 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โค โ ((๐ ยท 2) / 2) = ๐) |
59 | 53, 58 | breqan12rd 5123 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ / 2) / 2) โค ((๐ ยท 2) / 2) โ (๐ / 4) โค ๐)) |
60 | 45, 59 | bitrd 279 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / 2) โค (๐ ยท 2) โ (๐ / 4) โค ๐)) |
61 | 60 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โค โง ๐ โ โ) โง
((โโ(๐ / 4)) +
1) โค ๐) โ ((๐ / 2) โค (๐ ยท 2) โ (๐ / 4) โค ๐)) |
62 | 34, 61 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โค โง ๐ โ โ) โง
((โโ(๐ / 4)) +
1) โค ๐) โ (๐ / 2) โค (๐ ยท 2)) |
63 | 62 | exp31 421 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ (๐ โ โ โ
(((โโ(๐ / 4)) +
1) โค ๐ โ (๐ / 2) โค (๐ ยท 2)))) |
64 | 63 | com23 86 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ
(((โโ(๐ / 4)) +
1) โค ๐ โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2)))) |
65 | 12, 64 | biimtrid 241 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ((๐ + 1) โค ๐ โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2)))) |
66 | 65 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
โข (((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โ ((๐ + 1) โค ๐ โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2)))) |
67 | 66 | com12 32 |
. . . . . . . . . . . 12
โข ((๐ + 1) โค ๐ โ (((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2)))) |
68 | 67 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ + 1) โค ๐ โง ๐ โค ๐ป) โ (((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2)))) |
69 | 68 | impcom 409 |
. . . . . . . . . 10
โข ((((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โง ((๐ + 1) โค ๐ โง ๐ โค ๐ป)) โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2))) |
70 | 9, 69 | sylbi 216 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1)...๐ป) โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2))) |
71 | 70 | impcom 409 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ (๐ / 2) โค (๐ ยท 2)) |
72 | | elfzelz 13442 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + 1)...๐ป) โ ๐ โ โค) |
73 | 72 | zred 12608 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1)...๐ป) โ ๐ โ โ) |
74 | 37 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1)...๐ป) โ 2 โ โ) |
75 | 73, 74 | remulcld 11186 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1)...๐ป) โ (๐ ยท 2) โ โ) |
76 | | lenlt 11234 |
. . . . . . . . 9
โข (((๐ / 2) โ โ โง
(๐ ยท 2) โ
โ) โ ((๐ / 2)
โค (๐ ยท 2) โ
ยฌ (๐ ยท 2) <
(๐ / 2))) |
77 | 35, 75, 76 | syl2an 597 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ ((๐ / 2) โค (๐ ยท 2) โ ยฌ (๐ ยท 2) < (๐ / 2))) |
78 | 71, 77 | mpbid 231 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ ยฌ (๐ ยท 2) < (๐ / 2)) |
79 | 8, 78 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ ยฌ (๐ ยท 2) < (๐ / 2)) |
80 | 79 | adantr 482 |
. . . . 5
โข (((๐ โง ๐ โ ((๐ + 1)...๐ป)) โง ๐ฅ = ๐) โ ยฌ (๐ ยท 2) < (๐ / 2)) |
81 | 80 | iffalsed 4498 |
. . . 4
โข (((๐ โง ๐ โ ((๐ + 1)...๐ป)) โง ๐ฅ = ๐) โ if((๐ ยท 2) < (๐ / 2), (๐ ยท 2), (๐ โ (๐ ยท 2))) = (๐ โ (๐ ยท 2))) |
82 | 6, 81 | eqtrd 2777 |
. . 3
โข (((๐ โง ๐ โ ((๐ + 1)...๐ป)) โง ๐ฅ = ๐) โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = (๐ โ (๐ ยท 2))) |
83 | 7, 10 | gausslemma2dlem0d 26710 |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
84 | | nn0p1nn 12453 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
85 | | nnuz 12807 |
. . . . . . 7
โข โ =
(โคโฅโ1) |
86 | 84, 85 | eleqtrdi 2848 |
. . . . . 6
โข (๐ โ โ0
โ (๐ + 1) โ
(โคโฅโ1)) |
87 | 83, 86 | syl 17 |
. . . . 5
โข (๐ โ (๐ + 1) โ
(โคโฅโ1)) |
88 | | fzss1 13481 |
. . . . 5
โข ((๐ + 1) โ
(โคโฅโ1) โ ((๐ + 1)...๐ป) โ (1...๐ป)) |
89 | 87, 88 | syl 17 |
. . . 4
โข (๐ โ ((๐ + 1)...๐ป) โ (1...๐ป)) |
90 | 89 | sselda 3945 |
. . 3
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ ๐ โ (1...๐ป)) |
91 | | ovexd 7393 |
. . 3
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ (๐ โ (๐ ยท 2)) โ V) |
92 | 1, 82, 90, 91 | fvmptd2 6957 |
. 2
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ (๐
โ๐) = (๐ โ (๐ ยท 2))) |
93 | 92 | ralrimiva 3144 |
1
โข (๐ โ โ๐ โ ((๐ + 1)...๐ป)(๐
โ๐) = (๐ โ (๐ ยท 2))) |