Step | Hyp | Ref
| Expression |
1 | | ovolun.g1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
2 | | reex 9906 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
3 | 2, 2 | xpex 6860 |
. . . . . . . . . . . 12
⊢ (ℝ
× ℝ) ∈ V |
4 | 3 | inex2 4728 |
. . . . . . . . . . 11
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
5 | | nnex 10903 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
6 | 4, 5 | elmap 7772 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
7 | 1, 6 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
9 | 8 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
10 | | nneo 11337 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔
¬ ((𝑛 + 1) / 2) ∈
ℕ)) |
11 | 10 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈
ℕ)) |
12 | 11 | con2bid 343 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈
ℕ)) |
13 | 12 | biimpar 501 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) →
((𝑛 + 1) / 2) ∈
ℕ) |
14 | | ovolun.f1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
15 | 4, 5 | elmap 7772 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
16 | 14, 15 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
17 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
18 | 17 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ
× ℝ))) |
19 | 13, 18 | syldan 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) →
(𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩
(ℝ × ℝ))) |
20 | 9, 19 | ifclda 4070 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ
× ℝ))) |
21 | | ovolun.h |
. . . . . 6
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2)))) |
22 | 20, 21 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
23 | | eqid 2610 |
. . . . . 6
⊢ ((abs
∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻) |
24 | | ovolun.u |
. . . . . 6
⊢ 𝑈 = seq1( + , ((abs ∘
− ) ∘ 𝐻)) |
25 | 23, 24 | ovolsf 23048 |
. . . . 5
⊢ (𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞)) |
26 | 22, 25 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞)) |
27 | | rge0ssre 12151 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ |
28 | | fss 5969 |
. . . 4
⊢ ((𝑈:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ) |
29 | 26, 27, 28 | sylancl 693 |
. . 3
⊢ (𝜑 → 𝑈:ℕ⟶ℝ) |
30 | 29 | ffvelrnda 6267 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ∈ ℝ) |
31 | | 2nn 11062 |
. . . 4
⊢ 2 ∈
ℕ |
32 | | peano2nn 10909 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
33 | 32 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) |
34 | 33 | nnred 10912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ) |
35 | 34 | rehalfcld 11156 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ) |
36 | 35 | flcld 12461 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(⌊‘((𝑘 + 1) /
2)) ∈ ℤ) |
37 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
38 | 37 | 2timesi 11024 |
. . . . . . . 8
⊢ (2
· 1) = (1 + 1) |
39 | | nnge1 10923 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 1 ≤
𝑘) |
40 | 39 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘) |
41 | | nnre 10904 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
42 | 41 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ) |
43 | | 1re 9918 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
44 | | leadd1 10375 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 𝑘
∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1))) |
45 | 43, 43, 44 | mp3an13 1407 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℝ → (1 ≤
𝑘 ↔ (1 + 1) ≤
(𝑘 + 1))) |
46 | 42, 45 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1))) |
47 | 40, 46 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 + 1) ≤ (𝑘 + 1)) |
48 | 38, 47 | syl5eqbr 4618 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 1) ≤
(𝑘 + 1)) |
49 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
50 | | 2pos 10989 |
. . . . . . . . . 10
⊢ 0 <
2 |
51 | 49, 50 | pm3.2i 470 |
. . . . . . . . 9
⊢ (2 ∈
ℝ ∧ 0 < 2) |
52 | | lemuldiv2 10783 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (𝑘 +
1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 ·
1) ≤ (𝑘 + 1) ↔ 1
≤ ((𝑘 + 1) /
2))) |
53 | 43, 51, 52 | mp3an13 1407 |
. . . . . . . 8
⊢ ((𝑘 + 1) ∈ ℝ → ((2
· 1) ≤ (𝑘 + 1)
↔ 1 ≤ ((𝑘 + 1) /
2))) |
54 | 34, 53 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 1) ≤
(𝑘 + 1) ↔ 1 ≤
((𝑘 + 1) /
2))) |
55 | 48, 54 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ ((𝑘 + 1) / 2)) |
56 | | 1z 11284 |
. . . . . . 7
⊢ 1 ∈
ℤ |
57 | | flge 12468 |
. . . . . . 7
⊢ ((((𝑘 + 1) / 2) ∈ ℝ ∧
1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤
(⌊‘((𝑘 + 1) /
2)))) |
58 | 35, 56, 57 | sylancl 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤
(⌊‘((𝑘 + 1) /
2)))) |
59 | 55, 58 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤
(⌊‘((𝑘 + 1) /
2))) |
60 | | elnnz1 11280 |
. . . . 5
⊢
((⌊‘((𝑘
+ 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤
(⌊‘((𝑘 + 1) /
2)))) |
61 | 36, 59, 60 | sylanbrc 695 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(⌊‘((𝑘 + 1) /
2)) ∈ ℕ) |
62 | | nnmulcl 10920 |
. . . 4
⊢ ((2
∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2
· (⌊‘((𝑘
+ 1) / 2))) ∈ ℕ) |
63 | 31, 61, 62 | sylancr 694 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 ·
(⌊‘((𝑘 + 1) /
2))) ∈ ℕ) |
64 | 29 | ffvelrnda 6267 |
. . 3
⊢ ((𝜑 ∧ (2 ·
(⌊‘((𝑘 + 1) /
2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈
ℝ) |
65 | 63, 64 | syldan 486 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈
ℝ) |
66 | | ovolun.a |
. . . . . 6
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈
ℝ)) |
67 | 66 | simprd 478 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐴) ∈
ℝ) |
68 | | ovolun.b |
. . . . . 6
⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈
ℝ)) |
69 | 68 | simprd 478 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐵) ∈
ℝ) |
70 | 67, 69 | readdcld 9948 |
. . . 4
⊢ (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈
ℝ) |
71 | | ovolun.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
72 | 71 | rpred 11748 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
73 | 70, 72 | readdcld 9948 |
. . 3
⊢ (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ) |
74 | 73 | adantr 480 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ) |
75 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
76 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
77 | 75, 76 | syl6eleq 2698 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
78 | | nnz 11276 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
79 | 78 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
80 | | flhalf 12493 |
. . . . . 6
⊢ (𝑘 ∈ ℤ → 𝑘 ≤ (2 ·
(⌊‘((𝑘 + 1) /
2)))) |
81 | 79, 80 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))) |
82 | | nnz 11276 |
. . . . . . 7
⊢ ((2
· (⌊‘((𝑘
+ 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈
ℤ) |
83 | | eluz 11577 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ (2
· (⌊‘((𝑘
+ 1) / 2))) ∈ ℤ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈
(ℤ≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))) |
84 | 78, 82, 83 | syl2an 493 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ (2
· (⌊‘((𝑘
+ 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈
(ℤ≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))) |
85 | 75, 63, 84 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 ·
(⌊‘((𝑘 + 1) /
2))) ∈ (ℤ≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))) |
86 | 81, 85 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 ·
(⌊‘((𝑘 + 1) /
2))) ∈ (ℤ≥‘𝑘)) |
87 | | elfznn 12241 |
. . . . 5
⊢ (𝑗 ∈ (1...(2 ·
(⌊‘((𝑘 + 1) /
2)))) → 𝑗 ∈
ℕ) |
88 | 23 | ovolfsf 23047 |
. . . . . . . . . 10
⊢ (𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞)) |
89 | 22, 88 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐻):ℕ⟶(0[,)+∞)) |
90 | 89 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
) ∘ 𝐻):ℕ⟶(0[,)+∞)) |
91 | 90 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞)) |
92 | | elrege0 12149 |
. . . . . . 7
⊢ ((((abs
∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs
∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐻)‘𝑗))) |
93 | 91, 92 | sylib 207 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘
− ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐻)‘𝑗))) |
94 | 93 | simpld 474 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘𝑗) ∈ ℝ) |
95 | 87, 94 | sylan2 490 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 ·
(⌊‘((𝑘 + 1) /
2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ) |
96 | | elfzuz 12209 |
. . . . . 6
⊢ (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) |
97 | | eluznn 11634 |
. . . . . 6
⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ) |
98 | 33, 96, 97 | syl2an 493 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈
ℕ) |
99 | 93 | simprd 478 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘
− ) ∘ 𝐻)‘𝑗)) |
100 | 98, 99 | syldan 486 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤
(((abs ∘ − ) ∘ 𝐻)‘𝑗)) |
101 | 77, 86, 95, 100 | sermono 12695 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − )
∘ 𝐻))‘(2
· (⌊‘((𝑘
+ 1) / 2))))) |
102 | 24 | fveq1i 6104 |
. . 3
⊢ (𝑈‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐻))‘𝑘) |
103 | 24 | fveq1i 6104 |
. . 3
⊢ (𝑈‘(2 ·
(⌊‘((𝑘 + 1) /
2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))) |
104 | 101, 102,
103 | 3brtr4g 4617 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2))))) |
105 | | eqid 2610 |
. . . . . . . . . 10
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
106 | | ovolun.s |
. . . . . . . . . 10
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
107 | 105, 106 | ovolsf 23048 |
. . . . . . . . 9
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
108 | 16, 107 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
109 | | frn 5966 |
. . . . . . . 8
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ ran 𝑆 ⊆
(0[,)+∞)) |
110 | 108, 109 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
111 | 110, 27 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
112 | 111 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ) |
113 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ 𝑆 Fn
ℕ) |
114 | 108, 113 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 Fn ℕ) |
115 | 114 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑆 Fn ℕ) |
116 | | fnfvelrn 6264 |
. . . . . 6
⊢ ((𝑆 Fn ℕ ∧
(⌊‘((𝑘 + 1) /
2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) |
117 | 115, 61, 116 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) |
118 | 112, 117 | sseldd 3569 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ) |
119 | | eqid 2610 |
. . . . . . . . . 10
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
120 | | ovolun.t |
. . . . . . . . . 10
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
121 | 119, 120 | ovolsf 23048 |
. . . . . . . . 9
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞)) |
122 | 7, 121 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞)) |
123 | | frn 5966 |
. . . . . . . 8
⊢ (𝑇:ℕ⟶(0[,)+∞)
→ ran 𝑇 ⊆
(0[,)+∞)) |
124 | 122, 123 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞)) |
125 | 124, 27 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
126 | 125 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ) |
127 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑇:ℕ⟶(0[,)+∞)
→ 𝑇 Fn
ℕ) |
128 | 122, 127 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 Fn ℕ) |
129 | 128 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑇 Fn ℕ) |
130 | | fnfvelrn 6264 |
. . . . . 6
⊢ ((𝑇 Fn ℕ ∧
(⌊‘((𝑘 + 1) /
2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) |
131 | 129, 61, 130 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) |
132 | 126, 131 | sseldd 3569 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ) |
133 | 72 | rehalfcld 11156 |
. . . . . 6
⊢ (𝜑 → (𝐶 / 2) ∈ ℝ) |
134 | 67, 133 | readdcld 9948 |
. . . . 5
⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) |
135 | 134 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) |
136 | 69, 133 | readdcld 9948 |
. . . . 5
⊢ (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) |
137 | 136 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) |
138 | | ressxr 9962 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
139 | 111, 138 | syl6ss 3580 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
140 | | supxrcl 12017 |
. . . . . . . 8
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
141 | 139, 140 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
142 | | 1nn 10908 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
143 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ dom 𝑆 =
ℕ) |
144 | 108, 143 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑆 = ℕ) |
145 | 142, 144 | syl5eleqr 2695 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈ dom 𝑆) |
146 | | ne0i 3880 |
. . . . . . . . . 10
⊢ (1 ∈
dom 𝑆 → dom 𝑆 ≠ ∅) |
147 | 145, 146 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑆 ≠ ∅) |
148 | | dm0rn0 5263 |
. . . . . . . . . 10
⊢ (dom
𝑆 = ∅ ↔ ran
𝑆 =
∅) |
149 | 148 | necon3bii 2834 |
. . . . . . . . 9
⊢ (dom
𝑆 ≠ ∅ ↔ ran
𝑆 ≠
∅) |
150 | 147, 149 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑆 ≠ ∅) |
151 | | supxrgtmnf 12031 |
. . . . . . . 8
⊢ ((ran
𝑆 ⊆ ℝ ∧ ran
𝑆 ≠ ∅) →
-∞ < sup(ran 𝑆,
ℝ*, < )) |
152 | 111, 150,
151 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → -∞ < sup(ran
𝑆, ℝ*,
< )) |
153 | | ovolun.f3 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 / 2))) |
154 | | xrre 11874 |
. . . . . . 7
⊢
(((sup(ran 𝑆,
ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ <
sup(ran 𝑆,
ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ*, < )
∈ ℝ) |
155 | 141, 134,
152, 153, 154 | syl22anc 1319 |
. . . . . 6
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ) |
156 | 155 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
∈ ℝ) |
157 | 139 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆
ℝ*) |
158 | | supxrub 12026 |
. . . . . 6
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, <
)) |
159 | 157, 117,
158 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, <
)) |
160 | 153 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
≤ ((vol*‘𝐴) +
(𝐶 / 2))) |
161 | 118, 156,
135, 159, 160 | letrd 10073 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2))) |
162 | 125, 138 | syl6ss 3580 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
163 | | supxrcl 12017 |
. . . . . . . 8
⊢ (ran
𝑇 ⊆
ℝ* → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) |
164 | 162, 163 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) |
165 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝑇:ℕ⟶(0[,)+∞)
→ dom 𝑇 =
ℕ) |
166 | 122, 165 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑇 = ℕ) |
167 | 142, 166 | syl5eleqr 2695 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈ dom 𝑇) |
168 | | ne0i 3880 |
. . . . . . . . . 10
⊢ (1 ∈
dom 𝑇 → dom 𝑇 ≠ ∅) |
169 | 167, 168 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑇 ≠ ∅) |
170 | | dm0rn0 5263 |
. . . . . . . . . 10
⊢ (dom
𝑇 = ∅ ↔ ran
𝑇 =
∅) |
171 | 170 | necon3bii 2834 |
. . . . . . . . 9
⊢ (dom
𝑇 ≠ ∅ ↔ ran
𝑇 ≠
∅) |
172 | 169, 171 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑇 ≠ ∅) |
173 | | supxrgtmnf 12031 |
. . . . . . . 8
⊢ ((ran
𝑇 ⊆ ℝ ∧ ran
𝑇 ≠ ∅) →
-∞ < sup(ran 𝑇,
ℝ*, < )) |
174 | 125, 172,
173 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → -∞ < sup(ran
𝑇, ℝ*,
< )) |
175 | | ovolun.g3 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐵) + (𝐶 / 2))) |
176 | | xrre 11874 |
. . . . . . 7
⊢
(((sup(ran 𝑇,
ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ <
sup(ran 𝑇,
ℝ*, < ) ∧ sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ*, < )
∈ ℝ) |
177 | 164, 136,
174, 175, 176 | syl22anc 1319 |
. . . . . 6
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
178 | 177 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < )
∈ ℝ) |
179 | 162 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑇 ⊆
ℝ*) |
180 | | supxrub 12026 |
. . . . . 6
⊢ ((ran
𝑇 ⊆
ℝ* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, <
)) |
181 | 179, 131,
180 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, <
)) |
182 | 175 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < )
≤ ((vol*‘𝐵) +
(𝐶 / 2))) |
183 | 132, 178,
137, 181, 182 | letrd 10073 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2))) |
184 | 118, 132,
135, 137, 161, 183 | le2addd 10525 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2)))) |
185 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (2 · 𝑧) = (2 ·
1)) |
186 | 185 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1))) |
187 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (𝑆‘𝑧) = (𝑆‘1)) |
188 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (𝑇‘𝑧) = (𝑇‘1)) |
189 | 187, 188 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑧 = 1 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘1) + (𝑇‘1))) |
190 | 186, 189 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))) |
191 | 190 | imbi2d 329 |
. . . . . 6
⊢ (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))) |
192 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘)) |
193 | 192 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘))) |
194 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 𝑘 → (𝑆‘𝑧) = (𝑆‘𝑘)) |
195 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 𝑘 → (𝑇‘𝑧) = (𝑇‘𝑘)) |
196 | 194, 195 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑧 = 𝑘 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘𝑘) + (𝑇‘𝑘))) |
197 | 193, 196 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))) |
198 | 197 | imbi2d 329 |
. . . . . 6
⊢ (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))))) |
199 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1))) |
200 | 199 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1)))) |
201 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = (𝑘 + 1) → (𝑆‘𝑧) = (𝑆‘(𝑘 + 1))) |
202 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = (𝑘 + 1) → (𝑇‘𝑧) = (𝑇‘(𝑘 + 1))) |
203 | 201, 202 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑧 = (𝑘 + 1) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))) |
204 | 200, 203 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))) |
205 | 204 | imbi2d 329 |
. . . . . 6
⊢ (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))) |
206 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 ·
𝑧) = (2 ·
(⌊‘((𝑘 + 1) /
2)))) |
207 | 206 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2))))) |
208 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆‘𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2)))) |
209 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇‘𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2)))) |
210 | 208, 209 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))) |
211 | 207, 210 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))) |
212 | 211 | imbi2d 329 |
. . . . . 6
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) /
2))))))) |
213 | 24 | fveq1i 6104 |
. . . . . . . 8
⊢ (𝑈‘(2 · 1)) = (seq1(
+ , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) |
214 | 23 | ovolfsval 23046 |
. . . . . . . . . . . 12
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) −
(1st ‘(𝐻‘1)))) |
215 | 22, 142, 214 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘1) =
((2nd ‘(𝐻‘1)) − (1st
‘(𝐻‘1)))) |
216 | | halfnz 11331 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ (1
/ 2) ∈ ℤ |
217 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 / 2) ∈ ℕ →
(𝑛 / 2) ∈
ℤ) |
218 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → (𝑛 / 2) = (1 / 2)) |
219 | 218 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈
ℤ)) |
220 | 217, 219 | syl5ib 233 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈
ℤ)) |
221 | 216, 220 | mtoi 189 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → ¬ (𝑛 / 2) ∈
ℕ) |
222 | 221 | iffalsed 4047 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2))) |
223 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → (𝑛 + 1) = (1 + 1)) |
224 | | df-2 10956 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 = (1 +
1) |
225 | 223, 224 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → (𝑛 + 1) = 2) |
226 | 225 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2)) |
227 | | 2div2e1 11027 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 / 2) =
1 |
228 | 226, 227 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = 1) |
229 | 228 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1)) |
230 | 222, 229 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1)) |
231 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘1) ∈
V |
232 | 230, 21, 231 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℕ → (𝐻‘1)
= (𝐹‘1)) |
233 | 142, 232 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐻‘1) = (𝐹‘1) |
234 | 233 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(2nd ‘(𝐻‘1)) = (2nd ‘(𝐹‘1)) |
235 | 233 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(1st ‘(𝐻‘1)) = (1st ‘(𝐹‘1)) |
236 | 234, 235 | oveq12i 6561 |
. . . . . . . . . . 11
⊢
((2nd ‘(𝐻‘1)) − (1st
‘(𝐻‘1))) =
((2nd ‘(𝐹‘1)) − (1st
‘(𝐹‘1))) |
237 | 215, 236 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘1) =
((2nd ‘(𝐹‘1)) − (1st
‘(𝐹‘1)))) |
238 | 56, 237 | seq1i 12677 |
. . . . . . . . 9
⊢ (𝜑 → (seq1( + , ((abs ∘
− ) ∘ 𝐻))‘1) = ((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1)))) |
239 | | 2t1e2 11053 |
. . . . . . . . . . 11
⊢ (2
· 1) = 2 |
240 | 239 | fveq2i 6106 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘
− ) ∘ 𝐻)‘2) |
241 | 23 | ovolfsval 23046 |
. . . . . . . . . . . 12
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) −
(1st ‘(𝐻‘2)))) |
242 | 22, 31, 241 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘2) =
((2nd ‘(𝐻‘2)) − (1st
‘(𝐻‘2)))) |
243 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 2 → (𝑛 / 2) = (2 / 2)) |
244 | 243, 227 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 2 → (𝑛 / 2) = 1) |
245 | 244, 142 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 2 → (𝑛 / 2) ∈ ℕ) |
246 | 245 | iftrued 4044 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2))) |
247 | 244 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1)) |
248 | 246, 247 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1)) |
249 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘1) ∈
V |
250 | 248, 21, 249 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℕ → (𝐻‘2)
= (𝐺‘1)) |
251 | 31, 250 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐻‘2) = (𝐺‘1) |
252 | 251 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(2nd ‘(𝐻‘2)) = (2nd ‘(𝐺‘1)) |
253 | 251 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(1st ‘(𝐻‘2)) = (1st ‘(𝐺‘1)) |
254 | 252, 253 | oveq12i 6561 |
. . . . . . . . . . 11
⊢
((2nd ‘(𝐻‘2)) − (1st
‘(𝐻‘2))) =
((2nd ‘(𝐺‘1)) − (1st
‘(𝐺‘1))) |
255 | 242, 254 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘2) =
((2nd ‘(𝐺‘1)) − (1st
‘(𝐺‘1)))) |
256 | 240, 255 | syl5eq 2656 |
. . . . . . . . 9
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘(2
· 1)) = ((2nd ‘(𝐺‘1)) − (1st
‘(𝐺‘1)))) |
257 | 76, 142, 38, 238, 256 | seqp1i 12679 |
. . . . . . . 8
⊢ (𝜑 → (seq1( + , ((abs ∘
− ) ∘ 𝐻))‘(2 · 1)) = (((2nd
‘(𝐹‘1)) −
(1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1))))) |
258 | 213, 257 | syl5eq 2656 |
. . . . . . 7
⊢ (𝜑 → (𝑈‘(2 · 1)) = (((2nd
‘(𝐹‘1)) −
(1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1))))) |
259 | 106 | fveq1i 6104 |
. . . . . . . . 9
⊢ (𝑆‘1) = (seq1( + , ((abs
∘ − ) ∘ 𝐹))‘1) |
260 | 105 | ovolfsval 23046 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1)))) |
261 | 16, 142, 260 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐹)‘1) =
((2nd ‘(𝐹‘1)) − (1st
‘(𝐹‘1)))) |
262 | 56, 261 | seq1i 12677 |
. . . . . . . . 9
⊢ (𝜑 → (seq1( + , ((abs ∘
− ) ∘ 𝐹))‘1) = ((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1)))) |
263 | 259, 262 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘1) = ((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1)))) |
264 | 120 | fveq1i 6104 |
. . . . . . . . 9
⊢ (𝑇‘1) = (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘1) |
265 | 119 | ovolfsval 23046 |
. . . . . . . . . . 11
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1)))) |
266 | 7, 142, 265 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐺)‘1) =
((2nd ‘(𝐺‘1)) − (1st
‘(𝐺‘1)))) |
267 | 56, 266 | seq1i 12677 |
. . . . . . . . 9
⊢ (𝜑 → (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘1) = ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1)))) |
268 | 264, 267 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘1) = ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1)))) |
269 | 263, 268 | oveq12d 6567 |
. . . . . . 7
⊢ (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1))))) |
270 | 258, 269 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))) |
271 | | oveq1 6556 |
. . . . . . . . 9
⊢ ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
272 | 38 | oveq2i 6560 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑘) + (2 ·
1)) = ((2 · 𝑘) + (1
+ 1)) |
273 | | 2cnd 10970 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ∈
ℂ) |
274 | 42 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ) |
275 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ∈
ℂ) |
276 | 273, 274,
275 | adddid 9943 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 ·
1))) |
277 | | nnmulcl 10920 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ) → (2 · 𝑘) ∈ ℕ) |
278 | 31, 277 | mpan 702 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℕ) |
279 | 278 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈
ℕ) |
280 | 279 | nncnd 10913 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈
ℂ) |
281 | 280, 275,
275 | addassd 9941 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1))) |
282 | 272, 276,
281 | 3eqtr4a 2670 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1)) |
283 | 282 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1))) |
284 | 24 | fveq1i 6104 |
. . . . . . . . . . . 12
⊢ (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) |
285 | 279 | peano2nnd 10914 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈
ℕ) |
286 | 285, 76 | syl6eleq 2698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈
(ℤ≥‘1)) |
287 | | seqp1 12678 |
. . . . . . . . . . . . . 14
⊢ (((2
· 𝑘) + 1) ∈
(ℤ≥‘1) → (seq1( + , ((abs ∘ − )
∘ 𝐻))‘(((2
· 𝑘) + 1) + 1)) =
((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘
𝐻)‘(((2 ·
𝑘) + 1) +
1)))) |
288 | 286, 287 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘
− ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘
𝐻)‘(((2 ·
𝑘) + 1) +
1)))) |
289 | 279, 76 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈
(ℤ≥‘1)) |
290 | | seqp1 12678 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑘) ∈
(ℤ≥‘1) → (seq1( + , ((abs ∘ − )
∘ 𝐻))‘((2
· 𝑘) + 1)) = ((seq1(
+ , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))) |
291 | 289, 290 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − )
∘ 𝐻))‘(2
· 𝑘)) + (((abs
∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))) |
292 | 24 | fveq1i 6104 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘
− ) ∘ 𝐻))‘(2 · 𝑘)) |
293 | 292 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − )
∘ 𝐻))‘(2
· 𝑘))) |
294 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2)) |
295 | 294 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2
· 𝑘) + 1) / 2)
∈ ℕ)) |
296 | 294 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2))) |
297 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1)) |
298 | 297 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 + 1) / 2) = ((((2 ·
𝑘) + 1) + 1) /
2)) |
299 | 298 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) |
300 | 295, 296,
299 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ,
(𝐺‘(((2 ·
𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) /
2)))) |
301 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈
V |
302 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈
V |
303 | 301, 302 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ if((((2
· 𝑘) + 1) / 2)
∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V |
304 | 300, 21, 303 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝑘) + 1) ∈
ℕ → (𝐻‘((2
· 𝑘) + 1)) = if((((2
· 𝑘) + 1) / 2)
∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))) |
305 | 285, 304 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))) |
306 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ≠
0 |
307 | 306 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ≠
0) |
308 | 274, 273,
307 | divcan3d 10685 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘) |
309 | 308, 75 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈
ℕ) |
310 | | nneo 11337 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
· 𝑘) ∈ ℕ
→ (((2 · 𝑘) /
2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ)) |
311 | 279, 310 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) / 2) ∈ ℕ ↔
¬ (((2 · 𝑘) + 1)
/ 2) ∈ ℕ)) |
312 | 309, 311 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ¬ (((2 ·
𝑘) + 1) / 2) ∈
ℕ) |
313 | 312 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((((2 ·
𝑘) + 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑘) + 1) / 2)),
(𝐹‘((((2 ·
𝑘) + 1) + 1) / 2))) =
(𝐹‘((((2 ·
𝑘) + 1) + 1) /
2))) |
314 | 282 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 ·
𝑘) + 1) + 1) /
2)) |
315 | 33 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ) |
316 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℂ |
317 | | divcan3 10590 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑘 + 1) ∈ ℂ ∧ 2
∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1)) |
318 | 316, 306,
317 | mp3an23 1408 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 + 1) ∈ ℂ → ((2
· (𝑘 + 1)) / 2) =
(𝑘 + 1)) |
319 | 315, 318 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1)) |
320 | 314, 319 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1)) |
321 | 320 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1))) |
322 | 305, 313,
321 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1))) |
323 | 322 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐻‘((2
· 𝑘) + 1))) =
(2nd ‘(𝐹‘(𝑘 + 1)))) |
324 | 322 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐻‘((2
· 𝑘) + 1))) =
(1st ‘(𝐹‘(𝑘 + 1)))) |
325 | 323, 324 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2nd
‘(𝐻‘((2
· 𝑘) + 1))) −
(1st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1))))) |
326 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
327 | 23 | ovolfsval 23046 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st
‘(𝐻‘((2
· 𝑘) +
1))))) |
328 | 326, 285,
327 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st
‘(𝐻‘((2
· 𝑘) +
1))))) |
329 | 105 | ovolfsval 23046 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1))))) |
330 | 16, 32, 329 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1))))) |
331 | 325, 328,
330 | 3eqtr4rd 2655 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘
𝐻)‘((2 · 𝑘) + 1))) |
332 | 293, 331 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − )
∘ 𝐻))‘(2
· 𝑘)) + (((abs
∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))) |
333 | 291, 332 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))) |
334 | 282 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1))) |
335 | 285 | peano2nnd 10914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈
ℕ) |
336 | 282, 335 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈
ℕ) |
337 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2)) |
338 | 337 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2
· (𝑘 + 1)) / 2)
∈ ℕ)) |
339 | 337 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2))) |
340 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1)) |
341 | 340 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 + 1) / 2) = (((2 ·
(𝑘 + 1)) + 1) /
2)) |
342 | 341 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) |
343 | 338, 339,
342 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ,
(𝐺‘((2 ·
(𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) /
2)))) |
344 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈
V |
345 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈
V |
346 | 344, 345 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ if(((2
· (𝑘 + 1)) / 2)
∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V |
347 | 343, 21, 346 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· (𝑘 + 1)) ∈
ℕ → (𝐻‘(2
· (𝑘 + 1))) = if(((2
· (𝑘 + 1)) / 2)
∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))) |
348 | 336, 347 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))) |
349 | 319, 33 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈
ℕ) |
350 | 349 | iftrued 4044 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(((2 ·
(𝑘 + 1)) / 2) ∈
ℕ, (𝐺‘((2
· (𝑘 + 1)) / 2)),
(𝐹‘(((2 ·
(𝑘 + 1)) + 1) / 2))) =
(𝐺‘((2 ·
(𝑘 + 1)) /
2))) |
351 | 319 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1))) |
352 | 348, 350,
351 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1))) |
353 | 334, 352 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1))) |
354 | 353 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐻‘(((2
· 𝑘) + 1) + 1))) =
(2nd ‘(𝐺‘(𝑘 + 1)))) |
355 | 353 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐻‘(((2
· 𝑘) + 1) + 1))) =
(1st ‘(𝐺‘(𝑘 + 1)))) |
356 | 354, 355 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2nd
‘(𝐻‘(((2
· 𝑘) + 1) + 1)))
− (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2nd
‘(𝐺‘(𝑘 + 1))) − (1st
‘(𝐺‘(𝑘 + 1))))) |
357 | 23 | ovolfsval 23046 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs
∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) −
(1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))))) |
358 | 326, 335,
357 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) −
(1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))))) |
359 | 119 | ovolfsval 23046 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1))))) |
360 | 7, 32, 359 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1))))) |
361 | 356, 358,
360 | 3eqtr4d 2654 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − )
∘ 𝐺)‘(𝑘 + 1))) |
362 | 333, 361 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , ((abs
∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘
𝐻)‘(((2 ·
𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − )
∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ −
) ∘ 𝐺)‘(𝑘 + 1)))) |
363 | 288, 362 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))) |
364 | 284, 363 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))) |
365 | | ffvelrn 6265 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈:ℕ⟶(0[,)+∞)
∧ (2 · 𝑘) ∈
ℕ) → (𝑈‘(2
· 𝑘)) ∈
(0[,)+∞)) |
366 | 26, 278, 365 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞)) |
367 | 27, 366 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ) |
368 | 367 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ) |
369 | 105 | ovolfsf 23047 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞)) |
370 | 16, 369 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹):ℕ⟶(0[,)+∞)) |
371 | | ffvelrn 6265 |
. . . . . . . . . . . . . . 15
⊢ ((((abs
∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) →
(((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈
(0[,)+∞)) |
372 | 370, 32, 371 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) ∈
(0[,)+∞)) |
373 | 27, 372 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ) |
374 | 373 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ) |
375 | 119 | ovolfsf 23047 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞)) |
376 | 7, 375 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐺):ℕ⟶(0[,)+∞)) |
377 | | ffvelrn 6265 |
. . . . . . . . . . . . . . 15
⊢ ((((abs
∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) →
(((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈
(0[,)+∞)) |
378 | 376, 32, 377 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) ∈
(0[,)+∞)) |
379 | 27, 378 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ) |
380 | 379 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ) |
381 | 368, 374,
380 | addassd 9941 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
382 | 283, 364,
381 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
383 | | seqp1 12678 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘1) → (seq1( + , ((abs ∘ − )
∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs
∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))) |
384 | 77, 383 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) + (((abs ∘ − )
∘ 𝐹)‘(𝑘 + 1)))) |
385 | 106 | fveq1i 6104 |
. . . . . . . . . . . . 13
⊢ (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘(𝑘 + 1)) |
386 | 106 | fveq1i 6104 |
. . . . . . . . . . . . . 14
⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) |
387 | 386 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢ ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) + (((abs ∘ − )
∘ 𝐹)‘(𝑘 + 1))) |
388 | 384, 385,
387 | 3eqtr4g 2669 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))) |
389 | | seqp1 12678 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘1) → (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs
∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) |
390 | 77, 389 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) + (((abs ∘ − )
∘ 𝐺)‘(𝑘 + 1)))) |
391 | 120 | fveq1i 6104 |
. . . . . . . . . . . . 13
⊢ (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑘 + 1)) |
392 | 120 | fveq1i 6104 |
. . . . . . . . . . . . . 14
⊢ (𝑇‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) |
393 | 392 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢ ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) + (((abs ∘ − )
∘ 𝐺)‘(𝑘 + 1))) |
394 | 390, 391,
393 | 3eqtr4g 2669 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) |
395 | 388, 394 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))) |
396 | 108 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ (0[,)+∞)) |
397 | 27, 396 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ) |
398 | 397 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℂ) |
399 | 122 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ (0[,)+∞)) |
400 | 27, 399 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℝ) |
401 | 400 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℂ) |
402 | 398, 374,
401, 380 | add4d 10143 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
403 | 395, 402 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
404 | 382, 403 | eqeq12d 2625 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))))) |
405 | 271, 404 | syl5ibr 235 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))) |
406 | 405 | expcom 450 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))) |
407 | 406 | a2d 29 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))) |
408 | 191, 198,
205, 212, 270, 407 | nnind 10915 |
. . . . 5
⊢
((⌊‘((𝑘
+ 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))) |
409 | 408 | impcom 445 |
. . . 4
⊢ ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
→ (𝑈‘(2 ·
(⌊‘((𝑘 + 1) /
2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))) |
410 | 61, 409 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))) |
411 | 67 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
412 | 411 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈
ℂ) |
413 | 72 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℝ) |
414 | 413 | rehalfcld 11156 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ) |
415 | 414 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ) |
416 | 69 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈
ℝ) |
417 | 416 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈
ℂ) |
418 | 412, 415,
417, 415 | add4d 10143 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2)))) |
419 | 413 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ) |
420 | 419 | 2halvesd 11155 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶) |
421 | 420 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |
422 | 418, 421 | eqtr2d 2645 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) = (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2)))) |
423 | 184, 410,
422 | 3brtr4d 4615 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤
(((vol*‘𝐴) +
(vol*‘𝐵)) + 𝐶)) |
424 | 30, 65, 74, 104, 423 | letrd 10073 |
1
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |