Metamath Proof Explorer

Theorem ioombl1lem3

Description: Lemma for ioombl1 . (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses ioombl1.b ⊢ 𝐵 = ( 𝐴 (,) +∞ )
ioombl1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ioombl1.e ⊢ ( 𝜑 → 𝐸 ⊆ ℝ )
ioombl1.v ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
ioombl1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
ioombl1.s ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
ioombl1.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
ioombl1.u ⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
ioombl1.f1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
ioombl1.f2 ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
ioombl1.f3 ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
ioombl1.p ⊢ 𝑃 = ( 1st ‘ ( 𝐹 ‘ 𝑛 ) )
ioombl1.q ⊢ 𝑄 = ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) )
ioombl1.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ )
ioombl1.h ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ )
Assertion ioombl1lem3 ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 ioombl1.b ⊢ 𝐵 = ( 𝐴 (,) +∞ )
2 ioombl1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ioombl1.e ⊢ ( 𝜑 → 𝐸 ⊆ ℝ )
4 ioombl1.v ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
5 ioombl1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
6 ioombl1.s ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
7 ioombl1.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
8 ioombl1.u ⊢ 𝑈 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐻 ) )
9 ioombl1.f1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
10 ioombl1.f2 ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
11 ioombl1.f3 ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
12 ioombl1.p ⊢ 𝑃 = ( 1st ‘ ( 𝐹 ‘ 𝑛 ) )
13 ioombl1.q ⊢ 𝑄 = ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) )
14 ioombl1.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ )
15 ioombl1.h ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ )
16 ovolfcl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
17 9 16 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
18 17 simp2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
19 13 18 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑄 ∈ ℝ )
20 19 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑄 ∈ ℂ )
21 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ )
22 17 simp1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
23 12 22 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ℝ )
24 21 23 ifcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ∈ ℝ )
25 24 19 ifcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ )
26 25 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℂ )
27 23 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑃 ∈ ℂ )
28 20 26 27 npncand ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑄 − if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) + ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) − 𝑃 ) ) = ( 𝑄 − 𝑃 ) )
29 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 ioombl1lem1 ⊢ ( 𝜑 → ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) )
30 29 simpld ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
31 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
32 31 ovolfsval ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
33 30 32 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
35 opex ⊢ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ∈ V
36 14 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ∈ V ) → ( 𝐺 ‘ 𝑛 ) = ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ )
37 34 35 36 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) = ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ )
38 37 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2nd ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) )
39 op2ndg ⊢ ( ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → ( 2nd ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) = 𝑄 )
40 25 19 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) = 𝑄 )
41 38 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) = 𝑄 )
42 37 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 1st ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) )
43 op1stg ⊢ ( ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ) → ( 1st ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
44 25 19 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ⟨ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) , 𝑄 ⟩ ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
45 42 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
46 41 45 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( 𝑄 − if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) )
47 33 46 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( 𝑄 − if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) )
48 29 simprd ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
49 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐻 ) = ( ( abs ∘ − ) ∘ 𝐻 )
50 49 ovolfsval ⊢ ( ( 𝐻 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ) )
51 48 50 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ) )
52 opex ⊢ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ∈ V
53 15 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ∈ V ) → ( 𝐻 ‘ 𝑛 ) = ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ )
54 34 52 53 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐻 ‘ 𝑛 ) = ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ )
55 54 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) = ( 2nd ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) )
56 op2ndg ⊢ ( ( 𝑃 ∈ ℝ ∧ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ) → ( 2nd ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
57 23 25 56 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
58 55 57 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) = if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) )
59 54 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) = ( 1st ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) )
60 op1stg ⊢ ( ( 𝑃 ∈ ℝ ∧ if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ∈ ℝ ) → ( 1st ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) = 𝑃 )
61 23 25 60 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ⟨ 𝑃 , if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ⟩ ) = 𝑃 )
62 59 61 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) = 𝑃 )
63 58 62 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐻 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐻 ‘ 𝑛 ) ) ) = ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) − 𝑃 ) )
64 51 63 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) = ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) − 𝑃 ) )
65 47 64 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) = ( ( 𝑄 − if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) ) + ( if ( if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) ≤ 𝑄 , if ( 𝑃 ≤ 𝐴 , 𝐴 , 𝑃 ) , 𝑄 ) − 𝑃 ) ) )
66 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
67 66 ovolfsval ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
68 9 67 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
69 13 12 oveq12i ⊢ ( 𝑄 − 𝑃 ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) )
70 68 69 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( 𝑄 − 𝑃 ) )
71 28 65 70 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) + ( ( ( abs ∘ − ) ∘ 𝐻 ) ‘ 𝑛 ) ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )