Step | Hyp | Ref
| Expression |
1 | | ovolun.g1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
2 | | elovolmlem 23758 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
3 | 1, 2 | sylib 219 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
4 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
5 | 4 | ffvelrnda 6716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
6 | | nneo 11915 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔
¬ ((𝑛 + 1) / 2) ∈
ℕ)) |
7 | 6 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈
ℕ)) |
8 | 7 | con2bid 356 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈
ℕ)) |
9 | 8 | biimpar 478 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) →
((𝑛 + 1) / 2) ∈
ℕ) |
10 | | ovolun.f1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
11 | | elovolmlem 23758 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
12 | 10, 11 | sylib 219 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
13 | 12 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
14 | 13 | ffvelrnda 6716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ
× ℝ))) |
15 | 9, 14 | syldan 591 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) →
(𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩
(ℝ × ℝ))) |
16 | 5, 15 | ifclda 4415 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ
× ℝ))) |
17 | | ovolun.h |
. . . . . 6
⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2)))) |
18 | 16, 17 | fmptd 6741 |
. . . . 5
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
19 | | eqid 2795 |
. . . . . 6
⊢ ((abs
∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻) |
20 | | ovolun.u |
. . . . . 6
⊢ 𝑈 = seq1( + , ((abs ∘
− ) ∘ 𝐻)) |
21 | 19, 20 | ovolsf 23756 |
. . . . 5
⊢ (𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞)) |
22 | 18, 21 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞)) |
23 | | rge0ssre 12694 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ |
24 | | fss 6395 |
. . . 4
⊢ ((𝑈:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ) |
25 | 22, 23, 24 | sylancl 586 |
. . 3
⊢ (𝜑 → 𝑈:ℕ⟶ℝ) |
26 | 25 | ffvelrnda 6716 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ∈ ℝ) |
27 | | 2nn 11558 |
. . . 4
⊢ 2 ∈
ℕ |
28 | | peano2nn 11498 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
29 | 28 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) |
30 | 29 | nnred 11501 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ) |
31 | 30 | rehalfcld 11732 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ) |
32 | 31 | flcld 13018 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(⌊‘((𝑘 + 1) /
2)) ∈ ℤ) |
33 | | ax-1cn 10441 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
34 | 33 | 2timesi 11623 |
. . . . . . . 8
⊢ (2
· 1) = (1 + 1) |
35 | | nnge1 11513 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 1 ≤
𝑘) |
36 | 35 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘) |
37 | | nnre 11493 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
38 | 37 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ) |
39 | | 1re 10487 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
40 | | leadd1 10956 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 𝑘
∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1))) |
41 | 39, 39, 40 | mp3an13 1444 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℝ → (1 ≤
𝑘 ↔ (1 + 1) ≤
(𝑘 + 1))) |
42 | 38, 41 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1))) |
43 | 36, 42 | mpbid 233 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 + 1) ≤ (𝑘 + 1)) |
44 | 34, 43 | eqbrtrid 4997 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 1) ≤
(𝑘 + 1)) |
45 | | 2re 11559 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
46 | | 2pos 11588 |
. . . . . . . . . 10
⊢ 0 <
2 |
47 | 45, 46 | pm3.2i 471 |
. . . . . . . . 9
⊢ (2 ∈
ℝ ∧ 0 < 2) |
48 | | lemuldiv2 11369 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (𝑘 +
1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 ·
1) ≤ (𝑘 + 1) ↔ 1
≤ ((𝑘 + 1) /
2))) |
49 | 39, 47, 48 | mp3an13 1444 |
. . . . . . . 8
⊢ ((𝑘 + 1) ∈ ℝ → ((2
· 1) ≤ (𝑘 + 1)
↔ 1 ≤ ((𝑘 + 1) /
2))) |
50 | 30, 49 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 1) ≤
(𝑘 + 1) ↔ 1 ≤
((𝑘 + 1) /
2))) |
51 | 44, 50 | mpbid 233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤ ((𝑘 + 1) / 2)) |
52 | | 1z 11861 |
. . . . . . 7
⊢ 1 ∈
ℤ |
53 | | flge 13025 |
. . . . . . 7
⊢ ((((𝑘 + 1) / 2) ∈ ℝ ∧
1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤
(⌊‘((𝑘 + 1) /
2)))) |
54 | 31, 52, 53 | sylancl 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤
(⌊‘((𝑘 + 1) /
2)))) |
55 | 51, 54 | mpbid 233 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ≤
(⌊‘((𝑘 + 1) /
2))) |
56 | | elnnz1 11857 |
. . . . 5
⊢
((⌊‘((𝑘
+ 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤
(⌊‘((𝑘 + 1) /
2)))) |
57 | 32, 55, 56 | sylanbrc 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(⌊‘((𝑘 + 1) /
2)) ∈ ℕ) |
58 | | nnmulcl 11509 |
. . . 4
⊢ ((2
∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2
· (⌊‘((𝑘
+ 1) / 2))) ∈ ℕ) |
59 | 27, 57, 58 | sylancr 587 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 ·
(⌊‘((𝑘 + 1) /
2))) ∈ ℕ) |
60 | 25 | ffvelrnda 6716 |
. . 3
⊢ ((𝜑 ∧ (2 ·
(⌊‘((𝑘 + 1) /
2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈
ℝ) |
61 | 59, 60 | syldan 591 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈
ℝ) |
62 | | ovolun.a |
. . . . . 6
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈
ℝ)) |
63 | 62 | simprd 496 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐴) ∈
ℝ) |
64 | | ovolun.b |
. . . . . 6
⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈
ℝ)) |
65 | 64 | simprd 496 |
. . . . 5
⊢ (𝜑 → (vol*‘𝐵) ∈
ℝ) |
66 | 63, 65 | readdcld 10516 |
. . . 4
⊢ (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈
ℝ) |
67 | | ovolun.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
68 | 67 | rpred 12281 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
69 | 66, 68 | readdcld 10516 |
. . 3
⊢ (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ) |
70 | 69 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ) |
71 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
72 | | nnuz 12130 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
73 | 71, 72 | syl6eleq 2893 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
74 | | nnz 11853 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
75 | 74 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
76 | | flhalf 13050 |
. . . . . 6
⊢ (𝑘 ∈ ℤ → 𝑘 ≤ (2 ·
(⌊‘((𝑘 + 1) /
2)))) |
77 | 75, 76 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))) |
78 | | nnz 11853 |
. . . . . . 7
⊢ ((2
· (⌊‘((𝑘
+ 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈
ℤ) |
79 | | eluz 12107 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ (2
· (⌊‘((𝑘
+ 1) / 2))) ∈ ℤ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈
(ℤ≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))) |
80 | 74, 78, 79 | syl2an 595 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ (2
· (⌊‘((𝑘
+ 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈
(ℤ≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))) |
81 | 71, 59, 80 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 ·
(⌊‘((𝑘 + 1) /
2))) ∈ (ℤ≥‘𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))) |
82 | 77, 81 | mpbird 258 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 ·
(⌊‘((𝑘 + 1) /
2))) ∈ (ℤ≥‘𝑘)) |
83 | | elfznn 12786 |
. . . . 5
⊢ (𝑗 ∈ (1...(2 ·
(⌊‘((𝑘 + 1) /
2)))) → 𝑗 ∈
ℕ) |
84 | 19 | ovolfsf 23755 |
. . . . . . . . . 10
⊢ (𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞)) |
85 | 18, 84 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐻):ℕ⟶(0[,)+∞)) |
86 | 85 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
) ∘ 𝐻):ℕ⟶(0[,)+∞)) |
87 | 86 | ffvelrnda 6716 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞)) |
88 | | elrege0 12692 |
. . . . . . 7
⊢ ((((abs
∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs
∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐻)‘𝑗))) |
89 | 87, 88 | sylib 219 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘
− ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐻)‘𝑗))) |
90 | 89 | simpld 495 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘𝑗) ∈ ℝ) |
91 | 83, 90 | sylan2 592 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 ·
(⌊‘((𝑘 + 1) /
2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ) |
92 | | elfzuz 12754 |
. . . . . 6
⊢ (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) |
93 | | eluznn 12167 |
. . . . . 6
⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ) |
94 | 29, 92, 93 | syl2an 595 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈
ℕ) |
95 | 89 | simprd 496 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘
− ) ∘ 𝐻)‘𝑗)) |
96 | 94, 95 | syldan 591 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤
(((abs ∘ − ) ∘ 𝐻)‘𝑗)) |
97 | 73, 82, 91, 96 | sermono 13252 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − )
∘ 𝐻))‘(2
· (⌊‘((𝑘
+ 1) / 2))))) |
98 | 20 | fveq1i 6539 |
. . 3
⊢ (𝑈‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐻))‘𝑘) |
99 | 20 | fveq1i 6539 |
. . 3
⊢ (𝑈‘(2 ·
(⌊‘((𝑘 + 1) /
2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))) |
100 | 97, 98, 99 | 3brtr4g 4996 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2))))) |
101 | | eqid 2795 |
. . . . . . . . . 10
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
102 | | ovolun.s |
. . . . . . . . . 10
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
103 | 101, 102 | ovolsf 23756 |
. . . . . . . . 9
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
104 | 12, 103 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
105 | 104 | frnd 6389 |
. . . . . . 7
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
106 | 105, 23 | syl6ss 3901 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
107 | 106 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ) |
108 | 104 | ffnd 6383 |
. . . . . 6
⊢ (𝜑 → 𝑆 Fn ℕ) |
109 | | fnfvelrn 6713 |
. . . . . 6
⊢ ((𝑆 Fn ℕ ∧
(⌊‘((𝑘 + 1) /
2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) |
110 | 108, 57, 109 | syl2an2r 681 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) |
111 | 107, 110 | sseldd 3890 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ) |
112 | | eqid 2795 |
. . . . . . . . . 10
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
113 | | ovolun.t |
. . . . . . . . . 10
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) |
114 | 112, 113 | ovolsf 23756 |
. . . . . . . . 9
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞)) |
115 | 3, 114 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞)) |
116 | 115 | frnd 6389 |
. . . . . . 7
⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞)) |
117 | 116, 23 | syl6ss 3901 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
118 | 117 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ) |
119 | 115 | ffnd 6383 |
. . . . . 6
⊢ (𝜑 → 𝑇 Fn ℕ) |
120 | | fnfvelrn 6713 |
. . . . . 6
⊢ ((𝑇 Fn ℕ ∧
(⌊‘((𝑘 + 1) /
2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) |
121 | 119, 57, 120 | syl2an2r 681 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) |
122 | 118, 121 | sseldd 3890 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ) |
123 | 68 | rehalfcld 11732 |
. . . . . 6
⊢ (𝜑 → (𝐶 / 2) ∈ ℝ) |
124 | 63, 123 | readdcld 10516 |
. . . . 5
⊢ (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) |
125 | 124 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) |
126 | 65, 123 | readdcld 10516 |
. . . . 5
⊢ (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) |
127 | 126 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) |
128 | | ressxr 10531 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
129 | 106, 128 | syl6ss 3901 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
130 | | supxrcl 12558 |
. . . . . . . 8
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
131 | 129, 130 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
132 | | 1nn 11497 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
133 | 104 | fdmd 6391 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑆 = ℕ) |
134 | 132, 133 | syl5eleqr 2890 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈ dom 𝑆) |
135 | 134 | ne0d 4221 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑆 ≠ ∅) |
136 | | dm0rn0 5679 |
. . . . . . . . . 10
⊢ (dom
𝑆 = ∅ ↔ ran
𝑆 =
∅) |
137 | 136 | necon3bii 3036 |
. . . . . . . . 9
⊢ (dom
𝑆 ≠ ∅ ↔ ran
𝑆 ≠
∅) |
138 | 135, 137 | sylib 219 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑆 ≠ ∅) |
139 | | supxrgtmnf 12572 |
. . . . . . . 8
⊢ ((ran
𝑆 ⊆ ℝ ∧ ran
𝑆 ≠ ∅) →
-∞ < sup(ran 𝑆,
ℝ*, < )) |
140 | 106, 138,
139 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → -∞ < sup(ran
𝑆, ℝ*,
< )) |
141 | | ovolun.f3 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 / 2))) |
142 | | xrre 12412 |
. . . . . . 7
⊢
(((sup(ran 𝑆,
ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ <
sup(ran 𝑆,
ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ*, < )
∈ ℝ) |
143 | 131, 124,
140, 141, 142 | syl22anc 835 |
. . . . . 6
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ) |
144 | 143 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
∈ ℝ) |
145 | | supxrub 12567 |
. . . . . 6
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, <
)) |
146 | 129, 110,
145 | syl2an2r 681 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, <
)) |
147 | 141 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
≤ ((vol*‘𝐴) +
(𝐶 / 2))) |
148 | 111, 144,
125, 146, 147 | letrd 10644 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2))) |
149 | 117, 128 | syl6ss 3901 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
150 | | supxrcl 12558 |
. . . . . . . 8
⊢ (ran
𝑇 ⊆
ℝ* → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) |
151 | 149, 150 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) |
152 | 115 | fdmd 6391 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑇 = ℕ) |
153 | 132, 152 | syl5eleqr 2890 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈ dom 𝑇) |
154 | 153 | ne0d 4221 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑇 ≠ ∅) |
155 | | dm0rn0 5679 |
. . . . . . . . . 10
⊢ (dom
𝑇 = ∅ ↔ ran
𝑇 =
∅) |
156 | 155 | necon3bii 3036 |
. . . . . . . . 9
⊢ (dom
𝑇 ≠ ∅ ↔ ran
𝑇 ≠
∅) |
157 | 154, 156 | sylib 219 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑇 ≠ ∅) |
158 | | supxrgtmnf 12572 |
. . . . . . . 8
⊢ ((ran
𝑇 ⊆ ℝ ∧ ran
𝑇 ≠ ∅) →
-∞ < sup(ran 𝑇,
ℝ*, < )) |
159 | 117, 157,
158 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → -∞ < sup(ran
𝑇, ℝ*,
< )) |
160 | | ovolun.g3 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐵) + (𝐶 / 2))) |
161 | | xrre 12412 |
. . . . . . 7
⊢
(((sup(ran 𝑇,
ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ <
sup(ran 𝑇,
ℝ*, < ) ∧ sup(ran 𝑇, ℝ*, < ) ≤
((vol*‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ*, < )
∈ ℝ) |
162 | 151, 126,
159, 160, 161 | syl22anc 835 |
. . . . . 6
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
163 | 162 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < )
∈ ℝ) |
164 | | supxrub 12567 |
. . . . . 6
⊢ ((ran
𝑇 ⊆
ℝ* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, <
)) |
165 | 149, 121,
164 | syl2an2r 681 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, <
)) |
166 | 160 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < )
≤ ((vol*‘𝐵) +
(𝐶 / 2))) |
167 | 122, 163,
127, 165, 166 | letrd 10644 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2))) |
168 | 111, 122,
125, 127, 148, 167 | le2addd 11107 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2)))) |
169 | | oveq2 7024 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (2 · 𝑧) = (2 ·
1)) |
170 | 169 | fveq2d 6542 |
. . . . . . . 8
⊢ (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1))) |
171 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (𝑆‘𝑧) = (𝑆‘1)) |
172 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (𝑇‘𝑧) = (𝑇‘1)) |
173 | 171, 172 | oveq12d 7034 |
. . . . . . . 8
⊢ (𝑧 = 1 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘1) + (𝑇‘1))) |
174 | 170, 173 | eqeq12d 2810 |
. . . . . . 7
⊢ (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))) |
175 | 174 | imbi2d 342 |
. . . . . 6
⊢ (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))) |
176 | | oveq2 7024 |
. . . . . . . . 9
⊢ (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘)) |
177 | 176 | fveq2d 6542 |
. . . . . . . 8
⊢ (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘))) |
178 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑧 = 𝑘 → (𝑆‘𝑧) = (𝑆‘𝑘)) |
179 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑧 = 𝑘 → (𝑇‘𝑧) = (𝑇‘𝑘)) |
180 | 178, 179 | oveq12d 7034 |
. . . . . . . 8
⊢ (𝑧 = 𝑘 → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘𝑘) + (𝑇‘𝑘))) |
181 | 177, 180 | eqeq12d 2810 |
. . . . . . 7
⊢ (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)))) |
182 | 181 | imbi2d 342 |
. . . . . 6
⊢ (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))))) |
183 | | oveq2 7024 |
. . . . . . . . 9
⊢ (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1))) |
184 | 183 | fveq2d 6542 |
. . . . . . . 8
⊢ (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1)))) |
185 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑧 = (𝑘 + 1) → (𝑆‘𝑧) = (𝑆‘(𝑘 + 1))) |
186 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑧 = (𝑘 + 1) → (𝑇‘𝑧) = (𝑇‘(𝑘 + 1))) |
187 | 185, 186 | oveq12d 7034 |
. . . . . . . 8
⊢ (𝑧 = (𝑘 + 1) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))) |
188 | 184, 187 | eqeq12d 2810 |
. . . . . . 7
⊢ (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))) |
189 | 188 | imbi2d 342 |
. . . . . 6
⊢ (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))) |
190 | | oveq2 7024 |
. . . . . . . . 9
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 ·
𝑧) = (2 ·
(⌊‘((𝑘 + 1) /
2)))) |
191 | 190 | fveq2d 6542 |
. . . . . . . 8
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2))))) |
192 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆‘𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2)))) |
193 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇‘𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2)))) |
194 | 192, 193 | oveq12d 7034 |
. . . . . . . 8
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆‘𝑧) + (𝑇‘𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))) |
195 | 191, 194 | eqeq12d 2810 |
. . . . . . 7
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧)) ↔ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))) |
196 | 195 | imbi2d 342 |
. . . . . 6
⊢ (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆‘𝑧) + (𝑇‘𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) /
2))))))) |
197 | 20 | fveq1i 6539 |
. . . . . . . 8
⊢ (𝑈‘(2 · 1)) = (seq1(
+ , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) |
198 | 19 | ovolfsval 23754 |
. . . . . . . . . . . 12
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) −
(1st ‘(𝐻‘1)))) |
199 | 18, 132, 198 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘1) =
((2nd ‘(𝐻‘1)) − (1st
‘(𝐻‘1)))) |
200 | | halfnz 11909 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ (1
/ 2) ∈ ℤ |
201 | | nnz 11853 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 / 2) ∈ ℕ →
(𝑛 / 2) ∈
ℤ) |
202 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → (𝑛 / 2) = (1 / 2)) |
203 | 202 | eleq1d 2867 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈
ℤ)) |
204 | 201, 203 | syl5ib 245 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈
ℤ)) |
205 | 200, 204 | mtoi 200 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → ¬ (𝑛 / 2) ∈
ℕ) |
206 | 205 | iffalsed 4392 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2))) |
207 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → (𝑛 + 1) = (1 + 1)) |
208 | | df-2 11548 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 = (1 +
1) |
209 | 207, 208 | syl6eqr 2849 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → (𝑛 + 1) = 2) |
210 | 209 | oveq1d 7031 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2)) |
211 | | 2div2e1 11626 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 / 2) =
1 |
212 | 210, 211 | syl6eq 2847 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → ((𝑛 + 1) / 2) = 1) |
213 | 212 | fveq2d 6542 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1)) |
214 | 206, 213 | eqtrd 2831 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1)) |
215 | | fvex 6551 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘1) ∈
V |
216 | 214, 17, 215 | fvmpt 6635 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℕ → (𝐻‘1)
= (𝐹‘1)) |
217 | 132, 216 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐻‘1) = (𝐹‘1) |
218 | 217 | fveq2i 6541 |
. . . . . . . . . . . 12
⊢
(2nd ‘(𝐻‘1)) = (2nd ‘(𝐹‘1)) |
219 | 217 | fveq2i 6541 |
. . . . . . . . . . . 12
⊢
(1st ‘(𝐻‘1)) = (1st ‘(𝐹‘1)) |
220 | 218, 219 | oveq12i 7028 |
. . . . . . . . . . 11
⊢
((2nd ‘(𝐻‘1)) − (1st
‘(𝐻‘1))) =
((2nd ‘(𝐹‘1)) − (1st
‘(𝐹‘1))) |
221 | 199, 220 | syl6eq 2847 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘1) =
((2nd ‘(𝐹‘1)) − (1st
‘(𝐹‘1)))) |
222 | 52, 221 | seq1i 13233 |
. . . . . . . . 9
⊢ (𝜑 → (seq1( + , ((abs ∘
− ) ∘ 𝐻))‘1) = ((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1)))) |
223 | | 2t1e2 11648 |
. . . . . . . . . . 11
⊢ (2
· 1) = 2 |
224 | 223 | fveq2i 6541 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘
− ) ∘ 𝐻)‘2) |
225 | 19 | ovolfsval 23754 |
. . . . . . . . . . . 12
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) −
(1st ‘(𝐻‘2)))) |
226 | 18, 27, 225 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘2) =
((2nd ‘(𝐻‘2)) − (1st
‘(𝐻‘2)))) |
227 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 2 → (𝑛 / 2) = (2 / 2)) |
228 | 227, 211 | syl6eq 2847 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 2 → (𝑛 / 2) = 1) |
229 | 228, 132 | syl6eqel 2891 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 2 → (𝑛 / 2) ∈ ℕ) |
230 | 229 | iftrued 4389 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2))) |
231 | 228 | fveq2d 6542 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1)) |
232 | 230, 231 | eqtrd 2831 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1)) |
233 | | fvex 6551 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘1) ∈
V |
234 | 232, 17, 233 | fvmpt 6635 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℕ → (𝐻‘2)
= (𝐺‘1)) |
235 | 27, 234 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐻‘2) = (𝐺‘1) |
236 | 235 | fveq2i 6541 |
. . . . . . . . . . . 12
⊢
(2nd ‘(𝐻‘2)) = (2nd ‘(𝐺‘1)) |
237 | 235 | fveq2i 6541 |
. . . . . . . . . . . 12
⊢
(1st ‘(𝐻‘2)) = (1st ‘(𝐺‘1)) |
238 | 236, 237 | oveq12i 7028 |
. . . . . . . . . . 11
⊢
((2nd ‘(𝐻‘2)) − (1st
‘(𝐻‘2))) =
((2nd ‘(𝐺‘1)) − (1st
‘(𝐺‘1))) |
239 | 226, 238 | syl6eq 2847 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘2) =
((2nd ‘(𝐺‘1)) − (1st
‘(𝐺‘1)))) |
240 | 224, 239 | syl5eq 2843 |
. . . . . . . . 9
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐻)‘(2
· 1)) = ((2nd ‘(𝐺‘1)) − (1st
‘(𝐺‘1)))) |
241 | 72, 132, 34, 222, 240 | seqp1i 13236 |
. . . . . . . 8
⊢ (𝜑 → (seq1( + , ((abs ∘
− ) ∘ 𝐻))‘(2 · 1)) = (((2nd
‘(𝐹‘1)) −
(1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1))))) |
242 | 197, 241 | syl5eq 2843 |
. . . . . . 7
⊢ (𝜑 → (𝑈‘(2 · 1)) = (((2nd
‘(𝐹‘1)) −
(1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1))))) |
243 | 102 | fveq1i 6539 |
. . . . . . . . 9
⊢ (𝑆‘1) = (seq1( + , ((abs
∘ − ) ∘ 𝐹))‘1) |
244 | 101 | ovolfsval 23754 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1)))) |
245 | 12, 132, 244 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐹)‘1) =
((2nd ‘(𝐹‘1)) − (1st
‘(𝐹‘1)))) |
246 | 52, 245 | seq1i 13233 |
. . . . . . . . 9
⊢ (𝜑 → (seq1( + , ((abs ∘
− ) ∘ 𝐹))‘1) = ((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1)))) |
247 | 243, 246 | syl5eq 2843 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘1) = ((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1)))) |
248 | 113 | fveq1i 6539 |
. . . . . . . . 9
⊢ (𝑇‘1) = (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘1) |
249 | 112 | ovolfsval 23754 |
. . . . . . . . . . 11
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1)))) |
250 | 3, 132, 249 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs ∘ − )
∘ 𝐺)‘1) =
((2nd ‘(𝐺‘1)) − (1st
‘(𝐺‘1)))) |
251 | 52, 250 | seq1i 13233 |
. . . . . . . . 9
⊢ (𝜑 → (seq1( + , ((abs ∘
− ) ∘ 𝐺))‘1) = ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1)))) |
252 | 248, 251 | syl5eq 2843 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘1) = ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1)))) |
253 | 247, 252 | oveq12d 7034 |
. . . . . . 7
⊢ (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2nd ‘(𝐹‘1)) −
(1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) −
(1st ‘(𝐺‘1))))) |
254 | 242, 253 | eqtr4d 2834 |
. . . . . 6
⊢ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))) |
255 | | oveq1 7023 |
. . . . . . . . 9
⊢ ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
256 | 34 | oveq2i 7027 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑘) + (2 ·
1)) = ((2 · 𝑘) + (1
+ 1)) |
257 | | 2cnd 11563 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ∈
ℂ) |
258 | 38 | recnd 10515 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ) |
259 | | 1cnd 10482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 1 ∈
ℂ) |
260 | 257, 258,
259 | adddid 10511 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 ·
1))) |
261 | | nnmulcl 11509 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ) → (2 · 𝑘) ∈ ℕ) |
262 | 27, 261 | mpan 686 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) ∈
ℕ) |
263 | 262 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈
ℕ) |
264 | 263 | nncnd 11502 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈
ℂ) |
265 | 264, 259,
259 | addassd 10509 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1))) |
266 | 256, 260,
265 | 3eqtr4a 2857 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1)) |
267 | 266 | fveq2d 6542 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1))) |
268 | 20 | fveq1i 6539 |
. . . . . . . . . . . 12
⊢ (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) |
269 | 263 | peano2nnd 11503 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈
ℕ) |
270 | 269, 72 | syl6eleq 2893 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈
(ℤ≥‘1)) |
271 | | seqp1 13234 |
. . . . . . . . . . . . . 14
⊢ (((2
· 𝑘) + 1) ∈
(ℤ≥‘1) → (seq1( + , ((abs ∘ − )
∘ 𝐻))‘(((2
· 𝑘) + 1) + 1)) =
((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘
𝐻)‘(((2 ·
𝑘) + 1) +
1)))) |
272 | 270, 271 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘
− ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘
𝐻)‘(((2 ·
𝑘) + 1) +
1)))) |
273 | 263, 72 | syl6eleq 2893 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈
(ℤ≥‘1)) |
274 | | seqp1 13234 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑘) ∈
(ℤ≥‘1) → (seq1( + , ((abs ∘ − )
∘ 𝐻))‘((2
· 𝑘) + 1)) = ((seq1(
+ , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))) |
275 | 273, 274 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − )
∘ 𝐻))‘(2
· 𝑘)) + (((abs
∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))) |
276 | 20 | fveq1i 6539 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘
− ) ∘ 𝐻))‘(2 · 𝑘)) |
277 | 276 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − )
∘ 𝐻))‘(2
· 𝑘))) |
278 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2)) |
279 | 278 | eleq1d 2867 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2
· 𝑘) + 1) / 2)
∈ ℕ)) |
280 | 278 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2))) |
281 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1)) |
282 | 281 | fvoveq1d 7038 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) |
283 | 279, 280,
282 | ifbieq12d 4408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ,
(𝐺‘(((2 ·
𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) /
2)))) |
284 | | fvex 6551 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈
V |
285 | | fvex 6551 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈
V |
286 | 284, 285 | ifex 4429 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ if((((2
· 𝑘) + 1) / 2)
∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V |
287 | 283, 17, 286 | fvmpt 6635 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝑘) + 1) ∈
ℕ → (𝐻‘((2
· 𝑘) + 1)) = if((((2
· 𝑘) + 1) / 2)
∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))) |
288 | 269, 287 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))) |
289 | | 2ne0 11589 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ≠
0 |
290 | 289 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 2 ≠
0) |
291 | 258, 257,
290 | divcan3d 11269 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘) |
292 | 291, 71 | eqeltrd 2883 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈
ℕ) |
293 | | nneo 11915 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
· 𝑘) ∈ ℕ
→ (((2 · 𝑘) /
2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ)) |
294 | 263, 293 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) / 2) ∈ ℕ ↔
¬ (((2 · 𝑘) + 1)
/ 2) ∈ ℕ)) |
295 | 292, 294 | mpbid 233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ¬ (((2 ·
𝑘) + 1) / 2) ∈
ℕ) |
296 | 295 | iffalsed 4392 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if((((2 ·
𝑘) + 1) / 2) ∈
ℕ, (𝐺‘(((2
· 𝑘) + 1) / 2)),
(𝐹‘((((2 ·
𝑘) + 1) + 1) / 2))) =
(𝐹‘((((2 ·
𝑘) + 1) + 1) /
2))) |
297 | 266 | oveq1d 7031 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 ·
𝑘) + 1) + 1) /
2)) |
298 | 29 | nncnd 11502 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ) |
299 | | 2cn 11560 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℂ |
300 | | divcan3 11172 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑘 + 1) ∈ ℂ ∧ 2
∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1)) |
301 | 299, 289,
300 | mp3an23 1445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 + 1) ∈ ℂ → ((2
· (𝑘 + 1)) / 2) =
(𝑘 + 1)) |
302 | 298, 301 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1)) |
303 | 297, 302 | eqtr3d 2833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1)) |
304 | 303 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1))) |
305 | 288, 296,
304 | 3eqtrd 2835 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1))) |
306 | 305 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐻‘((2
· 𝑘) + 1))) =
(2nd ‘(𝐹‘(𝑘 + 1)))) |
307 | 305 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐻‘((2
· 𝑘) + 1))) =
(1st ‘(𝐹‘(𝑘 + 1)))) |
308 | 306, 307 | oveq12d 7034 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2nd
‘(𝐻‘((2
· 𝑘) + 1))) −
(1st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1))))) |
309 | 19 | ovolfsval 23754 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st
‘(𝐻‘((2
· 𝑘) +
1))))) |
310 | 18, 269, 309 | syl2an2r 681 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st
‘(𝐻‘((2
· 𝑘) +
1))))) |
311 | 101 | ovolfsval 23754 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1))))) |
312 | 12, 28, 311 | syl2an 595 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1))))) |
313 | 308, 310,
312 | 3eqtr4rd 2842 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘
𝐻)‘((2 · 𝑘) + 1))) |
314 | 277, 313 | oveq12d 7034 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − )
∘ 𝐻))‘(2
· 𝑘)) + (((abs
∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))) |
315 | 275, 314 | eqtr4d 2834 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))) |
316 | 266 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1))) |
317 | 269 | peano2nnd 11503 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈
ℕ) |
318 | 266, 317 | eqeltrd 2883 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈
ℕ) |
319 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2)) |
320 | 319 | eleq1d 2867 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2
· (𝑘 + 1)) / 2)
∈ ℕ)) |
321 | 319 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2))) |
322 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1)) |
323 | 322 | fvoveq1d 7038 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) |
324 | 320, 321,
323 | ifbieq12d 4408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ,
(𝐺‘((2 ·
(𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) /
2)))) |
325 | | fvex 6551 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈
V |
326 | | fvex 6551 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈
V |
327 | 325, 326 | ifex 4429 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ if(((2
· (𝑘 + 1)) / 2)
∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V |
328 | 324, 17, 327 | fvmpt 6635 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· (𝑘 + 1)) ∈
ℕ → (𝐻‘(2
· (𝑘 + 1))) = if(((2
· (𝑘 + 1)) / 2)
∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))) |
329 | 318, 328 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))) |
330 | 302, 29 | eqeltrd 2883 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈
ℕ) |
331 | 330 | iftrued 4389 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → if(((2 ·
(𝑘 + 1)) / 2) ∈
ℕ, (𝐺‘((2
· (𝑘 + 1)) / 2)),
(𝐹‘(((2 ·
(𝑘 + 1)) + 1) / 2))) =
(𝐺‘((2 ·
(𝑘 + 1)) /
2))) |
332 | 302 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1))) |
333 | 329, 331,
332 | 3eqtrd 2835 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1))) |
334 | 316, 333 | eqtr3d 2833 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1))) |
335 | 334 | fveq2d 6542 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐻‘(((2
· 𝑘) + 1) + 1))) =
(2nd ‘(𝐺‘(𝑘 + 1)))) |
336 | 334 | fveq2d 6542 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐻‘(((2
· 𝑘) + 1) + 1))) =
(1st ‘(𝐺‘(𝑘 + 1)))) |
337 | 335, 336 | oveq12d 7034 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2nd
‘(𝐻‘(((2
· 𝑘) + 1) + 1)))
− (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2nd
‘(𝐺‘(𝑘 + 1))) − (1st
‘(𝐺‘(𝑘 + 1))))) |
338 | 19 | ovolfsval 23754 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs
∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) −
(1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))))) |
339 | 18, 317, 338 | syl2an2r 681 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) −
(1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))))) |
340 | 112 | ovolfsval 23754 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1))))) |
341 | 3, 28, 340 | syl2an 595 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1))))) |
342 | 337, 339,
341 | 3eqtr4d 2841 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − )
∘ 𝐺)‘(𝑘 + 1))) |
343 | 315, 342 | oveq12d 7034 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , ((abs
∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘
𝐻)‘(((2 ·
𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − )
∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ −
) ∘ 𝐺)‘(𝑘 + 1)))) |
344 | 272, 343 | eqtrd 2831 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))) |
345 | 268, 344 | syl5eq 2843 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))) |
346 | | ffvelrn 6714 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈:ℕ⟶(0[,)+∞)
∧ (2 · 𝑘) ∈
ℕ) → (𝑈‘(2
· 𝑘)) ∈
(0[,)+∞)) |
347 | 22, 262, 346 | syl2an 595 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞)) |
348 | 23, 347 | sseldi 3887 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ) |
349 | 348 | recnd 10515 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ) |
350 | 101 | ovolfsf 23755 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞)) |
351 | 12, 350 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹):ℕ⟶(0[,)+∞)) |
352 | | ffvelrn 6714 |
. . . . . . . . . . . . . . 15
⊢ ((((abs
∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) →
(((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈
(0[,)+∞)) |
353 | 351, 28, 352 | syl2an 595 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) ∈
(0[,)+∞)) |
354 | 23, 353 | sseldi 3887 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ) |
355 | 354 | recnd 10515 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ) |
356 | 112 | ovolfsf 23755 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞)) |
357 | 3, 356 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐺):ℕ⟶(0[,)+∞)) |
358 | | ffvelrn 6714 |
. . . . . . . . . . . . . . 15
⊢ ((((abs
∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) →
(((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈
(0[,)+∞)) |
359 | 357, 28, 358 | syl2an 595 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) ∈
(0[,)+∞)) |
360 | 23, 359 | sseldi 3887 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ) |
361 | 360 | recnd 10515 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ) |
362 | 349, 355,
361 | addassd 10509 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
363 | 267, 345,
362 | 3eqtrd 2835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
364 | | seqp1 13234 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘1) → (seq1( + , ((abs ∘ − )
∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs
∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))) |
365 | 73, 364 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) + (((abs ∘ − )
∘ 𝐹)‘(𝑘 + 1)))) |
366 | 102 | fveq1i 6539 |
. . . . . . . . . . . . 13
⊢ (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘(𝑘 + 1)) |
367 | 102 | fveq1i 6539 |
. . . . . . . . . . . . . 14
⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) |
368 | 367 | oveq1i 7026 |
. . . . . . . . . . . . 13
⊢ ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) + (((abs ∘ − )
∘ 𝐹)‘(𝑘 + 1))) |
369 | 365, 366,
368 | 3eqtr4g 2856 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))) |
370 | | seqp1 13234 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘1) → (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs
∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) |
371 | 73, 370 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) + (((abs ∘ − )
∘ 𝐺)‘(𝑘 + 1)))) |
372 | 113 | fveq1i 6539 |
. . . . . . . . . . . . 13
⊢ (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘(𝑘 + 1)) |
373 | 113 | fveq1i 6539 |
. . . . . . . . . . . . . 14
⊢ (𝑇‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) |
374 | 373 | oveq1i 7026 |
. . . . . . . . . . . . 13
⊢ ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) + (((abs ∘ − )
∘ 𝐺)‘(𝑘 + 1))) |
375 | 371, 372,
374 | 3eqtr4g 2856 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) |
376 | 369, 375 | oveq12d 7034 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))) |
377 | 104 | ffvelrnda 6716 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ (0[,)+∞)) |
378 | 23, 377 | sseldi 3887 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ) |
379 | 378 | recnd 10515 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℂ) |
380 | 115 | ffvelrnda 6716 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ (0[,)+∞)) |
381 | 23, 380 | sseldi 3887 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℝ) |
382 | 381 | recnd 10515 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ∈ ℂ) |
383 | 379, 355,
382, 361 | add4d 10715 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝑆‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
384 | 376, 383 | eqtrd 2831 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1))))) |
385 | 363, 384 | eqeq12d 2810 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))) = (((𝑆‘𝑘) + (𝑇‘𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘
𝐺)‘(𝑘 + 1)))))) |
386 | 255, 385 | syl5ibr 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))) |
387 | 386 | expcom 414 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))) |
388 | 387 | a2d 29 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆‘𝑘) + (𝑇‘𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))) |
389 | 175, 182,
189, 196, 254, 388 | nnind 11504 |
. . . . 5
⊢
((⌊‘((𝑘
+ 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))) |
390 | 389 | impcom 408 |
. . . 4
⊢ ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
→ (𝑈‘(2 ·
(⌊‘((𝑘 + 1) /
2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))) |
391 | 57, 390 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))) |
392 | 63 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
393 | 392 | recnd 10515 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐴) ∈
ℂ) |
394 | 68 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℝ) |
395 | 394 | rehalfcld 11732 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ) |
396 | 395 | recnd 10515 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ) |
397 | 65 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈
ℝ) |
398 | 397 | recnd 10515 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (vol*‘𝐵) ∈
ℂ) |
399 | 393, 396,
398, 396 | add4d 10715 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2)))) |
400 | 394 | recnd 10515 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ) |
401 | 400 | 2halvesd 11731 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶) |
402 | 401 | oveq2d 7032 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |
403 | 399, 402 | eqtr2d 2832 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) = (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2)))) |
404 | 168, 391,
403 | 3brtr4d 4994 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤
(((vol*‘𝐴) +
(vol*‘𝐵)) + 𝐶)) |
405 | 26, 61, 70, 100, 404 | letrd 10644 |
1
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) |