Metamath Proof Explorer


Theorem itgcnlem

Description: Expand out the sum in dfitg . (Contributed by Mario Carneiro, 1-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses itgcnlem.r R = 2 x if x A 0 B B 0
itgcnlem.s S = 2 x if x A 0 B B 0
itgcnlem.t T = 2 x if x A 0 B B 0
itgcnlem.u U = 2 x if x A 0 B B 0
itgcnlem.v φ x A B V
itgcnlem.i φ x A B 𝐿 1
Assertion itgcnlem φ A B dx = R - S + i T U

Proof

Step Hyp Ref Expression
1 itgcnlem.r R = 2 x if x A 0 B B 0
2 itgcnlem.s S = 2 x if x A 0 B B 0
3 itgcnlem.t T = 2 x if x A 0 B B 0
4 itgcnlem.u U = 2 x if x A 0 B B 0
5 itgcnlem.v φ x A B V
6 itgcnlem.i φ x A B 𝐿 1
7 eqid B i k = B i k
8 7 dfitg A B dx = k = 0 3 i k 2 x if x A 0 B i k B i k 0
9 nn0uz 0 = 0
10 df-3 3 = 2 + 1
11 oveq2 k = 3 i k = i 3
12 i3 i 3 = i
13 11 12 syl6eq k = 3 i k = i
14 12 itgvallem k = 3 2 x if x A 0 B i k B i k 0 = 2 x if x A 0 B i B i 0
15 13 14 oveq12d k = 3 i k 2 x if x A 0 B i k B i k 0 = i 2 x if x A 0 B i B i 0
16 ax-icn i
17 16 a1i φ i
18 expcl i k 0 i k
19 17 18 sylan φ k 0 i k
20 nn0z k 0 k
21 eqidd φ x if x A 0 B i k B i k 0 = x if x A 0 B i k B i k 0
22 eqidd φ x A B i k = B i k
23 21 22 6 5 iblitg φ k 2 x if x A 0 B i k B i k 0
24 23 recnd φ k 2 x if x A 0 B i k B i k 0
25 20 24 sylan2 φ k 0 2 x if x A 0 B i k B i k 0
26 19 25 mulcld φ k 0 i k 2 x if x A 0 B i k B i k 0
27 df-2 2 = 1 + 1
28 oveq2 k = 2 i k = i 2
29 i2 i 2 = 1
30 28 29 syl6eq k = 2 i k = 1
31 29 itgvallem k = 2 2 x if x A 0 B i k B i k 0 = 2 x if x A 0 B 1 B 1 0
32 30 31 oveq12d k = 2 i k 2 x if x A 0 B i k B i k 0 = -1 2 x if x A 0 B 1 B 1 0
33 1e0p1 1 = 0 + 1
34 oveq2 k = 1 i k = i 1
35 exp1 i i 1 = i
36 16 35 ax-mp i 1 = i
37 34 36 syl6eq k = 1 i k = i
38 36 itgvallem k = 1 2 x if x A 0 B i k B i k 0 = 2 x if x A 0 B i B i 0
39 37 38 oveq12d k = 1 i k 2 x if x A 0 B i k B i k 0 = i 2 x if x A 0 B i B i 0
40 0z 0
41 iblmbf x A B 𝐿 1 x A B MblFn
42 6 41 syl φ x A B MblFn
43 42 5 mbfmptcl φ x A B
44 43 div1d φ x A B 1 = B
45 44 fveq2d φ x A B 1 = B
46 45 ibllem φ if x A 0 B 1 B 1 0 = if x A 0 B B 0
47 46 mpteq2dv φ x if x A 0 B 1 B 1 0 = x if x A 0 B B 0
48 47 fveq2d φ 2 x if x A 0 B 1 B 1 0 = 2 x if x A 0 B B 0
49 48 1 syl6reqr φ R = 2 x if x A 0 B 1 B 1 0
50 49 oveq2d φ 1 R = 1 2 x if x A 0 B 1 B 1 0
51 1 2 3 4 5 iblcnlem φ x A B 𝐿 1 x A B MblFn R S T U
52 6 51 mpbid φ x A B MblFn R S T U
53 52 simp2d φ R S
54 53 simpld φ R
55 54 recnd φ R
56 55 mulid2d φ 1 R = R
57 50 56 eqtr3d φ 1 2 x if x A 0 B 1 B 1 0 = R
58 57 55 eqeltrd φ 1 2 x if x A 0 B 1 B 1 0
59 oveq2 k = 0 i k = i 0
60 exp0 i i 0 = 1
61 16 60 ax-mp i 0 = 1
62 59 61 syl6eq k = 0 i k = 1
63 61 itgvallem k = 0 2 x if x A 0 B i k B i k 0 = 2 x if x A 0 B 1 B 1 0
64 62 63 oveq12d k = 0 i k 2 x if x A 0 B i k B i k 0 = 1 2 x if x A 0 B 1 B 1 0
65 64 fsum1 0 1 2 x if x A 0 B 1 B 1 0 k = 0 0 i k 2 x if x A 0 B i k B i k 0 = 1 2 x if x A 0 B 1 B 1 0
66 40 58 65 sylancr φ k = 0 0 i k 2 x if x A 0 B i k B i k 0 = 1 2 x if x A 0 B 1 B 1 0
67 66 57 eqtrd φ k = 0 0 i k 2 x if x A 0 B i k B i k 0 = R
68 0nn0 0 0
69 67 68 jctil φ 0 0 k = 0 0 i k 2 x if x A 0 B i k B i k 0 = R
70 imval B B = B i
71 43 70 syl φ x A B = B i
72 71 ibllem φ if x A 0 B B 0 = if x A 0 B i B i 0
73 72 mpteq2dv φ x if x A 0 B B 0 = x if x A 0 B i B i 0
74 73 fveq2d φ 2 x if x A 0 B B 0 = 2 x if x A 0 B i B i 0
75 3 74 syl5req φ 2 x if x A 0 B i B i 0 = T
76 75 oveq2d φ i 2 x if x A 0 B i B i 0 = i T
77 76 oveq2d φ R + i 2 x if x A 0 B i B i 0 = R + i T
78 9 33 39 26 69 77 fsump1i φ 1 0 k = 0 1 i k 2 x if x A 0 B i k B i k 0 = R + i T
79 43 renegd φ x A B = B
80 ax-1cn 1
81 80 negnegi -1 = 1
82 81 oveq2i B -1 = B 1
83 43 negcld φ x A B
84 83 div1d φ x A B 1 = B
85 82 84 syl5eq φ x A B -1 = B
86 80 negcli 1
87 neg1ne0 1 0
88 div2neg B 1 1 0 B -1 = B 1
89 86 87 88 mp3an23 B B -1 = B 1
90 43 89 syl φ x A B -1 = B 1
91 85 90 eqtr3d φ x A B = B 1
92 91 fveq2d φ x A B = B 1
93 79 92 eqtr3d φ x A B = B 1
94 93 ibllem φ if x A 0 B B 0 = if x A 0 B 1 B 1 0
95 94 mpteq2dv φ x if x A 0 B B 0 = x if x A 0 B 1 B 1 0
96 95 fveq2d φ 2 x if x A 0 B B 0 = 2 x if x A 0 B 1 B 1 0
97 2 96 syl5eq φ S = 2 x if x A 0 B 1 B 1 0
98 97 oveq2d φ -1 S = -1 2 x if x A 0 B 1 B 1 0
99 53 simprd φ S
100 99 recnd φ S
101 100 mulm1d φ -1 S = S
102 98 101 eqtr3d φ -1 2 x if x A 0 B 1 B 1 0 = S
103 102 oveq2d φ R + i T + -1 2 x if x A 0 B 1 B 1 0 = R + i T + S
104 52 simp3d φ T U
105 104 simpld φ T
106 105 recnd φ T
107 mulcl i T i T
108 16 106 107 sylancr φ i T
109 55 108 addcld φ R + i T
110 109 100 negsubd φ R + i T + S = R + i T - S
111 55 108 100 addsubd φ R + i T - S = R - S + i T
112 103 110 111 3eqtrd φ R + i T + -1 2 x if x A 0 B 1 B 1 0 = R - S + i T
113 9 27 32 26 78 112 fsump1i φ 2 0 k = 0 2 i k 2 x if x A 0 B i k B i k 0 = R - S + i T
114 imval B B = B i
115 83 114 syl φ x A B = B i
116 43 imnegd φ x A B = B
117 16 negnegi i = i
118 117 eqcomi i = i
119 118 oveq2i B i = B i
120 16 negcli i
121 ine0 i 0
122 16 121 negne0i i 0
123 div2neg B i i 0 B i = B i
124 120 122 123 mp3an23 B B i = B i
125 43 124 syl φ x A B i = B i
126 119 125 syl5eq φ x A B i = B i
127 126 fveq2d φ x A B i = B i
128 115 116 127 3eqtr3d φ x A B = B i
129 128 ibllem φ if x A 0 B B 0 = if x A 0 B i B i 0
130 129 mpteq2dv φ x if x A 0 B B 0 = x if x A 0 B i B i 0
131 130 fveq2d φ 2 x if x A 0 B B 0 = 2 x if x A 0 B i B i 0
132 4 131 syl5eq φ U = 2 x if x A 0 B i B i 0
133 132 oveq2d φ i U = i 2 x if x A 0 B i B i 0
134 104 simprd φ U
135 134 recnd φ U
136 mulneg12 i U i U = i U
137 16 135 136 sylancr φ i U = i U
138 133 137 eqtr3d φ i 2 x if x A 0 B i B i 0 = i U
139 138 oveq2d φ R S + i T + i 2 x if x A 0 B i B i 0 = R S + i T + i U
140 9 10 15 26 113 139 fsump1i φ 3 0 k = 0 3 i k 2 x if x A 0 B i k B i k 0 = R S + i T + i U
141 140 simprd φ k = 0 3 i k 2 x if x A 0 B i k B i k 0 = R S + i T + i U
142 8 141 syl5eq φ A B dx = R S + i T + i U
143 55 100 subcld φ R S
144 135 negcld φ U
145 mulcl i U i U
146 16 144 145 sylancr φ i U
147 143 108 146 addassd φ R S + i T + i U = R S + i T + i U
148 17 106 144 adddid φ i T + U = i T + i U
149 106 135 negsubd φ T + U = T U
150 149 oveq2d φ i T + U = i T U
151 148 150 eqtr3d φ i T + i U = i T U
152 151 oveq2d φ R S + i T + i U = R - S + i T U
153 142 147 152 3eqtrd φ A B dx = R - S + i T U