Metamath Proof Explorer

Theorem ovolunlem1a

Description: Lemma for ovolun . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses ovolun.a ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) )
ovolun.b ⊢ ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
ovolun.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
ovolun.s ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
ovolun.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
ovolun.u ⊢ 𝑈 = seq 1 ( + , ( ( 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 ovolunlem1a ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ovolun.a ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) )
2 ovolun.b ⊢ ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
3 ovolun.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4 ovolun.s ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
5 ovolun.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
6 ovolun.u ⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
7 ovolun.f1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
8 ovolun.f2 ⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
9 ovolun.f3 ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) )
10 ovolun.g1 ⊢ ( 𝜑 → 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
11 ovolun.g2 ⊢ ( 𝜑 → 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
12 ovolun.g3 ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) )
13 ovolun.h ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) )
14 elovolmlem ⊢ ( 𝐺 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
15 10 14 sylib ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
17 16 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑛 / 2 ) ∈ ℕ ) → ( 𝐺 ‘ ( 𝑛 / 2 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
18 nneo ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ ) )
20 19 con2bid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ ↔ ¬ ( 𝑛 / 2 ) ∈ ℕ ) )
21 20 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝑛 / 2 ) ∈ ℕ ) → ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ )
22 elovolmlem ⊢ ( 𝐹 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
23 7 22 sylib ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
25 24 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑛 + 1 ) / 2 ) ∈ ℕ ) → ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
26 21 25 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝑛 / 2 ) ∈ ℕ ) → ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
27 17 26 ifclda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
28 27 13 fmptd ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
29 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐻 ) = ( ( abs ∘ − ) ∘ 𝐻 )
30 29 6 ovolsf ⊢ ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) )
31 28 30 syl ⊢ ( 𝜑 → 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) )
32 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
33 fss ⊢ ( ( 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝑈 : ℕ ⟶ ℝ )
34 31 32 33 sylancl ⊢ ( 𝜑 → 𝑈 : ℕ ⟶ ℝ )
35 34 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ 𝑘 ) ∈ ℝ )
36 2nn ⊢ 2 ∈ ℕ
37 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
39 38 nnred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℝ )
40 39 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 1 ) / 2 ) ∈ ℝ )
41 40 flcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ∈ ℤ )
42 ax-1cn ⊢ 1 ∈ ℂ
43 42 2timesi ⊢ ( 2 · 1 ) = ( 1 + 1 )
44 nnge1 ⊢ ( 𝑘 ∈ ℕ → 1 ≤ 𝑘 )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 1 ≤ 𝑘 )
46 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ )
48 1re ⊢ 1 ∈ ℝ
49 leadd1 ⊢ ( ( 1 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 ≤ 𝑘 ↔ ( 1 + 1 ) ≤ ( 𝑘 + 1 ) ) )
50 48 48 49 mp3an13 ⊢ ( 𝑘 ∈ ℝ → ( 1 ≤ 𝑘 ↔ ( 1 + 1 ) ≤ ( 𝑘 + 1 ) ) )
51 47 50 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 ≤ 𝑘 ↔ ( 1 + 1 ) ≤ ( 𝑘 + 1 ) ) )
52 45 51 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 + 1 ) ≤ ( 𝑘 + 1 ) )
53 43 52 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · 1 ) ≤ ( 𝑘 + 1 ) )
54 2re ⊢ 2 ∈ ℝ
55 2pos ⊢ 0 < 2
56 54 55 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
57 lemuldiv2 ⊢ ( ( 1 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 1 ) ≤ ( 𝑘 + 1 ) ↔ 1 ≤ ( ( 𝑘 + 1 ) / 2 ) ) )
58 48 56 57 mp3an13 ⊢ ( ( 𝑘 + 1 ) ∈ ℝ → ( ( 2 · 1 ) ≤ ( 𝑘 + 1 ) ↔ 1 ≤ ( ( 𝑘 + 1 ) / 2 ) ) )
59 39 58 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 1 ) ≤ ( 𝑘 + 1 ) ↔ 1 ≤ ( ( 𝑘 + 1 ) / 2 ) ) )
60 53 59 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 1 ≤ ( ( 𝑘 + 1 ) / 2 ) )
61 1z ⊢ 1 ∈ ℤ
62 flge ⊢ ( ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( 1 ≤ ( ( 𝑘 + 1 ) / 2 ) ↔ 1 ≤ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) )
63 40 61 62 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 ≤ ( ( 𝑘 + 1 ) / 2 ) ↔ 1 ≤ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) )
64 60 63 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 1 ≤ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) )
65 elnnz1 ⊢ ( ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ∈ ℕ ↔ ( ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ∈ ℤ ∧ 1 ≤ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) )
66 41 64 65 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ∈ ℕ )
67 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ∈ ℕ ) → ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ℕ )
68 36 66 67 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ℕ )
69 34 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ℕ ) → ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ∈ ℝ )
70 68 69 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ∈ ℝ )
71 1 simprd ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ∈ ℝ )
72 2 simprd ⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) ∈ ℝ )
73 71 72 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ )
74 3 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
75 73 74 readdcld ⊢ ( 𝜑 → ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ∈ ℝ )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ∈ ℝ )
77 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
78 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
79 77 78 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
80 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
81 80 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
82 flhalf ⊢ ( 𝑘 ∈ ℤ → 𝑘 ≤ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) )
83 81 82 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ≤ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) )
84 nnz ⊢ ( ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ℕ → ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ℤ )
85 eluz ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ℤ ) → ( ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ( ℤ≥ ‘ 𝑘 ) ↔ 𝑘 ≤ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) )
86 80 84 85 syl2an ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ℕ ) → ( ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ( ℤ≥ ‘ 𝑘 ) ↔ 𝑘 ≤ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) )
87 77 68 86 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ( ℤ≥ ‘ 𝑘 ) ↔ 𝑘 ≤ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) )
88 83 87 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ( ℤ≥ ‘ 𝑘 ) )
89 elfznn ⊢ ( 𝑗 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) → 𝑗 ∈ ℕ )
90 29 ovolfsf ⊢ ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐻 ) : ℕ ⟶ ( 0 [,) +∞ ) )
91 28 90 syl ⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐻 ) : ℕ ⟶ ( 0 [,) +∞ ) )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( abs ∘ − ) ∘ 𝐻 ) : ℕ ⟶ ( 0 [,) +∞ ) )
93 92 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) )
94 elrege0 ⊢ ( ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) ) )
95 93 94 sylib ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) ∈ ℝ ∧ 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) ) )
96 95 simpld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) ∈ ℝ )
97 89 96 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) ∈ ℝ )
98 elfzuz ⊢ ( 𝑗 ∈ ( ( 𝑘 + 1 ) ... ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
99 eluznn ⊢ ( ( ( 𝑘 + 1 ) ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑗 ∈ ℕ )
100 38 98 99 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 𝑘 + 1 ) ... ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ) → 𝑗 ∈ ℕ )
101 95 simprd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) )
102 100 101 syldan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ( 𝑘 + 1 ) ... ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ) → 0 ≤ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑗 ) )
103 79 88 97 102 sermono ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑘 ) ≤ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) )
104 6 fveq1i ⊢ ( 𝑈 ‘ 𝑘 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 𝑘 )
105 6 fveq1i ⊢ ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) )
106 103 104 105 3brtr4g ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ 𝑘 ) ≤ ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) )
107 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
108 107 4 ovolsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
109 23 108 syl ⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
110 109 frnd ⊢ ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
111 110 32 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ )
112 111 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ran 𝑆 ⊆ ℝ )
113 109 ffnd ⊢ ( 𝜑 → 𝑆 Fn ℕ )
114 fnfvelrn ⊢ ( ( 𝑆 Fn ℕ ∧ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ∈ ℕ ) → ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ran 𝑆 )
115 113 66 114 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ran 𝑆 )
116 112 115 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ℝ )
117 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
118 117 5 ovolsf ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
119 15 118 syl ⊢ ( 𝜑 → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
120 119 frnd ⊢ ( 𝜑 → ran 𝑇 ⊆ ( 0 [,) +∞ ) )
121 120 32 sstrdi ⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ran 𝑇 ⊆ ℝ )
123 119 ffnd ⊢ ( 𝜑 → 𝑇 Fn ℕ )
124 fnfvelrn ⊢ ( ( 𝑇 Fn ℕ ∧ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ∈ ℕ ) → ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ran 𝑇 )
125 123 66 124 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ran 𝑇 )
126 122 125 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ℝ )
127 74 rehalfcld ⊢ ( 𝜑 → ( 𝐶 / 2 ) ∈ ℝ )
128 71 127 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ∈ ℝ )
129 128 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ∈ ℝ )
130 72 127 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ∈ ℝ )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ∈ ℝ )
132 ressxr ⊢ ℝ ⊆ ℝ*
133 111 132 sstrdi ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ* )
134 supxrcl ⊢ ( ran 𝑆 ⊆ ℝ* → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
135 133 134 syl ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
136 1nn ⊢ 1 ∈ ℕ
137 109 fdmd ⊢ ( 𝜑 → dom 𝑆 = ℕ )
138 136 137 eleqtrrid ⊢ ( 𝜑 → 1 ∈ dom 𝑆 )
139 138 ne0d ⊢ ( 𝜑 → dom 𝑆 ≠ ∅ )
140 dm0rn0 ⊢ ( dom 𝑆 = ∅ ↔ ran 𝑆 = ∅ )
141 140 necon3bii ⊢ ( dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅ )
142 139 141 sylib ⊢ ( 𝜑 → ran 𝑆 ≠ ∅ )
143 supxrgtmnf ⊢ ( ( ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ) → -∞ < sup ( ran 𝑆 , ℝ* , < ) )
144 111 142 143 syl2anc ⊢ ( 𝜑 → -∞ < sup ( ran 𝑆 , ℝ* , < ) )
145 xrre ⊢ ( ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* ∧ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ∈ ℝ ) ∧ ( -∞ < sup ( ran 𝑆 , ℝ* , < ) ∧ sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
146 135 128 144 9 145 syl22anc ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
147 146 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
148 supxrub ⊢ ( ( ran 𝑆 ⊆ ℝ* ∧ ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ran 𝑆 ) → ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
149 133 115 148 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
150 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) )
151 116 147 129 149 150 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) )
152 121 132 sstrdi ⊢ ( 𝜑 → ran 𝑇 ⊆ ℝ* )
153 supxrcl ⊢ ( ran 𝑇 ⊆ ℝ* → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
154 152 153 syl ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
155 119 fdmd ⊢ ( 𝜑 → dom 𝑇 = ℕ )
156 136 155 eleqtrrid ⊢ ( 𝜑 → 1 ∈ dom 𝑇 )
157 156 ne0d ⊢ ( 𝜑 → dom 𝑇 ≠ ∅ )
158 dm0rn0 ⊢ ( dom 𝑇 = ∅ ↔ ran 𝑇 = ∅ )
159 158 necon3bii ⊢ ( dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅ )
160 157 159 sylib ⊢ ( 𝜑 → ran 𝑇 ≠ ∅ )
161 supxrgtmnf ⊢ ( ( ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ) → -∞ < sup ( ran 𝑇 , ℝ* , < ) )
162 121 160 161 syl2anc ⊢ ( 𝜑 → -∞ < sup ( ran 𝑇 , ℝ* , < ) )
163 xrre ⊢ ( ( ( sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* ∧ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ∈ ℝ ) ∧ ( -∞ < sup ( ran 𝑇 , ℝ* , < ) ∧ sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
164 154 130 162 12 163 syl22anc ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
165 164 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
166 supxrub ⊢ ( ( ran 𝑇 ⊆ ℝ* ∧ ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ∈ ran 𝑇 ) → ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
167 152 125 166 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
168 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) )
169 126 165 131 167 168 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) )
170 116 126 129 131 151 169 le2addd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) + ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) + ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) )
171 oveq2 ⊢ ( 𝑧 = 1 → ( 2 · 𝑧 ) = ( 2 · 1 ) )
172 171 fveq2d ⊢ ( 𝑧 = 1 → ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( 𝑈 ‘ ( 2 · 1 ) ) )
173 fveq2 ⊢ ( 𝑧 = 1 → ( 𝑆 ‘ 𝑧 ) = ( 𝑆 ‘ 1 ) )
174 fveq2 ⊢ ( 𝑧 = 1 → ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 1 ) )
175 173 174 oveq12d ⊢ ( 𝑧 = 1 → ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑆 ‘ 1 ) + ( 𝑇 ‘ 1 ) ) )
176 172 175 eqeq12d ⊢ ( 𝑧 = 1 → ( ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) ↔ ( 𝑈 ‘ ( 2 · 1 ) ) = ( ( 𝑆 ‘ 1 ) + ( 𝑇 ‘ 1 ) ) ) )
177 176 imbi2d ⊢ ( 𝑧 = 1 → ( ( 𝜑 → ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( 𝑈 ‘ ( 2 · 1 ) ) = ( ( 𝑆 ‘ 1 ) + ( 𝑇 ‘ 1 ) ) ) ) )
178 oveq2 ⊢ ( 𝑧 = 𝑘 → ( 2 · 𝑧 ) = ( 2 · 𝑘 ) )
179 178 fveq2d ⊢ ( 𝑧 = 𝑘 → ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( 𝑈 ‘ ( 2 · 𝑘 ) ) )
180 fveq2 ⊢ ( 𝑧 = 𝑘 → ( 𝑆 ‘ 𝑧 ) = ( 𝑆 ‘ 𝑘 ) )
181 fveq2 ⊢ ( 𝑧 = 𝑘 → ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑘 ) )
182 180 181 oveq12d ⊢ ( 𝑧 = 𝑘 → ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) )
183 179 182 eqeq12d ⊢ ( 𝑧 = 𝑘 → ( ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) ↔ ( 𝑈 ‘ ( 2 · 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) ) )
184 183 imbi2d ⊢ ( 𝑧 = 𝑘 → ( ( 𝜑 → ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( 𝑈 ‘ ( 2 · 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) ) ) )
185 oveq2 ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( 2 · 𝑧 ) = ( 2 · ( 𝑘 + 1 ) ) )
186 185 fveq2d ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( 𝑈 ‘ ( 2 · ( 𝑘 + 1 ) ) ) )
187 fveq2 ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( 𝑆 ‘ 𝑧 ) = ( 𝑆 ‘ ( 𝑘 + 1 ) ) )
188 fveq2 ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ ( 𝑘 + 1 ) ) )
189 187 188 oveq12d ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) + ( 𝑇 ‘ ( 𝑘 + 1 ) ) ) )
190 186 189 eqeq12d ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) ↔ ( 𝑈 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) + ( 𝑇 ‘ ( 𝑘 + 1 ) ) ) ) )
191 190 imbi2d ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( 𝑈 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) + ( 𝑇 ‘ ( 𝑘 + 1 ) ) ) ) ) )
192 oveq2 ⊢ ( 𝑧 = ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) → ( 2 · 𝑧 ) = ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) )
193 192 fveq2d ⊢ ( 𝑧 = ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) → ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) )
194 fveq2 ⊢ ( 𝑧 = ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) → ( 𝑆 ‘ 𝑧 ) = ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) )
195 fveq2 ⊢ ( 𝑧 = ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) → ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) )
196 194 195 oveq12d ⊢ ( 𝑧 = ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) → ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) + ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) )
197 193 196 eqeq12d ⊢ ( 𝑧 = ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) → ( ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) ↔ ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) = ( ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) + ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ) )
198 197 imbi2d ⊢ ( 𝑧 = ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) → ( ( 𝜑 → ( 𝑈 ‘ ( 2 · 𝑧 ) ) = ( ( 𝑆 ‘ 𝑧 ) + ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) = ( ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) + ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ) ) )
199 6 fveq1i ⊢ ( 𝑈 ‘ ( 2 · 1 ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( 2 · 1 ) )
200 136 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
201 29 ovolfsval ⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 1 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐻 ‘ 1 ) ) − ( 1st ‘ ( 𝐻 ‘ 1 ) ) ) )
202 28 136 201 sylancl ⊢ ( 𝜑 → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐻 ‘ 1 ) ) − ( 1st ‘ ( 𝐻 ‘ 1 ) ) ) )
203 halfnz ⊢ ¬ ( 1 / 2 ) ∈ ℤ
204 nnz ⊢ ( ( 𝑛 / 2 ) ∈ ℕ → ( 𝑛 / 2 ) ∈ ℤ )
205 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 / 2 ) = ( 1 / 2 ) )
206 205 eleq1d ⊢ ( 𝑛 = 1 → ( ( 𝑛 / 2 ) ∈ ℤ ↔ ( 1 / 2 ) ∈ ℤ ) )
207 204 206 syl5ib ⊢ ( 𝑛 = 1 → ( ( 𝑛 / 2 ) ∈ ℕ → ( 1 / 2 ) ∈ ℤ ) )
208 203 207 mtoi ⊢ ( 𝑛 = 1 → ¬ ( 𝑛 / 2 ) ∈ ℕ )
209 208 iffalsed ⊢ ( 𝑛 = 1 → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) = ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) )
210 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 + 1 ) = ( 1 + 1 ) )
211 df-2 ⊢ 2 = ( 1 + 1 )
212 210 211 eqtr4di ⊢ ( 𝑛 = 1 → ( 𝑛 + 1 ) = 2 )
213 212 oveq1d ⊢ ( 𝑛 = 1 → ( ( 𝑛 + 1 ) / 2 ) = ( 2 / 2 ) )
214 2div2e1 ⊢ ( 2 / 2 ) = 1
215 213 214 eqtrdi ⊢ ( 𝑛 = 1 → ( ( 𝑛 + 1 ) / 2 ) = 1 )
216 215 fveq2d ⊢ ( 𝑛 = 1 → ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) = ( 𝐹 ‘ 1 ) )
217 209 216 eqtrd ⊢ ( 𝑛 = 1 → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) = ( 𝐹 ‘ 1 ) )
218 fvex ⊢ ( 𝐹 ‘ 1 ) ∈ V
219 217 13 218 fvmpt ⊢ ( 1 ∈ ℕ → ( 𝐻 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
220 136 219 ax-mp ⊢ ( 𝐻 ‘ 1 ) = ( 𝐹 ‘ 1 )
221 220 fveq2i ⊢ ( 2nd ‘ ( 𝐻 ‘ 1 ) ) = ( 2nd ‘ ( 𝐹 ‘ 1 ) )
222 220 fveq2i ⊢ ( 1st ‘ ( 𝐻 ‘ 1 ) ) = ( 1st ‘ ( 𝐹 ‘ 1 ) )
223 221 222 oveq12i ⊢ ( ( 2nd ‘ ( 𝐻 ‘ 1 ) ) − ( 1st ‘ ( 𝐻 ‘ 1 ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) )
224 202 223 eqtrdi ⊢ ( 𝜑 → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) ) )
225 61 224 seq1i ⊢ ( 𝜑 → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) ) )
226 2t1e2 ⊢ ( 2 · 1 ) = 2
227 226 fveq2i ⊢ ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( 2 · 1 ) ) = ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 2 )
228 29 ovolfsval ⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 2 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 2 ) = ( ( 2nd ‘ ( 𝐻 ‘ 2 ) ) − ( 1st ‘ ( 𝐻 ‘ 2 ) ) ) )
229 28 36 228 sylancl ⊢ ( 𝜑 → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 2 ) = ( ( 2nd ‘ ( 𝐻 ‘ 2 ) ) − ( 1st ‘ ( 𝐻 ‘ 2 ) ) ) )
230 oveq1 ⊢ ( 𝑛 = 2 → ( 𝑛 / 2 ) = ( 2 / 2 ) )
231 230 214 eqtrdi ⊢ ( 𝑛 = 2 → ( 𝑛 / 2 ) = 1 )
232 231 136 eqeltrdi ⊢ ( 𝑛 = 2 → ( 𝑛 / 2 ) ∈ ℕ )
233 232 iftrued ⊢ ( 𝑛 = 2 → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) = ( 𝐺 ‘ ( 𝑛 / 2 ) ) )
234 231 fveq2d ⊢ ( 𝑛 = 2 → ( 𝐺 ‘ ( 𝑛 / 2 ) ) = ( 𝐺 ‘ 1 ) )
235 233 234 eqtrd ⊢ ( 𝑛 = 2 → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) = ( 𝐺 ‘ 1 ) )
236 fvex ⊢ ( 𝐺 ‘ 1 ) ∈ V
237 235 13 236 fvmpt ⊢ ( 2 ∈ ℕ → ( 𝐻 ‘ 2 ) = ( 𝐺 ‘ 1 ) )
238 36 237 ax-mp ⊢ ( 𝐻 ‘ 2 ) = ( 𝐺 ‘ 1 )
239 238 fveq2i ⊢ ( 2nd ‘ ( 𝐻 ‘ 2 ) ) = ( 2nd ‘ ( 𝐺 ‘ 1 ) )
240 238 fveq2i ⊢ ( 1st ‘ ( 𝐻 ‘ 2 ) ) = ( 1st ‘ ( 𝐺 ‘ 1 ) )
241 239 240 oveq12i ⊢ ( ( 2nd ‘ ( 𝐻 ‘ 2 ) ) − ( 1st ‘ ( 𝐻 ‘ 2 ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) )
242 229 241 eqtrdi ⊢ ( 𝜑 → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 2 ) = ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) )
243 227 242 syl5eq ⊢ ( 𝜑 → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( 2 · 1 ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) )
244 78 200 43 225 243 seqp1d ⊢ ( 𝜑 → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( 2 · 1 ) ) = ( ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) ) + ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) ) )
245 199 244 syl5eq ⊢ ( 𝜑 → ( 𝑈 ‘ ( 2 · 1 ) ) = ( ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) ) + ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) ) )
246 4 fveq1i ⊢ ( 𝑆 ‘ 1 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 1 )
247 107 ovolfsval ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 1 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) ) )
248 23 136 247 sylancl ⊢ ( 𝜑 → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) ) )
249 61 248 seq1i ⊢ ( 𝜑 → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) ) )
250 246 249 syl5eq ⊢ ( 𝜑 → ( 𝑆 ‘ 1 ) = ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) ) )
251 5 fveq1i ⊢ ( 𝑇 ‘ 1 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 1 )
252 117 ovolfsval ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 1 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) )
253 15 136 252 sylancl ⊢ ( 𝜑 → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) )
254 61 253 seq1i ⊢ ( 𝜑 → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 1 ) = ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) )
255 251 254 syl5eq ⊢ ( 𝜑 → ( 𝑇 ‘ 1 ) = ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) )
256 250 255 oveq12d ⊢ ( 𝜑 → ( ( 𝑆 ‘ 1 ) + ( 𝑇 ‘ 1 ) ) = ( ( ( 2nd ‘ ( 𝐹 ‘ 1 ) ) − ( 1st ‘ ( 𝐹 ‘ 1 ) ) ) + ( ( 2nd ‘ ( 𝐺 ‘ 1 ) ) − ( 1st ‘ ( 𝐺 ‘ 1 ) ) ) ) )
257 245 256 eqtr4d ⊢ ( 𝜑 → ( 𝑈 ‘ ( 2 · 1 ) ) = ( ( 𝑆 ‘ 1 ) + ( 𝑇 ‘ 1 ) ) )
258 oveq1 ⊢ ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) → ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) + ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) )
259 43 oveq2i ⊢ ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) = ( ( 2 · 𝑘 ) + ( 1 + 1 ) )
260 2cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 2 ∈ ℂ )
261 47 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
262 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℂ )
263 260 261 262 adddid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · ( 𝑘 + 1 ) ) = ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) )
264 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℕ )
265 36 264 mpan ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℕ )
266 265 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℕ )
267 266 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℂ )
268 267 262 262 addassd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) = ( ( 2 · 𝑘 ) + ( 1 + 1 ) ) )
269 259 263 268 3eqtr4a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · ( 𝑘 + 1 ) ) = ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) )
270 269 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( 𝑈 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) )
271 6 fveq1i ⊢ ( 𝑈 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) )
272 266 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ )
273 272 78 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
274 seqp1 ⊢ ( ( ( 2 · 𝑘 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) )
275 273 274 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) )
276 266 78 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ( ℤ≥ ‘ 1 ) )
277 seqp1 ⊢ ( ( 2 · 𝑘 ) ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( 2 · 𝑘 ) ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
278 276 277 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( 2 · 𝑘 ) ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
279 6 fveq1i ⊢ ( 𝑈 ‘ ( 2 · 𝑘 ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( 2 · 𝑘 ) )
280 279 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( 2 · 𝑘 ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( 2 · 𝑘 ) ) )
281 oveq1 ⊢ ( 𝑛 = ( ( 2 · 𝑘 ) + 1 ) → ( 𝑛 / 2 ) = ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) )
282 281 eleq1d ⊢ ( 𝑛 = ( ( 2 · 𝑘 ) + 1 ) → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ∈ ℕ ) )
283 281 fveq2d ⊢ ( 𝑛 = ( ( 2 · 𝑘 ) + 1 ) → ( 𝐺 ‘ ( 𝑛 / 2 ) ) = ( 𝐺 ‘ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ) )
284 oveq1 ⊢ ( 𝑛 = ( ( 2 · 𝑘 ) + 1 ) → ( 𝑛 + 1 ) = ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) )
285 284 fvoveq1d ⊢ ( 𝑛 = ( ( 2 · 𝑘 ) + 1 ) → ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) = ( 𝐹 ‘ ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) ) )
286 282 283 285 ifbieq12d ⊢ ( 𝑛 = ( ( 2 · 𝑘 ) + 1 ) → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) = if ( ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) ) ) )
287 fvex ⊢ ( 𝐺 ‘ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ) ∈ V
288 fvex ⊢ ( 𝐹 ‘ ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) ) ∈ V
289 287 288 ifex ⊢ if ( ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) ) ) ∈ V
290 286 13 289 fvmpt ⊢ ( ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ → ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) = if ( ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) ) ) )
291 272 290 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) = if ( ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) ) ) )
292 2ne0 ⊢ 2 ≠ 0
293 292 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 2 ≠ 0 )
294 261 260 293 divcan3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) / 2 ) = 𝑘 )
295 294 77 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) / 2 ) ∈ ℕ )
296 nneo ⊢ ( ( 2 · 𝑘 ) ∈ ℕ → ( ( ( 2 · 𝑘 ) / 2 ) ∈ ℕ ↔ ¬ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ∈ ℕ ) )
297 266 296 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 2 · 𝑘 ) / 2 ) ∈ ℕ ↔ ¬ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ∈ ℕ ) )
298 295 297 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ¬ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ∈ ℕ )
299 298 iffalsed ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → if ( ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( ( 2 · 𝑘 ) + 1 ) / 2 ) ) , ( 𝐹 ‘ ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) ) ) = ( 𝐹 ‘ ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) ) )
300 269 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) = ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) )
301 38 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℂ )
302 2cn ⊢ 2 ∈ ℂ
303 divcan3 ⊢ ( ( ( 𝑘 + 1 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) = ( 𝑘 + 1 ) )
304 302 292 303 mp3an23 ⊢ ( ( 𝑘 + 1 ) ∈ ℂ → ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) = ( 𝑘 + 1 ) )
305 301 304 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) = ( 𝑘 + 1 ) )
306 300 305 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) = ( 𝑘 + 1 ) )
307 306 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) / 2 ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
308 291 299 307 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
309 308 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2nd ‘ ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( 2nd ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
310 308 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) = ( 1st ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
311 309 310 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) − ( 1st ‘ ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
312 29 ovolfsval ⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 2nd ‘ ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) − ( 1st ‘ ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
313 28 272 312 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 2nd ‘ ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) − ( 1st ‘ ( 𝐻 ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
314 107 ovolfsval ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( 2nd ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
315 23 37 314 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( 2nd ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) − ( 1st ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
316 311 313 315 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) )
317 280 316 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( 2 · 𝑘 ) ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) ) )
318 278 317 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) )
319 269 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) )
320 272 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ∈ ℕ )
321 269 320 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · ( 𝑘 + 1 ) ) ∈ ℕ )
322 oveq1 ⊢ ( 𝑛 = ( 2 · ( 𝑘 + 1 ) ) → ( 𝑛 / 2 ) = ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) )
323 322 eleq1d ⊢ ( 𝑛 = ( 2 · ( 𝑘 + 1 ) ) → ( ( 𝑛 / 2 ) ∈ ℕ ↔ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ∈ ℕ ) )
324 322 fveq2d ⊢ ( 𝑛 = ( 2 · ( 𝑘 + 1 ) ) → ( 𝐺 ‘ ( 𝑛 / 2 ) ) = ( 𝐺 ‘ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ) )
325 oveq1 ⊢ ( 𝑛 = ( 2 · ( 𝑘 + 1 ) ) → ( 𝑛 + 1 ) = ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) )
326 325 fvoveq1d ⊢ ( 𝑛 = ( 2 · ( 𝑘 + 1 ) ) → ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) = ( 𝐹 ‘ ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) / 2 ) ) )
327 323 324 326 ifbieq12d ⊢ ( 𝑛 = ( 2 · ( 𝑘 + 1 ) ) → if ( ( 𝑛 / 2 ) ∈ ℕ , ( 𝐺 ‘ ( 𝑛 / 2 ) ) , ( 𝐹 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) = if ( ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) / 2 ) ) ) )
328 fvex ⊢ ( 𝐺 ‘ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ) ∈ V
329 fvex ⊢ ( 𝐹 ‘ ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) / 2 ) ) ∈ V
330 328 329 ifex ⊢ if ( ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) / 2 ) ) ) ∈ V
331 327 13 330 fvmpt ⊢ ( ( 2 · ( 𝑘 + 1 ) ) ∈ ℕ → ( 𝐻 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = if ( ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) / 2 ) ) ) )
332 321 331 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = if ( ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) / 2 ) ) ) )
333 305 38 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ∈ ℕ )
334 333 iftrued ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → if ( ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ∈ ℕ , ( 𝐺 ‘ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ) , ( 𝐹 ‘ ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) / 2 ) ) ) = ( 𝐺 ‘ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ) )
335 305 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ ( ( 2 · ( 𝑘 + 1 ) ) / 2 ) ) = ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
336 332 334 335 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
337 319 336 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
338 337 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2nd ‘ ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) = ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
339 337 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) = ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
340 338 339 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) − ( 1st ‘ ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) )
341 29 ovolfsval ⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( ( 2nd ‘ ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) − ( 1st ‘ ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) ) )
342 28 320 341 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( ( 2nd ‘ ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) − ( 1st ‘ ( 𝐻 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) ) )
343 117 ovolfsval ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) = ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) )
344 15 37 343 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) = ( ( 2nd ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) − ( 1st ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) )
345 340 342 344 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) )
346 318 345 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( 2 · 𝑘 ) + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) ) = ( ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) )
347 275 346 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) ) ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) )
348 271 347 syl5eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) )
349 ffvelrn ⊢ ( ( 𝑈 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 2 · 𝑘 ) ∈ ℕ ) → ( 𝑈 ‘ ( 2 · 𝑘 ) ) ∈ ( 0 [,) +∞ ) )
350 31 265 349 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( 2 · 𝑘 ) ) ∈ ( 0 [,) +∞ ) )
351 32 350 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( 2 · 𝑘 ) ) ∈ ℝ )
352 351 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( 2 · 𝑘 ) ) ∈ ℂ )
353 107 ovolfsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
354 23 353 syl ⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
355 ffvelrn ⊢ ( ( ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 0 [,) +∞ ) )
356 354 37 355 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 0 [,) +∞ ) )
357 32 356 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
358 357 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
359 117 ovolfsf ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) )
360 15 359 syl ⊢ ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) )
361 ffvelrn ⊢ ( ( ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 0 [,) +∞ ) )
362 360 37 361 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ( 0 [,) +∞ ) )
363 32 362 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
364 363 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
365 352 358 364 addassd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) )
366 270 348 365 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) )
367 seqp1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) )
368 79 367 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) )
369 4 fveq1i ⊢ ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ ( 𝑘 + 1 ) )
370 4 fveq1i ⊢ ( 𝑆 ‘ 𝑘 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑘 )
371 370 oveq1i ⊢ ( ( 𝑆 ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) )
372 368 369 371 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) )
373 seqp1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) )
374 79 373 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) )
375 5 fveq1i ⊢ ( 𝑇 ‘ ( 𝑘 + 1 ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ ( 𝑘 + 1 ) )
376 5 fveq1i ⊢ ( 𝑇 ‘ 𝑘 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 )
377 376 oveq1i ⊢ ( ( 𝑇 ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) )
378 374 375 377 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑇 ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) )
379 372 378 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) + ( 𝑇 ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) + ( ( 𝑇 ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) )
380 109 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ( 0 [,) +∞ ) )
381 32 380 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ℝ )
382 381 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ℂ )
383 119 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ 𝑘 ) ∈ ( 0 [,) +∞ ) )
384 32 383 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ 𝑘 ) ∈ ℝ )
385 384 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ 𝑘 ) ∈ ℂ )
386 382 358 385 364 add4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑆 ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) + ( ( 𝑇 ‘ 𝑘 ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) + ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) )
387 379 386 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) + ( 𝑇 ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) + ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) )
388 366 387 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑈 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) + ( 𝑇 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) + ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) + ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ ( 𝑘 + 1 ) ) + ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ ( 𝑘 + 1 ) ) ) ) ) )
389 258 388 syl5ibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) → ( 𝑈 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) + ( 𝑇 ‘ ( 𝑘 + 1 ) ) ) ) )
390 389 expcom ⊢ ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( 𝑈 ‘ ( 2 · 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) → ( 𝑈 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) + ( 𝑇 ‘ ( 𝑘 + 1 ) ) ) ) ) )
391 390 a2d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝜑 → ( 𝑈 ‘ ( 2 · 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) + ( 𝑇 ‘ 𝑘 ) ) ) → ( 𝜑 → ( 𝑈 ‘ ( 2 · ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) + ( 𝑇 ‘ ( 𝑘 + 1 ) ) ) ) ) )
392 177 184 191 198 257 391 nnind ⊢ ( ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ∈ ℕ → ( 𝜑 → ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) = ( ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) + ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ) )
393 392 impcom ⊢ ( ( 𝜑 ∧ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ∈ ℕ ) → ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) = ( ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) + ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) )
394 66 393 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) = ( ( 𝑆 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) + ( 𝑇 ‘ ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) )
395 71 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
396 395 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℂ )
397 74 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐶 ∈ ℝ )
398 397 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐶 / 2 ) ∈ ℝ )
399 398 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐶 / 2 ) ∈ ℂ )
400 72 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol* ‘ 𝐵 ) ∈ ℝ )
401 400 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol* ‘ 𝐵 ) ∈ ℂ )
402 396 399 401 399 add4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) + ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) = ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) ) )
403 397 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐶 ∈ ℂ )
404 403 2halvesd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) = 𝐶 )
405 404 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) ) = ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )
406 402 405 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) = ( ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) + ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) )
407 170 394 406 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ ( 2 · ( ⌊ ‘ ( ( 𝑘 + 1 ) / 2 ) ) ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )
408 35 70 76 106 407 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑈 ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )