Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ftc2ditg Unicode version

Theorem ftc2ditg 19341
 Description: Directed integral analog of ftc2 19339. (Contributed by Mario Carneiro, 3-Sep-2014.)
Hypotheses
Ref Expression
ftc2ditg.x
ftc2ditg.y
ftc2ditg.a
ftc2ditg.b
ftc2ditg.c
ftc2ditg.i
ftc2ditg.f
Assertion
Ref Expression
ftc2ditg _
Distinct variable groups:   ,   ,   ,   ,   ,   ,

Proof of Theorem ftc2ditg
StepHypRef Expression
1 ftc2ditg.x . . . 4
2 ftc2ditg.y . . . 4
3 iccssre 10683 . . . 4
41, 2, 3syl2anc 645 . . 3
5 ftc2ditg.a . . 3
64, 5sseldd 3142 . 2
7 ftc2ditg.b . . 3
84, 7sseldd 3142 . 2
9 ftc2ditg.c . . 3
10 ftc2ditg.i . . 3
11 ftc2ditg.f . . 3
121, 2, 5, 7, 9, 10, 11ftc2ditglem 19340 . 2 _
13 fvex 5458 . . . . . 6
1413a1i 12 . . . . 5
15 cncff 18345 . . . . . . . 8
169, 15syl 17 . . . . . . 7
1716feqmptd 5495 . . . . . 6
1817, 10eqeltrrd 2331 . . . . 5
191, 2, 7, 5, 14, 18ditgswap 19157 . . . 4 _ _
2019adantr 453 . . 3 _ _
211, 2, 7, 5, 9, 10, 11ftc2ditglem 19340 . . . 4 _
2221negeqd 9000 . . 3 _
23 cncff 18345 . . . . . . 7
2411, 23syl 17 . . . . . 6
25 ffvelrn 5583 . . . . . 6
2624, 5, 25syl2anc 645 . . . . 5
27 ffvelrn 5583 . . . . . 6
2824, 7, 27syl2anc 645 . . . . 5
2926, 28negsubdi2d 9127 . . . 4