Metamath Proof Explorer

Theorem itgaddlem2

Description: Lemma for itgadd . (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itgadd.1 ⊢ φ ∧ x ∈ A → B ∈ V
itgadd.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
itgadd.3 ⊢ φ ∧ x ∈ A → C ∈ V
itgadd.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1
itgadd.5 ⊢ φ ∧ x ∈ A → B ∈ ℝ
itgadd.6 ⊢ φ ∧ x ∈ A → C ∈ ℝ
Assertion itgaddlem2 ⊢ φ → ∫ A B + C dx = ∫ A B dx + ∫ A C dx

Proof

Step Hyp Ref Expression
1 itgadd.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 itgadd.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 itgadd.3 ⊢ φ ∧ x ∈ A → C ∈ V
4 itgadd.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1
5 itgadd.5 ⊢ φ ∧ x ∈ A → B ∈ ℝ
6 itgadd.6 ⊢ φ ∧ x ∈ A → C ∈ ℝ
7 max0sub ⊢ B ∈ ℝ → if 0 ≤ B B 0 − if 0 ≤ − B − B 0 = B
8 5 7 syl ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 − if 0 ≤ − B − B 0 = B
9 max0sub ⊢ C ∈ ℝ → if 0 ≤ C C 0 − if 0 ≤ − C − C 0 = C
10 6 9 syl ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 − if 0 ≤ − C − C 0 = C
11 8 10 oveq12d ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 − if 0 ≤ − B − B 0 + if 0 ≤ C C 0 - if 0 ≤ − C − C 0 = B + C
12 0re ⊢ 0 ∈ ℝ
13 ifcl ⊢ B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ B B 0 ∈ ℝ
14 5 12 13 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ∈ ℝ
15 14 recnd ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ∈ ℂ
16 ifcl ⊢ C ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ C C 0 ∈ ℝ
17 6 12 16 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ∈ ℝ
18 17 recnd ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ∈ ℂ
19 5 renegcld ⊢ φ ∧ x ∈ A → − B ∈ ℝ
20 ifcl ⊢ − B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ − B − B 0 ∈ ℝ
21 19 12 20 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ − B − B 0 ∈ ℝ
22 21 recnd ⊢ φ ∧ x ∈ A → if 0 ≤ − B − B 0 ∈ ℂ
23 6 renegcld ⊢ φ ∧ x ∈ A → − C ∈ ℝ
24 ifcl ⊢ − C ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ − C − C 0 ∈ ℝ
25 23 12 24 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ∈ ℝ
26 25 recnd ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ∈ ℂ
27 15 18 22 26 addsub4d ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 + if 0 ≤ C C 0 - if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 = if 0 ≤ B B 0 − if 0 ≤ − B − B 0 + if 0 ≤ C C 0 - if 0 ≤ − C − C 0
28 5 6 readdcld ⊢ φ ∧ x ∈ A → B + C ∈ ℝ
29 max0sub ⊢ B + C ∈ ℝ → if 0 ≤ B + C B + C 0 − if 0 ≤ − B + C − B + C 0 = B + C
30 28 29 syl ⊢ φ ∧ x ∈ A → if 0 ≤ B + C B + C 0 − if 0 ≤ − B + C − B + C 0 = B + C
31 11 27 30 3eqtr4rd ⊢ φ ∧ x ∈ A → if 0 ≤ B + C B + C 0 − if 0 ≤ − B + C − B + C 0 = if 0 ≤ B B 0 + if 0 ≤ C C 0 - if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0
32 28 renegcld ⊢ φ ∧ x ∈ A → − B + C ∈ ℝ
33 ifcl ⊢ − B + C ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ − B + C − B + C 0 ∈ ℝ
34 32 12 33 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ − B + C − B + C 0 ∈ ℝ
35 34 recnd ⊢ φ ∧ x ∈ A → if 0 ≤ − B + C − B + C 0 ∈ ℂ
36 15 18 addcld ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ ℂ
37 ifcl ⊢ B + C ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ B + C B + C 0 ∈ ℝ
38 28 12 37 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ B + C B + C 0 ∈ ℝ
39 38 recnd ⊢ φ ∧ x ∈ A → if 0 ≤ B + C B + C 0 ∈ ℂ
40 22 26 addcld ⊢ φ ∧ x ∈ A → if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 ∈ ℂ
41 35 36 39 40 addsubeq4d ⊢ φ ∧ x ∈ A → if 0 ≤ − B + C − B + C 0 + if 0 ≤ B B 0 + if 0 ≤ C C 0 = if 0 ≤ B + C B + C 0 + if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 ↔ if 0 ≤ B + C B + C 0 − if 0 ≤ − B + C − B + C 0 = if 0 ≤ B B 0 + if 0 ≤ C C 0 - if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0
42 31 41 mpbird ⊢ φ ∧ x ∈ A → if 0 ≤ − B + C − B + C 0 + if 0 ≤ B B 0 + if 0 ≤ C C 0 = if 0 ≤ B + C B + C 0 + if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0
43 42 itgeq2dv ⊢ φ → ∫ A if 0 ≤ − B + C − B + C 0 + if 0 ≤ B B 0 + if 0 ≤ C C 0 dx = ∫ A if 0 ≤ B + C B + C 0 + if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx
44 1 2 3 4 ibladd ⊢ φ → x ∈ A ⟼ B + C ∈ 𝐿 1
45 28 iblre ⊢ φ → x ∈ A ⟼ B + C ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ B + C B + C 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − B + C − B + C 0 ∈ 𝐿 1
46 44 45 mpbid ⊢ φ → x ∈ A ⟼ if 0 ≤ B + C B + C 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − B + C − B + C 0 ∈ 𝐿 1
47 46 simprd ⊢ φ → x ∈ A ⟼ if 0 ≤ − B + C − B + C 0 ∈ 𝐿 1
48 14 17 readdcld ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ ℝ
49 5 iblre ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ B B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ 𝐿 1
50 2 49 mpbid ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ 𝐿 1
51 50 simpld ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 ∈ 𝐿 1
52 6 iblre ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ C C 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − C − C 0 ∈ 𝐿 1
53 4 52 mpbid ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − C − C 0 ∈ 𝐿 1
54 53 simpld ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ∈ 𝐿 1
55 14 51 17 54 ibladd ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ 𝐿 1
56 max1 ⊢ 0 ∈ ℝ ∧ − B + C ∈ ℝ → 0 ≤ if 0 ≤ − B + C − B + C 0
57 12 32 56 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ − B + C − B + C 0
58 max1 ⊢ 0 ∈ ℝ ∧ B ∈ ℝ → 0 ≤ if 0 ≤ B B 0
59 12 5 58 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ B B 0
60 max1 ⊢ 0 ∈ ℝ ∧ C ∈ ℝ → 0 ≤ if 0 ≤ C C 0
61 12 6 60 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ C C 0
62 14 17 59 61 addge0d ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0
63 34 47 48 55 34 48 57 62 itgaddlem1 ⊢ φ → ∫ A if 0 ≤ − B + C − B + C 0 + if 0 ≤ B B 0 + if 0 ≤ C C 0 dx = ∫ A if 0 ≤ − B + C − B + C 0 dx + ∫ A if 0 ≤ B B 0 + if 0 ≤ C C 0 dx
64 46 simpld ⊢ φ → x ∈ A ⟼ if 0 ≤ B + C B + C 0 ∈ 𝐿 1
65 21 25 readdcld ⊢ φ ∧ x ∈ A → if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 ∈ ℝ
66 50 simprd ⊢ φ → x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ 𝐿 1
67 53 simprd ⊢ φ → x ∈ A ⟼ if 0 ≤ − C − C 0 ∈ 𝐿 1
68 21 66 25 67 ibladd ⊢ φ → x ∈ A ⟼ if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 ∈ 𝐿 1
69 max1 ⊢ 0 ∈ ℝ ∧ B + C ∈ ℝ → 0 ≤ if 0 ≤ B + C B + C 0
70 12 28 69 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ B + C B + C 0
71 max1 ⊢ 0 ∈ ℝ ∧ − B ∈ ℝ → 0 ≤ if 0 ≤ − B − B 0
72 12 19 71 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ − B − B 0
73 max1 ⊢ 0 ∈ ℝ ∧ − C ∈ ℝ → 0 ≤ if 0 ≤ − C − C 0
74 12 23 73 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ − C − C 0
75 21 25 72 74 addge0d ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0
76 38 64 65 68 38 65 70 75 itgaddlem1 ⊢ φ → ∫ A if 0 ≤ B + C B + C 0 + if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx = ∫ A if 0 ≤ B + C B + C 0 dx + ∫ A if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx
77 43 63 76 3eqtr3d ⊢ φ → ∫ A if 0 ≤ − B + C − B + C 0 dx + ∫ A if 0 ≤ B B 0 + if 0 ≤ C C 0 dx = ∫ A if 0 ≤ B + C B + C 0 dx + ∫ A if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx
78 34 47 itgcl ⊢ φ → ∫ A if 0 ≤ − B + C − B + C 0 dx ∈ ℂ
79 14 51 17 54 14 17 59 61 itgaddlem1 ⊢ φ → ∫ A if 0 ≤ B B 0 + if 0 ≤ C C 0 dx = ∫ A if 0 ≤ B B 0 dx + ∫ A if 0 ≤ C C 0 dx
80 14 51 itgcl ⊢ φ → ∫ A if 0 ≤ B B 0 dx ∈ ℂ
81 17 54 itgcl ⊢ φ → ∫ A if 0 ≤ C C 0 dx ∈ ℂ
82 80 81 addcld ⊢ φ → ∫ A if 0 ≤ B B 0 dx + ∫ A if 0 ≤ C C 0 dx ∈ ℂ
83 79 82 eqeltrd ⊢ φ → ∫ A if 0 ≤ B B 0 + if 0 ≤ C C 0 dx ∈ ℂ
84 38 64 itgcl ⊢ φ → ∫ A if 0 ≤ B + C B + C 0 dx ∈ ℂ
85 21 66 25 67 21 25 72 74 itgaddlem1 ⊢ φ → ∫ A if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx = ∫ A if 0 ≤ − B − B 0 dx + ∫ A if 0 ≤ − C − C 0 dx
86 21 66 itgcl ⊢ φ → ∫ A if 0 ≤ − B − B 0 dx ∈ ℂ
87 25 67 itgcl ⊢ φ → ∫ A if 0 ≤ − C − C 0 dx ∈ ℂ
88 86 87 addcld ⊢ φ → ∫ A if 0 ≤ − B − B 0 dx + ∫ A if 0 ≤ − C − C 0 dx ∈ ℂ
89 85 88 eqeltrd ⊢ φ → ∫ A if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx ∈ ℂ
90 78 83 84 89 addsubeq4d ⊢ φ → ∫ A if 0 ≤ − B + C − B + C 0 dx + ∫ A if 0 ≤ B B 0 + if 0 ≤ C C 0 dx = ∫ A if 0 ≤ B + C B + C 0 dx + ∫ A if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx ↔ ∫ A if 0 ≤ B + C B + C 0 dx − ∫ A if 0 ≤ − B + C − B + C 0 dx = ∫ A if 0 ≤ B B 0 + if 0 ≤ C C 0 dx − ∫ A if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx
91 77 90 mpbid ⊢ φ → ∫ A if 0 ≤ B + C B + C 0 dx − ∫ A if 0 ≤ − B + C − B + C 0 dx = ∫ A if 0 ≤ B B 0 + if 0 ≤ C C 0 dx − ∫ A if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx
92 79 85 oveq12d ⊢ φ → ∫ A if 0 ≤ B B 0 + if 0 ≤ C C 0 dx − ∫ A if 0 ≤ − B − B 0 + if 0 ≤ − C − C 0 dx = ∫ A if 0 ≤ B B 0 dx + ∫ A if 0 ≤ C C 0 dx - ∫ A if 0 ≤ − B − B 0 dx + ∫ A if 0 ≤ − C − C 0 dx
93 80 81 86 87 addsub4d ⊢ φ → ∫ A if 0 ≤ B B 0 dx + ∫ A if 0 ≤ C C 0 dx - ∫ A if 0 ≤ − B − B 0 dx + ∫ A if 0 ≤ − C − C 0 dx = ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx + ∫ A if 0 ≤ C C 0 dx - ∫ A if 0 ≤ − C − C 0 dx
94 91 92 93 3eqtrd ⊢ φ → ∫ A if 0 ≤ B + C B + C 0 dx − ∫ A if 0 ≤ − B + C − B + C 0 dx = ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx + ∫ A if 0 ≤ C C 0 dx - ∫ A if 0 ≤ − C − C 0 dx
95 28 44 itgreval ⊢ φ → ∫ A B + C dx = ∫ A if 0 ≤ B + C B + C 0 dx − ∫ A if 0 ≤ − B + C − B + C 0 dx
96 5 2 itgreval ⊢ φ → ∫ A B dx = ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx
97 6 4 itgreval ⊢ φ → ∫ A C dx = ∫ A if 0 ≤ C C 0 dx − ∫ A if 0 ≤ − C − C 0 dx
98 96 97 oveq12d ⊢ φ → ∫ A B dx + ∫ A C dx = ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx + ∫ A if 0 ≤ C C 0 dx - ∫ A if 0 ≤ − C − C 0 dx
99 94 95 98 3eqtr4d ⊢ φ → ∫ A B + C dx = ∫ A B dx + ∫ A C dx