Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . 3
โข ๐
= (๐ฅ โ (1...๐ป) โฆ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2)))) |
2 | | oveq1 7420 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ฅ ยท 2) = (๐ ยท 2)) |
3 | 2 | breq1d 5159 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ฅ ยท 2) < (๐ / 2) โ (๐ ยท 2) < (๐ / 2))) |
4 | 2 | oveq2d 7429 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ โ (๐ฅ ยท 2)) = (๐ โ (๐ ยท 2))) |
5 | 3, 2, 4 | ifbieq12d 4557 |
. . . . 5
โข (๐ฅ = ๐ โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = if((๐ ยท 2) < (๐ / 2), (๐ ยท 2), (๐ โ (๐ ยท 2)))) |
6 | 5 | adantl 480 |
. . . 4
โข (((๐ โง ๐ โ ((๐ + 1)...๐ป)) โง ๐ฅ = ๐) โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = if((๐ ยท 2) < (๐ / 2), (๐ ยท 2), (๐ โ (๐ ยท 2)))) |
7 | | gausslemma2d.p |
. . . . . . . 8
โข (๐ โ ๐ โ (โ โ
{2})) |
8 | 7 | gausslemma2dlem0a 27093 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
9 | | elfz2 13497 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1)...๐ป) โ (((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โง ((๐ + 1) โค ๐ โง ๐ โค ๐ป))) |
10 | | gausslemma2d.m |
. . . . . . . . . . . . . . . . 17
โข ๐ = (โโ(๐ / 4)) |
11 | 10 | oveq1i 7423 |
. . . . . . . . . . . . . . . 16
โข (๐ + 1) = ((โโ(๐ / 4)) + 1) |
12 | 11 | breq1i 5156 |
. . . . . . . . . . . . . . 15
โข ((๐ + 1) โค ๐ โ ((โโ(๐ / 4)) + 1) โค ๐) |
13 | | nnre 12225 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
14 | | 4re 12302 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 4 โ
โ |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ 4 โ
โ) |
16 | | 4ne0 12326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 4 โ
0 |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ 4 โ
0) |
18 | 13, 15, 17 | redivcld 12048 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐ / 4) โ
โ) |
19 | 18 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / 4) โ
โ) |
20 | | fllelt 13768 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ / 4) โ โ โ
((โโ(๐ / 4))
โค (๐ / 4) โง (๐ / 4) <
((โโ(๐ / 4)) +
1))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ๐ โ โ) โ
((โโ(๐ / 4))
โค (๐ / 4) โง (๐ / 4) <
((โโ(๐ / 4)) +
1))) |
22 | 18 | flcld 13769 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ โ โ
(โโ(๐ / 4))
โ โค) |
23 | 22 | zred 12672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ
(โโ(๐ / 4))
โ โ) |
24 | | peano2re 11393 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
((โโ(๐ /
4)) โ โ โ ((โโ(๐ / 4)) + 1) โ โ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ
((โโ(๐ / 4)) +
1) โ โ) |
26 | 25 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โค โง ๐ โ โ) โ
((โโ(๐ / 4)) +
1) โ โ) |
27 | | zre 12568 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โค โ ๐ โ
โ) |
28 | 27 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
29 | | ltleletr 11313 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ / 4) โ โ โง
((โโ(๐ / 4)) +
1) โ โ โง ๐
โ โ) โ (((๐
/ 4) < ((โโ(๐ / 4)) + 1) โง ((โโ(๐ / 4)) + 1) โค ๐) โ (๐ / 4) โค ๐)) |
30 | 19, 26, 28, 29 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ / 4) <
((โโ(๐ / 4)) +
1) โง ((โโ(๐
/ 4)) + 1) โค ๐) โ
(๐ / 4) โค ๐)) |
31 | 30 | expd 414 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / 4) <
((โโ(๐ / 4)) +
1) โ (((โโ(๐ / 4)) + 1) โค ๐ โ (๐ / 4) โค ๐))) |
32 | 31 | adantld 489 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ๐ โ โ) โ
(((โโ(๐ / 4))
โค (๐ / 4) โง (๐ / 4) <
((โโ(๐ / 4)) +
1)) โ (((โโ(๐ / 4)) + 1) โค ๐ โ (๐ / 4) โค ๐))) |
33 | 21, 32 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐ โ โ) โ
(((โโ(๐ / 4)) +
1) โค ๐ โ (๐ / 4) โค ๐)) |
34 | 33 | imp 405 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โค โง ๐ โ โ) โง
((โโ(๐ / 4)) +
1) โค ๐) โ (๐ / 4) โค ๐) |
35 | 13 | rehalfcld 12465 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐ / 2) โ
โ) |
36 | 35 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / 2) โ
โ) |
37 | | 2re 12292 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 2 โ
โ |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โค โ 2 โ
โ) |
39 | 27, 38 | remulcld 11250 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ (๐ ยท 2) โ
โ) |
40 | 39 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท 2) โ
โ) |
41 | | 2pos 12321 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 0 <
2 |
42 | 37, 41 | pm3.2i 469 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (2 โ
โ โง 0 < 2) |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โ) โ (2
โ โ โง 0 < 2)) |
44 | | lediv1 12085 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ / 2) โ โ โง
(๐ ยท 2) โ
โ โง (2 โ โ โง 0 < 2)) โ ((๐ / 2) โค (๐ ยท 2) โ ((๐ / 2) / 2) โค ((๐ ยท 2) / 2))) |
45 | 36, 40, 43, 44 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / 2) โค (๐ ยท 2) โ ((๐ / 2) / 2) โค ((๐ ยท 2) / 2))) |
46 | | nncn 12226 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
47 | | 2cnne0 12428 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (2 โ
โ โง 2 โ 0) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ (2 โ
โ โง 2 โ 0)) |
49 | | divdiv1 11931 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ โง (2 โ
โ โง 2 โ 0) โง (2 โ โ โง 2 โ 0)) โ ((๐ / 2) / 2) = (๐ / (2 ยท 2))) |
50 | 46, 48, 48, 49 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ((๐ / 2) / 2) = (๐ / (2 ยท 2))) |
51 | | 2t2e4 12382 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (2
ยท 2) = 4 |
52 | 51 | oveq2i 7424 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ / (2 ยท 2)) = (๐ / 4) |
53 | 50, 52 | eqtrdi 2786 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ((๐ / 2) / 2) = (๐ / 4)) |
54 | | zcn 12569 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ ๐ โ
โ) |
55 | | 2cnd 12296 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ 2 โ
โ) |
56 | | 2ne0 12322 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 2 โ
0 |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ 2 โ
0) |
58 | 54, 55, 57 | divcan4d 12002 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โค โ ((๐ ยท 2) / 2) = ๐) |
59 | 53, 58 | breqan12rd 5166 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ / 2) / 2) โค ((๐ ยท 2) / 2) โ (๐ / 4) โค ๐)) |
60 | 45, 59 | bitrd 278 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / 2) โค (๐ ยท 2) โ (๐ / 4) โค ๐)) |
61 | 60 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โค โง ๐ โ โ) โง
((โโ(๐ / 4)) +
1) โค ๐) โ ((๐ / 2) โค (๐ ยท 2) โ (๐ / 4) โค ๐)) |
62 | 34, 61 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โค โง ๐ โ โ) โง
((โโ(๐ / 4)) +
1) โค ๐) โ (๐ / 2) โค (๐ ยท 2)) |
63 | 62 | exp31 418 |
. . . . . . . . . . . . . . . 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 1133 |
. . . . . . . . . . . . 13
โข (((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โ ((๐ + 1) โค ๐ โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2)))) |
67 | 66 | com12 32 |
. . . . . . . . . . . 12
โข ((๐ + 1) โค ๐ โ (((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2)))) |
68 | 67 | adantr 479 |
. . . . . . . . . . 11
โข (((๐ + 1) โค ๐ โง ๐ โค ๐ป) โ (((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2)))) |
69 | 68 | impcom 406 |
. . . . . . . . . 10
โข ((((๐ + 1) โ โค โง ๐ป โ โค โง ๐ โ โค) โง ((๐ + 1) โค ๐ โง ๐ โค ๐ป)) โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2))) |
70 | 9, 69 | sylbi 216 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1)...๐ป) โ (๐ โ โ โ (๐ / 2) โค (๐ ยท 2))) |
71 | 70 | impcom 406 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ (๐ / 2) โค (๐ ยท 2)) |
72 | | elfzelz 13507 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + 1)...๐ป) โ ๐ โ โค) |
73 | 72 | zred 12672 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1)...๐ป) โ ๐ โ โ) |
74 | 37 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1)...๐ป) โ 2 โ โ) |
75 | 73, 74 | remulcld 11250 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1)...๐ป) โ (๐ ยท 2) โ โ) |
76 | | lenlt 11298 |
. . . . . . . . 9
โข (((๐ / 2) โ โ โง
(๐ ยท 2) โ
โ) โ ((๐ / 2)
โค (๐ ยท 2) โ
ยฌ (๐ ยท 2) <
(๐ / 2))) |
77 | 35, 75, 76 | syl2an 594 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ ((๐ / 2) โค (๐ ยท 2) โ ยฌ (๐ ยท 2) < (๐ / 2))) |
78 | 71, 77 | mpbid 231 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ ((๐ + 1)...๐ป)) โ ยฌ (๐ ยท 2) < (๐ / 2)) |
79 | 8, 78 | sylan 578 |
. . . . . 6
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ ยฌ (๐ ยท 2) < (๐ / 2)) |
80 | 79 | adantr 479 |
. . . . 5
โข (((๐ โง ๐ โ ((๐ + 1)...๐ป)) โง ๐ฅ = ๐) โ ยฌ (๐ ยท 2) < (๐ / 2)) |
81 | 80 | iffalsed 4540 |
. . . 4
โข (((๐ โง ๐ โ ((๐ + 1)...๐ป)) โง ๐ฅ = ๐) โ if((๐ ยท 2) < (๐ / 2), (๐ ยท 2), (๐ โ (๐ ยท 2))) = (๐ โ (๐ ยท 2))) |
82 | 6, 81 | eqtrd 2770 |
. . 3
โข (((๐ โง ๐ โ ((๐ + 1)...๐ป)) โง ๐ฅ = ๐) โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = (๐ โ (๐ ยท 2))) |
83 | 7, 10 | gausslemma2dlem0d 27096 |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
84 | | nn0p1nn 12517 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
85 | | nnuz 12871 |
. . . . . . 7
โข โ =
(โคโฅโ1) |
86 | 84, 85 | eleqtrdi 2841 |
. . . . . 6
โข (๐ โ โ0
โ (๐ + 1) โ
(โคโฅโ1)) |
87 | 83, 86 | syl 17 |
. . . . 5
โข (๐ โ (๐ + 1) โ
(โคโฅโ1)) |
88 | | fzss1 13546 |
. . . . 5
โข ((๐ + 1) โ
(โคโฅโ1) โ ((๐ + 1)...๐ป) โ (1...๐ป)) |
89 | 87, 88 | syl 17 |
. . . 4
โข (๐ โ ((๐ + 1)...๐ป) โ (1...๐ป)) |
90 | 89 | sselda 3983 |
. . 3
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ ๐ โ (1...๐ป)) |
91 | | ovexd 7448 |
. . 3
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ (๐ โ (๐ ยท 2)) โ V) |
92 | 1, 82, 90, 91 | fvmptd2 7007 |
. 2
โข ((๐ โง ๐ โ ((๐ + 1)...๐ป)) โ (๐
โ๐) = (๐ โ (๐ ยท 2))) |
93 | 92 | ralrimiva 3144 |
1
โข (๐ โ โ๐ โ ((๐ + 1)...๐ป)(๐
โ๐) = (๐ โ (๐ ยท 2))) |