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

Theorem ovolunlem1a 23780
Description: Lemma for ovolun 23783. (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 (𝜑𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
ovolun.f2 (𝜑𝐴 ran ((,) ∘ 𝐹))
ovolun.f3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
ovolun.g1 (𝜑𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
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 (𝜑𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
2 elovolmlem 23758 . . . . . . . . . 10 (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
31, 2sylib 219 . . . . . . . . 9 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
43adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
54ffvelrnda 6716 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
6 nneo 11915 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
76adantl 482 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
87con2bid 356 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
98biimpar 478 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
10 ovolun.f1 . . . . . . . . . . 11 (𝜑𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
11 elovolmlem 23758 . . . . . . . . . . 11 (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1210, 11sylib 219 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1312adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1413ffvelrnda 6716 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
159, 14syldan 591 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
165, 15ifclda 4415 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
17 ovolun.h . . . . . 6 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
1816, 17fmptd 6741 . . . . 5 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
19 eqid 2795 . . . . . 6 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
20 ovolun.u . . . . . 6 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
2119, 20ovolsf 23756 . . . . 5 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
2218, 21syl 17 . . . 4 (𝜑𝑈:ℕ⟶(0[,)+∞))
23 rge0ssre 12694 . . . 4 (0[,)+∞) ⊆ ℝ
24 fss 6395 . . . 4 ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
2522, 23, 24sylancl 586 . . 3 (𝜑𝑈:ℕ⟶ℝ)
2625ffvelrnda 6716 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ∈ ℝ)
27 2nn 11558 . . . 4 2 ∈ ℕ
28 peano2nn 11498 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
2928adantl 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
3029nnred 11501 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
3130rehalfcld 11732 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
3231flcld 13018 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
33 ax-1cn 10441 . . . . . . . . 9 1 ∈ ℂ
34332timesi 11623 . . . . . . . 8 (2 · 1) = (1 + 1)
35 nnge1 11513 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
3635adantl 482 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 1 ≤ 𝑘)
37 nnre 11493 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
3837adantl 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
39 1re 10487 . . . . . . . . . . 11 1 ∈ ℝ
40 leadd1 10956 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4139, 39, 40mp3an13 1444 . . . . . . . . . 10 (𝑘 ∈ ℝ → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4238, 41syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4336, 42mpbid 233 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (1 + 1) ≤ (𝑘 + 1))
4434, 43eqbrtrid 4997 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
45 2re 11559 . . . . . . . . . 10 2 ∈ ℝ
46 2pos 11588 . . . . . . . . . 10 0 < 2
4745, 46pm3.2i 471 . . . . . . . . 9 (2 ∈ ℝ ∧ 0 < 2)
48 lemuldiv2 11369 . . . . . . . . 9 ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
4939, 47, 48mp3an13 1444 . . . . . . . 8 ((𝑘 + 1) ∈ ℝ → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5030, 49syl 17 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5144, 50mpbid 233 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 1 ≤ ((𝑘 + 1) / 2))
52 1z 11861 . . . . . . 7 1 ∈ ℤ
53 flge 13025 . . . . . . 7 ((((𝑘 + 1) / 2) ∈ ℝ ∧ 1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5431, 52, 53sylancl 586 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5551, 54mpbid 233 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 1 ≤ (⌊‘((𝑘 + 1) / 2)))
56 elnnz1 11857 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5732, 55, 56sylanbrc 583 . . . 4 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
58 nnmulcl 11509 . . . 4 ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
5927, 57, 58sylancr 587 . . 3 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
6025ffvelrnda 6716 . . 3 ((𝜑 ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
6159, 60syldan 591 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
62 ovolun.a . . . . . 6 (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
6362simprd 496 . . . . 5 (𝜑 → (vol*‘𝐴) ∈ ℝ)
64 ovolun.b . . . . . 6 (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
6564simprd 496 . . . . 5 (𝜑 → (vol*‘𝐵) ∈ ℝ)
6663, 65readdcld 10516 . . . 4 (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ)
67 ovolun.c . . . . 5 (𝜑𝐶 ∈ ℝ+)
6867rpred 12281 . . . 4 (𝜑𝐶 ∈ ℝ)
6966, 68readdcld 10516 . . 3 (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
7069adantr 481 . 2 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
71 simpr 485 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
72 nnuz 12130 . . . . 5 ℕ = (ℤ‘1)
7371, 72syl6eleq 2893 . . . 4 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
74 nnz 11853 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
7574adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
76 flhalf 13050 . . . . . 6 (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
7775, 76syl 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)))))
8074, 78, 79syl2an 595 . . . . . 6 ((𝑘 ∈ ℕ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8171, 59, 80syl2anc 584 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8277, 81mpbird 258 . . . 4 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘))
83 elfznn 12786 . . . . 5 (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
8419ovolfsf 23755 . . . . . . . . . 10 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8518, 84syl 17 . . . . . . . . 9 (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8685adantr 481 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8786ffvelrnda 6716 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
88 elrege0 12692 . . . . . . 7 ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
8987, 88sylib 219 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
9089simpld 495 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
9183, 90sylan2 592 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
92 elfzuz 12754 . . . . . 6 (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ‘(𝑘 + 1)))
93 eluznn 12167 . . . . . 6 (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
9429, 92, 93syl2an 595 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈ ℕ)
9589simprd 496 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
9694, 95syldan 591 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
9773, 82, 91, 96sermono 13252 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
9820fveq1i 6539 . . 3 (𝑈𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
9920fveq1i 6539 . . 3 (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
10097, 98, 993brtr4g 4996 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
101 eqid 2795 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
102 ovolun.s . . . . . . . . . 10 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
103101, 102ovolsf 23756 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
10412, 103syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
105104frnd 6389 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
106105, 23syl6ss 3901 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
107106adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
108104ffnd 6383 . . . . . 6 (𝜑𝑆 Fn ℕ)
109 fnfvelrn 6713 . . . . . 6 ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
110108, 57, 109syl2an2r 681 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
111107, 110sseldd 3890 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
112 eqid 2795 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
113 ovolun.t . . . . . . . . . 10 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
114112, 113ovolsf 23756 . . . . . . . . 9 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
1153, 114syl 17 . . . . . . . 8 (𝜑𝑇:ℕ⟶(0[,)+∞))
116115frnd 6389 . . . . . . 7 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
117116, 23syl6ss 3901 . . . . . 6 (𝜑 → ran 𝑇 ⊆ ℝ)
118117adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
119115ffnd 6383 . . . . . 6 (𝜑𝑇 Fn ℕ)
120 fnfvelrn 6713 . . . . . 6 ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
121119, 57, 120syl2an2r 681 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
122118, 121sseldd 3890 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
12368rehalfcld 11732 . . . . . 6 (𝜑 → (𝐶 / 2) ∈ ℝ)
12463, 123readdcld 10516 . . . . 5 (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
125124adantr 481 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
12665, 123readdcld 10516 . . . . 5 (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
127126adantr 481 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
128 ressxr 10531 . . . . . . . . 9 ℝ ⊆ ℝ*
129106, 128syl6ss 3901 . . . . . . . 8 (𝜑 → ran 𝑆 ⊆ ℝ*)
130 supxrcl 12558 . . . . . . . 8 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
131129, 130syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
132 1nn 11497 . . . . . . . . . . 11 1 ∈ ℕ
133104fdmd 6391 . . . . . . . . . . 11 (𝜑 → dom 𝑆 = ℕ)
134132, 133syl5eleqr 2890 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑆)
135134ne0d 4221 . . . . . . . . 9 (𝜑 → dom 𝑆 ≠ ∅)
136 dm0rn0 5679 . . . . . . . . . 10 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
137136necon3bii 3036 . . . . . . . . 9 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
138135, 137sylib 219 . . . . . . . 8 (𝜑 → ran 𝑆 ≠ ∅)
139 supxrgtmnf 12572 . . . . . . . 8 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ*, < ))
140106, 138, 139syl2anc 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 𝑆, ℝ*, < ) ∈ ℝ)
143131, 124, 140, 141, 142syl22anc 835 . . . . . 6 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
144143adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
145 supxrub 12567 . . . . . 6 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
146129, 110, 145syl2an2r 681 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
147141adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
148111, 144, 125, 146, 147letrd 10644 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
149117, 128syl6ss 3901 . . . . . . . 8 (𝜑 → ran 𝑇 ⊆ ℝ*)
150 supxrcl 12558 . . . . . . . 8 (ran 𝑇 ⊆ ℝ* → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
151149, 150syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
152115fdmd 6391 . . . . . . . . . . 11 (𝜑 → dom 𝑇 = ℕ)
153132, 152syl5eleqr 2890 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑇)
154153ne0d 4221 . . . . . . . . 9 (𝜑 → dom 𝑇 ≠ ∅)
155 dm0rn0 5679 . . . . . . . . . 10 (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
156155necon3bii 3036 . . . . . . . . 9 (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
157154, 156sylib 219 . . . . . . . 8 (𝜑 → ran 𝑇 ≠ ∅)
158 supxrgtmnf 12572 . . . . . . . 8 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ*, < ))
159117, 157, 158syl2anc 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 𝑇, ℝ*, < ) ∈ ℝ)
162151, 126, 159, 160, 161syl22anc 835 . . . . . 6 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
163162adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
164 supxrub 12567 . . . . . 6 ((ran 𝑇 ⊆ ℝ* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
165149, 121, 164syl2an2r 681 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
166160adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
167122, 163, 127, 165, 166letrd 10644 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
168111, 122, 125, 127, 148, 167le2addd 11107 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
169 oveq2 7024 . . . . . . . . 9 (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
170169fveq2d 6542 . . . . . . . 8 (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
171 fveq2 6538 . . . . . . . . 9 (𝑧 = 1 → (𝑆𝑧) = (𝑆‘1))
172 fveq2 6538 . . . . . . . . 9 (𝑧 = 1 → (𝑇𝑧) = (𝑇‘1))
173171, 172oveq12d 7034 . . . . . . . 8 (𝑧 = 1 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘1) + (𝑇‘1)))
174170, 173eqeq12d 2810 . . . . . . 7 (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
175174imbi2d 342 . . . . . 6 (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
176 oveq2 7024 . . . . . . . . 9 (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
177176fveq2d 6542 . . . . . . . 8 (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
178 fveq2 6538 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑆𝑧) = (𝑆𝑘))
179 fveq2 6538 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑇𝑧) = (𝑇𝑘))
180178, 179oveq12d 7034 . . . . . . . 8 (𝑧 = 𝑘 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆𝑘) + (𝑇𝑘)))
181177, 180eqeq12d 2810 . . . . . . 7 (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))))
182181imbi2d 342 . . . . . 6 (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)))))
183 oveq2 7024 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
184183fveq2d 6542 . . . . . . . 8 (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
185 fveq2 6538 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑆𝑧) = (𝑆‘(𝑘 + 1)))
186 fveq2 6538 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑇𝑧) = (𝑇‘(𝑘 + 1)))
187185, 186oveq12d 7034 . . . . . . . 8 (𝑧 = (𝑘 + 1) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
188184, 187eqeq12d 2810 . . . . . . 7 (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
189188imbi2d 342 . . . . . 6 (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
190 oveq2 7024 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
191190fveq2d 6542 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
192 fveq2 6538 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
193 fveq2 6538 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
194192, 193oveq12d 7034 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
195191, 194eqeq12d 2810 . . . . . . 7 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
196195imbi2d 342 . . . . . 6 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))))
19720fveq1i 6539 . . . . . . . 8 (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
19819ovolfsval 23754 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))))
19918, 132, 198sylancl 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))
203202eleq1d 2867 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
204201, 203syl5ib 245 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈ ℤ))
205200, 204mtoi 200 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ¬ (𝑛 / 2) ∈ ℕ)
206205iffalsed 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)
209207, 208syl6eqr 2849 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 + 1) = 2)
210209oveq1d 7031 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
211 2div2e1 11626 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
212210, 211syl6eq 2847 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
213212fveq2d 6542 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
214206, 213eqtrd 2831 . . . . . . . . . . . . . . 15 (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
215 fvex 6551 . . . . . . . . . . . . . . 15 (𝐹‘1) ∈ V
216214, 17, 215fvmpt 6635 . . . . . . . . . . . . . 14 (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
217132, 216ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘1) = (𝐹‘1)
218217fveq2i 6541 . . . . . . . . . . . 12 (2nd ‘(𝐻‘1)) = (2nd ‘(𝐹‘1))
219217fveq2i 6541 . . . . . . . . . . . 12 (1st ‘(𝐻‘1)) = (1st ‘(𝐹‘1))
220218, 219oveq12i 7028 . . . . . . . . . . 11 ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1)))
221199, 220syl6eq 2847 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
22252, 221seq1i 13233 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
223 2t1e2 11648 . . . . . . . . . . 11 (2 · 1) = 2
224223fveq2i 6541 . . . . . . . . . 10 (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
22519ovolfsval 23754 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
22618, 27, 225sylancl 586 . . . . . . . . . . 11 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
227 oveq1 7023 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
228227, 211syl6eq 2847 . . . . . . . . . . . . . . . . . 18 (𝑛 = 2 → (𝑛 / 2) = 1)
229228, 132syl6eqel 2891 . . . . . . . . . . . . . . . . 17 (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
230229iftrued 4389 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
231228fveq2d 6542 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
232230, 231eqtrd 2831 . . . . . . . . . . . . . . 15 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
233 fvex 6551 . . . . . . . . . . . . . . 15 (𝐺‘1) ∈ V
234232, 17, 233fvmpt 6635 . . . . . . . . . . . . . 14 (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
23527, 234ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘2) = (𝐺‘1)
236235fveq2i 6541 . . . . . . . . . . . 12 (2nd ‘(𝐻‘2)) = (2nd ‘(𝐺‘1))
237235fveq2i 6541 . . . . . . . . . . . 12 (1st ‘(𝐻‘2)) = (1st ‘(𝐺‘1))
238236, 237oveq12i 7028 . . . . . . . . . . 11 ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))
239226, 238syl6eq 2847 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
240224, 239syl5eq 2843 . . . . . . . . 9 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
24172, 132, 34, 222, 240seqp1i 13236 . . . . . . . 8 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
242197, 241syl5eq 2843 . . . . . . 7 (𝜑 → (𝑈‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
243102fveq1i 6539 . . . . . . . . 9 (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
244101ovolfsval 23754 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
24512, 132, 244sylancl 586 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
24652, 245seq1i 13233 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
247243, 246syl5eq 2843 . . . . . . . 8 (𝜑 → (𝑆‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
248113fveq1i 6539 . . . . . . . . 9 (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
249112ovolfsval 23754 . . . . . . . . . . 11 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
2503, 132, 249sylancl 586 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
25152, 250seq1i 13233 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
252248, 251syl5eq 2843 . . . . . . . 8 (𝜑 → (𝑇‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
253247, 252oveq12d 7034 . . . . . . 7 (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
254242, 253eqtr4d 2834 . . . . . 6 (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))
255 oveq1 7023 . . . . . . . . 9 ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
25634oveq2i 7027 . . . . . . . . . . . . 13 ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
257 2cnd 11563 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 2 ∈ ℂ)
25838recnd 10515 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
259 1cnd 10482 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 1 ∈ ℂ)
260257, 258, 259adddid 10511 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
261 nnmulcl 11509 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
26227, 261mpan 686 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
263262adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
264263nncnd 11502 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
265264, 259, 259addassd 10509 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
266256, 260, 2653eqtr4a 2857 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
267266fveq2d 6542 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
26820fveq1i 6539 . . . . . . . . . . . 12 (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
269263peano2nnd 11503 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
270269, 72syl6eleq 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))))
272270, 271syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))))
273263, 72syl6eleq 2893 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ (ℤ‘1))
274 seqp1 13234 . . . . . . . . . . . . . . . 16 ((2 · 𝑘) ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
275273, 274syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
27620fveq1i 6539 . . . . . . . . . . . . . . . . 17 (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
277276a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
278 oveq1 7023 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
279278eleq1d 2867 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
280278fveq2d 6542 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
281 oveq1 7023 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
282281fvoveq1d 7038 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
283279, 280, 282ifbieq12d 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
286284, 285ifex 4429 . . . . . . . . . . . . . . . . . . . . . 22 if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
287283, 17, 286fvmpt 6635 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑘) + 1) ∈ ℕ → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
288269, 287syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
289 2ne0 11589 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ≠ 0
290289a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → 2 ≠ 0)
291258, 257, 290divcan3d 11269 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
292291, 71eqeltrd 2883 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
293 nneo 11915 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 · 𝑘) ∈ ℕ → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
294263, 293syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
295292, 294mpbid 233 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ)
296295iffalsed 4392 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
297266oveq1d 7031 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
29829nncnd 11502 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
299 2cn 11560 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℂ
300 divcan3 11172 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
301299, 289, 300mp3an23 1445 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 + 1) ∈ ℂ → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
302298, 301syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
303297, 302eqtr3d 2833 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1))
304303fveq2d 6542 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
305288, 296, 3043eqtrd 2835 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
306305fveq2d 6542 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2nd ‘(𝐹‘(𝑘 + 1))))
307305fveq2d 6542 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘((2 · 𝑘) + 1))) = (1st ‘(𝐹‘(𝑘 + 1))))
308306, 307oveq12d 7034 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
30919ovolfsval 23754 . . . . . . . . . . . . . . . . . 18 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
31018, 269, 309syl2an2r 681 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
311101ovolfsval 23754 . . . . . . . . . . . . . . . . . 18 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
31212, 28, 311syl2an 595 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
313308, 310, 3123eqtr4rd 2842 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))
314277, 313oveq12d 7034 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
315275, 314eqtr4d 2834 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
316266fveq2d 6542 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
317269peano2nnd 11503 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
318266, 317eqeltrd 2883 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
319 oveq1 7023 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
320319eleq1d 2867 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
321319fveq2d 6542 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
322 oveq1 7023 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
323322fvoveq1d 7038 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
324320, 321, 323ifbieq12d 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
327325, 326ifex 4429 . . . . . . . . . . . . . . . . . . . . 21 if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
328324, 17, 327fvmpt 6635 . . . . . . . . . . . . . . . . . . . 20 ((2 · (𝑘 + 1)) ∈ ℕ → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
329318, 328syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
330302, 29eqeltrd 2883 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈ ℕ)
331330iftrued 4389 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
332302fveq2d 6542 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1)))
333329, 331, 3323eqtrd 2835 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1)))
334316, 333eqtr3d 2833 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1)))
335334fveq2d 6542 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2nd ‘(𝐺‘(𝑘 + 1))))
336334fveq2d 6542 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1st ‘(𝐺‘(𝑘 + 1))))
337335, 336oveq12d 7034 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
33819ovolfsval 23754 . . . . . . . . . . . . . . . 16 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
33918, 317, 338syl2an2r 681 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
340112ovolfsval 23754 . . . . . . . . . . . . . . . 16 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
3413, 28, 340syl2an 595 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
342337, 339, 3413eqtr4d 2841 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
343315, 342oveq12d 7034 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
344272, 343eqtrd 2831 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
345268, 344syl5eq 2843 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
346 ffvelrn 6714 . . . . . . . . . . . . . . 15 ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
34722, 262, 346syl2an 595 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
34823, 347sseldi 3887 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
349348recnd 10515 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
350101ovolfsf 23755 . . . . . . . . . . . . . . . 16 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
35112, 350syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
352 ffvelrn 6714 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
353351, 28, 352syl2an 595 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
35423, 353sseldi 3887 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
355354recnd 10515 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
356112ovolfsf 23755 . . . . . . . . . . . . . . . 16 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
3573, 356syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
358 ffvelrn 6714 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
359357, 28, 358syl2an 595 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
36023, 359sseldi 3887 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
361360recnd 10515 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
362349, 355, 361addassd 10509 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
363267, 345, 3623eqtrd 2835 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
364 seqp1 13234 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
36573, 364syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
366102fveq1i 6539 . . . . . . . . . . . . 13 (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
367102fveq1i 6539 . . . . . . . . . . . . . 14 (𝑆𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
368367oveq1i 7026 . . . . . . . . . . . . 13 ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
369365, 366, 3683eqtr4g 2856 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
370 seqp1 13234 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
37173, 370syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
372113fveq1i 6539 . . . . . . . . . . . . 13 (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
373113fveq1i 6539 . . . . . . . . . . . . . 14 (𝑇𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
374373oveq1i 7026 . . . . . . . . . . . . 13 ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
375371, 372, 3743eqtr4g 2856 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
376369, 375oveq12d 7034 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
377104ffvelrnda 6716 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ (0[,)+∞))
37823, 377sseldi 3887 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
379378recnd 10515 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℂ)
380115ffvelrnda 6716 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ (0[,)+∞))
38123, 380sseldi 3887 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℝ)
382381recnd 10515 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℂ)
383379, 355, 382, 361add4d 10715 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
384376, 383eqtrd 2831 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
385363, 384eqeq12d 2810 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))))
386255, 385syl5ibr 247 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
387386expcom 414 . . . . . . 7 (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
388387a2d 29 . . . . . 6 (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
389175, 182, 189, 196, 254, 388nnind 11504 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
390389impcom 408 . . . 4 ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
39157, 390syldan 591 . . 3 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
39263adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
393392recnd 10515 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
39468adantr 481 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
395394rehalfcld 11732 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
396395recnd 10515 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
39765adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
398397recnd 10515 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
399393, 396, 398, 396add4d 10715 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
400394recnd 10515 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
4014002halvesd 11731 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
402401oveq2d 7032 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
403399, 402eqtr2d 2832 . . 3 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) = (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
404168, 391, 4033brtr4d 4994 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
40526, 61, 70, 100, 404letrd 10644 1 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1522  wcel 2081  wne 2984  cin 3858  wss 3859  c0 4211  ifcif 4381   cuni 4745   class class class wbr 4962  cmpt 5041   × cxp 5441  dom cdm 5443  ran crn 5444  ccom 5447   Fn wfn 6220  wf 6221  cfv 6225  (class class class)co 7016  1st c1st 7543  2nd c2nd 7544  𝑚 cmap 8256  supcsup 8750  cc 10381  cr 10382  0cc0 10383  1c1 10384   + caddc 10386   · cmul 10388  +∞cpnf 10518  -∞cmnf 10519  *cxr 10520   < clt 10521  cle 10522  cmin 10717   / cdiv 11145  cn 11486  2c2 11540  cz 11829  cuz 12093  +crp 12239  (,)cioo 12588  [,)cico 12590  ...cfz 12742  cfl 13010  seqcseq 13219  abscabs 14427  vol*covol 23746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-er 8139  df-map 8258  df-en 8358  df-dom 8359  df-sdom 8360  df-sup 8752  df-inf 8753  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-n0 11746  df-z 11830  df-uz 12094  df-rp 12240  df-ico 12594  df-fz 12743  df-fl 13012  df-seq 13220  df-exp 13280  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429
This theorem is referenced by:  ovolunlem1  23781
  Copyright terms: Public domain W3C validator