Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolunlem1a Structured version   Visualization version   GIF version

Theorem ovolunlem1a 24107
 Description: Lemma for ovolun 24110. (Contributed by Mario Carneiro, 7-May-2015.)
Hypotheses
Ref Expression
ovolun.a (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
ovolun.b (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
ovolun.c (𝜑𝐶 ∈ ℝ+)
ovolun.s 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovolun.t 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
ovolun.u 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
ovolun.f1 (𝜑𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
ovolun.f2 (𝜑𝐴 ran ((,) ∘ 𝐹))
ovolun.f3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
ovolun.g1 (𝜑𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
ovolun.g2 (𝜑𝐵 ran ((,) ∘ 𝐺))
ovolun.g3 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
ovolun.h 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
Assertion
Ref Expression
ovolunlem1a ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Distinct variable groups:   𝑘,𝑛,𝐶   𝑘,𝐹,𝑛   𝑘,𝐻   𝐴,𝑘,𝑛   𝐵,𝑘,𝑛   𝑆,𝑘   𝑇,𝑘   𝑘,𝐺,𝑛   𝜑,𝑘,𝑛   𝑈,𝑘
Allowed substitution hints:   𝑆(𝑛)   𝑇(𝑛)   𝑈(𝑛)   𝐻(𝑛)

Proof of Theorem ovolunlem1a
Dummy variables 𝑧 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovolun.g1 . . . . . . . . . 10 (𝜑𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
2 elovolmlem 24085 . . . . . . . . . 10 (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
31, 2sylib 221 . . . . . . . . 9 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
43adantr 484 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
54ffvelrnda 6828 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
6 nneo 12056 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
76adantl 485 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
87con2bid 358 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
98biimpar 481 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
10 ovolun.f1 . . . . . . . . . . 11 (𝜑𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
11 elovolmlem 24085 . . . . . . . . . . 11 (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1210, 11sylib 221 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1312adantr 484 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1413ffvelrnda 6828 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
159, 14syldan 594 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
165, 15ifclda 4459 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
17 ovolun.h . . . . . 6 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
1816, 17fmptd 6855 . . . . 5 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
19 eqid 2798 . . . . . 6 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
20 ovolun.u . . . . . 6 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
2119, 20ovolsf 24083 . . . . 5 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
2218, 21syl 17 . . . 4 (𝜑𝑈:ℕ⟶(0[,)+∞))
23 rge0ssre 12836 . . . 4 (0[,)+∞) ⊆ ℝ
24 fss 6501 . . . 4 ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
2522, 23, 24sylancl 589 . . 3 (𝜑𝑈:ℕ⟶ℝ)
2625ffvelrnda 6828 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ∈ ℝ)
27 2nn 11700 . . . 4 2 ∈ ℕ
28 peano2nn 11639 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
2928adantl 485 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
3029nnred 11642 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
3130rehalfcld 11874 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
3231flcld 13165 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
33 ax-1cn 10586 . . . . . . . . 9 1 ∈ ℂ
34332timesi 11765 . . . . . . . 8 (2 · 1) = (1 + 1)
35 nnge1 11655 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
3635adantl 485 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 1 ≤ 𝑘)
37 nnre 11634 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
3837adantl 485 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
39 1re 10632 . . . . . . . . . . 11 1 ∈ ℝ
40 leadd1 11099 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4139, 39, 40mp3an13 1449 . . . . . . . . . 10 (𝑘 ∈ ℝ → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4238, 41syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4336, 42mpbid 235 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (1 + 1) ≤ (𝑘 + 1))
4434, 43eqbrtrid 5065 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
45 2re 11701 . . . . . . . . . 10 2 ∈ ℝ
46 2pos 11730 . . . . . . . . . 10 0 < 2
4745, 46pm3.2i 474 . . . . . . . . 9 (2 ∈ ℝ ∧ 0 < 2)
48 lemuldiv2 11512 . . . . . . . . 9 ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
4939, 47, 48mp3an13 1449 . . . . . . . 8 ((𝑘 + 1) ∈ ℝ → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5030, 49syl 17 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5144, 50mpbid 235 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 1 ≤ ((𝑘 + 1) / 2))
52 1z 12002 . . . . . . 7 1 ∈ ℤ
53 flge 13172 . . . . . . 7 ((((𝑘 + 1) / 2) ∈ ℝ ∧ 1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5431, 52, 53sylancl 589 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5551, 54mpbid 235 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 1 ≤ (⌊‘((𝑘 + 1) / 2)))
56 elnnz1 11998 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5732, 55, 56sylanbrc 586 . . . 4 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
58 nnmulcl 11651 . . . 4 ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
5927, 57, 58sylancr 590 . . 3 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
6025ffvelrnda 6828 . . 3 ((𝜑 ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
6159, 60syldan 594 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
62 ovolun.a . . . . . 6 (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
6362simprd 499 . . . . 5 (𝜑 → (vol*‘𝐴) ∈ ℝ)
64 ovolun.b . . . . . 6 (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
6564simprd 499 . . . . 5 (𝜑 → (vol*‘𝐵) ∈ ℝ)
6663, 65readdcld 10661 . . . 4 (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ)
67 ovolun.c . . . . 5 (𝜑𝐶 ∈ ℝ+)
6867rpred 12421 . . . 4 (𝜑𝐶 ∈ ℝ)
6966, 68readdcld 10661 . . 3 (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
7069adantr 484 . 2 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
71 simpr 488 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
72 nnuz 12271 . . . . 5 ℕ = (ℤ‘1)
7371, 72eleqtrdi 2900 . . . 4 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
74 nnz 11994 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
7574adantl 485 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
76 flhalf 13197 . . . . . 6 (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
7775, 76syl 17 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
78 nnz 11994 . . . . . . 7 ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ)
79 eluz 12247 . . . . . . 7 ((𝑘 ∈ ℤ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8074, 78, 79syl2an 598 . . . . . 6 ((𝑘 ∈ ℕ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8171, 59, 80syl2anc 587 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8277, 81mpbird 260 . . . 4 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘))
83 elfznn 12933 . . . . 5 (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
8419ovolfsf 24082 . . . . . . . . . 10 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8518, 84syl 17 . . . . . . . . 9 (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8685adantr 484 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8786ffvelrnda 6828 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
88 elrege0 12834 . . . . . . 7 ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
8987, 88sylib 221 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
9089simpld 498 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
9183, 90sylan2 595 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
92 elfzuz 12900 . . . . . 6 (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ‘(𝑘 + 1)))
93 eluznn 12308 . . . . . 6 (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
9429, 92, 93syl2an 598 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈ ℕ)
9589simprd 499 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
9694, 95syldan 594 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
9773, 82, 91, 96sermono 13400 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
9820fveq1i 6646 . . 3 (𝑈𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
9920fveq1i 6646 . . 3 (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
10097, 98, 993brtr4g 5064 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
101 eqid 2798 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
102 ovolun.s . . . . . . . . . 10 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
103101, 102ovolsf 24083 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
10412, 103syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
105104frnd 6494 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
106105, 23sstrdi 3927 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
107106adantr 484 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
108104ffnd 6488 . . . . . 6 (𝜑𝑆 Fn ℕ)
109 fnfvelrn 6825 . . . . . 6 ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
110108, 57, 109syl2an2r 684 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
111107, 110sseldd 3916 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
112 eqid 2798 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
113 ovolun.t . . . . . . . . . 10 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
114112, 113ovolsf 24083 . . . . . . . . 9 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
1153, 114syl 17 . . . . . . . 8 (𝜑𝑇:ℕ⟶(0[,)+∞))
116115frnd 6494 . . . . . . 7 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
117116, 23sstrdi 3927 . . . . . 6 (𝜑 → ran 𝑇 ⊆ ℝ)
118117adantr 484 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
119115ffnd 6488 . . . . . 6 (𝜑𝑇 Fn ℕ)
120 fnfvelrn 6825 . . . . . 6 ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
121119, 57, 120syl2an2r 684 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
122118, 121sseldd 3916 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
12368rehalfcld 11874 . . . . . 6 (𝜑 → (𝐶 / 2) ∈ ℝ)
12463, 123readdcld 10661 . . . . 5 (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
125124adantr 484 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
12665, 123readdcld 10661 . . . . 5 (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
127126adantr 484 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
128 ressxr 10676 . . . . . . . . 9 ℝ ⊆ ℝ*
129106, 128sstrdi 3927 . . . . . . . 8 (𝜑 → ran 𝑆 ⊆ ℝ*)
130 supxrcl 12698 . . . . . . . 8 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
131129, 130syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
132 1nn 11638 . . . . . . . . . . 11 1 ∈ ℕ
133104fdmd 6497 . . . . . . . . . . 11 (𝜑 → dom 𝑆 = ℕ)
134132, 133eleqtrrid 2897 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑆)
135134ne0d 4251 . . . . . . . . 9 (𝜑 → dom 𝑆 ≠ ∅)
136 dm0rn0 5759 . . . . . . . . . 10 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
137136necon3bii 3039 . . . . . . . . 9 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
138135, 137sylib 221 . . . . . . . 8 (𝜑 → ran 𝑆 ≠ ∅)
139 supxrgtmnf 12712 . . . . . . . 8 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ*, < ))
140106, 138, 139syl2anc 587 . . . . . . 7 (𝜑 → -∞ < sup(ran 𝑆, ℝ*, < ))
141 ovolun.f3 . . . . . . 7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
142 xrre 12552 . . . . . . 7 (((sup(ran 𝑆, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
143131, 124, 140, 141, 142syl22anc 837 . . . . . 6 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
144143adantr 484 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
145 supxrub 12707 . . . . . 6 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
146129, 110, 145syl2an2r 684 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
147141adantr 484 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
148111, 144, 125, 146, 147letrd 10788 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
149117, 128sstrdi 3927 . . . . . . . 8 (𝜑 → ran 𝑇 ⊆ ℝ*)
150 supxrcl 12698 . . . . . . . 8 (ran 𝑇 ⊆ ℝ* → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
151149, 150syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
152115fdmd 6497 . . . . . . . . . . 11 (𝜑 → dom 𝑇 = ℕ)
153132, 152eleqtrrid 2897 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑇)
154153ne0d 4251 . . . . . . . . 9 (𝜑 → dom 𝑇 ≠ ∅)
155 dm0rn0 5759 . . . . . . . . . 10 (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
156155necon3bii 3039 . . . . . . . . 9 (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
157154, 156sylib 221 . . . . . . . 8 (𝜑 → ran 𝑇 ≠ ∅)
158 supxrgtmnf 12712 . . . . . . . 8 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ*, < ))
159117, 157, 158syl2anc 587 . . . . . . 7 (𝜑 → -∞ < sup(ran 𝑇, ℝ*, < ))
160 ovolun.g3 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
161 xrre 12552 . . . . . . 7 (((sup(ran 𝑇, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
162151, 126, 159, 160, 161syl22anc 837 . . . . . 6 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
163162adantr 484 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
164 supxrub 12707 . . . . . 6 ((ran 𝑇 ⊆ ℝ* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
165149, 121, 164syl2an2r 684 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
166160adantr 484 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
167122, 163, 127, 165, 166letrd 10788 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
168111, 122, 125, 127, 148, 167le2addd 11250 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
169 oveq2 7143 . . . . . . . . 9 (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
170169fveq2d 6649 . . . . . . . 8 (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
171 fveq2 6645 . . . . . . . . 9 (𝑧 = 1 → (𝑆𝑧) = (𝑆‘1))
172 fveq2 6645 . . . . . . . . 9 (𝑧 = 1 → (𝑇𝑧) = (𝑇‘1))
173171, 172oveq12d 7153 . . . . . . . 8 (𝑧 = 1 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘1) + (𝑇‘1)))
174170, 173eqeq12d 2814 . . . . . . 7 (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
175174imbi2d 344 . . . . . 6 (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
176 oveq2 7143 . . . . . . . . 9 (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
177176fveq2d 6649 . . . . . . . 8 (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
178 fveq2 6645 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑆𝑧) = (𝑆𝑘))
179 fveq2 6645 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑇𝑧) = (𝑇𝑘))
180178, 179oveq12d 7153 . . . . . . . 8 (𝑧 = 𝑘 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆𝑘) + (𝑇𝑘)))
181177, 180eqeq12d 2814 . . . . . . 7 (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))))
182181imbi2d 344 . . . . . 6 (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)))))
183 oveq2 7143 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
184183fveq2d 6649 . . . . . . . 8 (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
185 fveq2 6645 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑆𝑧) = (𝑆‘(𝑘 + 1)))
186 fveq2 6645 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑇𝑧) = (𝑇‘(𝑘 + 1)))
187185, 186oveq12d 7153 . . . . . . . 8 (𝑧 = (𝑘 + 1) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
188184, 187eqeq12d 2814 . . . . . . 7 (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
189188imbi2d 344 . . . . . 6 (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
190 oveq2 7143 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
191190fveq2d 6649 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
192 fveq2 6645 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
193 fveq2 6645 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
194192, 193oveq12d 7153 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
195191, 194eqeq12d 2814 . . . . . . 7 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
196195imbi2d 344 . . . . . 6 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))))
19720fveq1i 6646 . . . . . . . 8 (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
198132a1i 11 . . . . . . . . 9 (𝜑 → 1 ∈ ℕ)
19919ovolfsval 24081 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))))
20018, 132, 199sylancl 589 . . . . . . . . . . 11 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))))
201 halfnz 12050 . . . . . . . . . . . . . . . . . 18 ¬ (1 / 2) ∈ ℤ
202 nnz 11994 . . . . . . . . . . . . . . . . . . 19 ((𝑛 / 2) ∈ ℕ → (𝑛 / 2) ∈ ℤ)
203 oveq1 7142 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 / 2) = (1 / 2))
204203eleq1d 2874 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
205202, 204syl5ib 247 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈ ℤ))
206201, 205mtoi 202 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ¬ (𝑛 / 2) ∈ ℕ)
207206iffalsed 4436 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2)))
208 oveq1 7142 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
209 df-2 11690 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
210208, 209eqtr4di 2851 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 + 1) = 2)
211210oveq1d 7150 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
212 2div2e1 11768 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
213211, 212eqtrdi 2849 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
214213fveq2d 6649 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
215207, 214eqtrd 2833 . . . . . . . . . . . . . . 15 (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
216 fvex 6658 . . . . . . . . . . . . . . 15 (𝐹‘1) ∈ V
217215, 17, 216fvmpt 6745 . . . . . . . . . . . . . 14 (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
218132, 217ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘1) = (𝐹‘1)
219218fveq2i 6648 . . . . . . . . . . . 12 (2nd ‘(𝐻‘1)) = (2nd ‘(𝐹‘1))
220218fveq2i 6648 . . . . . . . . . . . 12 (1st ‘(𝐻‘1)) = (1st ‘(𝐹‘1))
221219, 220oveq12i 7147 . . . . . . . . . . 11 ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1)))
222200, 221eqtrdi 2849 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
22352, 222seq1i 13380 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
224 2t1e2 11790 . . . . . . . . . . 11 (2 · 1) = 2
225224fveq2i 6648 . . . . . . . . . 10 (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
22619ovolfsval 24081 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
22718, 27, 226sylancl 589 . . . . . . . . . . 11 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
228 oveq1 7142 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
229228, 212eqtrdi 2849 . . . . . . . . . . . . . . . . . 18 (𝑛 = 2 → (𝑛 / 2) = 1)
230229, 132eqeltrdi 2898 . . . . . . . . . . . . . . . . 17 (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
231230iftrued 4433 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
232229fveq2d 6649 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
233231, 232eqtrd 2833 . . . . . . . . . . . . . . 15 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
234 fvex 6658 . . . . . . . . . . . . . . 15 (𝐺‘1) ∈ V
235233, 17, 234fvmpt 6745 . . . . . . . . . . . . . 14 (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
23627, 235ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘2) = (𝐺‘1)
237236fveq2i 6648 . . . . . . . . . . . 12 (2nd ‘(𝐻‘2)) = (2nd ‘(𝐺‘1))
238236fveq2i 6648 . . . . . . . . . . . 12 (1st ‘(𝐻‘2)) = (1st ‘(𝐺‘1))
239237, 238oveq12i 7147 . . . . . . . . . . 11 ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))
240227, 239eqtrdi 2849 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
241225, 240syl5eq 2845 . . . . . . . . 9 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
24272, 198, 34, 223, 241seqp1d 13383 . . . . . . . 8 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
243197, 242syl5eq 2845 . . . . . . 7 (𝜑 → (𝑈‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
244102fveq1i 6646 . . . . . . . . 9 (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
245101ovolfsval 24081 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
24612, 132, 245sylancl 589 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
24752, 246seq1i 13380 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
248244, 247syl5eq 2845 . . . . . . . 8 (𝜑 → (𝑆‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
249113fveq1i 6646 . . . . . . . . 9 (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
250112ovolfsval 24081 . . . . . . . . . . 11 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
2513, 132, 250sylancl 589 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
25252, 251seq1i 13380 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
253249, 252syl5eq 2845 . . . . . . . 8 (𝜑 → (𝑇‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
254248, 253oveq12d 7153 . . . . . . 7 (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
255243, 254eqtr4d 2836 . . . . . 6 (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))
256 oveq1 7142 . . . . . . . . 9 ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
25734oveq2i 7146 . . . . . . . . . . . . 13 ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
258 2cnd 11705 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 2 ∈ ℂ)
25938recnd 10660 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
260 1cnd 10627 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 1 ∈ ℂ)
261258, 259, 260adddid 10656 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
262 nnmulcl 11651 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
26327, 262mpan 689 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
264263adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
265264nncnd 11643 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
266265, 260, 260addassd 10654 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
267257, 261, 2663eqtr4a 2859 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
268267fveq2d 6649 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
26920fveq1i 6646 . . . . . . . . . . . 12 (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
270264peano2nnd 11644 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
271270, 72eleqtrdi 2900 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ (ℤ‘1))
272 seqp1 13381 . . . . . . . . . . . . . 14 (((2 · 𝑘) + 1) ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))))
273271, 272syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))))
274264, 72eleqtrdi 2900 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ (ℤ‘1))
275 seqp1 13381 . . . . . . . . . . . . . . . 16 ((2 · 𝑘) ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
276274, 275syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
27720fveq1i 6646 . . . . . . . . . . . . . . . . 17 (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
278277a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
279 oveq1 7142 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
280279eleq1d 2874 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
281279fveq2d 6649 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
282 oveq1 7142 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
283282fvoveq1d 7157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
284280, 281, 283ifbieq12d 4452 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
285 fvex 6658 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈ V
286 fvex 6658 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈ V
287285, 286ifex 4473 . . . . . . . . . . . . . . . . . . . . . 22 if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
288284, 17, 287fvmpt 6745 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑘) + 1) ∈ ℕ → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
289270, 288syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
290 2ne0 11731 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ≠ 0
291290a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → 2 ≠ 0)
292259, 258, 291divcan3d 11412 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
293292, 71eqeltrd 2890 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
294 nneo 12056 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 · 𝑘) ∈ ℕ → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
295264, 294syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
296293, 295mpbid 235 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ)
297296iffalsed 4436 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
298267oveq1d 7150 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
29929nncnd 11643 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
300 2cn 11702 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℂ
301 divcan3 11315 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
302300, 290, 301mp3an23 1450 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 + 1) ∈ ℂ → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
303299, 302syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
304298, 303eqtr3d 2835 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1))
305304fveq2d 6649 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
306289, 297, 3053eqtrd 2837 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
307306fveq2d 6649 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2nd ‘(𝐹‘(𝑘 + 1))))
308306fveq2d 6649 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘((2 · 𝑘) + 1))) = (1st ‘(𝐹‘(𝑘 + 1))))
309307, 308oveq12d 7153 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
31019ovolfsval 24081 . . . . . . . . . . . . . . . . . 18 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
31118, 270, 310syl2an2r 684 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
312101ovolfsval 24081 . . . . . . . . . . . . . . . . . 18 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
31312, 28, 312syl2an 598 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
314309, 311, 3133eqtr4rd 2844 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))
315278, 314oveq12d 7153 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
316276, 315eqtr4d 2836 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
317267fveq2d 6649 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
318270peano2nnd 11644 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
319267, 318eqeltrd 2890 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
320 oveq1 7142 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
321320eleq1d 2874 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
322320fveq2d 6649 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
323 oveq1 7142 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
324323fvoveq1d 7157 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
325321, 322, 324ifbieq12d 4452 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
326 fvex 6658 . . . . . . . . . . . . . . . . . . . . . 22 (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈ V
327 fvex 6658 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈ V
328326, 327ifex 4473 . . . . . . . . . . . . . . . . . . . . 21 if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
329325, 17, 328fvmpt 6745 . . . . . . . . . . . . . . . . . . . 20 ((2 · (𝑘 + 1)) ∈ ℕ → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
330319, 329syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
331303, 29eqeltrd 2890 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈ ℕ)
332331iftrued 4433 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
333303fveq2d 6649 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1)))
334330, 332, 3333eqtrd 2837 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1)))
335317, 334eqtr3d 2835 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1)))
336335fveq2d 6649 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2nd ‘(𝐺‘(𝑘 + 1))))
337335fveq2d 6649 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1st ‘(𝐺‘(𝑘 + 1))))
338336, 337oveq12d 7153 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
33919ovolfsval 24081 . . . . . . . . . . . . . . . 16 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
34018, 318, 339syl2an2r 684 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
341112ovolfsval 24081 . . . . . . . . . . . . . . . 16 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
3423, 28, 341syl2an 598 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
343338, 340, 3423eqtr4d 2843 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
344316, 343oveq12d 7153 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
345273, 344eqtrd 2833 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
346269, 345syl5eq 2845 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
347 ffvelrn 6826 . . . . . . . . . . . . . . 15 ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
34822, 263, 347syl2an 598 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
34923, 348sseldi 3913 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
350349recnd 10660 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
351101ovolfsf 24082 . . . . . . . . . . . . . . . 16 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
35212, 351syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
353 ffvelrn 6826 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
354352, 28, 353syl2an 598 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
35523, 354sseldi 3913 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
356355recnd 10660 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
357112ovolfsf 24082 . . . . . . . . . . . . . . . 16 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
3583, 357syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
359 ffvelrn 6826 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
360358, 28, 359syl2an 598 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
36123, 360sseldi 3913 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
362361recnd 10660 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
363350, 356, 362addassd 10654 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
364268, 346, 3633eqtrd 2837 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
365 seqp1 13381 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
36673, 365syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
367102fveq1i 6646 . . . . . . . . . . . . 13 (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
368102fveq1i 6646 . . . . . . . . . . . . . 14 (𝑆𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
369368oveq1i 7145 . . . . . . . . . . . . 13 ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
370366, 367, 3693eqtr4g 2858 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
371 seqp1 13381 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
37273, 371syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
373113fveq1i 6646 . . . . . . . . . . . . 13 (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
374113fveq1i 6646 . . . . . . . . . . . . . 14 (𝑇𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
375374oveq1i 7145 . . . . . . . . . . . . 13 ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
376372, 373, 3753eqtr4g 2858 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
377370, 376oveq12d 7153 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
378104ffvelrnda 6828 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ (0[,)+∞))
37923, 378sseldi 3913 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
380379recnd 10660 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℂ)
381115ffvelrnda 6828 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ (0[,)+∞))
38223, 381sseldi 3913 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℝ)
383382recnd 10660 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℂ)
384380, 356, 383, 362add4d 10859 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
385377, 384eqtrd 2833 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
386364, 385eqeq12d 2814 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))))
387256, 386syl5ibr 249 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
388387expcom 417 . . . . . . 7 (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
389388a2d 29 . . . . . 6 (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
390175, 182, 189, 196, 255, 389nnind 11645 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
391390impcom 411 . . . 4 ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
39257, 391syldan 594 . . 3 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
39363adantr 484 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
394393recnd 10660 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
39568adantr 484 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
396395rehalfcld 11874 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
397396recnd 10660 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
39865adantr 484 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
399398recnd 10660 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
400394, 397, 399, 397add4d 10859 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
401395recnd 10660 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
4024012halvesd 11873 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
403402oveq2d 7151 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
404400, 403eqtr2d 2834 . . 3 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) = (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
405168, 392, 4043brtr4d 5062 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
40626, 61, 70, 100, 405letrd 10788 1 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2987   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ifcif 4425  ∪ cuni 4800   class class class wbr 5030   ↦ cmpt 5110   × cxp 5517  dom cdm 5519  ran crn 5520   ∘ ccom 5523   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  1st c1st 7671  2nd c2nd 7672   ↑m cmap 8391  supcsup 8890  ℂcc 10526  ℝcr 10527  0cc0 10528  1c1 10529   + caddc 10531   · cmul 10533  +∞cpnf 10663  -∞cmnf 10664  ℝ*cxr 10665   < clt 10666   ≤ cle 10667   − cmin 10861   / cdiv 11288  ℕcn 11627  2c2 11682  ℤcz 11971  ℤ≥cuz 12233  ℝ+crp 12379  (,)cioo 12728  [,)cico 12730  ...cfz 12887  ⌊cfl 13157  seqcseq 13366  abscabs 14587  vol*covol 24073 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-er 8274  df-map 8393  df-en 8495  df-dom 8496  df-sdom 8497  df-sup 8892  df-inf 8893  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-3 11691  df-n0 11888  df-z 11972  df-uz 12234  df-rp 12380  df-ico 12734  df-fz 12888  df-fl 13159  df-seq 13367  df-exp 13428  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589 This theorem is referenced by:  ovolunlem1  24108
 Copyright terms: Public domain W3C validator