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 ⊢φ→∫AB+Cdx=∫ABdx+∫ACdx

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