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	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿¹ ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ 𝐿¹ ) ∧ ∫ 𝐵 𝐶 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 ) ) → ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
85	84	eleq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
86	85	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
87	6 86	anbi12d	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ 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	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿¹ ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ 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	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ 𝐿¹ ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
94	87 90 93	3bitr4d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿¹ ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ 𝐿¹ ) )
95	84	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( i ↑ 𝑘 ) · ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
96	95	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
97		eqid	⊢ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
98	97	dfitg	⊢ ∫ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
99		eqid	⊢ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) )
100	99	dfitg	⊢ ∫ 𝐵 𝐷 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫₂ ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐷 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
101	96 98 100	3eqtr4g	⊢ ( 𝜑 → ∫ 𝐵 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 )
102	94 101	jca	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿¹ ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ 𝐿¹ ) ∧ ∫ 𝐵 𝐶 d 𝑥 = ∫ 𝐵 𝐷 d 𝑥 ) )

Metamath Proof Explorer

Theorem itgeqa

Proof