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

Theorem ftc2ditg 19930
 Description: Directed integral analog of ftc2 19928. (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 10992 . . . 4
41, 2, 3syl2anc 643 . . 3
5 ftc2ditg.a . . 3
64, 5sseldd 3349 . 2
7 ftc2ditg.b . . 3
84, 7sseldd 3349 . 2
9 ftc2ditg.c . . 3
10 ftc2ditg.i . . 3
11 ftc2ditg.f . . 3
121, 2, 5, 7, 9, 10, 11ftc2ditglem 19929 . 2 _
13 fvex 5742 . . . . . 6
1413a1i 11 . . . . 5
15 cncff 18923 . . . . . . . 8
169, 15syl 16 . . . . . . 7
1716feqmptd 5779 . . . . . 6
1817, 10eqeltrrd 2511 . . . . 5
191, 2, 7, 5, 14, 18ditgswap 19746 . . . 4 _ _
2019adantr 452 . . 3 _ _
211, 2, 7, 5, 9, 10, 11ftc2ditglem 19929 . . . 4 _
2221negeqd 9300 . . 3 _
23 cncff 18923 . . . . . . 7
2411, 23syl 16 . . . . . 6
2524, 5ffvelrnd 5871 . . . . 5
2624, 7ffvelrnd 5871 . . . . 5
2725, 26negsubdi2d 9427 . . . 4