Metamath Proof Explorer


Theorem ftc2nc

Description: Choice-free proof of ftc2 . (Contributed by Brendan Leahy, 19-Jun-2018)

Ref Expression
Hypotheses ftc2nc.a φ A
ftc2nc.b φ B
ftc2nc.le φ A B
ftc2nc.c φ F : A B cn
ftc2nc.i φ D F 𝐿 1
ftc2nc.f φ F : A B cn
Assertion ftc2nc φ A B F t dt = F B F A

Proof

Step Hyp Ref Expression
1 ftc2nc.a φ A
2 ftc2nc.b φ B
3 ftc2nc.le φ A B
4 ftc2nc.c φ F : A B cn
5 ftc2nc.i φ D F 𝐿 1
6 ftc2nc.f φ F : A B cn
7 1 rexrd φ A *
8 2 rexrd φ B *
9 ubicc2 A * B * A B B A B
10 7 8 3 9 syl3anc φ B A B
11 fvex x A B A x F t dt F x A V
12 11 fvconst2 B A B A B × x A B A x F t dt F x A B = x A B A x F t dt F x A
13 10 12 syl φ A B × x A B A x F t dt F x A B = x A B A x F t dt F x A
14 eqid TopOpen fld = TopOpen fld
15 14 subcn TopOpen fld × t TopOpen fld Cn TopOpen fld
16 15 a1i φ TopOpen fld × t TopOpen fld Cn TopOpen fld
17 eqid x A B A x F t dt = x A B A x F t dt
18 ssidd φ A B A B
19 ioossre A B
20 19 a1i φ A B
21 cncff F : A B cn F : A B
22 4 21 syl φ F : A B
23 ioof . : * × * 𝒫
24 ffun . : * × * 𝒫 Fun .
25 23 24 ax-mp Fun .
26 fvelima Fun . s . A B × A B x A B × A B . x = s
27 25 26 mpan s . A B × A B x A B × A B . x = s
28 1st2nd2 x A B × A B x = 1 st x 2 nd x
29 28 fveq2d x A B × A B . x = . 1 st x 2 nd x
30 df-ov 1 st x 2 nd x = . 1 st x 2 nd x
31 29 30 eqtr4di x A B × A B . x = 1 st x 2 nd x
32 31 eqeq1d x A B × A B . x = s 1 st x 2 nd x = s
33 32 adantl φ x A B × A B . x = s 1 st x 2 nd x = s
34 7 8 jca φ A * B *
35 34 adantr φ x A B × A B A * B *
36 xp1st x A B × A B 1 st x A B
37 elicc1 A * B * 1 st x A B 1 st x * A 1 st x 1 st x B
38 7 8 37 syl2anc φ 1 st x A B 1 st x * A 1 st x 1 st x B
39 38 biimpa φ 1 st x A B 1 st x * A 1 st x 1 st x B
40 39 simp2d φ 1 st x A B A 1 st x
41 36 40 sylan2 φ x A B × A B A 1 st x
42 xp2nd x A B × A B 2 nd x A B
43 iccleub A * B * 2 nd x A B 2 nd x B
44 43 3expa A * B * 2 nd x A B 2 nd x B
45 34 42 44 syl2an φ x A B × A B 2 nd x B
46 ioossioo A * B * A 1 st x 2 nd x B 1 st x 2 nd x A B
47 35 41 45 46 syl12anc φ x A B × A B 1 st x 2 nd x A B
48 47 sselda φ x A B × A B t 1 st x 2 nd x t A B
49 22 ffvelrnda φ t A B F t
50 49 adantlr φ x A B × A B t A B F t
51 48 50 syldan φ x A B × A B t 1 st x 2 nd x F t
52 ioombl 1 st x 2 nd x dom vol
53 52 a1i φ x A B × A B 1 st x 2 nd x dom vol
54 fvexd φ x A B × A B t A B F t V
55 22 feqmptd φ D F = t A B F t
56 55 5 eqeltrrd φ t A B F t 𝐿 1
57 56 adantr φ x A B × A B t A B F t 𝐿 1
58 47 53 54 57 iblss φ x A B × A B t 1 st x 2 nd x F t 𝐿 1
59 ax-resscn
60 ssid
61 cncfss cn cn
62 59 60 61 mp2an cn cn
63 abscncf abs : cn
64 62 63 sselii abs : cn
65 64 a1i φ x A B × A B abs : cn
66 55 reseq1d φ F 1 st x 2 nd x = t A B F t 1 st x 2 nd x
67 66 adantr φ x A B × A B F 1 st x 2 nd x = t A B F t 1 st x 2 nd x
68 47 resmptd φ x A B × A B t A B F t 1 st x 2 nd x = t 1 st x 2 nd x F t
69 67 68 eqtrd φ x A B × A B F 1 st x 2 nd x = t 1 st x 2 nd x F t
70 4 adantr φ x A B × A B F : A B cn
71 rescncf 1 st x 2 nd x A B F : A B cn F 1 st x 2 nd x : 1 st x 2 nd x cn
72 47 70 71 sylc φ x A B × A B F 1 st x 2 nd x : 1 st x 2 nd x cn
73 69 72 eqeltrrd φ x A B × A B t 1 st x 2 nd x F t : 1 st x 2 nd x cn
74 65 73 cncfmpt1f φ x A B × A B t 1 st x 2 nd x F t : 1 st x 2 nd x cn
75 cnmbf 1 st x 2 nd x dom vol t 1 st x 2 nd x F t : 1 st x 2 nd x cn t 1 st x 2 nd x F t MblFn
76 52 74 75 sylancr φ x A B × A B t 1 st x 2 nd x F t MblFn
77 51 58 itgcl φ x A B × A B 1 st x 2 nd x F t dt
78 77 cjcld φ x A B × A B 1 st x 2 nd x F t dt
79 ioossre 1 st x 2 nd x
80 79 59 sstri 1 st x 2 nd x
81 cncfmptc 1 st x 2 nd x F t dt 1 st x 2 nd x s 1 st x 2 nd x 1 st x 2 nd x F t dt : 1 st x 2 nd x cn
82 80 60 81 mp3an23 1 st x 2 nd x F t dt s 1 st x 2 nd x 1 st x 2 nd x F t dt : 1 st x 2 nd x cn
83 78 82 syl φ x A B × A B s 1 st x 2 nd x 1 st x 2 nd x F t dt : 1 st x 2 nd x cn
84 nfcv _ s F t
85 nfcsb1v _ t s / t F t
86 csbeq1a t = s F t = s / t F t
87 84 85 86 cbvmpt t 1 st x 2 nd x F t = s 1 st x 2 nd x s / t F t
88 87 73 eqeltrrid φ x A B × A B s 1 st x 2 nd x s / t F t : 1 st x 2 nd x cn
89 83 88 mulcncf φ x A B × A B s 1 st x 2 nd x 1 st x 2 nd x F t dt s / t F t : 1 st x 2 nd x cn
90 cnmbf 1 st x 2 nd x dom vol s 1 st x 2 nd x 1 st x 2 nd x F t dt s / t F t : 1 st x 2 nd x cn s 1 st x 2 nd x 1 st x 2 nd x F t dt s / t F t MblFn
91 52 89 90 sylancr φ x A B × A B s 1 st x 2 nd x 1 st x 2 nd x F t dt s / t F t MblFn
92 51 58 76 91 itgabsnc φ x A B × A B 1 st x 2 nd x F t dt 1 st x 2 nd x F t dt
93 51 abscld φ x A B × A B t 1 st x 2 nd x F t
94 fvexd φ x A B × A B t 1 st x 2 nd x F t V
95 94 58 76 iblabsnc φ x A B × A B t 1 st x 2 nd x F t 𝐿 1
96 51 absge0d φ x A B × A B t 1 st x 2 nd x 0 F t
97 93 95 96 itgposval φ x A B × A B 1 st x 2 nd x F t dt = 2 t if t 1 st x 2 nd x F t 0
98 92 97 breqtrd φ x A B × A B 1 st x 2 nd x F t dt 2 t if t 1 st x 2 nd x F t 0
99 itgeq1 1 st x 2 nd x = s 1 st x 2 nd x F t dt = s F t dt
100 99 fveq2d 1 st x 2 nd x = s 1 st x 2 nd x F t dt = s F t dt
101 eleq2 1 st x 2 nd x = s t 1 st x 2 nd x t s
102 101 ifbid 1 st x 2 nd x = s if t 1 st x 2 nd x F t 0 = if t s F t 0
103 102 mpteq2dv 1 st x 2 nd x = s t if t 1 st x 2 nd x F t 0 = t if t s F t 0
104 103 fveq2d 1 st x 2 nd x = s 2 t if t 1 st x 2 nd x F t 0 = 2 t if t s F t 0
105 100 104 breq12d 1 st x 2 nd x = s 1 st x 2 nd x F t dt 2 t if t 1 st x 2 nd x F t 0 s F t dt 2 t if t s F t 0
106 98 105 syl5ibcom φ x A B × A B 1 st x 2 nd x = s s F t dt 2 t if t s F t 0
107 33 106 sylbid φ x A B × A B . x = s s F t dt 2 t if t s F t 0
108 107 rexlimdva φ x A B × A B . x = s s F t dt 2 t if t s F t 0
109 27 108 syl5 φ s . A B × A B s F t dt 2 t if t s F t 0
110 109 ralrimiv φ s . A B × A B s F t dt 2 t if t s F t 0
111 17 1 2 3 18 20 5 22 110 ftc1anc φ x A B A x F t dt : A B cn
112 cncff F : A B cn F : A B
113 6 112 syl φ F : A B
114 113 feqmptd φ F = x A B F x
115 114 6 eqeltrrd φ x A B F x : A B cn
116 14 16 111 115 cncfmpt2f φ x A B A x F t dt F x : A B cn
117 59 a1i φ
118 iccssre A B A B
119 1 2 118 syl2anc φ A B
120 fvexd φ x A B t A x F t V
121 2 adantr φ x A B B
122 121 rexrd φ x A B B *
123 elicc2 A B x A B x A x x B
124 1 2 123 syl2anc φ x A B x A x x B
125 124 biimpa φ x A B x A x x B
126 125 simp3d φ x A B x B
127 iooss2 B * x B A x A B
128 122 126 127 syl2anc φ x A B A x A B
129 ioombl A x dom vol
130 129 a1i φ x A B A x dom vol
131 fvexd φ x A B t A B F t V
132 56 adantr φ x A B t A B F t 𝐿 1
133 128 130 131 132 iblss φ x A B t A x F t 𝐿 1
134 120 133 itgcl φ x A B A x F t dt
135 113 ffvelrnda φ x A B F x
136 134 135 subcld φ x A B A x F t dt F x
137 14 tgioo2 topGen ran . = TopOpen fld 𝑡
138 iccntr A B int topGen ran . A B = A B
139 1 2 138 syl2anc φ int topGen ran . A B = A B
140 117 119 136 137 14 139 dvmptntr φ dx A B A x F t dt F x d x = dx A B A x F t dt F x d x
141 reelprrecn
142 141 a1i φ
143 ioossicc A B A B
144 143 sseli x A B x A B
145 144 134 sylan2 φ x A B A x F t dt
146 22 ffvelrnda φ x A B F x
147 17 1 2 3 4 5 ftc1cnnc φ dx A B A x F t dt d x = D F
148 117 119 134 137 14 139 dvmptntr φ dx A B A x F t dt d x = dx A B A x F t dt d x
149 22 feqmptd φ D F = x A B F x
150 147 148 149 3eqtr3d φ dx A B A x F t dt d x = x A B F x
151 144 135 sylan2 φ x A B F x
152 114 oveq2d φ D F = dx A B F x d x
153 117 119 135 137 14 139 dvmptntr φ dx A B F x d x = dx A B F x d x
154 152 149 153 3eqtr3rd φ dx A B F x d x = x A B F x
155 142 145 146 150 151 146 154 dvmptsub φ dx A B A x F t dt F x d x = x A B F x F x
156 146 subidd φ x A B F x F x = 0
157 156 mpteq2dva φ x A B F x F x = x A B 0
158 140 155 157 3eqtrd φ dx A B A x F t dt F x d x = x A B 0
159 fconstmpt A B × 0 = x A B 0
160 158 159 eqtr4di φ dx A B A x F t dt F x d x = A B × 0
161 1 2 116 160 dveq0 φ x A B A x F t dt F x = A B × x A B A x F t dt F x A
162 161 fveq1d φ x A B A x F t dt F x B = A B × x A B A x F t dt F x A B
163 oveq2 x = B A x = A B
164 itgeq1 A x = A B A x F t dt = A B F t dt
165 163 164 syl x = B A x F t dt = A B F t dt
166 fveq2 x = B F x = F B
167 165 166 oveq12d x = B A x F t dt F x = A B F t dt F B
168 eqid x A B A x F t dt F x = x A B A x F t dt F x
169 ovex A B F t dt F B V
170 167 168 169 fvmpt B A B x A B A x F t dt F x B = A B F t dt F B
171 10 170 syl φ x A B A x F t dt F x B = A B F t dt F B
172 162 171 eqtr3d φ A B × x A B A x F t dt F x A B = A B F t dt F B
173 lbicc2 A * B * A B A A B
174 7 8 3 173 syl3anc φ A A B
175 oveq2 x = A A x = A A
176 iooid A A =
177 175 176 eqtrdi x = A A x =
178 itgeq1 A x = A x F t dt = F t dt
179 177 178 syl x = A A x F t dt = F t dt
180 itg0 F t dt = 0
181 179 180 eqtrdi x = A A x F t dt = 0
182 fveq2 x = A F x = F A
183 181 182 oveq12d x = A A x F t dt F x = 0 F A
184 df-neg F A = 0 F A
185 183 184 eqtr4di x = A A x F t dt F x = F A
186 negex F A V
187 185 168 186 fvmpt A A B x A B A x F t dt F x A = F A
188 174 187 syl φ x A B A x F t dt F x A = F A
189 13 172 188 3eqtr3d φ A B F t dt F B = F A
190 189 oveq2d φ F B + A B F t dt - F B = F B + F A
191 113 10 ffvelrnd φ F B
192 fvexd φ t A B F t V
193 192 56 itgcl φ A B F t dt
194 191 193 pncan3d φ F B + A B F t dt - F B = A B F t dt
195 113 174 ffvelrnd φ F A
196 191 195 negsubd φ F B + F A = F B F A
197 190 194 196 3eqtr3d φ A B F t dt = F B F A