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 | | elfz1b 13511 |
. . . . . . . 8
โข (๐ โ (1...๐) โ (๐ โ โ โง ๐ โ โ โง ๐ โค ๐)) |
8 | | nnre 12161 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
9 | 8 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
10 | | nnre 12161 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
11 | 10 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
12 | | 2re 12228 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
13 | | 2pos 12257 |
. . . . . . . . . . . . 13
โข 0 <
2 |
14 | 12, 13 | pm3.2i 472 |
. . . . . . . . . . . 12
โข (2 โ
โ โง 0 < 2) |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (2
โ โ โง 0 < 2)) |
16 | | lemul1 12008 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ โง (2 โ
โ โง 0 < 2)) โ (๐ โค ๐ โ (๐ ยท 2) โค (๐ ยท 2))) |
17 | 9, 11, 15, 16 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โค ๐ โ (๐ ยท 2) โค (๐ ยท 2))) |
18 | | gausslemma2d.p |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ (โ โ
{2})) |
19 | | gausslemma2d.m |
. . . . . . . . . . . . . . 15
โข ๐ = (โโ(๐ / 4)) |
20 | 18, 19 | gausslemma2dlem0e 26711 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ ยท 2) < (๐ / 2)) |
21 | 20 | adantl 483 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐) โ (๐ ยท 2) < (๐ / 2)) |
22 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 2 โ
โ) |
23 | 8, 22 | remulcld 11186 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ ยท 2) โ
โ) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท 2) โ
โ) |
25 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 2 โ
โ) |
26 | 10, 25 | remulcld 11186 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ ยท 2) โ
โ) |
27 | 26 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท 2) โ
โ) |
28 | 18 | gausslemma2dlem0a 26707 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โ) |
29 | 28 | nnred 12169 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ) |
30 | 29 | rehalfcld 12401 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ / 2) โ โ) |
31 | | lelttr 11246 |
. . . . . . . . . . . . . 14
โข (((๐ ยท 2) โ โ
โง (๐ ยท 2) โ
โ โง (๐ / 2)
โ โ) โ (((๐
ยท 2) โค (๐
ยท 2) โง (๐
ยท 2) < (๐ / 2))
โ (๐ ยท 2) <
(๐ / 2))) |
32 | 24, 27, 30, 31 | syl2an3an 1423 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐) โ (((๐ ยท 2) โค (๐ ยท 2) โง (๐ ยท 2) < (๐ / 2)) โ (๐ ยท 2) < (๐ / 2))) |
33 | 21, 32 | mpan2d 693 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐) โ ((๐ ยท 2) โค (๐ ยท 2) โ (๐ ยท 2) < (๐ / 2))) |
34 | 33 | ex 414 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โ ((๐ ยท 2) โค (๐ ยท 2) โ (๐ ยท 2) < (๐ / 2)))) |
35 | 34 | com23 86 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท 2) โค (๐ ยท 2) โ (๐ โ (๐ ยท 2) < (๐ / 2)))) |
36 | 17, 35 | sylbid 239 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โค ๐ โ (๐ โ (๐ ยท 2) < (๐ / 2)))) |
37 | 36 | 3impia 1118 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง ๐ โค ๐) โ (๐ โ (๐ ยท 2) < (๐ / 2))) |
38 | 7, 37 | sylbi 216 |
. . . . . . 7
โข (๐ โ (1...๐) โ (๐ โ (๐ ยท 2) < (๐ / 2))) |
39 | 38 | impcom 409 |
. . . . . 6
โข ((๐ โง ๐ โ (1...๐)) โ (๐ ยท 2) < (๐ / 2)) |
40 | 39 | adantr 482 |
. . . . 5
โข (((๐ โง ๐ โ (1...๐)) โง ๐ฅ = ๐) โ (๐ ยท 2) < (๐ / 2)) |
41 | 40 | iftrued 4495 |
. . . 4
โข (((๐ โง ๐ โ (1...๐)) โง ๐ฅ = ๐) โ if((๐ ยท 2) < (๐ / 2), (๐ ยท 2), (๐ โ (๐ ยท 2))) = (๐ ยท 2)) |
42 | 6, 41 | eqtrd 2777 |
. . 3
โข (((๐ โง ๐ โ (1...๐)) โง ๐ฅ = ๐) โ if((๐ฅ ยท 2) < (๐ / 2), (๐ฅ ยท 2), (๐ โ (๐ฅ ยท 2))) = (๐ ยท 2)) |
43 | 18, 19 | gausslemma2dlem0d 26710 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
44 | 43 | nn0zd 12526 |
. . . . . 6
โข (๐ โ ๐ โ โค) |
45 | | gausslemma2d.h |
. . . . . . . 8
โข ๐ป = ((๐ โ 1) / 2) |
46 | 18, 45 | gausslemma2dlem0b 26708 |
. . . . . . 7
โข (๐ โ ๐ป โ โ) |
47 | 46 | nnzd 12527 |
. . . . . 6
โข (๐ โ ๐ป โ โค) |
48 | 18, 19, 45 | gausslemma2dlem0g 26713 |
. . . . . 6
โข (๐ โ ๐ โค ๐ป) |
49 | | eluz2 12770 |
. . . . . 6
โข (๐ป โ
(โคโฅโ๐) โ (๐ โ โค โง ๐ป โ โค โง ๐ โค ๐ป)) |
50 | 44, 47, 48, 49 | syl3anbrc 1344 |
. . . . 5
โข (๐ โ ๐ป โ (โคโฅโ๐)) |
51 | | fzss2 13482 |
. . . . 5
โข (๐ป โ
(โคโฅโ๐) โ (1...๐) โ (1...๐ป)) |
52 | 50, 51 | syl 17 |
. . . 4
โข (๐ โ (1...๐) โ (1...๐ป)) |
53 | 52 | sselda 3945 |
. . 3
โข ((๐ โง ๐ โ (1...๐)) โ ๐ โ (1...๐ป)) |
54 | | ovexd 7393 |
. . 3
โข ((๐ โง ๐ โ (1...๐)) โ (๐ ยท 2) โ V) |
55 | 1, 42, 53, 54 | fvmptd2 6957 |
. 2
โข ((๐ โง ๐ โ (1...๐)) โ (๐
โ๐) = (๐ ยท 2)) |
56 | 55 | ralrimiva 3144 |
1
โข (๐ โ โ๐ โ (1...๐)(๐
โ๐) = (๐ ยท 2)) |