This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgeqa

Description: Approximate equality of integrals. If C ( x ) = D ( x ) for almost all x , then S. B C ( x )d x = S. B D ( x ) d x and one is integrable iff the other is. (Contributed by Mario Carneiro, 12-Aug-2014) (Revised by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses itgeqa.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
itgeqa.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℂ )
itgeqa.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
itgeqa.4 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
itgeqa.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 𝐷 )
Assertion itgeqa ( 𝜑 → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ 𝐿1 ) ∧ ∫ 𝐵 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgeqa.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
2 itgeqa.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℂ )
3 itgeqa.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4 itgeqa.4 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
5 itgeqa.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 𝐷 )
6 3 4 5 1 2 mbfeqa ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ) )
7 ifan ⊢ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
8 1 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
9 ax-icn ⊢ i ∈ ℂ
10 ine0 ⊢ i ≠ 0
11 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
12 11 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑘 ∈ ℤ )
13 expclz ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ∈ ℂ )
14 9 10 12 13 mp3an12i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( i ↑ 𝑘 ) ∈ ℂ )
15 expne0i ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
16 9 10 12 15 mp3an12i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( i ↑ 𝑘 ) ≠ 0 )
17 8 14 16 divcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐶 / ( i ↑ 𝑘 ) ) ∈ ℂ )
18 17 recld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ∈ ℝ )
19 0re ⊢ 0 ∈ ℝ
20 ifcl ⊢ ( ( ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
21 18 19 20 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
22 21 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* )
23 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
24 19 18 23 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
25 elxrge0 ⊢ ( if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) ↔ ( if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* ∧ 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
26 22 24 25 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
27 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
28 27 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐵 ) → 0 ∈ ( 0 [,] +∞ ) )
29 26 28 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
30 7 29 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
32 31 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
33 ifan ⊢ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
34 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℂ )
35 34 14 16 divcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐷 / ( i ↑ 𝑘 ) ) ∈ ℂ )
36 35 recld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ∈ ℝ )
37 ifcl ⊢ ( ( ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
38 36 19 37 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
39 38 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* )
40 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) )
41 19 36 40 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) )
42 elxrge0 ⊢ ( if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) ↔ ( if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* ∧ 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
43 39 41 42 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐵 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
44 43 28 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
45 33 44 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
47 46 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
48 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝐴 ⊆ ℝ )
49 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( vol* ‘ 𝐴 ) = 0 )
50 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝜑 )
51 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
52 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
53 52 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ 𝐴 )
54 51 53 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) )
55 50 54 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐶 = 𝐷 )
56 55 fvoveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) )
57 56 ibllem ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) )
58 eldifi ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 𝑥 ∈ ℝ )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 𝑥 ∈ ℝ )
60 fvex ⊢ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ∈ V
61 c0ex ⊢ 0 ∈ V
62 60 61 ifex ⊢ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ V
63 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
64 63 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ V ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
65 59 62 64 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
66 fvex ⊢ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ∈ V
67 66 61 ifex ⊢ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ V
68 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) )
69 68 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ V ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) )
70 59 67 69 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) )
71 57 65 70 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) )
72 71 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) )
73 nfv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 )
74 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 )
75 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 )
76 74 75 nfeq ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 )
77 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) )
78 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) )
79 77 78 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) ↔ ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) ) )
80 73 76 79 cbvralw ⊢ ( ∀ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) )
81 72 80 sylib ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) )
82 81 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) )
83 82 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ‘ 𝑦 ) )
84 32 47 48 49 83 itg2eqa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
85 84 eleq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
86 85 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
87 6 86 anbi12d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
88 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
89 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) )
90 88 89 1 isibl2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
91 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
92 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) )
93 91 92 2 isibl2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
94 87 90 93 3bitr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ 𝐿1 ) )
95 84 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
96 95 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
97 eqid ⊢ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
98 97 dfitg ⊢ ∫ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
99 eqid ⊢ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) )
100 99 dfitg ⊢ ∫ 𝐵 𝐷 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
101 96 98 100 3eqtr4g ⊢ ( 𝜑 → ∫ 𝐵 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 )
102 94 101 jca ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ 𝐿1 ) ∧ ∫ 𝐵 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 ) )