Metamath Proof Explorer


Theorem itgmulc2lem2

Description: Lemma for itgmulc2 : real case. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgmulc2.1 φC
itgmulc2.2 φxABV
itgmulc2.3 φxAB𝐿1
itgmulc2.4 φC
itgmulc2.5 φxAB
Assertion itgmulc2lem2 φCABdx=ACBdx

Proof

Step Hyp Ref Expression
1 itgmulc2.1 φC
2 itgmulc2.2 φxABV
3 itgmulc2.3 φxAB𝐿1
4 itgmulc2.4 φC
5 itgmulc2.5 φxAB
6 4 adantr φxAC
7 max0sub Cif0CC0if0CC0=C
8 6 7 syl φxAif0CC0if0CC0=C
9 8 oveq1d φxAif0CC0if0CC0B=CB
10 0re 0
11 ifcl C0if0CC0
12 4 10 11 sylancl φif0CC0
13 12 recnd φif0CC0
14 13 adantr φxAif0CC0
15 4 renegcld φC
16 ifcl C0if0CC0
17 15 10 16 sylancl φif0CC0
18 17 recnd φif0CC0
19 18 adantr φxAif0CC0
20 5 recnd φxAB
21 14 19 20 subdird φxAif0CC0if0CC0B=if0CC0Bif0CC0B
22 9 21 eqtr3d φxACB=if0CC0Bif0CC0B
23 22 itgeq2dv φACBdx=Aif0CC0Bif0CC0Bdx
24 12 adantr φxAif0CC0
25 24 5 remulcld φxAif0CC0B
26 13 2 3 iblmulc2 φxAif0CC0B𝐿1
27 17 adantr φxAif0CC0
28 27 5 remulcld φxAif0CC0B
29 18 2 3 iblmulc2 φxAif0CC0B𝐿1
30 25 26 28 29 itgsub φAif0CC0Bif0CC0Bdx=Aif0CC0BdxAif0CC0Bdx
31 ifcl B0if0BB0
32 5 10 31 sylancl φxAif0BB0
33 24 32 remulcld φxAif0CC0if0BB0
34 5 iblre φxAB𝐿1xAif0BB0𝐿1xAif0BB0𝐿1
35 3 34 mpbid φxAif0BB0𝐿1xAif0BB0𝐿1
36 35 simpld φxAif0BB0𝐿1
37 13 32 36 iblmulc2 φxAif0CC0if0BB0𝐿1
38 5 renegcld φxAB
39 ifcl B0if0BB0
40 38 10 39 sylancl φxAif0BB0
41 24 40 remulcld φxAif0CC0if0BB0
42 35 simprd φxAif0BB0𝐿1
43 13 40 42 iblmulc2 φxAif0CC0if0BB0𝐿1
44 33 37 41 43 itgsub φAif0CC0if0BB0if0CC0if0BB0dx=Aif0CC0if0BB0dxAif0CC0if0BB0dx
45 max0sub Bif0BB0if0BB0=B
46 5 45 syl φxAif0BB0if0BB0=B
47 46 oveq2d φxAif0CC0if0BB0if0BB0=if0CC0B
48 32 recnd φxAif0BB0
49 40 recnd φxAif0BB0
50 14 48 49 subdid φxAif0CC0if0BB0if0BB0=if0CC0if0BB0if0CC0if0BB0
51 47 50 eqtr3d φxAif0CC0B=if0CC0if0BB0if0CC0if0BB0
52 51 itgeq2dv φAif0CC0Bdx=Aif0CC0if0BB0if0CC0if0BB0dx
53 5 3 itgreval φABdx=Aif0BB0dxAif0BB0dx
54 53 oveq2d φif0CC0ABdx=if0CC0Aif0BB0dxAif0BB0dx
55 32 36 itgcl φAif0BB0dx
56 40 42 itgcl φAif0BB0dx
57 13 55 56 subdid φif0CC0Aif0BB0dxAif0BB0dx=if0CC0Aif0BB0dxif0CC0Aif0BB0dx
58 max1 0C0if0CC0
59 10 4 58 sylancr φ0if0CC0
60 max1 0B0if0BB0
61 10 5 60 sylancr φxA0if0BB0
62 13 32 36 12 32 59 61 itgmulc2lem1 φif0CC0Aif0BB0dx=Aif0CC0if0BB0dx
63 max1 0B0if0BB0
64 10 38 63 sylancr φxA0if0BB0
65 13 40 42 12 40 59 64 itgmulc2lem1 φif0CC0Aif0BB0dx=Aif0CC0if0BB0dx
66 62 65 oveq12d φif0CC0Aif0BB0dxif0CC0Aif0BB0dx=Aif0CC0if0BB0dxAif0CC0if0BB0dx
67 54 57 66 3eqtrd φif0CC0ABdx=Aif0CC0if0BB0dxAif0CC0if0BB0dx
68 44 52 67 3eqtr4d φAif0CC0Bdx=if0CC0ABdx
69 27 32 remulcld φxAif0CC0if0BB0
70 18 32 36 iblmulc2 φxAif0CC0if0BB0𝐿1
71 27 40 remulcld φxAif0CC0if0BB0
72 18 40 42 iblmulc2 φxAif0CC0if0BB0𝐿1
73 69 70 71 72 itgsub φAif0CC0if0BB0if0CC0if0BB0dx=Aif0CC0if0BB0dxAif0CC0if0BB0dx
74 46 oveq2d φxAif0CC0if0BB0if0BB0=if0CC0B
75 19 48 49 subdid φxAif0CC0if0BB0if0BB0=if0CC0if0BB0if0CC0if0BB0
76 74 75 eqtr3d φxAif0CC0B=if0CC0if0BB0if0CC0if0BB0
77 76 itgeq2dv φAif0CC0Bdx=Aif0CC0if0BB0if0CC0if0BB0dx
78 53 oveq2d φif0CC0ABdx=if0CC0Aif0BB0dxAif0BB0dx
79 18 55 56 subdid φif0CC0Aif0BB0dxAif0BB0dx=if0CC0Aif0BB0dxif0CC0Aif0BB0dx
80 max1 0C0if0CC0
81 10 15 80 sylancr φ0if0CC0
82 18 32 36 17 32 81 61 itgmulc2lem1 φif0CC0Aif0BB0dx=Aif0CC0if0BB0dx
83 18 40 42 17 40 81 64 itgmulc2lem1 φif0CC0Aif0BB0dx=Aif0CC0if0BB0dx
84 82 83 oveq12d φif0CC0Aif0BB0dxif0CC0Aif0BB0dx=Aif0CC0if0BB0dxAif0CC0if0BB0dx
85 78 79 84 3eqtrd φif0CC0ABdx=Aif0CC0if0BB0dxAif0CC0if0BB0dx
86 73 77 85 3eqtr4d φAif0CC0Bdx=if0CC0ABdx
87 68 86 oveq12d φAif0CC0BdxAif0CC0Bdx=if0CC0ABdxif0CC0ABdx
88 2 3 itgcl φABdx
89 13 18 88 subdird φif0CC0if0CC0ABdx=if0CC0ABdxif0CC0ABdx
90 4 7 syl φif0CC0if0CC0=C
91 90 oveq1d φif0CC0if0CC0ABdx=CABdx
92 87 89 91 3eqtr2d φAif0CC0BdxAif0CC0Bdx=CABdx
93 23 30 92 3eqtrrd φCABdx=ACBdx