Step | Hyp | Ref
| Expression |
1 | | ovolun.g1 |
. . . . . . . . . 10
β’ (π β πΊ β (( β€ β© (β Γ
β)) βm β)) |
2 | | elovolmlem 24861 |
. . . . . . . . . 10
β’ (πΊ β (( β€ β© (β
Γ β)) βm β) β πΊ:ββΆ( β€ β© (β
Γ β))) |
3 | 1, 2 | sylib 217 |
. . . . . . . . 9
β’ (π β πΊ:ββΆ( β€ β© (β
Γ β))) |
4 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β πΊ:ββΆ( β€ β© (β
Γ β))) |
5 | 4 | ffvelcdmda 7039 |
. . . . . . 7
β’ (((π β§ π β β) β§ (π / 2) β β) β (πΊβ(π / 2)) β ( β€ β© (β Γ
β))) |
6 | | nneo 12595 |
. . . . . . . . . . 11
β’ (π β β β ((π / 2) β β β
Β¬ ((π + 1) / 2) β
β)) |
7 | 6 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π / 2) β β β Β¬ ((π + 1) / 2) β
β)) |
8 | 7 | con2bid 355 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((π + 1) / 2) β β β Β¬ (π / 2) β
β)) |
9 | 8 | biimpar 479 |
. . . . . . . 8
β’ (((π β§ π β β) β§ Β¬ (π / 2) β β) β
((π + 1) / 2) β
β) |
10 | | ovolun.f1 |
. . . . . . . . . . 11
β’ (π β πΉ β (( β€ β© (β Γ
β)) βm β)) |
11 | | elovolmlem 24861 |
. . . . . . . . . . 11
β’ (πΉ β (( β€ β© (β
Γ β)) βm β) β πΉ:ββΆ( β€ β© (β
Γ β))) |
12 | 10, 11 | sylib 217 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
13 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΉ:ββΆ( β€ β© (β
Γ β))) |
14 | 13 | ffvelcdmda 7039 |
. . . . . . . 8
β’ (((π β§ π β β) β§ ((π + 1) / 2) β β) β (πΉβ((π + 1) / 2)) β ( β€ β© (β
Γ β))) |
15 | 9, 14 | syldan 592 |
. . . . . . 7
β’ (((π β§ π β β) β§ Β¬ (π / 2) β β) β
(πΉβ((π + 1) / 2)) β ( β€ β©
(β Γ β))) |
16 | 5, 15 | ifclda 4525 |
. . . . . 6
β’ ((π β§ π β β) β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) β ( β€ β© (β
Γ β))) |
17 | | ovolun.h |
. . . . . 6
β’ π» = (π β β β¦ if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2)))) |
18 | 16, 17 | fmptd 7066 |
. . . . 5
β’ (π β π»:ββΆ( β€ β© (β
Γ β))) |
19 | | eqid 2733 |
. . . . . 6
β’ ((abs
β β ) β π») = ((abs β β ) β π») |
20 | | ovolun.u |
. . . . . 6
β’ π = seq1( + , ((abs β
β ) β π»)) |
21 | 19, 20 | ovolsf 24859 |
. . . . 5
β’ (π»:ββΆ( β€ β©
(β Γ β)) β π:ββΆ(0[,)+β)) |
22 | 18, 21 | syl 17 |
. . . 4
β’ (π β π:ββΆ(0[,)+β)) |
23 | | rge0ssre 13382 |
. . . 4
β’
(0[,)+β) β β |
24 | | fss 6689 |
. . . 4
β’ ((π:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β π:ββΆβ) |
25 | 22, 23, 24 | sylancl 587 |
. . 3
β’ (π β π:ββΆβ) |
26 | 25 | ffvelcdmda 7039 |
. 2
β’ ((π β§ π β β) β (πβπ) β β) |
27 | | 2nn 12234 |
. . . 4
β’ 2 β
β |
28 | | peano2nn 12173 |
. . . . . . . . 9
β’ (π β β β (π + 1) β
β) |
29 | 28 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β) β (π + 1) β β) |
30 | 29 | nnred 12176 |
. . . . . . 7
β’ ((π β§ π β β) β (π + 1) β β) |
31 | 30 | rehalfcld 12408 |
. . . . . 6
β’ ((π β§ π β β) β ((π + 1) / 2) β β) |
32 | 31 | flcld 13712 |
. . . . 5
β’ ((π β§ π β β) β
(ββ((π + 1) /
2)) β β€) |
33 | | ax-1cn 11117 |
. . . . . . . . 9
β’ 1 β
β |
34 | 33 | 2timesi 12299 |
. . . . . . . 8
β’ (2
Β· 1) = (1 + 1) |
35 | | nnge1 12189 |
. . . . . . . . . 10
β’ (π β β β 1 β€
π) |
36 | 35 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β) β 1 β€ π) |
37 | | nnre 12168 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
38 | 37 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
39 | | 1re 11163 |
. . . . . . . . . . 11
β’ 1 β
β |
40 | | leadd1 11631 |
. . . . . . . . . . 11
β’ ((1
β β β§ π
β β β§ 1 β β) β (1 β€ π β (1 + 1) β€ (π + 1))) |
41 | 39, 39, 40 | mp3an13 1453 |
. . . . . . . . . 10
β’ (π β β β (1 β€
π β (1 + 1) β€
(π + 1))) |
42 | 38, 41 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (1 β€ π β (1 + 1) β€ (π + 1))) |
43 | 36, 42 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β β) β (1 + 1) β€ (π + 1)) |
44 | 34, 43 | eqbrtrid 5144 |
. . . . . . 7
β’ ((π β§ π β β) β (2 Β· 1) β€
(π + 1)) |
45 | | 2re 12235 |
. . . . . . . . . 10
β’ 2 β
β |
46 | | 2pos 12264 |
. . . . . . . . . 10
β’ 0 <
2 |
47 | 45, 46 | pm3.2i 472 |
. . . . . . . . 9
β’ (2 β
β β§ 0 < 2) |
48 | | lemuldiv2 12044 |
. . . . . . . . 9
β’ ((1
β β β§ (π +
1) β β β§ (2 β β β§ 0 < 2)) β ((2 Β·
1) β€ (π + 1) β 1
β€ ((π + 1) /
2))) |
49 | 39, 47, 48 | mp3an13 1453 |
. . . . . . . 8
β’ ((π + 1) β β β ((2
Β· 1) β€ (π + 1)
β 1 β€ ((π + 1) /
2))) |
50 | 30, 49 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β ((2 Β· 1) β€
(π + 1) β 1 β€
((π + 1) /
2))) |
51 | 44, 50 | mpbid 231 |
. . . . . 6
β’ ((π β§ π β β) β 1 β€ ((π + 1) / 2)) |
52 | | 1z 12541 |
. . . . . . 7
β’ 1 β
β€ |
53 | | flge 13719 |
. . . . . . 7
β’ ((((π + 1) / 2) β β β§
1 β β€) β (1 β€ ((π + 1) / 2) β 1 β€
(ββ((π + 1) /
2)))) |
54 | 31, 52, 53 | sylancl 587 |
. . . . . 6
β’ ((π β§ π β β) β (1 β€ ((π + 1) / 2) β 1 β€
(ββ((π + 1) /
2)))) |
55 | 51, 54 | mpbid 231 |
. . . . 5
β’ ((π β§ π β β) β 1 β€
(ββ((π + 1) /
2))) |
56 | | elnnz1 12537 |
. . . . 5
β’
((ββ((π
+ 1) / 2)) β β β ((ββ((π + 1) / 2)) β β€ β§ 1 β€
(ββ((π + 1) /
2)))) |
57 | 32, 55, 56 | sylanbrc 584 |
. . . 4
β’ ((π β§ π β β) β
(ββ((π + 1) /
2)) β β) |
58 | | nnmulcl 12185 |
. . . 4
β’ ((2
β β β§ (ββ((π + 1) / 2)) β β) β (2
Β· (ββ((π
+ 1) / 2))) β β) |
59 | 27, 57, 58 | sylancr 588 |
. . 3
β’ ((π β§ π β β) β (2 Β·
(ββ((π + 1) /
2))) β β) |
60 | 25 | ffvelcdmda 7039 |
. . 3
β’ ((π β§ (2 Β·
(ββ((π + 1) /
2))) β β) β (πβ(2 Β· (ββ((π + 1) / 2)))) β
β) |
61 | 59, 60 | syldan 592 |
. 2
β’ ((π β§ π β β) β (πβ(2 Β· (ββ((π + 1) / 2)))) β
β) |
62 | | ovolun.a |
. . . . . 6
β’ (π β (π΄ β β β§ (vol*βπ΄) β
β)) |
63 | 62 | simprd 497 |
. . . . 5
β’ (π β (vol*βπ΄) β
β) |
64 | | ovolun.b |
. . . . . 6
β’ (π β (π΅ β β β§ (vol*βπ΅) β
β)) |
65 | 64 | simprd 497 |
. . . . 5
β’ (π β (vol*βπ΅) β
β) |
66 | 63, 65 | readdcld 11192 |
. . . 4
β’ (π β ((vol*βπ΄) + (vol*βπ΅)) β
β) |
67 | | ovolun.c |
. . . . 5
β’ (π β πΆ β
β+) |
68 | 67 | rpred 12965 |
. . . 4
β’ (π β πΆ β β) |
69 | 66, 68 | readdcld 11192 |
. . 3
β’ (π β (((vol*βπ΄) + (vol*βπ΅)) + πΆ) β β) |
70 | 69 | adantr 482 |
. 2
β’ ((π β§ π β β) β (((vol*βπ΄) + (vol*βπ΅)) + πΆ) β β) |
71 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
72 | | nnuz 12814 |
. . . . 5
β’ β =
(β€β₯β1) |
73 | 71, 72 | eleqtrdi 2844 |
. . . 4
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
74 | | nnz 12528 |
. . . . . . 7
β’ (π β β β π β
β€) |
75 | 74 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β π β β€) |
76 | | flhalf 13744 |
. . . . . 6
β’ (π β β€ β π β€ (2 Β·
(ββ((π + 1) /
2)))) |
77 | 75, 76 | syl 17 |
. . . . 5
β’ ((π β§ π β β) β π β€ (2 Β· (ββ((π + 1) / 2)))) |
78 | | nnz 12528 |
. . . . . . 7
β’ ((2
Β· (ββ((π
+ 1) / 2))) β β β (2 Β· (ββ((π + 1) / 2))) β
β€) |
79 | | eluz 12785 |
. . . . . . 7
β’ ((π β β€ β§ (2
Β· (ββ((π
+ 1) / 2))) β β€) β ((2 Β· (ββ((π + 1) / 2))) β
(β€β₯βπ) β π β€ (2 Β· (ββ((π + 1) / 2))))) |
80 | 74, 78, 79 | syl2an 597 |
. . . . . 6
β’ ((π β β β§ (2
Β· (ββ((π
+ 1) / 2))) β β) β ((2 Β· (ββ((π + 1) / 2))) β
(β€β₯βπ) β π β€ (2 Β· (ββ((π + 1) / 2))))) |
81 | 71, 59, 80 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β β) β ((2 Β·
(ββ((π + 1) /
2))) β (β€β₯βπ) β π β€ (2 Β· (ββ((π + 1) / 2))))) |
82 | 77, 81 | mpbird 257 |
. . . 4
β’ ((π β§ π β β) β (2 Β·
(ββ((π + 1) /
2))) β (β€β₯βπ)) |
83 | | elfznn 13479 |
. . . . 5
β’ (π β (1...(2 Β·
(ββ((π + 1) /
2)))) β π β
β) |
84 | 19 | ovolfsf 24858 |
. . . . . . . . . 10
β’ (π»:ββΆ( β€ β©
(β Γ β)) β ((abs β β ) β π»):ββΆ(0[,)+β)) |
85 | 18, 84 | syl 17 |
. . . . . . . . 9
β’ (π β ((abs β β )
β π»):ββΆ(0[,)+β)) |
86 | 85 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β ((abs β β
) β π»):ββΆ(0[,)+β)) |
87 | 86 | ffvelcdmda 7039 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β β) β (((abs β
β ) β π»)βπ) β (0[,)+β)) |
88 | | elrege0 13380 |
. . . . . . 7
β’ ((((abs
β β ) β π»)βπ) β (0[,)+β) β ((((abs
β β ) β π»)βπ) β β β§ 0 β€ (((abs β
β ) β π»)βπ))) |
89 | 87, 88 | sylib 217 |
. . . . . 6
β’ (((π β§ π β β) β§ π β β) β ((((abs β
β ) β π»)βπ) β β β§ 0 β€ (((abs β
β ) β π»)βπ))) |
90 | 89 | simpld 496 |
. . . . 5
β’ (((π β§ π β β) β§ π β β) β (((abs β
β ) β π»)βπ) β β) |
91 | 83, 90 | sylan2 594 |
. . . 4
β’ (((π β§ π β β) β§ π β (1...(2 Β·
(ββ((π + 1) /
2))))) β (((abs β β ) β π»)βπ) β β) |
92 | | elfzuz 13446 |
. . . . . 6
β’ (π β ((π + 1)...(2 Β· (ββ((π + 1) / 2)))) β π β
(β€β₯β(π + 1))) |
93 | | eluznn 12851 |
. . . . . 6
β’ (((π + 1) β β β§ π β
(β€β₯β(π + 1))) β π β β) |
94 | 29, 92, 93 | syl2an 597 |
. . . . 5
β’ (((π β§ π β β) β§ π β ((π + 1)...(2 Β· (ββ((π + 1) / 2))))) β π β
β) |
95 | 89 | simprd 497 |
. . . . 5
β’ (((π β§ π β β) β§ π β β) β 0 β€ (((abs β
β ) β π»)βπ)) |
96 | 94, 95 | syldan 592 |
. . . 4
β’ (((π β§ π β β) β§ π β ((π + 1)...(2 Β· (ββ((π + 1) / 2))))) β 0 β€
(((abs β β ) β π»)βπ)) |
97 | 73, 82, 91, 96 | sermono 13949 |
. . 3
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β π»))βπ) β€ (seq1( + , ((abs β β )
β π»))β(2
Β· (ββ((π
+ 1) / 2))))) |
98 | 20 | fveq1i 6847 |
. . 3
β’ (πβπ) = (seq1( + , ((abs β β )
β π»))βπ) |
99 | 20 | fveq1i 6847 |
. . 3
β’ (πβ(2 Β·
(ββ((π + 1) /
2)))) = (seq1( + , ((abs β β ) β π»))β(2 Β· (ββ((π + 1) / 2)))) |
100 | 97, 98, 99 | 3brtr4g 5143 |
. 2
β’ ((π β§ π β β) β (πβπ) β€ (πβ(2 Β· (ββ((π + 1) / 2))))) |
101 | | eqid 2733 |
. . . . . . . . . 10
β’ ((abs
β β ) β πΉ) = ((abs β β ) β πΉ) |
102 | | ovolun.s |
. . . . . . . . . 10
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
103 | 101, 102 | ovolsf 24859 |
. . . . . . . . 9
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β π:ββΆ(0[,)+β)) |
104 | 12, 103 | syl 17 |
. . . . . . . 8
β’ (π β π:ββΆ(0[,)+β)) |
105 | 104 | frnd 6680 |
. . . . . . 7
β’ (π β ran π β (0[,)+β)) |
106 | 105, 23 | sstrdi 3960 |
. . . . . 6
β’ (π β ran π β β) |
107 | 106 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β ran π β β) |
108 | 104 | ffnd 6673 |
. . . . . 6
β’ (π β π Fn β) |
109 | | fnfvelrn 7035 |
. . . . . 6
β’ ((π Fn β β§
(ββ((π + 1) /
2)) β β) β (πβ(ββ((π + 1) / 2))) β ran π) |
110 | 108, 57, 109 | syl2an2r 684 |
. . . . 5
β’ ((π β§ π β β) β (πβ(ββ((π + 1) / 2))) β ran π) |
111 | 107, 110 | sseldd 3949 |
. . . 4
β’ ((π β§ π β β) β (πβ(ββ((π + 1) / 2))) β β) |
112 | | eqid 2733 |
. . . . . . . . . 10
β’ ((abs
β β ) β πΊ) = ((abs β β ) β πΊ) |
113 | | ovolun.t |
. . . . . . . . . 10
β’ π = seq1( + , ((abs β
β ) β πΊ)) |
114 | 112, 113 | ovolsf 24859 |
. . . . . . . . 9
β’ (πΊ:ββΆ( β€ β©
(β Γ β)) β π:ββΆ(0[,)+β)) |
115 | 3, 114 | syl 17 |
. . . . . . . 8
β’ (π β π:ββΆ(0[,)+β)) |
116 | 115 | frnd 6680 |
. . . . . . 7
β’ (π β ran π β (0[,)+β)) |
117 | 116, 23 | sstrdi 3960 |
. . . . . 6
β’ (π β ran π β β) |
118 | 117 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β ran π β β) |
119 | 115 | ffnd 6673 |
. . . . . 6
β’ (π β π Fn β) |
120 | | fnfvelrn 7035 |
. . . . . 6
β’ ((π Fn β β§
(ββ((π + 1) /
2)) β β) β (πβ(ββ((π + 1) / 2))) β ran π) |
121 | 119, 57, 120 | syl2an2r 684 |
. . . . 5
β’ ((π β§ π β β) β (πβ(ββ((π + 1) / 2))) β ran π) |
122 | 118, 121 | sseldd 3949 |
. . . 4
β’ ((π β§ π β β) β (πβ(ββ((π + 1) / 2))) β β) |
123 | 68 | rehalfcld 12408 |
. . . . . 6
β’ (π β (πΆ / 2) β β) |
124 | 63, 123 | readdcld 11192 |
. . . . 5
β’ (π β ((vol*βπ΄) + (πΆ / 2)) β β) |
125 | 124 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β ((vol*βπ΄) + (πΆ / 2)) β β) |
126 | 65, 123 | readdcld 11192 |
. . . . 5
β’ (π β ((vol*βπ΅) + (πΆ / 2)) β β) |
127 | 126 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β ((vol*βπ΅) + (πΆ / 2)) β β) |
128 | | ressxr 11207 |
. . . . . . . . 9
β’ β
β β* |
129 | 106, 128 | sstrdi 3960 |
. . . . . . . 8
β’ (π β ran π β
β*) |
130 | | supxrcl 13243 |
. . . . . . . 8
β’ (ran
π β
β* β sup(ran π, β*, < ) β
β*) |
131 | 129, 130 | syl 17 |
. . . . . . 7
β’ (π β sup(ran π, β*, < ) β
β*) |
132 | | 1nn 12172 |
. . . . . . . . . . 11
β’ 1 β
β |
133 | 104 | fdmd 6683 |
. . . . . . . . . . 11
β’ (π β dom π = β) |
134 | 132, 133 | eleqtrrid 2841 |
. . . . . . . . . 10
β’ (π β 1 β dom π) |
135 | 134 | ne0d 4299 |
. . . . . . . . 9
β’ (π β dom π β β
) |
136 | | dm0rn0 5884 |
. . . . . . . . . 10
β’ (dom
π = β
β ran
π =
β
) |
137 | 136 | necon3bii 2993 |
. . . . . . . . 9
β’ (dom
π β β
β ran
π β
β
) |
138 | 135, 137 | sylib 217 |
. . . . . . . 8
β’ (π β ran π β β
) |
139 | | supxrgtmnf 13257 |
. . . . . . . 8
β’ ((ran
π β β β§ ran
π β β
) β
-β < sup(ran π,
β*, < )) |
140 | 106, 138,
139 | syl2anc 585 |
. . . . . . 7
β’ (π β -β < sup(ran
π, β*,
< )) |
141 | | ovolun.f3 |
. . . . . . 7
β’ (π β sup(ran π, β*, < ) β€
((vol*βπ΄) + (πΆ / 2))) |
142 | | xrre 13097 |
. . . . . . 7
β’
(((sup(ran π,
β*, < ) β β* β§ ((vol*βπ΄) + (πΆ / 2)) β β) β§ (-β <
sup(ran π,
β*, < ) β§ sup(ran π, β*, < ) β€
((vol*βπ΄) + (πΆ / 2)))) β sup(ran π, β*, < )
β β) |
143 | 131, 124,
140, 141, 142 | syl22anc 838 |
. . . . . 6
β’ (π β sup(ran π, β*, < ) β
β) |
144 | 143 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β sup(ran π, β*, < )
β β) |
145 | | supxrub 13252 |
. . . . . 6
β’ ((ran
π β
β* β§ (πβ(ββ((π + 1) / 2))) β ran π) β (πβ(ββ((π + 1) / 2))) β€ sup(ran π, β*, <
)) |
146 | 129, 110,
145 | syl2an2r 684 |
. . . . 5
β’ ((π β§ π β β) β (πβ(ββ((π + 1) / 2))) β€ sup(ran π, β*, <
)) |
147 | 141 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β sup(ran π, β*, < )
β€ ((vol*βπ΄) +
(πΆ / 2))) |
148 | 111, 144,
125, 146, 147 | letrd 11320 |
. . . 4
β’ ((π β§ π β β) β (πβ(ββ((π + 1) / 2))) β€ ((vol*βπ΄) + (πΆ / 2))) |
149 | 117, 128 | sstrdi 3960 |
. . . . . . . 8
β’ (π β ran π β
β*) |
150 | | supxrcl 13243 |
. . . . . . . 8
β’ (ran
π β
β* β sup(ran π, β*, < ) β
β*) |
151 | 149, 150 | syl 17 |
. . . . . . 7
β’ (π β sup(ran π, β*, < ) β
β*) |
152 | 115 | fdmd 6683 |
. . . . . . . . . . 11
β’ (π β dom π = β) |
153 | 132, 152 | eleqtrrid 2841 |
. . . . . . . . . 10
β’ (π β 1 β dom π) |
154 | 153 | ne0d 4299 |
. . . . . . . . 9
β’ (π β dom π β β
) |
155 | | dm0rn0 5884 |
. . . . . . . . . 10
β’ (dom
π = β
β ran
π =
β
) |
156 | 155 | necon3bii 2993 |
. . . . . . . . 9
β’ (dom
π β β
β ran
π β
β
) |
157 | 154, 156 | sylib 217 |
. . . . . . . 8
β’ (π β ran π β β
) |
158 | | supxrgtmnf 13257 |
. . . . . . . 8
β’ ((ran
π β β β§ ran
π β β
) β
-β < sup(ran π,
β*, < )) |
159 | 117, 157,
158 | syl2anc 585 |
. . . . . . 7
β’ (π β -β < sup(ran
π, β*,
< )) |
160 | | ovolun.g3 |
. . . . . . 7
β’ (π β sup(ran π, β*, < ) β€
((vol*βπ΅) + (πΆ / 2))) |
161 | | xrre 13097 |
. . . . . . 7
β’
(((sup(ran π,
β*, < ) β β* β§ ((vol*βπ΅) + (πΆ / 2)) β β) β§ (-β <
sup(ran π,
β*, < ) β§ sup(ran π, β*, < ) β€
((vol*βπ΅) + (πΆ / 2)))) β sup(ran π, β*, < )
β β) |
162 | 151, 126,
159, 160, 161 | syl22anc 838 |
. . . . . 6
β’ (π β sup(ran π, β*, < ) β
β) |
163 | 162 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β sup(ran π, β*, < )
β β) |
164 | | supxrub 13252 |
. . . . . 6
β’ ((ran
π β
β* β§ (πβ(ββ((π + 1) / 2))) β ran π) β (πβ(ββ((π + 1) / 2))) β€ sup(ran π, β*, <
)) |
165 | 149, 121,
164 | syl2an2r 684 |
. . . . 5
β’ ((π β§ π β β) β (πβ(ββ((π + 1) / 2))) β€ sup(ran π, β*, <
)) |
166 | 160 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β sup(ran π, β*, < )
β€ ((vol*βπ΅) +
(πΆ / 2))) |
167 | 122, 163,
127, 165, 166 | letrd 11320 |
. . . 4
β’ ((π β§ π β β) β (πβ(ββ((π + 1) / 2))) β€ ((vol*βπ΅) + (πΆ / 2))) |
168 | 111, 122,
125, 127, 148, 167 | le2addd 11782 |
. . 3
β’ ((π β§ π β β) β ((πβ(ββ((π + 1) / 2))) + (πβ(ββ((π + 1) / 2)))) β€ (((vol*βπ΄) + (πΆ / 2)) + ((vol*βπ΅) + (πΆ / 2)))) |
169 | | oveq2 7369 |
. . . . . . . . 9
β’ (π§ = 1 β (2 Β· π§) = (2 Β·
1)) |
170 | 169 | fveq2d 6850 |
. . . . . . . 8
β’ (π§ = 1 β (πβ(2 Β· π§)) = (πβ(2 Β· 1))) |
171 | | fveq2 6846 |
. . . . . . . . 9
β’ (π§ = 1 β (πβπ§) = (πβ1)) |
172 | | fveq2 6846 |
. . . . . . . . 9
β’ (π§ = 1 β (πβπ§) = (πβ1)) |
173 | 171, 172 | oveq12d 7379 |
. . . . . . . 8
β’ (π§ = 1 β ((πβπ§) + (πβπ§)) = ((πβ1) + (πβ1))) |
174 | 170, 173 | eqeq12d 2749 |
. . . . . . 7
β’ (π§ = 1 β ((πβ(2 Β· π§)) = ((πβπ§) + (πβπ§)) β (πβ(2 Β· 1)) = ((πβ1) + (πβ1)))) |
175 | 174 | imbi2d 341 |
. . . . . 6
β’ (π§ = 1 β ((π β (πβ(2 Β· π§)) = ((πβπ§) + (πβπ§))) β (π β (πβ(2 Β· 1)) = ((πβ1) + (πβ1))))) |
176 | | oveq2 7369 |
. . . . . . . . 9
β’ (π§ = π β (2 Β· π§) = (2 Β· π)) |
177 | 176 | fveq2d 6850 |
. . . . . . . 8
β’ (π§ = π β (πβ(2 Β· π§)) = (πβ(2 Β· π))) |
178 | | fveq2 6846 |
. . . . . . . . 9
β’ (π§ = π β (πβπ§) = (πβπ)) |
179 | | fveq2 6846 |
. . . . . . . . 9
β’ (π§ = π β (πβπ§) = (πβπ)) |
180 | 178, 179 | oveq12d 7379 |
. . . . . . . 8
β’ (π§ = π β ((πβπ§) + (πβπ§)) = ((πβπ) + (πβπ))) |
181 | 177, 180 | eqeq12d 2749 |
. . . . . . 7
β’ (π§ = π β ((πβ(2 Β· π§)) = ((πβπ§) + (πβπ§)) β (πβ(2 Β· π)) = ((πβπ) + (πβπ)))) |
182 | 181 | imbi2d 341 |
. . . . . 6
β’ (π§ = π β ((π β (πβ(2 Β· π§)) = ((πβπ§) + (πβπ§))) β (π β (πβ(2 Β· π)) = ((πβπ) + (πβπ))))) |
183 | | oveq2 7369 |
. . . . . . . . 9
β’ (π§ = (π + 1) β (2 Β· π§) = (2 Β· (π + 1))) |
184 | 183 | fveq2d 6850 |
. . . . . . . 8
β’ (π§ = (π + 1) β (πβ(2 Β· π§)) = (πβ(2 Β· (π + 1)))) |
185 | | fveq2 6846 |
. . . . . . . . 9
β’ (π§ = (π + 1) β (πβπ§) = (πβ(π + 1))) |
186 | | fveq2 6846 |
. . . . . . . . 9
β’ (π§ = (π + 1) β (πβπ§) = (πβ(π + 1))) |
187 | 185, 186 | oveq12d 7379 |
. . . . . . . 8
β’ (π§ = (π + 1) β ((πβπ§) + (πβπ§)) = ((πβ(π + 1)) + (πβ(π + 1)))) |
188 | 184, 187 | eqeq12d 2749 |
. . . . . . 7
β’ (π§ = (π + 1) β ((πβ(2 Β· π§)) = ((πβπ§) + (πβπ§)) β (πβ(2 Β· (π + 1))) = ((πβ(π + 1)) + (πβ(π + 1))))) |
189 | 188 | imbi2d 341 |
. . . . . 6
β’ (π§ = (π + 1) β ((π β (πβ(2 Β· π§)) = ((πβπ§) + (πβπ§))) β (π β (πβ(2 Β· (π + 1))) = ((πβ(π + 1)) + (πβ(π + 1)))))) |
190 | | oveq2 7369 |
. . . . . . . . 9
β’ (π§ = (ββ((π + 1) / 2)) β (2 Β·
π§) = (2 Β·
(ββ((π + 1) /
2)))) |
191 | 190 | fveq2d 6850 |
. . . . . . . 8
β’ (π§ = (ββ((π + 1) / 2)) β (πβ(2 Β· π§)) = (πβ(2 Β· (ββ((π + 1) / 2))))) |
192 | | fveq2 6846 |
. . . . . . . . 9
β’ (π§ = (ββ((π + 1) / 2)) β (πβπ§) = (πβ(ββ((π + 1) / 2)))) |
193 | | fveq2 6846 |
. . . . . . . . 9
β’ (π§ = (ββ((π + 1) / 2)) β (πβπ§) = (πβ(ββ((π + 1) / 2)))) |
194 | 192, 193 | oveq12d 7379 |
. . . . . . . 8
β’ (π§ = (ββ((π + 1) / 2)) β ((πβπ§) + (πβπ§)) = ((πβ(ββ((π + 1) / 2))) + (πβ(ββ((π + 1) / 2))))) |
195 | 191, 194 | eqeq12d 2749 |
. . . . . . 7
β’ (π§ = (ββ((π + 1) / 2)) β ((πβ(2 Β· π§)) = ((πβπ§) + (πβπ§)) β (πβ(2 Β· (ββ((π + 1) / 2)))) = ((πβ(ββ((π + 1) / 2))) + (πβ(ββ((π + 1) / 2)))))) |
196 | 195 | imbi2d 341 |
. . . . . 6
β’ (π§ = (ββ((π + 1) / 2)) β ((π β (πβ(2 Β· π§)) = ((πβπ§) + (πβπ§))) β (π β (πβ(2 Β· (ββ((π + 1) / 2)))) = ((πβ(ββ((π + 1) / 2))) + (πβ(ββ((π + 1) /
2))))))) |
197 | 20 | fveq1i 6847 |
. . . . . . . 8
β’ (πβ(2 Β· 1)) = (seq1(
+ , ((abs β β ) β π»))β(2 Β· 1)) |
198 | 132 | a1i 11 |
. . . . . . . . 9
β’ (π β 1 β
β) |
199 | 19 | ovolfsval 24857 |
. . . . . . . . . . . 12
β’ ((π»:ββΆ( β€ β©
(β Γ β)) β§ 1 β β) β (((abs β
β ) β π»)β1) = ((2nd β(π»β1)) β
(1st β(π»β1)))) |
200 | 18, 132, 199 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β (((abs β β )
β π»)β1) =
((2nd β(π»β1)) β (1st
β(π»β1)))) |
201 | | halfnz 12589 |
. . . . . . . . . . . . . . . . . 18
β’ Β¬ (1
/ 2) β β€ |
202 | | nnz 12528 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π / 2) β β β
(π / 2) β
β€) |
203 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 1 β (π / 2) = (1 / 2)) |
204 | 203 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 1 β ((π / 2) β β€ β (1 / 2) β
β€)) |
205 | 202, 204 | imbitrid 243 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 1 β ((π / 2) β β β (1 / 2) β
β€)) |
206 | 201, 205 | mtoi 198 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β Β¬ (π / 2) β
β) |
207 | 206 | iffalsed 4501 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) = (πΉβ((π + 1) / 2))) |
208 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 1 β (π + 1) = (1 + 1)) |
209 | | df-2 12224 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 = (1 +
1) |
210 | 208, 209 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 1 β (π + 1) = 2) |
211 | 210 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 1 β ((π + 1) / 2) = (2 / 2)) |
212 | | 2div2e1 12302 |
. . . . . . . . . . . . . . . . . 18
β’ (2 / 2) =
1 |
213 | 211, 212 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β ((π + 1) / 2) = 1) |
214 | 213 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β (πΉβ((π + 1) / 2)) = (πΉβ1)) |
215 | 207, 214 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) = (πΉβ1)) |
216 | | fvex 6859 |
. . . . . . . . . . . . . . 15
β’ (πΉβ1) β
V |
217 | 215, 17, 216 | fvmpt 6952 |
. . . . . . . . . . . . . 14
β’ (1 β
β β (π»β1)
= (πΉβ1)) |
218 | 132, 217 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (π»β1) = (πΉβ1) |
219 | 218 | fveq2i 6849 |
. . . . . . . . . . . 12
β’
(2nd β(π»β1)) = (2nd β(πΉβ1)) |
220 | 218 | fveq2i 6849 |
. . . . . . . . . . . 12
β’
(1st β(π»β1)) = (1st β(πΉβ1)) |
221 | 219, 220 | oveq12i 7373 |
. . . . . . . . . . 11
β’
((2nd β(π»β1)) β (1st
β(π»β1))) =
((2nd β(πΉβ1)) β (1st
β(πΉβ1))) |
222 | 200, 221 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π β (((abs β β )
β π»)β1) =
((2nd β(πΉβ1)) β (1st
β(πΉβ1)))) |
223 | 52, 222 | seq1i 13929 |
. . . . . . . . 9
β’ (π β (seq1( + , ((abs β
β ) β π»))β1) = ((2nd β(πΉβ1)) β
(1st β(πΉβ1)))) |
224 | | 2t1e2 12324 |
. . . . . . . . . . 11
β’ (2
Β· 1) = 2 |
225 | 224 | fveq2i 6849 |
. . . . . . . . . 10
β’ (((abs
β β ) β π»)β(2 Β· 1)) = (((abs β
β ) β π»)β2) |
226 | 19 | ovolfsval 24857 |
. . . . . . . . . . . 12
β’ ((π»:ββΆ( β€ β©
(β Γ β)) β§ 2 β β) β (((abs β
β ) β π»)β2) = ((2nd β(π»β2)) β
(1st β(π»β2)))) |
227 | 18, 27, 226 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β (((abs β β )
β π»)β2) =
((2nd β(π»β2)) β (1st
β(π»β2)))) |
228 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 2 β (π / 2) = (2 / 2)) |
229 | 228, 212 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 2 β (π / 2) = 1) |
230 | 229, 132 | eqeltrdi 2842 |
. . . . . . . . . . . . . . . . 17
β’ (π = 2 β (π / 2) β β) |
231 | 230 | iftrued 4498 |
. . . . . . . . . . . . . . . 16
β’ (π = 2 β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) = (πΊβ(π / 2))) |
232 | 229 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ (π = 2 β (πΊβ(π / 2)) = (πΊβ1)) |
233 | 231, 232 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (π = 2 β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) = (πΊβ1)) |
234 | | fvex 6859 |
. . . . . . . . . . . . . . 15
β’ (πΊβ1) β
V |
235 | 233, 17, 234 | fvmpt 6952 |
. . . . . . . . . . . . . 14
β’ (2 β
β β (π»β2)
= (πΊβ1)) |
236 | 27, 235 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (π»β2) = (πΊβ1) |
237 | 236 | fveq2i 6849 |
. . . . . . . . . . . 12
β’
(2nd β(π»β2)) = (2nd β(πΊβ1)) |
238 | 236 | fveq2i 6849 |
. . . . . . . . . . . 12
β’
(1st β(π»β2)) = (1st β(πΊβ1)) |
239 | 237, 238 | oveq12i 7373 |
. . . . . . . . . . 11
β’
((2nd β(π»β2)) β (1st
β(π»β2))) =
((2nd β(πΊβ1)) β (1st
β(πΊβ1))) |
240 | 227, 239 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π β (((abs β β )
β π»)β2) =
((2nd β(πΊβ1)) β (1st
β(πΊβ1)))) |
241 | 225, 240 | eqtrid 2785 |
. . . . . . . . 9
β’ (π β (((abs β β )
β π»)β(2
Β· 1)) = ((2nd β(πΊβ1)) β (1st
β(πΊβ1)))) |
242 | 72, 198, 34, 223, 241 | seqp1d 13932 |
. . . . . . . 8
β’ (π β (seq1( + , ((abs β
β ) β π»))β(2 Β· 1)) = (((2nd
β(πΉβ1)) β
(1st β(πΉβ1))) + ((2nd β(πΊβ1)) β
(1st β(πΊβ1))))) |
243 | 197, 242 | eqtrid 2785 |
. . . . . . 7
β’ (π β (πβ(2 Β· 1)) = (((2nd
β(πΉβ1)) β
(1st β(πΉβ1))) + ((2nd β(πΊβ1)) β
(1st β(πΊβ1))))) |
244 | 102 | fveq1i 6847 |
. . . . . . . . 9
β’ (πβ1) = (seq1( + , ((abs
β β ) β πΉ))β1) |
245 | 101 | ovolfsval 24857 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ 1 β β) β (((abs β
β ) β πΉ)β1) = ((2nd β(πΉβ1)) β
(1st β(πΉβ1)))) |
246 | 12, 132, 245 | sylancl 587 |
. . . . . . . . . 10
β’ (π β (((abs β β )
β πΉ)β1) =
((2nd β(πΉβ1)) β (1st
β(πΉβ1)))) |
247 | 52, 246 | seq1i 13929 |
. . . . . . . . 9
β’ (π β (seq1( + , ((abs β
β ) β πΉ))β1) = ((2nd β(πΉβ1)) β
(1st β(πΉβ1)))) |
248 | 244, 247 | eqtrid 2785 |
. . . . . . . 8
β’ (π β (πβ1) = ((2nd β(πΉβ1)) β
(1st β(πΉβ1)))) |
249 | 113 | fveq1i 6847 |
. . . . . . . . 9
β’ (πβ1) = (seq1( + , ((abs
β β ) β πΊ))β1) |
250 | 112 | ovolfsval 24857 |
. . . . . . . . . . 11
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ 1 β β) β (((abs β
β ) β πΊ)β1) = ((2nd β(πΊβ1)) β
(1st β(πΊβ1)))) |
251 | 3, 132, 250 | sylancl 587 |
. . . . . . . . . 10
β’ (π β (((abs β β )
β πΊ)β1) =
((2nd β(πΊβ1)) β (1st
β(πΊβ1)))) |
252 | 52, 251 | seq1i 13929 |
. . . . . . . . 9
β’ (π β (seq1( + , ((abs β
β ) β πΊ))β1) = ((2nd β(πΊβ1)) β
(1st β(πΊβ1)))) |
253 | 249, 252 | eqtrid 2785 |
. . . . . . . 8
β’ (π β (πβ1) = ((2nd β(πΊβ1)) β
(1st β(πΊβ1)))) |
254 | 248, 253 | oveq12d 7379 |
. . . . . . 7
β’ (π β ((πβ1) + (πβ1)) = (((2nd β(πΉβ1)) β
(1st β(πΉβ1))) + ((2nd β(πΊβ1)) β
(1st β(πΊβ1))))) |
255 | 243, 254 | eqtr4d 2776 |
. . . . . 6
β’ (π β (πβ(2 Β· 1)) = ((πβ1) + (πβ1))) |
256 | | oveq1 7368 |
. . . . . . . . 9
β’ ((πβ(2 Β· π)) = ((πβπ) + (πβπ)) β ((πβ(2 Β· π)) + ((((abs β β ) β πΉ)β(π + 1)) + (((abs β β ) β
πΊ)β(π + 1)))) = (((πβπ) + (πβπ)) + ((((abs β β ) β πΉ)β(π + 1)) + (((abs β β ) β
πΊ)β(π + 1))))) |
257 | 34 | oveq2i 7372 |
. . . . . . . . . . . . 13
β’ ((2
Β· π) + (2 Β·
1)) = ((2 Β· π) + (1
+ 1)) |
258 | | 2cnd 12239 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β 2 β
β) |
259 | 38 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
260 | | 1cnd 11158 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β 1 β
β) |
261 | 258, 259,
260 | adddid 11187 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (2 Β· (π + 1)) = ((2 Β· π) + (2 Β·
1))) |
262 | | nnmulcl 12185 |
. . . . . . . . . . . . . . . . 17
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
263 | 27, 262 | mpan 689 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (2
Β· π) β
β) |
264 | 263 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (2 Β· π) β
β) |
265 | 264 | nncnd 12177 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (2 Β· π) β
β) |
266 | 265, 260,
260 | addassd 11185 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (((2 Β· π) + 1) + 1) = ((2 Β· π) + (1 + 1))) |
267 | 257, 261,
266 | 3eqtr4a 2799 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (2 Β· (π + 1)) = (((2 Β· π) + 1) + 1)) |
268 | 267 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβ(2 Β· (π + 1))) = (πβ(((2 Β· π) + 1) + 1))) |
269 | 20 | fveq1i 6847 |
. . . . . . . . . . . 12
β’ (πβ(((2 Β· π) + 1) + 1)) = (seq1( + , ((abs
β β ) β π»))β(((2 Β· π) + 1) + 1)) |
270 | 264 | peano2nnd 12178 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((2 Β· π) + 1) β
β) |
271 | 270, 72 | eleqtrdi 2844 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((2 Β· π) + 1) β
(β€β₯β1)) |
272 | | seqp1 13930 |
. . . . . . . . . . . . . 14
β’ (((2
Β· π) + 1) β
(β€β₯β1) β (seq1( + , ((abs β β )
β π»))β(((2
Β· π) + 1) + 1)) =
((seq1( + , ((abs β β ) β π»))β((2 Β· π) + 1)) + (((abs β β ) β
π»)β(((2 Β·
π) + 1) +
1)))) |
273 | 271, 272 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β π»))β(((2 Β· π) + 1) + 1)) = ((seq1( + , ((abs β
β ) β π»))β((2 Β· π) + 1)) + (((abs β β ) β
π»)β(((2 Β·
π) + 1) +
1)))) |
274 | 264, 72 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (2 Β· π) β
(β€β₯β1)) |
275 | | seqp1 13930 |
. . . . . . . . . . . . . . . 16
β’ ((2
Β· π) β
(β€β₯β1) β (seq1( + , ((abs β β )
β π»))β((2
Β· π) + 1)) = ((seq1(
+ , ((abs β β ) β π»))β(2 Β· π)) + (((abs β β ) β π»)β((2 Β· π) + 1)))) |
276 | 274, 275 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β π»))β((2 Β· π) + 1)) = ((seq1( + , ((abs β β )
β π»))β(2
Β· π)) + (((abs
β β ) β π»)β((2 Β· π) + 1)))) |
277 | 20 | fveq1i 6847 |
. . . . . . . . . . . . . . . . 17
β’ (πβ(2 Β· π)) = (seq1( + , ((abs β
β ) β π»))β(2 Β· π)) |
278 | 277 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πβ(2 Β· π)) = (seq1( + , ((abs β β )
β π»))β(2
Β· π))) |
279 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ((2 Β· π) + 1) β (π / 2) = (((2 Β· π) + 1) / 2)) |
280 | 279 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ((2 Β· π) + 1) β ((π / 2) β β β (((2
Β· π) + 1) / 2)
β β)) |
281 | 279 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ((2 Β· π) + 1) β (πΊβ(π / 2)) = (πΊβ(((2 Β· π) + 1) / 2))) |
282 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ((2 Β· π) + 1) β (π + 1) = (((2 Β· π) + 1) + 1)) |
283 | 282 | fvoveq1d 7383 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ((2 Β· π) + 1) β (πΉβ((π + 1) / 2)) = (πΉβ((((2 Β· π) + 1) + 1) / 2))) |
284 | 280, 281,
283 | ifbieq12d 4518 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = ((2 Β· π) + 1) β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) = if((((2 Β· π) + 1) / 2) β β,
(πΊβ(((2 Β·
π) + 1) / 2)), (πΉβ((((2 Β· π) + 1) + 1) /
2)))) |
285 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΊβ(((2 Β· π) + 1) / 2)) β
V |
286 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΉβ((((2 Β· π) + 1) + 1) / 2)) β
V |
287 | 285, 286 | ifex 4540 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ if((((2
Β· π) + 1) / 2)
β β, (πΊβ(((2 Β· π) + 1) / 2)), (πΉβ((((2 Β· π) + 1) + 1) / 2))) β V |
288 | 284, 17, 287 | fvmpt 6952 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((2
Β· π) + 1) β
β β (π»β((2
Β· π) + 1)) = if((((2
Β· π) + 1) / 2)
β β, (πΊβ(((2 Β· π) + 1) / 2)), (πΉβ((((2 Β· π) + 1) + 1) / 2)))) |
289 | 270, 288 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (π»β((2 Β· π) + 1)) = if((((2 Β· π) + 1) / 2) β β, (πΊβ(((2 Β· π) + 1) / 2)), (πΉβ((((2 Β· π) + 1) + 1) / 2)))) |
290 | | 2ne0 12265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 2 β
0 |
291 | 290 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β 2 β
0) |
292 | 259, 258,
291 | divcan3d 11944 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β ((2 Β· π) / 2) = π) |
293 | 292, 71 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β ((2 Β· π) / 2) β
β) |
294 | | nneo 12595 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((2
Β· π) β β
β (((2 Β· π) /
2) β β β Β¬ (((2 Β· π) + 1) / 2) β β)) |
295 | 264, 294 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β (((2 Β· π) / 2) β β β
Β¬ (((2 Β· π) + 1)
/ 2) β β)) |
296 | 293, 295 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β Β¬ (((2 Β·
π) + 1) / 2) β
β) |
297 | 296 | iffalsed 4501 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β if((((2 Β·
π) + 1) / 2) β
β, (πΊβ(((2
Β· π) + 1) / 2)),
(πΉβ((((2 Β·
π) + 1) + 1) / 2))) =
(πΉβ((((2 Β·
π) + 1) + 1) /
2))) |
298 | 267 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β ((2 Β· (π + 1)) / 2) = ((((2 Β·
π) + 1) + 1) /
2)) |
299 | 29 | nncnd 12177 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β (π + 1) β β) |
300 | | 2cn 12236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 2 β
β |
301 | | divcan3 11847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π + 1) β β β§ 2
β β β§ 2 β 0) β ((2 Β· (π + 1)) / 2) = (π + 1)) |
302 | 300, 290,
301 | mp3an23 1454 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π + 1) β β β ((2
Β· (π + 1)) / 2) =
(π + 1)) |
303 | 299, 302 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β ((2 Β· (π + 1)) / 2) = (π + 1)) |
304 | 298, 303 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β ((((2 Β· π) + 1) + 1) / 2) = (π + 1)) |
305 | 304 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (πΉβ((((2 Β· π) + 1) + 1) / 2)) = (πΉβ(π + 1))) |
306 | 289, 297,
305 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (π»β((2 Β· π) + 1)) = (πΉβ(π + 1))) |
307 | 306 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (2nd
β(π»β((2
Β· π) + 1))) =
(2nd β(πΉβ(π + 1)))) |
308 | 306 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (1st
β(π»β((2
Β· π) + 1))) =
(1st β(πΉβ(π + 1)))) |
309 | 307, 308 | oveq12d 7379 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((2nd
β(π»β((2
Β· π) + 1))) β
(1st β(π»β((2 Β· π) + 1)))) = ((2nd β(πΉβ(π + 1))) β (1st β(πΉβ(π + 1))))) |
310 | 19 | ovolfsval 24857 |
. . . . . . . . . . . . . . . . . 18
β’ ((π»:ββΆ( β€ β©
(β Γ β)) β§ ((2 Β· π) + 1) β β) β (((abs β
β ) β π»)β((2 Β· π) + 1)) = ((2nd β(π»β((2 Β· π) + 1))) β (1st
β(π»β((2
Β· π) +
1))))) |
311 | 18, 270, 310 | syl2an2r 684 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (((abs β
β ) β π»)β((2 Β· π) + 1)) = ((2nd β(π»β((2 Β· π) + 1))) β (1st
β(π»β((2
Β· π) +
1))))) |
312 | 101 | ovolfsval 24857 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ (π + 1) β β) β (((abs β
β ) β πΉ)β(π + 1)) = ((2nd β(πΉβ(π + 1))) β (1st β(πΉβ(π + 1))))) |
313 | 12, 28, 312 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (((abs β
β ) β πΉ)β(π + 1)) = ((2nd β(πΉβ(π + 1))) β (1st β(πΉβ(π + 1))))) |
314 | 309, 311,
313 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (((abs β
β ) β πΉ)β(π + 1)) = (((abs β β ) β
π»)β((2 Β· π) + 1))) |
315 | 278, 314 | oveq12d 7379 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((πβ(2 Β· π)) + (((abs β β ) β πΉ)β(π + 1))) = ((seq1( + , ((abs β β )
β π»))β(2
Β· π)) + (((abs
β β ) β π»)β((2 Β· π) + 1)))) |
316 | 276, 315 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β π»))β((2 Β· π) + 1)) = ((πβ(2 Β· π)) + (((abs β β ) β πΉ)β(π + 1)))) |
317 | 267 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π»β(2 Β· (π + 1))) = (π»β(((2 Β· π) + 1) + 1))) |
318 | 270 | peano2nnd 12178 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β (((2 Β· π) + 1) + 1) β
β) |
319 | 267, 318 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (2 Β· (π + 1)) β
β) |
320 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (2 Β· (π + 1)) β (π / 2) = ((2 Β· (π + 1)) / 2)) |
321 | 320 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (2 Β· (π + 1)) β ((π / 2) β β β ((2
Β· (π + 1)) / 2)
β β)) |
322 | 320 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (2 Β· (π + 1)) β (πΊβ(π / 2)) = (πΊβ((2 Β· (π + 1)) / 2))) |
323 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (2 Β· (π + 1)) β (π + 1) = ((2 Β· (π + 1)) + 1)) |
324 | 323 | fvoveq1d 7383 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (2 Β· (π + 1)) β (πΉβ((π + 1) / 2)) = (πΉβ(((2 Β· (π + 1)) + 1) / 2))) |
325 | 321, 322,
324 | ifbieq12d 4518 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (2 Β· (π + 1)) β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) = if(((2 Β· (π + 1)) / 2) β β,
(πΊβ((2 Β·
(π + 1)) / 2)), (πΉβ(((2 Β· (π + 1)) + 1) /
2)))) |
326 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΊβ((2 Β· (π + 1)) / 2)) β
V |
327 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΉβ(((2 Β· (π + 1)) + 1) / 2)) β
V |
328 | 326, 327 | ifex 4540 |
. . . . . . . . . . . . . . . . . . . . 21
β’ if(((2
Β· (π + 1)) / 2)
β β, (πΊβ((2 Β· (π + 1)) / 2)), (πΉβ(((2 Β· (π + 1)) + 1) / 2))) β V |
329 | 325, 17, 328 | fvmpt 6952 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((2
Β· (π + 1)) β
β β (π»β(2
Β· (π + 1))) = if(((2
Β· (π + 1)) / 2)
β β, (πΊβ((2 Β· (π + 1)) / 2)), (πΉβ(((2 Β· (π + 1)) + 1) / 2)))) |
330 | 319, 329 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (π»β(2 Β· (π + 1))) = if(((2 Β· (π + 1)) / 2) β β, (πΊβ((2 Β· (π + 1)) / 2)), (πΉβ(((2 Β· (π + 1)) + 1) / 2)))) |
331 | 303, 29 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β ((2 Β· (π + 1)) / 2) β
β) |
332 | 331 | iftrued 4498 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β if(((2 Β·
(π + 1)) / 2) β
β, (πΊβ((2
Β· (π + 1)) / 2)),
(πΉβ(((2 Β·
(π + 1)) + 1) / 2))) =
(πΊβ((2 Β·
(π + 1)) /
2))) |
333 | 303 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (πΊβ((2 Β· (π + 1)) / 2)) = (πΊβ(π + 1))) |
334 | 330, 332,
333 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π»β(2 Β· (π + 1))) = (πΊβ(π + 1))) |
335 | 317, 334 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (π»β(((2 Β· π) + 1) + 1)) = (πΊβ(π + 1))) |
336 | 335 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (2nd
β(π»β(((2
Β· π) + 1) + 1))) =
(2nd β(πΊβ(π + 1)))) |
337 | 335 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (1st
β(π»β(((2
Β· π) + 1) + 1))) =
(1st β(πΊβ(π + 1)))) |
338 | 336, 337 | oveq12d 7379 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((2nd
β(π»β(((2
Β· π) + 1) + 1)))
β (1st β(π»β(((2 Β· π) + 1) + 1)))) = ((2nd
β(πΊβ(π + 1))) β (1st
β(πΊβ(π + 1))))) |
339 | 19 | ovolfsval 24857 |
. . . . . . . . . . . . . . . 16
β’ ((π»:ββΆ( β€ β©
(β Γ β)) β§ (((2 Β· π) + 1) + 1) β β) β (((abs
β β ) β π»)β(((2 Β· π) + 1) + 1)) = ((2nd β(π»β(((2 Β· π) + 1) + 1))) β
(1st β(π»β(((2 Β· π) + 1) + 1))))) |
340 | 18, 318, 339 | syl2an2r 684 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (((abs β
β ) β π»)β(((2 Β· π) + 1) + 1)) = ((2nd β(π»β(((2 Β· π) + 1) + 1))) β
(1st β(π»β(((2 Β· π) + 1) + 1))))) |
341 | 112 | ovolfsval 24857 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ (π + 1) β β) β (((abs β
β ) β πΊ)β(π + 1)) = ((2nd β(πΊβ(π + 1))) β (1st β(πΊβ(π + 1))))) |
342 | 3, 28, 341 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (((abs β
β ) β πΊ)β(π + 1)) = ((2nd β(πΊβ(π + 1))) β (1st β(πΊβ(π + 1))))) |
343 | 338, 340,
342 | 3eqtr4d 2783 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (((abs β
β ) β π»)β(((2 Β· π) + 1) + 1)) = (((abs β β )
β πΊ)β(π + 1))) |
344 | 316, 343 | oveq12d 7379 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((seq1( + , ((abs
β β ) β π»))β((2 Β· π) + 1)) + (((abs β β ) β
π»)β(((2 Β·
π) + 1) + 1))) = (((πβ(2 Β· π)) + (((abs β β )
β πΉ)β(π + 1))) + (((abs β β
) β πΊ)β(π + 1)))) |
345 | 273, 344 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β π»))β(((2 Β· π) + 1) + 1)) = (((πβ(2 Β· π)) + (((abs β β ) β πΉ)β(π + 1))) + (((abs β β ) β
πΊ)β(π + 1)))) |
346 | 269, 345 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβ(((2 Β· π) + 1) + 1)) = (((πβ(2 Β· π)) + (((abs β β ) β πΉ)β(π + 1))) + (((abs β β ) β
πΊ)β(π + 1)))) |
347 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . 15
β’ ((π:ββΆ(0[,)+β)
β§ (2 Β· π) β
β) β (πβ(2
Β· π)) β
(0[,)+β)) |
348 | 22, 263, 347 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πβ(2 Β· π)) β (0[,)+β)) |
349 | 23, 348 | sselid 3946 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβ(2 Β· π)) β β) |
350 | 349 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβ(2 Β· π)) β β) |
351 | 101 | ovolfsf 24858 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β ((abs β β ) β πΉ):ββΆ(0[,)+β)) |
352 | 12, 351 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((abs β β )
β πΉ):ββΆ(0[,)+β)) |
353 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . 15
β’ ((((abs
β β ) β πΉ):ββΆ(0[,)+β) β§ (π + 1) β β) β
(((abs β β ) β πΉ)β(π + 1)) β
(0[,)+β)) |
354 | 352, 28, 353 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (((abs β
β ) β πΉ)β(π + 1)) β
(0[,)+β)) |
355 | 23, 354 | sselid 3946 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (((abs β
β ) β πΉ)β(π + 1)) β β) |
356 | 355 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (((abs β
β ) β πΉ)β(π + 1)) β β) |
357 | 112 | ovolfsf 24858 |
. . . . . . . . . . . . . . . 16
β’ (πΊ:ββΆ( β€ β©
(β Γ β)) β ((abs β β ) β πΊ):ββΆ(0[,)+β)) |
358 | 3, 357 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((abs β β )
β πΊ):ββΆ(0[,)+β)) |
359 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . 15
β’ ((((abs
β β ) β πΊ):ββΆ(0[,)+β) β§ (π + 1) β β) β
(((abs β β ) β πΊ)β(π + 1)) β
(0[,)+β)) |
360 | 358, 28, 359 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (((abs β
β ) β πΊ)β(π + 1)) β
(0[,)+β)) |
361 | 23, 360 | sselid 3946 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (((abs β
β ) β πΊ)β(π + 1)) β β) |
362 | 361 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (((abs β
β ) β πΊ)β(π + 1)) β β) |
363 | 350, 356,
362 | addassd 11185 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((πβ(2 Β· π)) + (((abs β β ) β πΉ)β(π + 1))) + (((abs β β ) β
πΊ)β(π + 1))) = ((πβ(2 Β· π)) + ((((abs β β ) β πΉ)β(π + 1)) + (((abs β β ) β
πΊ)β(π + 1))))) |
364 | 268, 346,
363 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ(2 Β· (π + 1))) = ((πβ(2 Β· π)) + ((((abs β β ) β πΉ)β(π + 1)) + (((abs β β ) β
πΊ)β(π + 1))))) |
365 | | seqp1 13930 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β1) β (seq1( + , ((abs β β )
β πΉ))β(π + 1)) = ((seq1( + , ((abs
β β ) β πΉ))βπ) + (((abs β β ) β πΉ)β(π + 1)))) |
366 | 73, 365 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β πΉ))β(π + 1)) = ((seq1( + , ((abs β β )
β πΉ))βπ) + (((abs β β )
β πΉ)β(π + 1)))) |
367 | 102 | fveq1i 6847 |
. . . . . . . . . . . . 13
β’ (πβ(π + 1)) = (seq1( + , ((abs β β )
β πΉ))β(π + 1)) |
368 | 102 | fveq1i 6847 |
. . . . . . . . . . . . . 14
β’ (πβπ) = (seq1( + , ((abs β β )
β πΉ))βπ) |
369 | 368 | oveq1i 7371 |
. . . . . . . . . . . . 13
β’ ((πβπ) + (((abs β β ) β πΉ)β(π + 1))) = ((seq1( + , ((abs β β )
β πΉ))βπ) + (((abs β β )
β πΉ)β(π + 1))) |
370 | 366, 367,
369 | 3eqtr4g 2798 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβ(π + 1)) = ((πβπ) + (((abs β β ) β πΉ)β(π + 1)))) |
371 | | seqp1 13930 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β1) β (seq1( + , ((abs β β )
β πΊ))β(π + 1)) = ((seq1( + , ((abs
β β ) β πΊ))βπ) + (((abs β β ) β πΊ)β(π + 1)))) |
372 | 73, 371 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β πΊ))β(π + 1)) = ((seq1( + , ((abs β β )
β πΊ))βπ) + (((abs β β )
β πΊ)β(π + 1)))) |
373 | 113 | fveq1i 6847 |
. . . . . . . . . . . . 13
β’ (πβ(π + 1)) = (seq1( + , ((abs β β )
β πΊ))β(π + 1)) |
374 | 113 | fveq1i 6847 |
. . . . . . . . . . . . . 14
β’ (πβπ) = (seq1( + , ((abs β β )
β πΊ))βπ) |
375 | 374 | oveq1i 7371 |
. . . . . . . . . . . . 13
β’ ((πβπ) + (((abs β β ) β πΊ)β(π + 1))) = ((seq1( + , ((abs β β )
β πΊ))βπ) + (((abs β β )
β πΊ)β(π + 1))) |
376 | 372, 373,
375 | 3eqtr4g 2798 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβ(π + 1)) = ((πβπ) + (((abs β β ) β πΊ)β(π + 1)))) |
377 | 370, 376 | oveq12d 7379 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((πβ(π + 1)) + (πβ(π + 1))) = (((πβπ) + (((abs β β ) β πΉ)β(π + 1))) + ((πβπ) + (((abs β β ) β πΊ)β(π + 1))))) |
378 | 104 | ffvelcdmda 7039 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πβπ) β (0[,)+β)) |
379 | 23, 378 | sselid 3946 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβπ) β β) |
380 | 379 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβπ) β β) |
381 | 115 | ffvelcdmda 7039 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πβπ) β (0[,)+β)) |
382 | 23, 381 | sselid 3946 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβπ) β β) |
383 | 382 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβπ) β β) |
384 | 380, 356,
383, 362 | add4d 11391 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((πβπ) + (((abs β β ) β πΉ)β(π + 1))) + ((πβπ) + (((abs β β ) β πΊ)β(π + 1)))) = (((πβπ) + (πβπ)) + ((((abs β β ) β πΉ)β(π + 1)) + (((abs β β ) β
πΊ)β(π + 1))))) |
385 | 377, 384 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πβ(π + 1)) + (πβ(π + 1))) = (((πβπ) + (πβπ)) + ((((abs β β ) β πΉ)β(π + 1)) + (((abs β β ) β
πΊ)β(π + 1))))) |
386 | 364, 385 | eqeq12d 2749 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβ(2 Β· (π + 1))) = ((πβ(π + 1)) + (πβ(π + 1))) β ((πβ(2 Β· π)) + ((((abs β β ) β πΉ)β(π + 1)) + (((abs β β ) β
πΊ)β(π + 1)))) = (((πβπ) + (πβπ)) + ((((abs β β ) β πΉ)β(π + 1)) + (((abs β β ) β
πΊ)β(π + 1)))))) |
387 | 256, 386 | syl5ibr 246 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πβ(2 Β· π)) = ((πβπ) + (πβπ)) β (πβ(2 Β· (π + 1))) = ((πβ(π + 1)) + (πβ(π + 1))))) |
388 | 387 | expcom 415 |
. . . . . . 7
β’ (π β β β (π β ((πβ(2 Β· π)) = ((πβπ) + (πβπ)) β (πβ(2 Β· (π + 1))) = ((πβ(π + 1)) + (πβ(π + 1)))))) |
389 | 388 | a2d 29 |
. . . . . 6
β’ (π β β β ((π β (πβ(2 Β· π)) = ((πβπ) + (πβπ))) β (π β (πβ(2 Β· (π + 1))) = ((πβ(π + 1)) + (πβ(π + 1)))))) |
390 | 175, 182,
189, 196, 255, 389 | nnind 12179 |
. . . . 5
β’
((ββ((π
+ 1) / 2)) β β β (π β (πβ(2 Β· (ββ((π + 1) / 2)))) = ((πβ(ββ((π + 1) / 2))) + (πβ(ββ((π + 1) / 2)))))) |
391 | 390 | impcom 409 |
. . . 4
β’ ((π β§ (ββ((π + 1) / 2)) β β)
β (πβ(2 Β·
(ββ((π + 1) /
2)))) = ((πβ(ββ((π + 1) / 2))) + (πβ(ββ((π + 1) / 2))))) |
392 | 57, 391 | syldan 592 |
. . 3
β’ ((π β§ π β β) β (πβ(2 Β· (ββ((π + 1) / 2)))) = ((πβ(ββ((π + 1) / 2))) + (πβ(ββ((π + 1) / 2))))) |
393 | 63 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β (vol*βπ΄) β
β) |
394 | 393 | recnd 11191 |
. . . . 5
β’ ((π β§ π β β) β (vol*βπ΄) β
β) |
395 | 68 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β πΆ β β) |
396 | 395 | rehalfcld 12408 |
. . . . . 6
β’ ((π β§ π β β) β (πΆ / 2) β β) |
397 | 396 | recnd 11191 |
. . . . 5
β’ ((π β§ π β β) β (πΆ / 2) β β) |
398 | 65 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β (vol*βπ΅) β
β) |
399 | 398 | recnd 11191 |
. . . . 5
β’ ((π β§ π β β) β (vol*βπ΅) β
β) |
400 | 394, 397,
399, 397 | add4d 11391 |
. . . 4
β’ ((π β§ π β β) β (((vol*βπ΄) + (πΆ / 2)) + ((vol*βπ΅) + (πΆ / 2))) = (((vol*βπ΄) + (vol*βπ΅)) + ((πΆ / 2) + (πΆ / 2)))) |
401 | 395 | recnd 11191 |
. . . . . 6
β’ ((π β§ π β β) β πΆ β β) |
402 | 401 | 2halvesd 12407 |
. . . . 5
β’ ((π β§ π β β) β ((πΆ / 2) + (πΆ / 2)) = πΆ) |
403 | 402 | oveq2d 7377 |
. . . 4
β’ ((π β§ π β β) β (((vol*βπ΄) + (vol*βπ΅)) + ((πΆ / 2) + (πΆ / 2))) = (((vol*βπ΄) + (vol*βπ΅)) + πΆ)) |
404 | 400, 403 | eqtr2d 2774 |
. . 3
β’ ((π β§ π β β) β (((vol*βπ΄) + (vol*βπ΅)) + πΆ) = (((vol*βπ΄) + (πΆ / 2)) + ((vol*βπ΅) + (πΆ / 2)))) |
405 | 168, 392,
404 | 3brtr4d 5141 |
. 2
β’ ((π β§ π β β) β (πβ(2 Β· (ββ((π + 1) / 2)))) β€
(((vol*βπ΄) +
(vol*βπ΅)) + πΆ)) |
406 | 26, 61, 70, 100, 405 | letrd 11320 |
1
β’ ((π β§ π β β) β (πβπ) β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ)) |