# 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 $⊢ φ ∧ x ∈ B → C ∈ ℂ$
itgeqa.2 $⊢ φ ∧ x ∈ B → D ∈ ℂ$
itgeqa.3 $⊢ φ → A ⊆ ℝ$
itgeqa.4 $⊢ φ → vol * ⁡ A = 0$
itgeqa.5 $⊢ φ ∧ x ∈ B ∖ A → C = D$
Assertion itgeqa $⊢ φ → x ∈ B ⟼ C ∈ 𝐿 1 ↔ x ∈ B ⟼ D ∈ 𝐿 1 ∧ ∫ B C dx = ∫ B D dx$

### Proof

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