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

Theorem ovolunlem1a 24765
Description: Lemma for ovolun 24768. (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 24743 . . . . . . . . . 10 (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
31, 2sylib 217 . . . . . . . . 9 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
43adantr 482 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
54ffvelcdmda 7021 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
6 nneo 12509 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
76adantl 483 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
87con2bid 355 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
98biimpar 479 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
10 ovolun.f1 . . . . . . . . . . 11 (𝜑𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
11 elovolmlem 24743 . . . . . . . . . . 11 (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1210, 11sylib 217 . . . . . . . . . 10 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1312adantr 482 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1413ffvelcdmda 7021 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
159, 14syldan 592 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
165, 15ifclda 4512 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
17 ovolun.h . . . . . 6 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
1816, 17fmptd 7048 . . . . 5 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
19 eqid 2737 . . . . . 6 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
20 ovolun.u . . . . . 6 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
2119, 20ovolsf 24741 . . . . 5 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
2218, 21syl 17 . . . 4 (𝜑𝑈:ℕ⟶(0[,)+∞))
23 rge0ssre 13293 . . . 4 (0[,)+∞) ⊆ ℝ
24 fss 6672 . . . 4 ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
2522, 23, 24sylancl 587 . . 3 (𝜑𝑈:ℕ⟶ℝ)
2625ffvelcdmda 7021 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ∈ ℝ)
27 2nn 12151 . . . 4 2 ∈ ℕ
28 peano2nn 12090 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
2928adantl 483 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
3029nnred 12093 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
3130rehalfcld 12325 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((𝑘 + 1) / 2) ∈ ℝ)
3231flcld 13623 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℤ)
33 ax-1cn 11034 . . . . . . . . 9 1 ∈ ℂ
34332timesi 12216 . . . . . . . 8 (2 · 1) = (1 + 1)
35 nnge1 12106 . . . . . . . . . 10 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
3635adantl 483 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 1 ≤ 𝑘)
37 nnre 12085 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
3837adantl 483 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
39 1re 11080 . . . . . . . . . . 11 1 ∈ ℝ
40 leadd1 11548 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4139, 39, 40mp3an13 1452 . . . . . . . . . 10 (𝑘 ∈ ℝ → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4238, 41syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1 ≤ 𝑘 ↔ (1 + 1) ≤ (𝑘 + 1)))
4336, 42mpbid 231 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (1 + 1) ≤ (𝑘 + 1))
4434, 43eqbrtrid 5131 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (2 · 1) ≤ (𝑘 + 1))
45 2re 12152 . . . . . . . . . 10 2 ∈ ℝ
46 2pos 12181 . . . . . . . . . 10 0 < 2
4745, 46pm3.2i 472 . . . . . . . . 9 (2 ∈ ℝ ∧ 0 < 2)
48 lemuldiv2 11961 . . . . . . . . 9 ((1 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
4939, 47, 48mp3an13 1452 . . . . . . . 8 ((𝑘 + 1) ∈ ℝ → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5030, 49syl 17 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((2 · 1) ≤ (𝑘 + 1) ↔ 1 ≤ ((𝑘 + 1) / 2)))
5144, 50mpbid 231 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 1 ≤ ((𝑘 + 1) / 2))
52 1z 12455 . . . . . . 7 1 ∈ ℤ
53 flge 13630 . . . . . . 7 ((((𝑘 + 1) / 2) ∈ ℝ ∧ 1 ∈ ℤ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5431, 52, 53sylancl 587 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (1 ≤ ((𝑘 + 1) / 2) ↔ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5551, 54mpbid 231 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 1 ≤ (⌊‘((𝑘 + 1) / 2)))
56 elnnz1 12451 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ ↔ ((⌊‘((𝑘 + 1) / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘((𝑘 + 1) / 2))))
5732, 55, 56sylanbrc 584 . . . 4 ((𝜑𝑘 ∈ ℕ) → (⌊‘((𝑘 + 1) / 2)) ∈ ℕ)
58 nnmulcl 12102 . . . 4 ((2 ∈ ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
5927, 57, 58sylancr 588 . . 3 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ)
6025ffvelcdmda 7021 . . 3 ((𝜑 ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
6159, 60syldan 592 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ∈ ℝ)
62 ovolun.a . . . . . 6 (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
6362simprd 497 . . . . 5 (𝜑 → (vol*‘𝐴) ∈ ℝ)
64 ovolun.b . . . . . 6 (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
6564simprd 497 . . . . 5 (𝜑 → (vol*‘𝐵) ∈ ℝ)
6663, 65readdcld 11109 . . . 4 (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ)
67 ovolun.c . . . . 5 (𝜑𝐶 ∈ ℝ+)
6867rpred 12877 . . . 4 (𝜑𝐶 ∈ ℝ)
6966, 68readdcld 11109 . . 3 (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
7069adantr 482 . 2 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
71 simpr 486 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
72 nnuz 12726 . . . . 5 ℕ = (ℤ‘1)
7371, 72eleqtrdi 2848 . . . 4 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
74 nnz 12447 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
7574adantl 483 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
76 flhalf 13655 . . . . . 6 (𝑘 ∈ ℤ → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
7775, 76syl 17 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2))))
78 nnz 12447 . . . . . . 7 ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ)
79 eluz 12701 . . . . . . 7 ((𝑘 ∈ ℤ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℤ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8074, 78, 79syl2an 597 . . . . . 6 ((𝑘 ∈ ℕ ∧ (2 · (⌊‘((𝑘 + 1) / 2))) ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8171, 59, 80syl2anc 585 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘) ↔ 𝑘 ≤ (2 · (⌊‘((𝑘 + 1) / 2)))))
8277, 81mpbird 257 . . . 4 ((𝜑𝑘 ∈ ℕ) → (2 · (⌊‘((𝑘 + 1) / 2))) ∈ (ℤ𝑘))
83 elfznn 13390 . . . . 5 (𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ ℕ)
8419ovolfsf 24740 . . . . . . . . . 10 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8518, 84syl 17 . . . . . . . . 9 (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8685adantr 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
8786ffvelcdmda 7021 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞))
88 elrege0 13291 . . . . . . 7 ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
8987, 88sylib 217 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗)))
9089simpld 496 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
9183, 90sylan2 594 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...(2 · (⌊‘((𝑘 + 1) / 2))))) → (((abs ∘ − ) ∘ 𝐻)‘𝑗) ∈ ℝ)
92 elfzuz 13357 . . . . . 6 (𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2)))) → 𝑗 ∈ (ℤ‘(𝑘 + 1)))
93 eluznn 12763 . . . . . 6 (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
9429, 92, 93syl2an 597 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 𝑗 ∈ ℕ)
9589simprd 497 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
9694, 95syldan 592 . . . 4 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ ((𝑘 + 1)...(2 · (⌊‘((𝑘 + 1) / 2))))) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑗))
9773, 82, 91, 96sermono 13860 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2)))))
9820fveq1i 6830 . . 3 (𝑈𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑘)
9920fveq1i 6830 . . 3 (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · (⌊‘((𝑘 + 1) / 2))))
10097, 98, 993brtr4g 5130 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
101 eqid 2737 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
102 ovolun.s . . . . . . . . . 10 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
103101, 102ovolsf 24741 . . . . . . . . 9 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
10412, 103syl 17 . . . . . . . 8 (𝜑𝑆:ℕ⟶(0[,)+∞))
105104frnd 6663 . . . . . . 7 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
106105, 23sstrdi 3947 . . . . . 6 (𝜑 → ran 𝑆 ⊆ ℝ)
107106adantr 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ)
108104ffnd 6656 . . . . . 6 (𝜑𝑆 Fn ℕ)
109 fnfvelrn 7018 . . . . . 6 ((𝑆 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
110108, 57, 109syl2an2r 683 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆)
111107, 110sseldd 3936 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
112 eqid 2737 . . . . . . . . . 10 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
113 ovolun.t . . . . . . . . . 10 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
114112, 113ovolsf 24741 . . . . . . . . 9 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
1153, 114syl 17 . . . . . . . 8 (𝜑𝑇:ℕ⟶(0[,)+∞))
116115frnd 6663 . . . . . . 7 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
117116, 23sstrdi 3947 . . . . . 6 (𝜑 → ran 𝑇 ⊆ ℝ)
118117adantr 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ran 𝑇 ⊆ ℝ)
119115ffnd 6656 . . . . . 6 (𝜑𝑇 Fn ℕ)
120 fnfvelrn 7018 . . . . . 6 ((𝑇 Fn ℕ ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
121119, 57, 120syl2an2r 683 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇)
122118, 121sseldd 3936 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ℝ)
12368rehalfcld 12325 . . . . . 6 (𝜑 → (𝐶 / 2) ∈ ℝ)
12463, 123readdcld 11109 . . . . 5 (𝜑 → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
125124adantr 482 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ)
12665, 123readdcld 11109 . . . . 5 (𝜑 → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
127126adantr 482 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ)
128 ressxr 11124 . . . . . . . . 9 ℝ ⊆ ℝ*
129106, 128sstrdi 3947 . . . . . . . 8 (𝜑 → ran 𝑆 ⊆ ℝ*)
130 supxrcl 13154 . . . . . . . 8 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
131129, 130syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
132 1nn 12089 . . . . . . . . . . 11 1 ∈ ℕ
133104fdmd 6666 . . . . . . . . . . 11 (𝜑 → dom 𝑆 = ℕ)
134132, 133eleqtrrid 2845 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑆)
135134ne0d 4286 . . . . . . . . 9 (𝜑 → dom 𝑆 ≠ ∅)
136 dm0rn0 5870 . . . . . . . . . 10 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
137136necon3bii 2994 . . . . . . . . 9 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
138135, 137sylib 217 . . . . . . . 8 (𝜑 → ran 𝑆 ≠ ∅)
139 supxrgtmnf 13168 . . . . . . . 8 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → -∞ < sup(ran 𝑆, ℝ*, < ))
140106, 138, 139syl2anc 585 . . . . . . 7 (𝜑 → -∞ < sup(ran 𝑆, ℝ*, < ))
141 ovolun.f3 . . . . . . 7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
142 xrre 13008 . . . . . . 7 (((sup(ran 𝑆, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
143131, 124, 140, 141, 142syl22anc 837 . . . . . 6 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
144143adantr 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
145 supxrub 13163 . . . . . 6 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑆) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
146129, 110, 145syl2an2r 683 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑆, ℝ*, < ))
147141adantr 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
148111, 144, 125, 146, 147letrd 11237 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
149117, 128sstrdi 3947 . . . . . . . 8 (𝜑 → ran 𝑇 ⊆ ℝ*)
150 supxrcl 13154 . . . . . . . 8 (ran 𝑇 ⊆ ℝ* → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
151149, 150syl 17 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
152115fdmd 6666 . . . . . . . . . . 11 (𝜑 → dom 𝑇 = ℕ)
153132, 152eleqtrrid 2845 . . . . . . . . . 10 (𝜑 → 1 ∈ dom 𝑇)
154153ne0d 4286 . . . . . . . . 9 (𝜑 → dom 𝑇 ≠ ∅)
155 dm0rn0 5870 . . . . . . . . . 10 (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
156155necon3bii 2994 . . . . . . . . 9 (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
157154, 156sylib 217 . . . . . . . 8 (𝜑 → ran 𝑇 ≠ ∅)
158 supxrgtmnf 13168 . . . . . . . 8 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅) → -∞ < sup(ran 𝑇, ℝ*, < ))
159117, 157, 158syl2anc 585 . . . . . . 7 (𝜑 → -∞ < sup(ran 𝑇, ℝ*, < ))
160 ovolun.g3 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
161 xrre 13008 . . . . . . 7 (((sup(ran 𝑇, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐵) + (𝐶 / 2)) ∈ ℝ) ∧ (-∞ < sup(ran 𝑇, ℝ*, < ) ∧ sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
162151, 126, 159, 160, 161syl22anc 837 . . . . . 6 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
163162adantr 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
164 supxrub 13163 . . . . . 6 ((ran 𝑇 ⊆ ℝ* ∧ (𝑇‘(⌊‘((𝑘 + 1) / 2))) ∈ ran 𝑇) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
165149, 121, 164syl2an2r 683 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ sup(ran 𝑇, ℝ*, < ))
166160adantr 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
167122, 163, 127, 165, 166letrd 11237 . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(⌊‘((𝑘 + 1) / 2))) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
168111, 122, 125, 127, 148, 167le2addd 11699 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
169 oveq2 7349 . . . . . . . . 9 (𝑧 = 1 → (2 · 𝑧) = (2 · 1))
170169fveq2d 6833 . . . . . . . 8 (𝑧 = 1 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 1)))
171 fveq2 6829 . . . . . . . . 9 (𝑧 = 1 → (𝑆𝑧) = (𝑆‘1))
172 fveq2 6829 . . . . . . . . 9 (𝑧 = 1 → (𝑇𝑧) = (𝑇‘1))
173171, 172oveq12d 7359 . . . . . . . 8 (𝑧 = 1 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘1) + (𝑇‘1)))
174170, 173eqeq12d 2753 . . . . . . 7 (𝑧 = 1 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1))))
175174imbi2d 341 . . . . . 6 (𝑧 = 1 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))))
176 oveq2 7349 . . . . . . . . 9 (𝑧 = 𝑘 → (2 · 𝑧) = (2 · 𝑘))
177176fveq2d 6833 . . . . . . . 8 (𝑧 = 𝑘 → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · 𝑘)))
178 fveq2 6829 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑆𝑧) = (𝑆𝑘))
179 fveq2 6829 . . . . . . . . 9 (𝑧 = 𝑘 → (𝑇𝑧) = (𝑇𝑘))
180178, 179oveq12d 7359 . . . . . . . 8 (𝑧 = 𝑘 → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆𝑘) + (𝑇𝑘)))
181177, 180eqeq12d 2753 . . . . . . 7 (𝑧 = 𝑘 → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))))
182181imbi2d 341 . . . . . 6 (𝑧 = 𝑘 → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)))))
183 oveq2 7349 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (2 · 𝑧) = (2 · (𝑘 + 1)))
184183fveq2d 6833 . . . . . . . 8 (𝑧 = (𝑘 + 1) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (𝑘 + 1))))
185 fveq2 6829 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑆𝑧) = (𝑆‘(𝑘 + 1)))
186 fveq2 6829 . . . . . . . . 9 (𝑧 = (𝑘 + 1) → (𝑇𝑧) = (𝑇‘(𝑘 + 1)))
187185, 186oveq12d 7359 . . . . . . . 8 (𝑧 = (𝑘 + 1) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))
188184, 187eqeq12d 2753 . . . . . . 7 (𝑧 = (𝑘 + 1) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
189188imbi2d 341 . . . . . 6 (𝑧 = (𝑘 + 1) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
190 oveq2 7349 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (2 · 𝑧) = (2 · (⌊‘((𝑘 + 1) / 2))))
191190fveq2d 6833 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑈‘(2 · 𝑧)) = (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))))
192 fveq2 6829 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑆𝑧) = (𝑆‘(⌊‘((𝑘 + 1) / 2))))
193 fveq2 6829 . . . . . . . . 9 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → (𝑇𝑧) = (𝑇‘(⌊‘((𝑘 + 1) / 2))))
194192, 193oveq12d 7359 . . . . . . . 8 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑆𝑧) + (𝑇𝑧)) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
195191, 194eqeq12d 2753 . . . . . . 7 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧)) ↔ (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
196195imbi2d 341 . . . . . 6 (𝑧 = (⌊‘((𝑘 + 1) / 2)) → ((𝜑 → (𝑈‘(2 · 𝑧)) = ((𝑆𝑧) + (𝑇𝑧))) ↔ (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))))
19720fveq1i 6830 . . . . . . . 8 (𝑈‘(2 · 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1))
198132a1i 11 . . . . . . . . 9 (𝜑 → 1 ∈ ℕ)
19919ovolfsval 24739 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))))
20018, 132, 199sylancl 587 . . . . . . . . . . 11 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))))
201 halfnz 12503 . . . . . . . . . . . . . . . . . 18 ¬ (1 / 2) ∈ ℤ
202 nnz 12447 . . . . . . . . . . . . . . . . . . 19 ((𝑛 / 2) ∈ ℕ → (𝑛 / 2) ∈ ℤ)
203 oveq1 7348 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 / 2) = (1 / 2))
204203eleq1d 2822 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → ((𝑛 / 2) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
205202, 204syl5ib 244 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 / 2) ∈ ℕ → (1 / 2) ∈ ℤ))
206201, 205mtoi 198 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ¬ (𝑛 / 2) ∈ ℕ)
207206iffalsed 4488 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘((𝑛 + 1) / 2)))
208 oveq1 7348 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
209 df-2 12141 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
210208, 209eqtr4di 2795 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 + 1) = 2)
211210oveq1d 7356 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → ((𝑛 + 1) / 2) = (2 / 2))
212 2div2e1 12219 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
213211, 212eqtrdi 2793 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → ((𝑛 + 1) / 2) = 1)
214213fveq2d 6833 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘1))
215207, 214eqtrd 2777 . . . . . . . . . . . . . . 15 (𝑛 = 1 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐹‘1))
216 fvex 6842 . . . . . . . . . . . . . . 15 (𝐹‘1) ∈ V
217215, 17, 216fvmpt 6935 . . . . . . . . . . . . . 14 (1 ∈ ℕ → (𝐻‘1) = (𝐹‘1))
218132, 217ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘1) = (𝐹‘1)
219218fveq2i 6832 . . . . . . . . . . . 12 (2nd ‘(𝐻‘1)) = (2nd ‘(𝐹‘1))
220218fveq2i 6832 . . . . . . . . . . . 12 (1st ‘(𝐻‘1)) = (1st ‘(𝐹‘1))
221219, 220oveq12i 7353 . . . . . . . . . . 11 ((2nd ‘(𝐻‘1)) − (1st ‘(𝐻‘1))) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1)))
222200, 221eqtrdi 2793 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
22352, 222seq1i 13840 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
224 2t1e2 12241 . . . . . . . . . . 11 (2 · 1) = 2
225224fveq2i 6832 . . . . . . . . . 10 (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = (((abs ∘ − ) ∘ 𝐻)‘2)
22619ovolfsval 24739 . . . . . . . . . . . 12 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 2 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
22718, 27, 226sylancl 587 . . . . . . . . . . 11 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))))
228 oveq1 7348 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 2 → (𝑛 / 2) = (2 / 2))
229228, 212eqtrdi 2793 . . . . . . . . . . . . . . . . . 18 (𝑛 = 2 → (𝑛 / 2) = 1)
230229, 132eqeltrdi 2846 . . . . . . . . . . . . . . . . 17 (𝑛 = 2 → (𝑛 / 2) ∈ ℕ)
231230iftrued 4485 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘(𝑛 / 2)))
232229fveq2d 6833 . . . . . . . . . . . . . . . 16 (𝑛 = 2 → (𝐺‘(𝑛 / 2)) = (𝐺‘1))
233231, 232eqtrd 2777 . . . . . . . . . . . . . . 15 (𝑛 = 2 → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = (𝐺‘1))
234 fvex 6842 . . . . . . . . . . . . . . 15 (𝐺‘1) ∈ V
235233, 17, 234fvmpt 6935 . . . . . . . . . . . . . 14 (2 ∈ ℕ → (𝐻‘2) = (𝐺‘1))
23627, 235ax-mp 5 . . . . . . . . . . . . 13 (𝐻‘2) = (𝐺‘1)
237236fveq2i 6832 . . . . . . . . . . . 12 (2nd ‘(𝐻‘2)) = (2nd ‘(𝐺‘1))
238236fveq2i 6832 . . . . . . . . . . . 12 (1st ‘(𝐻‘2)) = (1st ‘(𝐺‘1))
239237, 238oveq12i 7353 . . . . . . . . . . 11 ((2nd ‘(𝐻‘2)) − (1st ‘(𝐻‘2))) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))
240227, 239eqtrdi 2793 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘2) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
241225, 240eqtrid 2789 . . . . . . . . 9 (𝜑 → (((abs ∘ − ) ∘ 𝐻)‘(2 · 1)) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
24272, 198, 34, 223, 241seqp1d 13843 . . . . . . . 8 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
243197, 242eqtrid 2789 . . . . . . 7 (𝜑 → (𝑈‘(2 · 1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
244102fveq1i 6830 . . . . . . . . 9 (𝑆‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1)
245101ovolfsval 24739 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
24612, 132, 245sylancl 587 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐹)‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
24752, 246seq1i 13840 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
248244, 247eqtrid 2789 . . . . . . . 8 (𝜑 → (𝑆‘1) = ((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))))
249113fveq1i 6830 . . . . . . . . 9 (𝑇‘1) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1)
250112ovolfsval 24739 . . . . . . . . . . 11 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 1 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
2513, 132, 250sylancl 587 . . . . . . . . . 10 (𝜑 → (((abs ∘ − ) ∘ 𝐺)‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
25252, 251seq1i 13840 . . . . . . . . 9 (𝜑 → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
253249, 252eqtrid 2789 . . . . . . . 8 (𝜑 → (𝑇‘1) = ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1))))
254248, 253oveq12d 7359 . . . . . . 7 (𝜑 → ((𝑆‘1) + (𝑇‘1)) = (((2nd ‘(𝐹‘1)) − (1st ‘(𝐹‘1))) + ((2nd ‘(𝐺‘1)) − (1st ‘(𝐺‘1)))))
255243, 254eqtr4d 2780 . . . . . 6 (𝜑 → (𝑈‘(2 · 1)) = ((𝑆‘1) + (𝑇‘1)))
256 oveq1 7348 . . . . . . . . 9 ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
25734oveq2i 7352 . . . . . . . . . . . . 13 ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
258 2cnd 12156 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 2 ∈ ℂ)
25938recnd 11108 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
260 1cnd 11075 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → 1 ∈ ℂ)
261258, 259, 260adddid 11104 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
262 nnmulcl 12102 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
26327, 262mpan 688 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℕ)
264263adantl 483 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
265264nncnd 12094 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
266265, 260, 260addassd 11102 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
267257, 261, 2663eqtr4a 2803 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = (((2 · 𝑘) + 1) + 1))
268267fveq2d 6833 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = (𝑈‘(((2 · 𝑘) + 1) + 1)))
26920fveq1i 6830 . . . . . . . . . . . 12 (𝑈‘(((2 · 𝑘) + 1) + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1))
270264peano2nnd 12095 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
271270, 72eleqtrdi 2848 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ (ℤ‘1))
272 seqp1 13841 . . . . . . . . . . . . . 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 2848 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2 · 𝑘) ∈ (ℤ‘1))
275 seqp1 13841 . . . . . . . . . . . . . . . 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 6830 . . . . . . . . . . . . . . . . 17 (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘))
278277a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)))
279 oveq1 7348 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 / 2) = (((2 · 𝑘) + 1) / 2))
280279eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
281279fveq2d 6833 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑘) + 1) / 2)))
282 oveq1 7348 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = ((2 · 𝑘) + 1) → (𝑛 + 1) = (((2 · 𝑘) + 1) + 1))
283282fvoveq1d 7363 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = ((2 · 𝑘) + 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
284280, 281, 283ifbieq12d 4505 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = ((2 · 𝑘) + 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))))
285 fvex 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺‘(((2 · 𝑘) + 1) / 2)) ∈ V
286 fvex 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) ∈ V
287285, 286ifex 4527 . . . . . . . . . . . . . . . . . . . . . 22 if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) ∈ V
288284, 17, 287fvmpt 6935 . . . . . . . . . . . . . . . . . . . . 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 12182 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ≠ 0
291290a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → 2 ≠ 0)
292259, 258, 291divcan3d 11861 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) = 𝑘)
293292, 71eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · 𝑘) / 2) ∈ ℕ)
294 nneo 12509 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 · 𝑘) ∈ ℕ → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
295264, 294syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ))
296293, 295mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ¬ (((2 · 𝑘) + 1) / 2) ∈ ℕ)
297296iffalsed 4488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → if((((2 · 𝑘) + 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑘) + 1) / 2)), (𝐹‘((((2 · 𝑘) + 1) + 1) / 2))) = (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)))
298267oveq1d 7356 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = ((((2 · 𝑘) + 1) + 1) / 2))
29929nncnd 12094 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
300 2cn 12153 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℂ
301 divcan3 11764 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
302300, 290, 301mp3an23 1453 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 + 1) ∈ ℂ → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
303299, 302syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) = (𝑘 + 1))
304298, 303eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → ((((2 · 𝑘) + 1) + 1) / 2) = (𝑘 + 1))
305304fveq2d 6833 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (𝐹‘((((2 · 𝑘) + 1) + 1) / 2)) = (𝐹‘(𝑘 + 1)))
306289, 297, 3053eqtrd 2781 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐻‘((2 · 𝑘) + 1)) = (𝐹‘(𝑘 + 1)))
307306fveq2d 6833 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘((2 · 𝑘) + 1))) = (2nd ‘(𝐹‘(𝑘 + 1))))
308306fveq2d 6833 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘((2 · 𝑘) + 1))) = (1st ‘(𝐹‘(𝑘 + 1))))
309307, 308oveq12d 7359 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
31019ovolfsval 24739 . . . . . . . . . . . . . . . . . 18 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ((2 · 𝑘) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
31118, 270, 310syl2an2r 683 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)) = ((2nd ‘(𝐻‘((2 · 𝑘) + 1))) − (1st ‘(𝐻‘((2 · 𝑘) + 1)))))
312101ovolfsval 24739 . . . . . . . . . . . . . . . . . 18 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
31312, 28, 312syl2an 597 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = ((2nd ‘(𝐹‘(𝑘 + 1))) − (1st ‘(𝐹‘(𝑘 + 1)))))
314309, 311, 3133eqtr4rd 2788 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) = (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1)))
315278, 314oveq12d 7359 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐻)‘((2 · 𝑘) + 1))))
316276, 315eqtr4d 2780 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) = ((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
317267fveq2d 6833 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐻‘(((2 · 𝑘) + 1) + 1)))
318270peano2nnd 12095 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) ∈ ℕ)
319267, 318eqeltrd 2838 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) ∈ ℕ)
320 oveq1 7348 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 / 2) = ((2 · (𝑘 + 1)) / 2))
321320eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · (𝑘 + 1)) / 2) ∈ ℕ))
322320fveq2d 6833 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
323 oveq1 7348 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = (2 · (𝑘 + 1)) → (𝑛 + 1) = ((2 · (𝑘 + 1)) + 1))
324323fvoveq1d 7363 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = (2 · (𝑘 + 1)) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)))
325321, 322, 324ifbieq12d 4505 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = (2 · (𝑘 + 1)) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))))
326 fvex 6842 . . . . . . . . . . . . . . . . . . . . . 22 (𝐺‘((2 · (𝑘 + 1)) / 2)) ∈ V
327 fvex 6842 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2)) ∈ V
328326, 327ifex 4527 . . . . . . . . . . . . . . . . . . . . 21 if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) ∈ V
329325, 17, 328fvmpt 6935 . . . . . . . . . . . . . . . . . . . 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 2838 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ℕ) → ((2 · (𝑘 + 1)) / 2) ∈ ℕ)
332331iftrued 4485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → if(((2 · (𝑘 + 1)) / 2) ∈ ℕ, (𝐺‘((2 · (𝑘 + 1)) / 2)), (𝐹‘(((2 · (𝑘 + 1)) + 1) / 2))) = (𝐺‘((2 · (𝑘 + 1)) / 2)))
333303fveq2d 6833 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐺‘((2 · (𝑘 + 1)) / 2)) = (𝐺‘(𝑘 + 1)))
334330, 332, 3333eqtrd 2781 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(2 · (𝑘 + 1))) = (𝐺‘(𝑘 + 1)))
335317, 334eqtr3d 2779 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝐻‘(((2 · 𝑘) + 1) + 1)) = (𝐺‘(𝑘 + 1)))
336335fveq2d 6833 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (2nd ‘(𝐺‘(𝑘 + 1))))
337335fveq2d 6833 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) = (1st ‘(𝐺‘(𝑘 + 1))))
338336, 337oveq12d 7359 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
33919ovolfsval 24739 . . . . . . . . . . . . . . . 16 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (((2 · 𝑘) + 1) + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
34018, 318, 339syl2an2r 683 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = ((2nd ‘(𝐻‘(((2 · 𝑘) + 1) + 1))) − (1st ‘(𝐻‘(((2 · 𝑘) + 1) + 1)))))
341112ovolfsval 24739 . . . . . . . . . . . . . . . 16 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
3423, 28, 341syl2an 597 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) = ((2nd ‘(𝐺‘(𝑘 + 1))) − (1st ‘(𝐺‘(𝑘 + 1)))))
343338, 340, 3423eqtr4d 2787 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1)) = (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
344316, 343oveq12d 7359 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → ((seq1( + , ((abs ∘ − ) ∘ 𝐻))‘((2 · 𝑘) + 1)) + (((abs ∘ − ) ∘ 𝐻)‘(((2 · 𝑘) + 1) + 1))) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
345273, 344eqtrd 2777 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
346269, 345eqtrid 2789 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(((2 · 𝑘) + 1) + 1)) = (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
347 ffvelcdm 7019 . . . . . . . . . . . . . . 15 ((𝑈:ℕ⟶(0[,)+∞) ∧ (2 · 𝑘) ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
34822, 263, 347syl2an 597 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ (0[,)+∞))
34923, 348sselid 3933 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℝ)
350349recnd 11108 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · 𝑘)) ∈ ℂ)
351101ovolfsf 24740 . . . . . . . . . . . . . . . 16 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
35212, 351syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
353 ffvelcdm 7019 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
354352, 28, 353syl2an 597 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ (0[,)+∞))
35523, 354sselid 3933 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℝ)
356355recnd 11108 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) ∈ ℂ)
357112ovolfsf 24740 . . . . . . . . . . . . . . . 16 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
3583, 357syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
359 ffvelcdm 7019 . . . . . . . . . . . . . . 15 ((((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) ∧ (𝑘 + 1) ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
360358, 28, 359syl2an 597 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ (0[,)+∞))
36123, 360sselid 3933 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℝ)
362361recnd 11108 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)) ∈ ℂ)
363350, 356, 362addassd 11102 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑈‘(2 · 𝑘)) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
364268, 346, 3633eqtrd 2781 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
365 seqp1 13841 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
36673, 365syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
367102fveq1i 6830 . . . . . . . . . . . . 13 (𝑆‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘(𝑘 + 1))
368102fveq1i 6830 . . . . . . . . . . . . . 14 (𝑆𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
369368oveq1i 7351 . . . . . . . . . . . . 13 ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)))
370366, 367, 3693eqtr4g 2802 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))))
371 seqp1 13841 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘1) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
37273, 371syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
373113fveq1i 6830 . . . . . . . . . . . . 13 (𝑇‘(𝑘 + 1)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑘 + 1))
374113fveq1i 6830 . . . . . . . . . . . . . 14 (𝑇𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
375374oveq1i 7351 . . . . . . . . . . . . 13 ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))
376372, 373, 3753eqtr4g 2802 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇‘(𝑘 + 1)) = ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))
377370, 376oveq12d 7359 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
378104ffvelcdmda 7021 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ (0[,)+∞))
37923, 378sselid 3933 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
380379recnd 11108 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℂ)
381115ffvelcdmda 7021 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ (0[,)+∞))
38223, 381sselid 3933 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℝ)
383382recnd 11108 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ∈ ℂ)
384380, 356, 383, 362add4d 11308 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (((𝑆𝑘) + (((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1))) + ((𝑇𝑘) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
385377, 384eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))))
386364, 385eqeq12d 2753 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))) ↔ ((𝑈‘(2 · 𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1)))) = (((𝑆𝑘) + (𝑇𝑘)) + ((((abs ∘ − ) ∘ 𝐹)‘(𝑘 + 1)) + (((abs ∘ − ) ∘ 𝐺)‘(𝑘 + 1))))))
387256, 386syl5ibr 246 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1)))))
388387expcom 415 . . . . . . 7 (𝑘 ∈ ℕ → (𝜑 → ((𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘)) → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
389388a2d 29 . . . . . 6 (𝑘 ∈ ℕ → ((𝜑 → (𝑈‘(2 · 𝑘)) = ((𝑆𝑘) + (𝑇𝑘))) → (𝜑 → (𝑈‘(2 · (𝑘 + 1))) = ((𝑆‘(𝑘 + 1)) + (𝑇‘(𝑘 + 1))))))
390175, 182, 189, 196, 255, 389nnind 12096 . . . . 5 ((⌊‘((𝑘 + 1) / 2)) ∈ ℕ → (𝜑 → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2))))))
391390impcom 409 . . . 4 ((𝜑 ∧ (⌊‘((𝑘 + 1) / 2)) ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
39257, 391syldan 592 . . 3 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) = ((𝑆‘(⌊‘((𝑘 + 1) / 2))) + (𝑇‘(⌊‘((𝑘 + 1) / 2)))))
39363adantr 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
394393recnd 11108 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐴) ∈ ℂ)
39568adantr 482 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℝ)
396395rehalfcld 12325 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℝ)
397396recnd 11108 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝐶 / 2) ∈ ℂ)
39865adantr 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℝ)
399398recnd 11108 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (vol*‘𝐵) ∈ ℂ)
400394, 397, 399, 397add4d 11308 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))))
401395recnd 11108 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
4024012halvesd 12324 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
403402oveq2d 7357 . . . 4 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + ((𝐶 / 2) + (𝐶 / 2))) = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
404400, 403eqtr2d 2778 . . 3 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) = (((vol*‘𝐴) + (𝐶 / 2)) + ((vol*‘𝐵) + (𝐶 / 2))))
405168, 392, 4043brtr4d 5128 . 2 ((𝜑𝑘 ∈ ℕ) → (𝑈‘(2 · (⌊‘((𝑘 + 1) / 2)))) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
40626, 61, 70, 100, 405letrd 11237 1 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1541  wcel 2106  wne 2941  cin 3900  wss 3901  c0 4273  ifcif 4477   cuni 4856   class class class wbr 5096  cmpt 5179   × cxp 5622  dom cdm 5624  ran crn 5625  ccom 5628   Fn wfn 6478  wf 6479  cfv 6483  (class class class)co 7341  1st c1st 7901  2nd c2nd 7902  m cmap 8690  supcsup 9301  cc 10974  cr 10975  0cc0 10976  1c1 10977   + caddc 10979   · cmul 10981  +∞cpnf 11111  -∞cmnf 11112  *cxr 11113   < clt 11114  cle 11115  cmin 11310   / cdiv 11737  cn 12078  2c2 12133  cz 12424  cuz 12687  +crp 12835  (,)cioo 13184  [,)cico 13186  ...cfz 13344  cfl 13615  seqcseq 13826  abscabs 15044  vol*covol 24731
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-cnex 11032  ax-resscn 11033  ax-1cn 11034  ax-icn 11035  ax-addcl 11036  ax-addrcl 11037  ax-mulcl 11038  ax-mulrcl 11039  ax-mulcom 11040  ax-addass 11041  ax-mulass 11042  ax-distr 11043  ax-i2m1 11044  ax-1ne0 11045  ax-1rid 11046  ax-rnegex 11047  ax-rrecex 11048  ax-cnre 11049  ax-pre-lttri 11050  ax-pre-lttrn 11051  ax-pre-ltadd 11052  ax-pre-mulgt0 11053  ax-pre-sup 11054
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3920  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-iun 4947  df-br 5097  df-opab 5159  df-mpt 5180  df-tr 5214  df-id 5522  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5579  df-we 5581  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6242  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-riota 7297  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7785  df-1st 7903  df-2nd 7904  df-frecs 8171  df-wrecs 8202  df-recs 8276  df-rdg 8315  df-er 8573  df-map 8692  df-en 8809  df-dom 8810  df-sdom 8811  df-sup 9303  df-inf 9304  df-pnf 11116  df-mnf 11117  df-xr 11118  df-ltxr 11119  df-le 11120  df-sub 11312  df-neg 11313  df-div 11738  df-nn 12079  df-2 12141  df-3 12142  df-n0 12339  df-z 12425  df-uz 12688  df-rp 12836  df-ico 13190  df-fz 13345  df-fl 13617  df-seq 13827  df-exp 13888  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046
This theorem is referenced by:  ovolunlem1  24766
  Copyright terms: Public domain W3C validator