Metamath Proof Explorer


Theorem ibladdnclem

Description: Lemma for ibladdnc ; cf ibladdlem , whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc . (Contributed by Brendan Leahy, 31-Oct-2017)

Ref Expression
Hypotheses ibladdnclem.1 φxAB
ibladdnclem.2 φxAC
ibladdnclem.3 φxAD=B+C
ibladdnclem.4 φxABMblFn
ibladdnclem.6 φ2xifxA0BB0
ibladdnclem.7 φ2xifxA0CC0
Assertion ibladdnclem φ2xifxA0DD0

Proof

Step Hyp Ref Expression
1 ibladdnclem.1 φxAB
2 ibladdnclem.2 φxAC
3 ibladdnclem.3 φxAD=B+C
4 ibladdnclem.4 φxABMblFn
5 ibladdnclem.6 φ2xifxA0BB0
6 ibladdnclem.7 φ2xifxA0CC0
7 ifan ifxA0DD0=ifxAif0DD00
8 1 2 readdcld φxAB+C
9 3 8 eqeltrd φxAD
10 0re 0
11 ifcl D0if0DD0
12 9 10 11 sylancl φxAif0DD0
13 12 rexrd φxAif0DD0*
14 max1 0D0if0DD0
15 10 9 14 sylancr φxA0if0DD0
16 elxrge0 if0DD00+∞if0DD0*0if0DD0
17 13 15 16 sylanbrc φxAif0DD00+∞
18 0e0iccpnf 00+∞
19 18 a1i φ¬xA00+∞
20 17 19 ifclda φifxAif0DD000+∞
21 20 adantr φxifxAif0DD000+∞
22 7 21 eqeltrid φxifxA0DD00+∞
23 22 fmpttd φxifxA0DD0:0+∞
24 reex V
25 24 a1i φV
26 ifan ifxA0BB0=ifxAif0BB00
27 ifcl B0if0BB0
28 1 10 27 sylancl φxAif0BB0
29 10 a1i φ¬xA0
30 28 29 ifclda φifxAif0BB00
31 26 30 eqeltrid φifxA0BB0
32 31 adantr φxifxA0BB0
33 ifan ifxA0CC0=ifxAif0CC00
34 ifcl C0if0CC0
35 2 10 34 sylancl φxAif0CC0
36 35 29 ifclda φifxAif0CC00
37 33 36 eqeltrid φifxA0CC0
38 37 adantr φxifxA0CC0
39 eqidd φxifxA0BB0=xifxA0BB0
40 eqidd φxifxA0CC0=xifxA0CC0
41 25 32 38 39 40 offval2 φxifxA0BB0+fxifxA0CC0=xifxA0BB0+ifxA0CC0
42 iftrue xAifxAif0BB0+if0CC00=if0BB0+if0CC0
43 ibar xA0BxA0B
44 43 ifbid xAif0BB0=ifxA0BB0
45 ibar xA0CxA0C
46 45 ifbid xAif0CC0=ifxA0CC0
47 44 46 oveq12d xAif0BB0+if0CC0=ifxA0BB0+ifxA0CC0
48 42 47 eqtr2d xAifxA0BB0+ifxA0CC0=ifxAif0BB0+if0CC00
49 00id 0+0=0
50 simpl xA0BxA
51 50 con3i ¬xA¬xA0B
52 51 iffalsed ¬xAifxA0BB0=0
53 simpl xA0CxA
54 53 con3i ¬xA¬xA0C
55 54 iffalsed ¬xAifxA0CC0=0
56 52 55 oveq12d ¬xAifxA0BB0+ifxA0CC0=0+0
57 iffalse ¬xAifxAif0BB0+if0CC00=0
58 49 56 57 3eqtr4a ¬xAifxA0BB0+ifxA0CC0=ifxAif0BB0+if0CC00
59 48 58 pm2.61i ifxA0BB0+ifxA0CC0=ifxAif0BB0+if0CC00
60 59 mpteq2i xifxA0BB0+ifxA0CC0=xifxAif0BB0+if0CC00
61 41 60 eqtrdi φxifxA0BB0+fxifxA0CC0=xifxAif0BB0+if0CC00
62 61 fveq2d φ2xifxA0BB0+fxifxA0CC0=2xifxAif0BB0+if0CC00
63 4 1 mbfdm2 φAdomvol
64 mblss AdomvolA
65 63 64 syl φA
66 rembl domvol
67 66 a1i φdomvol
68 31 adantr φxAifxA0BB0
69 eldifn xA¬xA
70 69 adantl φxA¬xA
71 70 intnanrd φxA¬xA0B
72 71 iffalsed φxAifxA0BB0=0
73 44 mpteq2ia xAif0BB0=xAifxA0BB0
74 1 4 mbfpos φxAif0BB0MblFn
75 73 74 eqeltrrid φxAifxA0BB0MblFn
76 65 67 68 72 75 mbfss φxifxA0BB0MblFn
77 max1 0B0if0BB0
78 10 1 77 sylancr φxA0if0BB0
79 elrege0 if0BB00+∞if0BB00if0BB0
80 28 78 79 sylanbrc φxAif0BB00+∞
81 0e0icopnf 00+∞
82 81 a1i φ¬xA00+∞
83 80 82 ifclda φifxAif0BB000+∞
84 26 83 eqeltrid φifxA0BB00+∞
85 84 adantr φxifxA0BB00+∞
86 85 fmpttd φxifxA0BB0:0+∞
87 max1 0C0if0CC0
88 10 2 87 sylancr φxA0if0CC0
89 elrege0 if0CC00+∞if0CC00if0CC0
90 35 88 89 sylanbrc φxAif0CC00+∞
91 90 82 ifclda φifxAif0CC000+∞
92 33 91 eqeltrid φifxA0CC00+∞
93 92 adantr φxifxA0CC00+∞
94 93 fmpttd φxifxA0CC0:0+∞
95 76 86 5 94 6 itg2addnc φ2xifxA0BB0+fxifxA0CC0=2xifxA0BB0+2xifxA0CC0
96 62 95 eqtr3d φ2xifxAif0BB0+if0CC00=2xifxA0BB0+2xifxA0CC0
97 5 6 readdcld φ2xifxA0BB0+2xifxA0CC0
98 96 97 eqeltrd φ2xifxAif0BB0+if0CC00
99 28 35 readdcld φxAif0BB0+if0CC0
100 99 rexrd φxAif0BB0+if0CC0*
101 28 35 78 88 addge0d φxA0if0BB0+if0CC0
102 elxrge0 if0BB0+if0CC00+∞if0BB0+if0CC0*0if0BB0+if0CC0
103 100 101 102 sylanbrc φxAif0BB0+if0CC00+∞
104 103 19 ifclda φifxAif0BB0+if0CC000+∞
105 104 adantr φxifxAif0BB0+if0CC000+∞
106 105 fmpttd φxifxAif0BB0+if0CC00:0+∞
107 max2 0BBif0BB0
108 10 1 107 sylancr φxABif0BB0
109 max2 0CCif0CC0
110 10 2 109 sylancr φxACif0CC0
111 1 2 28 35 108 110 le2addd φxAB+Cif0BB0+if0CC0
112 3 111 eqbrtrd φxADif0BB0+if0CC0
113 breq1 D=if0DD0Dif0BB0+if0CC0if0DD0if0BB0+if0CC0
114 breq1 0=if0DD00if0BB0+if0CC0if0DD0if0BB0+if0CC0
115 113 114 ifboth Dif0BB0+if0CC00if0BB0+if0CC0if0DD0if0BB0+if0CC0
116 112 101 115 syl2anc φxAif0DD0if0BB0+if0CC0
117 iftrue xAifxAif0DD00=if0DD0
118 117 adantl φxAifxAif0DD00=if0DD0
119 42 adantl φxAifxAif0BB0+if0CC00=if0BB0+if0CC0
120 116 118 119 3brtr4d φxAifxAif0DD00ifxAif0BB0+if0CC00
121 120 ex φxAifxAif0DD00ifxAif0BB0+if0CC00
122 0le0 00
123 122 a1i ¬xA00
124 iffalse ¬xAifxAif0DD00=0
125 123 124 57 3brtr4d ¬xAifxAif0DD00ifxAif0BB0+if0CC00
126 121 125 pm2.61d1 φifxAif0DD00ifxAif0BB0+if0CC00
127 7 126 eqbrtrid φifxA0DD0ifxAif0BB0+if0CC00
128 127 ralrimivw φxifxA0DD0ifxAif0BB0+if0CC00
129 eqidd φxifxA0DD0=xifxA0DD0
130 eqidd φxifxAif0BB0+if0CC00=xifxAif0BB0+if0CC00
131 25 22 105 129 130 ofrfval2 φxifxA0DD0fxifxAif0BB0+if0CC00xifxA0DD0ifxAif0BB0+if0CC00
132 128 131 mpbird φxifxA0DD0fxifxAif0BB0+if0CC00
133 itg2le xifxA0DD0:0+∞xifxAif0BB0+if0CC00:0+∞xifxA0DD0fxifxAif0BB0+if0CC002xifxA0DD02xifxAif0BB0+if0CC00
134 23 106 132 133 syl3anc φ2xifxA0DD02xifxAif0BB0+if0CC00
135 itg2lecl xifxA0DD0:0+∞2xifxAif0BB0+if0CC002xifxA0DD02xifxAif0BB0+if0CC002xifxA0DD0
136 23 98 134 135 syl3anc φ2xifxA0DD0