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

Metamath Proof Explorer

Theorem itgeq1fOLD

Description: Obsolete version of itgeq1f as of 1-Sep-2025. (Contributed by Mario Carneiro, 28-Jun-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses itgeq1f.1 ⊢ Ⅎ _ x A
itgeq1f.2 ⊢ Ⅎ _ x B
Assertion itgeq1fOLD ⊢ A = B → ∫ A C dx = ∫ B C dx

Proof

Step Hyp Ref Expression
1 itgeq1f.1 ⊢ Ⅎ _ x A
2 itgeq1f.2 ⊢ Ⅎ _ x B
3 eqid ⊢ ℝ = ℝ
4 1 2 nfeq ⊢ Ⅎ x A = B
5 eleq2 ⊢ A = B → x ∈ A ↔ x ∈ B
6 5 anbi1d ⊢ A = B → x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ↔ x ∈ B ∧ 0 ≤ ℜ ⁡ C i k
7 6 ifbid ⊢ A = B → if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 = if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
8 7 a1d ⊢ A = B → x ∈ ℝ → if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 = if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
9 4 8 ralrimi ⊢ A = B → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 = if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
10 mpteq12 ⊢ ℝ = ℝ ∧ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 = if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 = x ∈ ℝ ⟼ if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
11 3 9 10 sylancr ⊢ A = B → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 = x ∈ ℝ ⟼ if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
12 11 fveq2d ⊢ A = B → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
13 12 oveq2d ⊢ A = B → i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 = i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
14 13 sumeq2sdv ⊢ A = B → ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0 = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
15 eqid ⊢ ℜ ⁡ C i k = ℜ ⁡ C i k
16 15 dfitg ⊢ ∫ A C dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
17 15 dfitg ⊢ ∫ B C dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ B ∧ 0 ≤ ℜ ⁡ C i k ℜ ⁡ C i k 0
18 14 16 17 3eqtr4g ⊢ A = B → ∫ A C dx = ∫ B C dx