Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . 3
β’
β²ππ |
2 | | nfcv 2904 |
. . 3
β’
β²πseq1(
+ , πΉ) |
3 | | nfcv 2904 |
. . . 4
β’
β²π1 |
4 | | nfcv 2904 |
. . . 4
β’
β²π
+ |
5 | | nfmpt1 5256 |
. . . 4
β’
β²π(π β β β¦ (πΉβ((2 Β· π) β 1))) |
6 | 3, 4, 5 | nfseq 13973 |
. . 3
β’
β²πseq1(
+ , (π β β
β¦ (πΉβ((2
Β· π) β
1)))) |
7 | | nfmpt1 5256 |
. . 3
β’
β²π(π β β β¦ ((2 Β· π) β 1)) |
8 | | nnuz 12862 |
. . 3
β’ β =
(β€β₯β1) |
9 | | 1zzd 12590 |
. . 3
β’ (π β 1 β
β€) |
10 | | seqex 13965 |
. . . 4
β’ seq1( + ,
πΉ) β
V |
11 | 10 | a1i 11 |
. . 3
β’ (π β seq1( + , πΉ) β V) |
12 | | sumnnodd.1 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
13 | 12 | ffvelcdmda 7084 |
. . . . 5
β’ ((π β§ π β β) β (πΉβπ) β β) |
14 | 8, 9, 13 | serf 13993 |
. . . 4
β’ (π β seq1( + , πΉ):ββΆβ) |
15 | 14 | ffvelcdmda 7084 |
. . 3
β’ ((π β§ π β β) β (seq1( + , πΉ)βπ) β β) |
16 | | sumnnodd.sc |
. . 3
β’ (π β seq1( + , πΉ) β π΅) |
17 | | 1nn 12220 |
. . . . . . 7
β’ 1 β
β |
18 | | oveq2 7414 |
. . . . . . . . 9
β’ (π = 1 β (2 Β· π) = (2 Β·
1)) |
19 | 18 | oveq1d 7421 |
. . . . . . . 8
β’ (π = 1 β ((2 Β· π) β 1) = ((2 Β· 1)
β 1)) |
20 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦ ((2
Β· π) β 1)) =
(π β β β¦
((2 Β· π) β
1)) |
21 | | ovex 7439 |
. . . . . . . 8
β’ ((2
Β· 1) β 1) β V |
22 | 19, 20, 21 | fvmpt 6996 |
. . . . . . 7
β’ (1 β
β β ((π β
β β¦ ((2 Β· π) β 1))β1) = ((2 Β· 1)
β 1)) |
23 | 17, 22 | ax-mp 5 |
. . . . . 6
β’ ((π β β β¦ ((2
Β· π) β
1))β1) = ((2 Β· 1) β 1) |
24 | | 2t1e2 12372 |
. . . . . . 7
β’ (2
Β· 1) = 2 |
25 | 24 | oveq1i 7416 |
. . . . . 6
β’ ((2
Β· 1) β 1) = (2 β 1) |
26 | | 2m1e1 12335 |
. . . . . 6
β’ (2
β 1) = 1 |
27 | 23, 25, 26 | 3eqtri 2765 |
. . . . 5
β’ ((π β β β¦ ((2
Β· π) β
1))β1) = 1 |
28 | 27, 17 | eqeltri 2830 |
. . . 4
β’ ((π β β β¦ ((2
Β· π) β
1))β1) β β |
29 | 28 | a1i 11 |
. . 3
β’ (π β ((π β β β¦ ((2 Β· π) β 1))β1) β
β) |
30 | | 2z 12591 |
. . . . . . . 8
β’ 2 β
β€ |
31 | 30 | a1i 11 |
. . . . . . 7
β’ (π β β β 2 β
β€) |
32 | | nnz 12576 |
. . . . . . 7
β’ (π β β β π β
β€) |
33 | 31, 32 | zmulcld 12669 |
. . . . . 6
β’ (π β β β (2
Β· π) β
β€) |
34 | 32 | peano2zd 12666 |
. . . . . . . 8
β’ (π β β β (π + 1) β
β€) |
35 | 31, 34 | zmulcld 12669 |
. . . . . . 7
β’ (π β β β (2
Β· (π + 1)) β
β€) |
36 | | 1zzd 12590 |
. . . . . . 7
β’ (π β β β 1 β
β€) |
37 | 35, 36 | zsubcld 12668 |
. . . . . 6
β’ (π β β β ((2
Β· (π + 1)) β
1) β β€) |
38 | | 2re 12283 |
. . . . . . . . . 10
β’ 2 β
β |
39 | 38 | a1i 11 |
. . . . . . . . 9
β’ (π β β β 2 β
β) |
40 | | nnre 12216 |
. . . . . . . . 9
β’ (π β β β π β
β) |
41 | 39, 40 | remulcld 11241 |
. . . . . . . 8
β’ (π β β β (2
Β· π) β
β) |
42 | 41 | lep1d 12142 |
. . . . . . 7
β’ (π β β β (2
Β· π) β€ ((2
Β· π) +
1)) |
43 | | 2cnd 12287 |
. . . . . . . . . . 11
β’ (π β β β 2 β
β) |
44 | | nncn 12217 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
45 | | 1cnd 11206 |
. . . . . . . . . . 11
β’ (π β β β 1 β
β) |
46 | 43, 44, 45 | adddid 11235 |
. . . . . . . . . 10
β’ (π β β β (2
Β· (π + 1)) = ((2
Β· π) + (2 Β·
1))) |
47 | 24 | oveq2i 7417 |
. . . . . . . . . 10
β’ ((2
Β· π) + (2 Β·
1)) = ((2 Β· π) +
2) |
48 | 46, 47 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π β β β (2
Β· (π + 1)) = ((2
Β· π) +
2)) |
49 | 48 | oveq1d 7421 |
. . . . . . . 8
β’ (π β β β ((2
Β· (π + 1)) β
1) = (((2 Β· π) + 2)
β 1)) |
50 | 43, 44 | mulcld 11231 |
. . . . . . . . 9
β’ (π β β β (2
Β· π) β
β) |
51 | 50, 43, 45 | addsubassd 11588 |
. . . . . . . 8
β’ (π β β β (((2
Β· π) + 2) β 1)
= ((2 Β· π) + (2
β 1))) |
52 | 26 | oveq2i 7417 |
. . . . . . . . 9
β’ ((2
Β· π) + (2 β
1)) = ((2 Β· π) +
1) |
53 | 52 | a1i 11 |
. . . . . . . 8
β’ (π β β β ((2
Β· π) + (2 β
1)) = ((2 Β· π) +
1)) |
54 | 49, 51, 53 | 3eqtrrd 2778 |
. . . . . . 7
β’ (π β β β ((2
Β· π) + 1) = ((2
Β· (π + 1)) β
1)) |
55 | 42, 54 | breqtrd 5174 |
. . . . . 6
β’ (π β β β (2
Β· π) β€ ((2
Β· (π + 1)) β
1)) |
56 | | eluz2 12825 |
. . . . . 6
β’ (((2
Β· (π + 1)) β
1) β (β€β₯β(2 Β· π)) β ((2 Β· π) β β€ β§ ((2 Β· (π + 1)) β 1) β β€
β§ (2 Β· π) β€
((2 Β· (π + 1))
β 1))) |
57 | 33, 37, 55, 56 | syl3anbrc 1344 |
. . . . 5
β’ (π β β β ((2
Β· (π + 1)) β
1) β (β€β₯β(2 Β· π))) |
58 | | oveq2 7414 |
. . . . . . . 8
β’ (π = π β (2 Β· π) = (2 Β· π)) |
59 | 58 | oveq1d 7421 |
. . . . . . 7
β’ (π = π β ((2 Β· π) β 1) = ((2 Β· π) β 1)) |
60 | 59 | cbvmptv 5261 |
. . . . . 6
β’ (π β β β¦ ((2
Β· π) β 1)) =
(π β β β¦
((2 Β· π) β
1)) |
61 | | oveq2 7414 |
. . . . . . 7
β’ (π = (π + 1) β (2 Β· π) = (2 Β· (π + 1))) |
62 | 61 | oveq1d 7421 |
. . . . . 6
β’ (π = (π + 1) β ((2 Β· π) β 1) = ((2 Β· (π + 1)) β
1)) |
63 | | peano2nn 12221 |
. . . . . 6
β’ (π β β β (π + 1) β
β) |
64 | 60, 62, 63, 37 | fvmptd3 7019 |
. . . . 5
β’ (π β β β ((π β β β¦ ((2
Β· π) β
1))β(π + 1)) = ((2
Β· (π + 1)) β
1)) |
65 | 33, 36 | zsubcld 12668 |
. . . . . . . . 9
β’ (π β β β ((2
Β· π) β 1)
β β€) |
66 | 20 | fvmpt2 7007 |
. . . . . . . . 9
β’ ((π β β β§ ((2
Β· π) β 1)
β β€) β ((π
β β β¦ ((2 Β· π) β 1))βπ) = ((2 Β· π) β 1)) |
67 | 65, 66 | mpdan 686 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ ((2
Β· π) β
1))βπ) = ((2 Β·
π) β
1)) |
68 | 67 | oveq1d 7421 |
. . . . . . 7
β’ (π β β β (((π β β β¦ ((2
Β· π) β
1))βπ) + 1) = (((2
Β· π) β 1) +
1)) |
69 | 50, 45 | npcand 11572 |
. . . . . . 7
β’ (π β β β (((2
Β· π) β 1) + 1)
= (2 Β· π)) |
70 | 68, 69 | eqtrd 2773 |
. . . . . 6
β’ (π β β β (((π β β β¦ ((2
Β· π) β
1))βπ) + 1) = (2
Β· π)) |
71 | 70 | fveq2d 6893 |
. . . . 5
β’ (π β β β
(β€β₯β(((π β β β¦ ((2 Β· π) β 1))βπ) + 1)) =
(β€β₯β(2 Β· π))) |
72 | 57, 64, 71 | 3eltr4d 2849 |
. . . 4
β’ (π β β β ((π β β β¦ ((2
Β· π) β
1))β(π + 1)) β
(β€β₯β(((π β β β¦ ((2 Β· π) β 1))βπ) + 1))) |
73 | 72 | adantl 483 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦ ((2 Β· π) β 1))β(π + 1)) β
(β€β₯β(((π β β β¦ ((2 Β· π) β 1))βπ) + 1))) |
74 | | seqex 13965 |
. . . 4
β’ seq1( + ,
(π β β β¦
(πΉβ((2 Β· π) β 1)))) β
V |
75 | 74 | a1i 11 |
. . 3
β’ (π β seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) β
V) |
76 | | incom 4201 |
. . . . . . . . . 10
β’
(((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β© ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β})) = (((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β© ((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β})) |
77 | | inss2 4229 |
. . . . . . . . . . 11
β’ ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β}) β {π β
β β£ (π / 2)
β β} |
78 | | ssrin 4233 |
. . . . . . . . . . 11
β’
(((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β {π β β β£ (π / 2) β β} β
(((1...((2 Β· π)
β 1)) β© {π β
β β£ (π / 2)
β β}) β© ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β ({π β β β£ (π / 2) β β} β©
((1...((2 Β· π)
β 1)) β {π
β β β£ (π /
2) β β}))) |
79 | 77, 78 | ax-mp 5 |
. . . . . . . . . 10
β’
(((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β© ((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β})) β ({π
β β β£ (π /
2) β β} β© ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) |
80 | 76, 79 | eqsstri 4016 |
. . . . . . . . 9
β’
(((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β© ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β})) β ({π
β β β£ (π /
2) β β} β© ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) |
81 | | disjdif 4471 |
. . . . . . . . 9
β’ ({π β β β£ (π / 2) β β} β©
((1...((2 Β· π)
β 1)) β {π
β β β£ (π /
2) β β})) = β
|
82 | 80, 81 | sseqtri 4018 |
. . . . . . . 8
β’
(((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β© ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β})) β β
|
83 | | ss0 4398 |
. . . . . . . 8
β’
((((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β© ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β})) β β
β (((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β© ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β})) = β
) |
84 | 82, 83 | mp1i 13 |
. . . . . . 7
β’ ((π β§ π β β) β (((1...((2 Β·
π) β 1)) β
{π β β β£
(π / 2) β β})
β© ((1...((2 Β· π)
β 1)) β© {π β
β β£ (π / 2)
β β})) = β
) |
85 | | uncom 4153 |
. . . . . . . . 9
β’
(((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) βͺ ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β})) = (((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) βͺ ((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β})) |
86 | | inundif 4478 |
. . . . . . . . 9
β’
(((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) βͺ ((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β})) = (1...((2 Β· π) β 1)) |
87 | 85, 86 | eqtr2i 2762 |
. . . . . . . 8
β’ (1...((2
Β· π) β 1)) =
(((1...((2 Β· π)
β 1)) β {π
β β β£ (π /
2) β β}) βͺ ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})) |
88 | 87 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β (1...((2 Β·
π) β 1)) = (((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β}) βͺ ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}))) |
89 | | fzfid 13935 |
. . . . . . 7
β’ ((π β§ π β β) β (1...((2 Β·
π) β 1)) β
Fin) |
90 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (1...((2 Β· π) β 1))) β πΉ:ββΆβ) |
91 | | elfznn 13527 |
. . . . . . . . . 10
β’ (π β (1...((2 Β· π) β 1)) β π β
β) |
92 | 91 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1...((2 Β· π) β 1))) β π β β) |
93 | 90, 92 | ffvelcdmd 7085 |
. . . . . . . 8
β’ ((π β§ π β (1...((2 Β· π) β 1))) β (πΉβπ) β β) |
94 | 93 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...((2 Β· π) β 1))) β (πΉβπ) β β) |
95 | 84, 88, 89, 94 | fsumsplit 15684 |
. . . . . 6
β’ ((π β§ π β β) β Ξ£π β (1...((2 Β· π) β 1))(πΉβπ) = (Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ) + Ξ£π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})(πΉβπ))) |
96 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})) β π) |
97 | | ssrab2 4077 |
. . . . . . . . . . . . . 14
β’ {π β β β£ (π / 2) β β} β
β |
98 | 77 | sseli 3978 |
. . . . . . . . . . . . . 14
β’ (π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β
π β {π β β β£ (π / 2) β
β}) |
99 | 97, 98 | sselid 3980 |
. . . . . . . . . . . . 13
β’ (π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β
π β
β) |
100 | 99 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})) β π β
β) |
101 | | oveq1 7413 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π / 2) = (π / 2)) |
102 | 101 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π / 2) β β β (π / 2) β
β)) |
103 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π / 2) = (π / 2)) |
104 | 103 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((π / 2) β β β (π / 2) β
β)) |
105 | 104 | elrab 3683 |
. . . . . . . . . . . . . . . 16
β’ (π β {π β β β£ (π / 2) β β} β (π β β β§ (π / 2) β
β)) |
106 | 105 | simprbi 498 |
. . . . . . . . . . . . . . 15
β’ (π β {π β β β£ (π / 2) β β} β (π / 2) β
β) |
107 | 102, 106 | vtoclga 3566 |
. . . . . . . . . . . . . 14
β’ (π β {π β β β£ (π / 2) β β} β (π / 2) β
β) |
108 | 98, 107 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β
(π / 2) β
β) |
109 | 108 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})) β (π / 2) β
β) |
110 | | eleq1w 2817 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π β β β π β β)) |
111 | 110, 102 | 3anbi23d 1440 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π β§ π β β β§ (π / 2) β β) β (π β§ π β β β§ (π / 2) β β))) |
112 | | fveqeq2 6898 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβπ) = 0 β (πΉβπ) = 0)) |
113 | 111, 112 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = π β (((π β§ π β β β§ (π / 2) β β) β (πΉβπ) = 0) β ((π β§ π β β β§ (π / 2) β β) β (πΉβπ) = 0))) |
114 | | sumnnodd.even0 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β β§ (π / 2) β β) β (πΉβπ) = 0) |
115 | 113, 114 | chvarvv 2003 |
. . . . . . . . . . . 12
β’ ((π β§ π β β β§ (π / 2) β β) β (πΉβπ) = 0) |
116 | 96, 100, 109, 115 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})) β (πΉβπ) = 0) |
117 | 116 | sumeq2dv 15646 |
. . . . . . . . . 10
β’ (π β Ξ£π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})(πΉβπ) = Ξ£π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})0) |
118 | | fzfid 13935 |
. . . . . . . . . . . . 13
β’ (π β (1...((2 Β· π) β 1)) β
Fin) |
119 | | inss1 4228 |
. . . . . . . . . . . . . 14
β’ ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β}) β (1...((2 Β· π) β 1)) |
120 | 119 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β
(1...((2 Β· π)
β 1))) |
121 | | ssfi 9170 |
. . . . . . . . . . . . 13
β’
(((1...((2 Β· π) β 1)) β Fin β§ ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β}) β (1...((2 Β· π) β 1))) β ((1...((2 Β·
π) β 1)) β© {π β β β£ (π / 2) β β}) β
Fin) |
122 | 118, 120,
121 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β
Fin) |
123 | 122 | olcd 873 |
. . . . . . . . . . 11
β’ (π β (((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β
(β€β₯βπΆ) β¨ ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β
Fin)) |
124 | | sumz 15665 |
. . . . . . . . . . 11
β’
((((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β
(β€β₯βπΆ) β¨ ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β}) β Fin) β
Ξ£π β ((1...((2
Β· π) β 1))
β© {π β β
β£ (π / 2) β
β})0 = 0) |
125 | 123, 124 | syl 17 |
. . . . . . . . . 10
β’ (π β Ξ£π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})0 = 0) |
126 | 117, 125 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β Ξ£π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})(πΉβπ) = 0) |
127 | 126 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β Ξ£π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})(πΉβπ) = 0) |
128 | 127 | oveq2d 7422 |
. . . . . . 7
β’ ((π β§ π β β) β (Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ) + Ξ£π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})(πΉβπ)) = (Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ) + 0)) |
129 | | fzfi 13934 |
. . . . . . . . . . . 12
β’ (1...((2
Β· π) β 1))
β Fin |
130 | | difss 4131 |
. . . . . . . . . . . 12
β’ ((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β}) β (1...((2 Β· π) β 1)) |
131 | | ssfi 9170 |
. . . . . . . . . . . 12
β’
(((1...((2 Β· π) β 1)) β Fin β§ ((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β}) β (1...((2 Β· π) β 1))) β ((1...((2 Β·
π) β 1)) β
{π β β β£
(π / 2) β β})
β Fin) |
132 | 129, 130,
131 | mp2an 691 |
. . . . . . . . . . 11
β’ ((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β}) β Fin |
133 | 132 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((1...((2 Β·
π) β 1)) β
{π β β β£
(π / 2) β β})
β Fin) |
134 | 130 | sseli 3978 |
. . . . . . . . . . . 12
β’ (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β
π β (1...((2 Β·
π) β
1))) |
135 | 134, 93 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β (πΉβπ) β β) |
136 | 135 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β (πΉβπ) β β) |
137 | 133, 136 | fsumcl 15676 |
. . . . . . . . 9
β’ ((π β§ π β β) β Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ) β β) |
138 | 137 | addridd 11411 |
. . . . . . . 8
β’ ((π β§ π β β) β (Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ) + 0) = Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ)) |
139 | | fveq2 6889 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
140 | 139 | cbvsumv 15639 |
. . . . . . . 8
β’
Ξ£π β
((1...((2 Β· π)
β 1)) β {π
β β β£ (π /
2) β β})(πΉβπ) = Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ) |
141 | 138, 140 | eqtrdi 2789 |
. . . . . . 7
β’ ((π β§ π β β) β (Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ) + 0) = Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ)) |
142 | 128, 141 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π β β) β (Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ) + Ξ£π β ((1...((2 Β· π) β 1)) β© {π β β β£ (π / 2) β β})(πΉβπ)) = Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ)) |
143 | | fveq2 6889 |
. . . . . . 7
β’ (π = ((2 Β· π) β 1) β (πΉβπ) = (πΉβ((2 Β· π) β 1))) |
144 | | fzfid 13935 |
. . . . . . 7
β’ ((π β§ π β β) β (1...π) β Fin) |
145 | | 1zzd 12590 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β (1...π)) β 1 β β€) |
146 | 65 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β (1...π)) β ((2 Β· π) β 1) β β€) |
147 | 30 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β 2 β β€) |
148 | | elfzelz 13498 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β π β β€) |
149 | 147, 148 | zmulcld 12669 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β (2 Β· π) β β€) |
150 | | 1zzd 12590 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β 1 β β€) |
151 | 149, 150 | zsubcld 12668 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β ((2 Β· π) β 1) β β€) |
152 | 151 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β (1...π)) β ((2 Β· π) β 1) β β€) |
153 | 25, 26 | eqtr2i 2762 |
. . . . . . . . . . . . . . 15
β’ 1 = ((2
Β· 1) β 1) |
154 | | 1re 11211 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β |
155 | 38, 154 | remulcli 11227 |
. . . . . . . . . . . . . . . . 17
β’ (2
Β· 1) β β |
156 | 155 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β (2 Β· 1) β
β) |
157 | 149 | zred 12663 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β (2 Β· π) β β) |
158 | | 1red 11212 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β 1 β β) |
159 | 148 | zred 12663 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β π β β) |
160 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β 2 β β) |
161 | | 0le2 12311 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β€
2 |
162 | 161 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β 0 β€ 2) |
163 | | elfzle1 13501 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β 1 β€ π) |
164 | 158, 159,
160, 162, 163 | lemul2ad 12151 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β (2 Β· 1) β€ (2 Β·
π)) |
165 | 156, 157,
158, 164 | lesub1dd 11827 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β ((2 Β· 1) β 1) β€ ((2
Β· π) β
1)) |
166 | 153, 165 | eqbrtrid 5183 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β 1 β€ ((2 Β· π) β 1)) |
167 | 166 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β (1...π)) β 1 β€ ((2 Β· π) β 1)) |
168 | 157 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β (1...π)) β (2 Β· π) β β) |
169 | 41 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β (1...π)) β (2 Β· π) β β) |
170 | | 1red 11212 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β (1...π)) β 1 β β) |
171 | 159 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β (1...π)) β π β β) |
172 | 40 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β (1...π)) β π β β) |
173 | 38 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β (1...π)) β 2 β β) |
174 | 161 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β (1...π)) β 0 β€ 2) |
175 | | elfzle2 13502 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β π β€ π) |
176 | 175 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β (1...π)) β π β€ π) |
177 | 171, 172,
173, 174, 176 | lemul2ad 12151 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β (1...π)) β (2 Β· π) β€ (2 Β· π)) |
178 | 168, 169,
170, 177 | lesub1dd 11827 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β (1...π)) β ((2 Β· π) β 1) β€ ((2 Β· π) β 1)) |
179 | 145, 146,
152, 167, 178 | elfzd 13489 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β (1...π)) β ((2 Β· π) β 1) β (1...((2 Β· π) β 1))) |
180 | 149 | zcnd 12664 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β (2 Β· π) β β) |
181 | | 1cnd 11206 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β 1 β β) |
182 | | 2cnd 12287 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β 2 β β) |
183 | | 2ne0 12313 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
0 |
184 | 183 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β 2 β 0) |
185 | 180, 181,
182, 184 | divsubdird 12026 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β (((2 Β· π) β 1) / 2) = (((2 Β· π) / 2) β (1 /
2))) |
186 | 148 | zcnd 12664 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β π β β) |
187 | 186, 182,
184 | divcan3d 11992 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β ((2 Β· π) / 2) = π) |
188 | 187 | oveq1d 7421 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β (((2 Β· π) / 2) β (1 / 2)) = (π β (1 / 2))) |
189 | 185, 188 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β (((2 Β· π) β 1) / 2) = (π β (1 / 2))) |
190 | 148, 150 | zsubcld 12668 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β (π β 1) β β€) |
191 | 160, 184 | rereccld 12038 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β (1 / 2) β
β) |
192 | | halflt1 12427 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1 / 2)
< 1 |
193 | 192 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β (1 / 2) < 1) |
194 | 191, 158,
159, 193 | ltsub2dd 11824 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β (π β 1) < (π β (1 / 2))) |
195 | | 2rp 12976 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 2 β
β+ |
196 | | rpreccl 12997 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (2 β
β+ β (1 / 2) β β+) |
197 | 195, 196 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β (1 / 2) β
β+) |
198 | 159, 197 | ltsubrpd 13045 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β (π β (1 / 2)) < π) |
199 | 186, 181 | npcand 11572 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β ((π β 1) + 1) = π) |
200 | 198, 199 | breqtrrd 5176 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β (π β (1 / 2)) < ((π β 1) + 1)) |
201 | | btwnnz 12635 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β 1) β β€ β§
(π β 1) < (π β (1 / 2)) β§ (π β (1 / 2)) < ((π β 1) + 1)) β Β¬
(π β (1 / 2)) β
β€) |
202 | 190, 194,
200, 201 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β Β¬ (π β (1 / 2)) β
β€) |
203 | | nnz 12576 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1 / 2)) β β
β (π β (1 / 2))
β β€) |
204 | 202, 203 | nsyl 140 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β Β¬ (π β (1 / 2)) β
β) |
205 | 189, 204 | eqneltrd 2854 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β Β¬ (((2 Β· π) β 1) / 2) β
β) |
206 | 205 | intnand 490 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β Β¬ (((2 Β· π) β 1) β β
β§ (((2 Β· π)
β 1) / 2) β β)) |
207 | | oveq1 7413 |
. . . . . . . . . . . . . . . 16
β’ (π = ((2 Β· π) β 1) β (π / 2) = (((2 Β· π) β 1) /
2)) |
208 | 207 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π = ((2 Β· π) β 1) β ((π / 2) β β β (((2
Β· π) β 1) / 2)
β β)) |
209 | 208 | elrab 3683 |
. . . . . . . . . . . . . 14
β’ (((2
Β· π) β 1)
β {π β β
β£ (π / 2) β
β} β (((2 Β· π) β 1) β β β§ (((2
Β· π) β 1) / 2)
β β)) |
210 | 206, 209 | sylnibr 329 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β Β¬ ((2 Β· π) β 1) β {π β β β£ (π / 2) β
β}) |
211 | 210 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β (1...π)) β Β¬ ((2 Β· π) β 1) β {π β β β£ (π / 2) β
β}) |
212 | 179, 211 | eldifd 3959 |
. . . . . . . . . . 11
β’ ((π β β β§ π β (1...π)) β ((2 Β· π) β 1) β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β
β})) |
213 | 212 | fmpttd 7112 |
. . . . . . . . . 10
β’ (π β β β (π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)βΆ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β
β})) |
214 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (1...π) β (π β (1...π) β¦ ((2 Β· π) β 1)) = (π β (1...π) β¦ ((2 Β· π) β 1))) |
215 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π₯ β (2 Β· π) = (2 Β· π₯)) |
216 | 215 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π₯ β ((2 Β· π) β 1) = ((2 Β· π₯) β 1)) |
217 | 216 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (1...π) β§ π = π₯) β ((2 Β· π) β 1) = ((2 Β· π₯) β 1)) |
218 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (1...π) β π₯ β (1...π)) |
219 | | ovexd 7441 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (1...π) β ((2 Β· π₯) β 1) β V) |
220 | 214, 217,
218, 219 | fvmptd 7003 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (1...π) β ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((2 Β· π₯) β 1)) |
221 | 220 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (1...π) β ((2 Β· π₯) β 1) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯)) |
222 | 221 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦)) β ((2 Β· π₯) β 1) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯)) |
223 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦)) β ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦)) |
224 | | eqidd 2734 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (1...π) β (π β (1...π) β¦ ((2 Β· π) β 1)) = (π β (1...π) β¦ ((2 Β· π) β 1))) |
225 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π¦ β (2 Β· π) = (2 Β· π¦)) |
226 | 225 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π¦ β ((2 Β· π) β 1) = ((2 Β· π¦) β 1)) |
227 | 226 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ β (1...π) β§ π = π¦) β ((2 Β· π) β 1) = ((2 Β· π¦) β 1)) |
228 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (1...π) β π¦ β (1...π)) |
229 | | ovexd 7441 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (1...π) β ((2 Β· π¦) β 1) β V) |
230 | 224, 227,
228, 229 | fvmptd 7003 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (1...π) β ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦) = ((2 Β· π¦) β 1)) |
231 | 230 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦)) β ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦) = ((2 Β· π¦) β 1)) |
232 | 222, 223,
231 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦)) β ((2 Β· π₯) β 1) = ((2 Β· π¦) β 1)) |
233 | | 2cnd 12287 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (1...π) β 2 β β) |
234 | | elfzelz 13498 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (1...π) β π₯ β β€) |
235 | 234 | zcnd 12664 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (1...π) β π₯ β β) |
236 | 233, 235 | mulcld 11231 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (1...π) β (2 Β· π₯) β β) |
237 | 236 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((2 Β· π₯) β 1) = ((2 Β· π¦) β 1)) β (2 Β·
π₯) β
β) |
238 | | 2cnd 12287 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β (1...π) β 2 β β) |
239 | | elfzelz 13498 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (1...π) β π¦ β β€) |
240 | 239 | zcnd 12664 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β (1...π) β π¦ β β) |
241 | 238, 240 | mulcld 11231 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (1...π) β (2 Β· π¦) β β) |
242 | 241 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((2 Β· π₯) β 1) = ((2 Β· π¦) β 1)) β (2 Β·
π¦) β
β) |
243 | | 1cnd 11206 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((2 Β· π₯) β 1) = ((2 Β· π¦) β 1)) β 1 β
β) |
244 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((2 Β· π₯) β 1) = ((2 Β· π¦) β 1)) β ((2
Β· π₯) β 1) =
((2 Β· π¦) β
1)) |
245 | 237, 242,
243, 244 | subcan2d 11610 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((2 Β· π₯) β 1) = ((2 Β· π¦) β 1)) β (2 Β·
π₯) = (2 Β· π¦)) |
246 | 235 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ (2 Β· π₯) = (2 Β· π¦)) β π₯ β β) |
247 | 240 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ (2 Β· π₯) = (2 Β· π¦)) β π¦ β β) |
248 | | 2cnd 12287 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ (2 Β· π₯) = (2 Β· π¦)) β 2 β β) |
249 | 183 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ (2 Β· π₯) = (2 Β· π¦)) β 2 β 0) |
250 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ (2 Β· π₯) = (2 Β· π¦)) β (2 Β· π₯) = (2 Β· π¦)) |
251 | 246, 247,
248, 249, 250 | mulcanad 11846 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ (2 Β· π₯) = (2 Β· π¦)) β π₯ = π¦) |
252 | 245, 251 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((2 Β· π₯) β 1) = ((2 Β· π¦) β 1)) β π₯ = π¦) |
253 | 232, 252 | syldan 592 |
. . . . . . . . . . . . 13
β’ (((π₯ β (1...π) β§ π¦ β (1...π)) β§ ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦)) β π₯ = π¦) |
254 | 253 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π₯ β (1...π) β§ π¦ β (1...π))) β§ ((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦)) β π₯ = π¦) |
255 | 254 | ex 414 |
. . . . . . . . . . 11
β’ ((π β β β§ (π₯ β (1...π) β§ π¦ β (1...π))) β (((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦) β π₯ = π¦)) |
256 | 255 | ralrimivva 3201 |
. . . . . . . . . 10
β’ (π β β β
βπ₯ β (1...π)βπ¦ β (1...π)(((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦) β π₯ = π¦)) |
257 | | dff13 7251 |
. . . . . . . . . 10
β’ ((π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)β1-1β((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β ((π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)βΆ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
βπ₯ β (1...π)βπ¦ β (1...π)(((π β (1...π) β¦ ((2 Β· π) β 1))βπ₯) = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ¦) β π₯ = π¦))) |
258 | 213, 256,
257 | sylanbrc 584 |
. . . . . . . . 9
β’ (π β β β (π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)β1-1β((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) |
259 | | 1zzd 12590 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β 1
β β€) |
260 | 32 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
π β
β€) |
261 | 134 | elfzelzd 13499 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β
π β
β€) |
262 | | zeo 12645 |
. . . . . . . . . . . . . . . . 17
β’ (π β β€ β ((π / 2) β β€ β¨
((π + 1) / 2) β
β€)) |
263 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β
((π / 2) β β€
β¨ ((π + 1) / 2) β
β€)) |
264 | 263 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
((π / 2) β β€
β¨ ((π + 1) / 2) β
β€)) |
265 | | eldifn 4127 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β
Β¬ π β {π β β β£ (π / 2) β
β}) |
266 | 134, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β
π β
β) |
267 | 266 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
(π / 2) β β€)
β π β
β) |
268 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
(π / 2) β β€)
β (π / 2) β
β€) |
269 | 267 | nnred 12224 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
(π / 2) β β€)
β π β
β) |
270 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
(π / 2) β β€)
β 2 β β) |
271 | 267 | nngt0d 12258 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
(π / 2) β β€)
β 0 < π) |
272 | | 2pos 12312 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 <
2 |
273 | 272 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
(π / 2) β β€)
β 0 < 2) |
274 | 269, 270,
271, 273 | divgt0d 12146 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
(π / 2) β β€)
β 0 < (π /
2)) |
275 | | elnnz 12565 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π / 2) β β β
((π / 2) β β€
β§ 0 < (π /
2))) |
276 | 268, 274,
275 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
(π / 2) β β€)
β (π / 2) β
β) |
277 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π / 2) = (π / 2)) |
278 | 277 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π / 2) β β β (π / 2) β
β)) |
279 | 278 | elrab 3683 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {π β β β£ (π / 2) β β} β (π β β β§ (π / 2) β
β)) |
280 | 267, 276,
279 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’ ((π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
(π / 2) β β€)
β π β {π β β β£ (π / 2) β
β}) |
281 | 265, 280 | mtand 815 |
. . . . . . . . . . . . . . . 16
β’ (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β
Β¬ (π / 2) β
β€) |
282 | 281 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
Β¬ (π / 2) β
β€) |
283 | | pm2.53 850 |
. . . . . . . . . . . . . . 15
β’ (((π / 2) β β€ β¨
((π + 1) / 2) β
β€) β (Β¬ (π /
2) β β€ β ((π + 1) / 2) β β€)) |
284 | 264, 282,
283 | sylc 65 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
((π + 1) / 2) β
β€) |
285 | | 1p1e2 12334 |
. . . . . . . . . . . . . . . . . . 19
β’ (1 + 1) =
2 |
286 | 285 | oveq1i 7416 |
. . . . . . . . . . . . . . . . . 18
β’ ((1 + 1)
/ 2) = (2 / 2) |
287 | | 2div2e1 12350 |
. . . . . . . . . . . . . . . . . 18
β’ (2 / 2) =
1 |
288 | 286, 287 | eqtr2i 2762 |
. . . . . . . . . . . . . . . . 17
β’ 1 = ((1 +
1) / 2) |
289 | | 1red 11212 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...((2 Β· π) β 1)) β 1 β
β) |
290 | 289, 289 | readdcld 11240 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...((2 Β· π) β 1)) β (1 + 1)
β β) |
291 | 91 | nnred 12224 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...((2 Β· π) β 1)) β π β
β) |
292 | 291, 289 | readdcld 11240 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...((2 Β· π) β 1)) β (π + 1) β
β) |
293 | 195 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...((2 Β· π) β 1)) β 2 β
β+) |
294 | | elfzle1 13501 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...((2 Β· π) β 1)) β 1 β€
π) |
295 | 289, 291,
289, 294 | leadd1dd 11825 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...((2 Β· π) β 1)) β (1 + 1)
β€ (π +
1)) |
296 | 290, 292,
293, 295 | lediv1dd 13071 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...((2 Β· π) β 1)) β ((1 + 1) /
2) β€ ((π + 1) /
2)) |
297 | 288, 296 | eqbrtrid 5183 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...((2 Β· π) β 1)) β 1 β€
((π + 1) /
2)) |
298 | 134, 297 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β 1
β€ ((π + 1) /
2)) |
299 | 298 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β 1
β€ ((π + 1) /
2)) |
300 | | elfzel2 13496 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...((2 Β· π) β 1)) β ((2
Β· π) β 1)
β β€) |
301 | 300 | zred 12663 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...((2 Β· π) β 1)) β ((2
Β· π) β 1)
β β) |
302 | 301, 289 | readdcld 11240 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...((2 Β· π) β 1)) β (((2
Β· π) β 1) + 1)
β β) |
303 | | elfzle2 13502 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...((2 Β· π) β 1)) β π β€ ((2 Β· π) β 1)) |
304 | 291, 301,
289, 303 | leadd1dd 11825 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...((2 Β· π) β 1)) β (π + 1) β€ (((2 Β· π) β 1) +
1)) |
305 | 292, 302,
293, 304 | lediv1dd 13071 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...((2 Β· π) β 1)) β ((π + 1) / 2) β€ ((((2 Β·
π) β 1) + 1) /
2)) |
306 | 305 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β (1...((2 Β· π) β 1))) β ((π + 1) / 2) β€ ((((2 Β·
π) β 1) + 1) /
2)) |
307 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β (1...((2 Β· π) β 1))) β (2
Β· π) β
β) |
308 | | 1cnd 11206 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β (1...((2 Β· π) β 1))) β 1 β
β) |
309 | 307, 308 | npcand 11572 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β (1...((2 Β· π) β 1))) β (((2
Β· π) β 1) + 1)
= (2 Β· π)) |
310 | 309 | oveq1d 7421 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β (1...((2 Β· π) β 1))) β ((((2
Β· π) β 1) + 1)
/ 2) = ((2 Β· π) /
2)) |
311 | 183 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β 2 β
0) |
312 | 44, 43, 311 | divcan3d 11992 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β ((2
Β· π) / 2) = π) |
313 | 312 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β (1...((2 Β· π) β 1))) β ((2
Β· π) / 2) = π) |
314 | 310, 313 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β (1...((2 Β· π) β 1))) β ((((2
Β· π) β 1) + 1)
/ 2) = π) |
315 | 306, 314 | breqtrd 5174 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β (1...((2 Β· π) β 1))) β ((π + 1) / 2) β€ π) |
316 | 134, 315 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
((π + 1) / 2) β€ π) |
317 | 259, 260,
284, 299, 316 | elfzd 13489 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
((π + 1) / 2) β
(1...π)) |
318 | 266 | nncnd 12225 |
. . . . . . . . . . . . . . 15
β’ (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β
π β
β) |
319 | | peano2cn 11383 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (π + 1) β
β) |
320 | | 2cnd 12287 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β 2 β
β) |
321 | 183 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β 2 β
0) |
322 | 319, 320,
321 | divcan2d 11989 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (2
Β· ((π + 1) / 2)) =
(π + 1)) |
323 | 322 | oveq1d 7421 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((2
Β· ((π + 1) / 2))
β 1) = ((π + 1)
β 1)) |
324 | | pncan1 11635 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π + 1) β 1) = π) |
325 | 323, 324 | eqtr2d 2774 |
. . . . . . . . . . . . . . 15
β’ (π β β β π = ((2 Β· ((π + 1) / 2)) β
1)) |
326 | 318, 325 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β
π = ((2 Β· ((π + 1) / 2)) β
1)) |
327 | 326 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
π = ((2 Β· ((π + 1) / 2)) β
1)) |
328 | | oveq2 7414 |
. . . . . . . . . . . . . . 15
β’ (π = ((π + 1) / 2) β (2 Β· π) = (2 Β· ((π + 1) / 2))) |
329 | 328 | oveq1d 7421 |
. . . . . . . . . . . . . 14
β’ (π = ((π + 1) / 2) β ((2 Β· π) β 1) = ((2 Β·
((π + 1) / 2)) β
1)) |
330 | 329 | rspceeqv 3633 |
. . . . . . . . . . . . 13
β’ ((((π + 1) / 2) β (1...π) β§ π = ((2 Β· ((π + 1) / 2)) β 1)) β βπ β (1...π)π = ((2 Β· π) β 1)) |
331 | 317, 327,
330 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
βπ β (1...π)π = ((2 Β· π) β 1)) |
332 | | eqidd 2734 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1...π) β§ π = ((2 Β· π) β 1)) β (π β (1...π) β¦ ((2 Β· π) β 1)) = (π β (1...π) β¦ ((2 Β· π) β 1))) |
333 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (2 Β· π) = (2 Β· π)) |
334 | 333 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((2 Β· π) β 1) = ((2 Β· π) β 1)) |
335 | 334 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (1...π) β§ π = ((2 Β· π) β 1)) β§ π = π) β ((2 Β· π) β 1) = ((2 Β· π) β 1)) |
336 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1...π) β§ π = ((2 Β· π) β 1)) β π β (1...π)) |
337 | | ovexd 7441 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1...π) β§ π = ((2 Β· π) β 1)) β ((2 Β· π) β 1) β
V) |
338 | 332, 335,
336, 337 | fvmptd 7003 |
. . . . . . . . . . . . . . . 16
β’ ((π β (1...π) β§ π = ((2 Β· π) β 1)) β ((π β (1...π) β¦ ((2 Β· π) β 1))βπ) = ((2 Β· π) β 1)) |
339 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π = ((2 Β· π) β 1) β π = ((2 Β· π) β 1)) |
340 | 339 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’ (π = ((2 Β· π) β 1) β ((2 Β·
π) β 1) = π) |
341 | 340 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β (1...π) β§ π = ((2 Β· π) β 1)) β ((2 Β· π) β 1) = π) |
342 | 338, 341 | eqtr2d 2774 |
. . . . . . . . . . . . . . 15
β’ ((π β (1...π) β§ π = ((2 Β· π) β 1)) β π = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ)) |
343 | 342 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β (π = ((2 Β· π) β 1) β π = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ))) |
344 | 343 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β§
π β (1...π)) β (π = ((2 Β· π) β 1) β π = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ))) |
345 | 344 | reximdva 3169 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
(βπ β (1...π)π = ((2 Β· π) β 1) β βπ β (1...π)π = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ))) |
346 | 331, 345 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β β β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β
βπ β (1...π)π = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ)) |
347 | 346 | ralrimiva 3147 |
. . . . . . . . . 10
β’ (π β β β
βπ β ((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β})βπ β
(1...π)π = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ)) |
348 | | dffo3 7101 |
. . . . . . . . . 10
β’ ((π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)βontoβ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β ((π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)βΆ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§
βπ β ((1...((2
Β· π) β 1))
β {π β β
β£ (π / 2) β
β})βπ β
(1...π)π = ((π β (1...π) β¦ ((2 Β· π) β 1))βπ))) |
349 | 213, 347,
348 | sylanbrc 584 |
. . . . . . . . 9
β’ (π β β β (π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)βontoβ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) |
350 | | df-f1o 6548 |
. . . . . . . . 9
β’ ((π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)β1-1-ontoβ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β ((π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)β1-1β((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β§ (π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)βontoβ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}))) |
351 | 258, 349,
350 | sylanbrc 584 |
. . . . . . . 8
β’ (π β β β (π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)β1-1-ontoβ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) |
352 | 351 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β) β (π β (1...π) β¦ ((2 Β· π) β 1)):(1...π)β1-1-ontoβ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) |
353 | | eqidd 2734 |
. . . . . . . . 9
β’ (π β (1...π) β (π β (1...π) β¦ ((2 Β· π) β 1)) = (π β (1...π) β¦ ((2 Β· π) β 1))) |
354 | | oveq2 7414 |
. . . . . . . . . . 11
β’ (π = π β (2 Β· π) = (2 Β· π)) |
355 | 354 | oveq1d 7421 |
. . . . . . . . . 10
β’ (π = π β ((2 Β· π) β 1) = ((2 Β· π) β 1)) |
356 | 355 | adantl 483 |
. . . . . . . . 9
β’ ((π β (1...π) β§ π = π) β ((2 Β· π) β 1) = ((2 Β· π) β 1)) |
357 | | id 22 |
. . . . . . . . 9
β’ (π β (1...π) β π β (1...π)) |
358 | | ovexd 7441 |
. . . . . . . . 9
β’ (π β (1...π) β ((2 Β· π) β 1) β V) |
359 | 353, 356,
357, 358 | fvmptd 7003 |
. . . . . . . 8
β’ (π β (1...π) β ((π β (1...π) β¦ ((2 Β· π) β 1))βπ) = ((2 Β· π) β 1)) |
360 | 359 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (1...π)) β ((π β (1...π) β¦ ((2 Β· π) β 1))βπ) = ((2 Β· π) β 1)) |
361 | | eleq1w 2817 |
. . . . . . . . . 10
β’ (π = π β (π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β}) β π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β
β}))) |
362 | 361 | anbi2d 630 |
. . . . . . . . 9
β’ (π = π β (((π β§ π β β) β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β ((π β§ π β β) β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})))) |
363 | 139 | eleq1d 2819 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
364 | 362, 363 | imbi12d 345 |
. . . . . . . 8
β’ (π = π β ((((π β§ π β β) β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β (πΉβπ) β β) β (((π β§ π β β) β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β (πΉβπ) β β))) |
365 | 364, 136 | chvarvv 2003 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})) β (πΉβπ) β β) |
366 | 143, 144,
352, 360, 365 | fsumf1o 15666 |
. . . . . 6
β’ ((π β§ π β β) β Ξ£π β ((1...((2 Β· π) β 1)) β {π β β β£ (π / 2) β β})(πΉβπ) = Ξ£π β (1...π)(πΉβ((2 Β· π) β 1))) |
367 | 95, 142, 366 | 3eqtrrd 2778 |
. . . . 5
β’ ((π β§ π β β) β Ξ£π β (1...π)(πΉβ((2 Β· π) β 1)) = Ξ£π β (1...((2 Β· π) β 1))(πΉβπ)) |
368 | | ovex 7439 |
. . . . . . . . . 10
β’ ((2
Β· π) β 1)
β V |
369 | 20 | fvmpt2 7007 |
. . . . . . . . . 10
β’ ((π β β β§ ((2
Β· π) β 1)
β V) β ((π β
β β¦ ((2 Β· π) β 1))βπ) = ((2 Β· π) β 1)) |
370 | 368, 369 | mpan2 690 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦ ((2
Β· π) β
1))βπ) = ((2 Β·
π) β
1)) |
371 | 370 | oveq2d 7422 |
. . . . . . . 8
β’ (π β β β
(1...((π β β
β¦ ((2 Β· π)
β 1))βπ)) =
(1...((2 Β· π)
β 1))) |
372 | 371 | eqcomd 2739 |
. . . . . . 7
β’ (π β β β (1...((2
Β· π) β 1)) =
(1...((π β β
β¦ ((2 Β· π)
β 1))βπ))) |
373 | 372 | sumeq1d 15644 |
. . . . . 6
β’ (π β β β
Ξ£π β (1...((2
Β· π) β
1))(πΉβπ) = Ξ£π β (1...((π β β β¦ ((2 Β· π) β 1))βπ))(πΉβπ)) |
374 | 373 | adantl 483 |
. . . . 5
β’ ((π β§ π β β) β Ξ£π β (1...((2 Β· π) β 1))(πΉβπ) = Ξ£π β (1...((π β β β¦ ((2 Β· π) β 1))βπ))(πΉβπ)) |
375 | 367, 374 | eqtrd 2773 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β (1...π)(πΉβ((2 Β· π) β 1)) = Ξ£π β (1...((π β β β¦ ((2 Β· π) β 1))βπ))(πΉβπ)) |
376 | | elfznn 13527 |
. . . . . . 7
β’ (π β (1...π) β π β β) |
377 | 376 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
378 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β πΉ:ββΆβ) |
379 | 30 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (1...π) β 2 β β€) |
380 | | elfzelz 13498 |
. . . . . . . . . . . 12
β’ (π β (1...π) β π β β€) |
381 | 379, 380 | zmulcld 12669 |
. . . . . . . . . . 11
β’ (π β (1...π) β (2 Β· π) β β€) |
382 | | 1zzd 12590 |
. . . . . . . . . . 11
β’ (π β (1...π) β 1 β β€) |
383 | 381, 382 | zsubcld 12668 |
. . . . . . . . . 10
β’ (π β (1...π) β ((2 Β· π) β 1) β β€) |
384 | | 0red 11214 |
. . . . . . . . . . 11
β’ (π β (1...π) β 0 β β) |
385 | 38 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β 2 β β) |
386 | 24, 385 | eqeltrid 2838 |
. . . . . . . . . . . 12
β’ (π β (1...π) β (2 Β· 1) β
β) |
387 | | 1red 11212 |
. . . . . . . . . . . 12
β’ (π β (1...π) β 1 β β) |
388 | 386, 387 | resubcld 11639 |
. . . . . . . . . . 11
β’ (π β (1...π) β ((2 Β· 1) β 1) β
β) |
389 | 383 | zred 12663 |
. . . . . . . . . . 11
β’ (π β (1...π) β ((2 Β· π) β 1) β β) |
390 | | 0lt1 11733 |
. . . . . . . . . . . 12
β’ 0 <
1 |
391 | 153 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (1...π) β 1 = ((2 Β· 1) β
1)) |
392 | 390, 391 | breqtrid 5185 |
. . . . . . . . . . 11
β’ (π β (1...π) β 0 < ((2 Β· 1) β
1)) |
393 | 381 | zred 12663 |
. . . . . . . . . . . 12
β’ (π β (1...π) β (2 Β· π) β β) |
394 | 376 | nnred 12224 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β π β β) |
395 | 161 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β 0 β€ 2) |
396 | | elfzle1 13501 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β 1 β€ π) |
397 | 387, 394,
385, 395, 396 | lemul2ad 12151 |
. . . . . . . . . . . 12
β’ (π β (1...π) β (2 Β· 1) β€ (2 Β·
π)) |
398 | 386, 393,
387, 397 | lesub1dd 11827 |
. . . . . . . . . . 11
β’ (π β (1...π) β ((2 Β· 1) β 1) β€ ((2
Β· π) β
1)) |
399 | 384, 388,
389, 392, 398 | ltletrd 11371 |
. . . . . . . . . 10
β’ (π β (1...π) β 0 < ((2 Β· π) β 1)) |
400 | | elnnz 12565 |
. . . . . . . . . 10
β’ (((2
Β· π) β 1)
β β β (((2 Β· π) β 1) β β€ β§ 0 < ((2
Β· π) β
1))) |
401 | 383, 399,
400 | sylanbrc 584 |
. . . . . . . . 9
β’ (π β (1...π) β ((2 Β· π) β 1) β β) |
402 | 401 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β ((2 Β· π) β 1) β β) |
403 | 378, 402 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (πΉβ((2 Β· π) β 1)) β
β) |
404 | 403 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...π)) β (πΉβ((2 Β· π) β 1)) β
β) |
405 | 59 | fveq2d 6893 |
. . . . . . . 8
β’ (π = π β (πΉβ((2 Β· π) β 1)) = (πΉβ((2 Β· π) β 1))) |
406 | 405 | cbvmptv 5261 |
. . . . . . 7
β’ (π β β β¦ (πΉβ((2 Β· π) β 1))) = (π β β β¦ (πΉβ((2 Β· π) β 1))) |
407 | 406 | fvmpt2 7007 |
. . . . . 6
β’ ((π β β β§ (πΉβ((2 Β· π) β 1)) β β)
β ((π β β
β¦ (πΉβ((2
Β· π) β
1)))βπ) = (πΉβ((2 Β· π) β 1))) |
408 | 377, 404,
407 | syl2anc 585 |
. . . . 5
β’ (((π β§ π β β) β§ π β (1...π)) β ((π β β β¦ (πΉβ((2 Β· π) β 1)))βπ) = (πΉβ((2 Β· π) β 1))) |
409 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
410 | 409, 8 | eleqtrdi 2844 |
. . . . 5
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
411 | 408, 410,
404 | fsumser 15673 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β (1...π)(πΉβ((2 Β· π) β 1)) = (seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1))))βπ)) |
412 | | eqidd 2734 |
. . . . 5
β’ (((π β§ π β β) β§ π β (1...((π β β β¦ ((2 Β· π) β 1))βπ))) β (πΉβπ) = (πΉβπ)) |
413 | 155 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β (2
Β· 1) β β) |
414 | | 1red 11212 |
. . . . . . . . . 10
β’ (π β β β 1 β
β) |
415 | 161 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β 0 β€
2) |
416 | | nnge1 12237 |
. . . . . . . . . . 11
β’ (π β β β 1 β€
π) |
417 | 414, 40, 39, 415, 416 | lemul2ad 12151 |
. . . . . . . . . 10
β’ (π β β β (2
Β· 1) β€ (2 Β· π)) |
418 | 413, 41, 414, 417 | lesub1dd 11827 |
. . . . . . . . 9
β’ (π β β β ((2
Β· 1) β 1) β€ ((2 Β· π) β 1)) |
419 | 153, 418 | eqbrtrid 5183 |
. . . . . . . 8
β’ (π β β β 1 β€
((2 Β· π) β
1)) |
420 | | eluz2 12825 |
. . . . . . . 8
β’ (((2
Β· π) β 1)
β (β€β₯β1) β (1 β β€ β§ ((2
Β· π) β 1)
β β€ β§ 1 β€ ((2 Β· π) β 1))) |
421 | 36, 65, 419, 420 | syl3anbrc 1344 |
. . . . . . 7
β’ (π β β β ((2
Β· π) β 1)
β (β€β₯β1)) |
422 | 67, 421 | eqeltrd 2834 |
. . . . . 6
β’ (π β β β ((π β β β¦ ((2
Β· π) β
1))βπ) β
(β€β₯β1)) |
423 | 422 | adantl 483 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ ((2 Β· π) β 1))βπ) β
(β€β₯β1)) |
424 | | simpll 766 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...((π β β β¦ ((2 Β· π) β 1))βπ))) β π) |
425 | | simpr 486 |
. . . . . . . 8
β’ ((π β β β§ π β (1...((π β β β¦ ((2
Β· π) β
1))βπ))) β π β (1...((π β β β¦ ((2
Β· π) β
1))βπ))) |
426 | 371 | adantr 482 |
. . . . . . . 8
β’ ((π β β β§ π β (1...((π β β β¦ ((2
Β· π) β
1))βπ))) β
(1...((π β β
β¦ ((2 Β· π)
β 1))βπ)) =
(1...((2 Β· π)
β 1))) |
427 | 425, 426 | eleqtrd 2836 |
. . . . . . 7
β’ ((π β β β§ π β (1...((π β β β¦ ((2
Β· π) β
1))βπ))) β π β (1...((2 Β· π) β 1))) |
428 | 427 | adantll 713 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (1...((π β β β¦ ((2 Β· π) β 1))βπ))) β π β (1...((2 Β· π) β 1))) |
429 | 424, 428,
93 | syl2anc 585 |
. . . . 5
β’ (((π β§ π β β) β§ π β (1...((π β β β¦ ((2 Β· π) β 1))βπ))) β (πΉβπ) β β) |
430 | 412, 423,
429 | fsumser 15673 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β (1...((π β β β¦ ((2
Β· π) β
1))βπ))(πΉβπ) = (seq1( + , πΉ)β((π β β β¦ ((2 Β· π) β 1))βπ))) |
431 | 375, 411,
430 | 3eqtr3d 2781 |
. . 3
β’ ((π β§ π β β) β (seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1))))βπ) = (seq1( + , πΉ)β((π β β β¦ ((2 Β· π) β 1))βπ))) |
432 | 1, 2, 6, 7, 8, 9, 11, 15, 16, 29, 73, 75, 431 | climsuse 44311 |
. 2
β’ (π β seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) β π΅) |
433 | | eqidd 2734 |
. . . 4
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
434 | 8, 9, 433, 13 | isum 15662 |
. . 3
β’ (π β Ξ£π β β (πΉβπ) = ( β βseq1( + , πΉ))) |
435 | | climrel 15433 |
. . . . . . 7
β’ Rel
β |
436 | 435 | releldmi 5946 |
. . . . . 6
β’ (seq1( +
, πΉ) β π΅ β seq1( + , πΉ) β dom β
) |
437 | 16, 436 | syl 17 |
. . . . 5
β’ (π β seq1( + , πΉ) β dom β
) |
438 | | climdm 15495 |
. . . . 5
β’ (seq1( +
, πΉ) β dom β
β seq1( + , πΉ) β
( β βseq1( + , πΉ))) |
439 | 437, 438 | sylib 217 |
. . . 4
β’ (π β seq1( + , πΉ) β ( β βseq1(
+ , πΉ))) |
440 | | climuni 15493 |
. . . 4
β’ ((seq1( +
, πΉ) β ( β
βseq1( + , πΉ)) β§
seq1( + , πΉ) β π΅) β ( β βseq1(
+ , πΉ)) = π΅) |
441 | 439, 16, 440 | syl2anc 585 |
. . 3
β’ (π β ( β βseq1( + ,
πΉ)) = π΅) |
442 | 435 | a1i 11 |
. . . . . . . 8
β’ (π β Rel β
) |
443 | | releldm 5942 |
. . . . . . . 8
β’ ((Rel
β β§ seq1( + , (π
β β β¦ (πΉβ((2 Β· π) β 1)))) β π΅) β seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) β dom β
) |
444 | 442, 432,
443 | syl2anc 585 |
. . . . . . 7
β’ (π β seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) β dom
β ) |
445 | | climdm 15495 |
. . . . . . 7
β’ (seq1( +
, (π β β β¦
(πΉβ((2 Β· π) β 1)))) β dom
β β seq1( + , (π
β β β¦ (πΉβ((2 Β· π) β 1)))) β ( β
βseq1( + , (π β
β β¦ (πΉβ((2 Β· π) β 1)))))) |
446 | 444, 445 | sylib 217 |
. . . . . 6
β’ (π β seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) β (
β βseq1( + , (π
β β β¦ (πΉβ((2 Β· π) β 1)))))) |
447 | 406 | a1i 11 |
. . . . . . . 8
β’ (π β (π β β β¦ (πΉβ((2 Β· π) β 1))) = (π β β β¦ (πΉβ((2 Β· π) β 1)))) |
448 | 447 | seqeq3d 13971 |
. . . . . . 7
β’ (π β seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) = seq1( + ,
(π β β β¦
(πΉβ((2 Β· π) β
1))))) |
449 | 448 | fveq2d 6893 |
. . . . . 6
β’ (π β ( β βseq1( + ,
(π β β β¦
(πΉβ((2 Β· π) β 1))))) = ( β
βseq1( + , (π β
β β¦ (πΉβ((2 Β· π) β 1)))))) |
450 | 446, 449 | breqtrd 5174 |
. . . . 5
β’ (π β seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) β (
β βseq1( + , (π
β β β¦ (πΉβ((2 Β· π) β 1)))))) |
451 | | climuni 15493 |
. . . . 5
β’ ((seq1( +
, (π β β β¦
(πΉβ((2 Β· π) β 1)))) β π΅ β§ seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) β (
β βseq1( + , (π
β β β¦ (πΉβ((2 Β· π) β 1)))))) β π΅ = ( β βseq1( + , (π β β β¦ (πΉβ((2 Β· π) β
1)))))) |
452 | 432, 450,
451 | syl2anc 585 |
. . . 4
β’ (π β π΅ = ( β βseq1( + , (π β β β¦ (πΉβ((2 Β· π) β
1)))))) |
453 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ π β β) β (π β β β¦ (πΉβ((2 Β· π) β 1))) = (π β β β¦ (πΉβ((2 Β· π) β 1)))) |
454 | | eqcom 2740 |
. . . . . . . 8
β’ (π = π β π = π) |
455 | | eqcom 2740 |
. . . . . . . 8
β’ ((πΉβ((2 Β· π) β 1)) = (πΉβ((2 Β· π) β 1)) β (πΉβ((2 Β· π) β 1)) = (πΉβ((2 Β· π) β 1))) |
456 | 405, 454,
455 | 3imtr3i 291 |
. . . . . . 7
β’ (π = π β (πΉβ((2 Β· π) β 1)) = (πΉβ((2 Β· π) β 1))) |
457 | 456 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ π = π) β (πΉβ((2 Β· π) β 1)) = (πΉβ((2 Β· π) β 1))) |
458 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β πΉ:ββΆβ) |
459 | 421, 8 | eleqtrrdi 2845 |
. . . . . . . 8
β’ (π β β β ((2
Β· π) β 1)
β β) |
460 | 459 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β) β ((2 Β· π) β 1) β
β) |
461 | 458, 460 | ffvelcdmd 7085 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβ((2 Β· π) β 1)) β
β) |
462 | 453, 457,
409, 461 | fvmptd 7003 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ (πΉβ((2 Β· π) β 1)))βπ) = (πΉβ((2 Β· π) β 1))) |
463 | 8, 9, 462, 461 | isum 15662 |
. . . 4
β’ (π β Ξ£π β β (πΉβ((2 Β· π) β 1)) = ( β βseq1( + ,
(π β β β¦
(πΉβ((2 Β· π) β
1)))))) |
464 | 452, 463 | eqtr4d 2776 |
. . 3
β’ (π β π΅ = Ξ£π β β (πΉβ((2 Β· π) β 1))) |
465 | 434, 441,
464 | 3eqtrd 2777 |
. 2
β’ (π β Ξ£π β β (πΉβπ) = Ξ£π β β (πΉβ((2 Β· π) β 1))) |
466 | 432, 465 | jca 513 |
1
β’ (π β (seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) β π΅ β§ Ξ£π β β (πΉβπ) = Ξ£π β β (πΉβ((2 Β· π) β 1)))) |