Metamath Proof Explorer

Theorem ftc1lem5

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 14-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses ftc1.g ⊢G=x∈AB⟼∫AxF⁡tdt
ftc1.a ⊢φ→A∈ℝ
ftc1.b ⊢φ→B∈ℝ
ftc1.le ⊢φ→A≤B
ftc1.s ⊢φ→AB⊆D
ftc1.d ⊢φ→D⊆ℝ
ftc1.i ⊢φ→F∈𝐿1
ftc1.c ⊢φ→C∈AB
ftc1.f ⊢φ→F∈KCnPL⁡C
ftc1.j ⊢J=L↾𝑡ℝ
ftc1.k ⊢K=L↾𝑡D
ftc1.l ⊢L=TopOpen⁡ℂfld
ftc1.h ⊢H=z∈AB∖C⟼G⁡z−G⁡Cz−C
ftc1.e ⊢φ→E∈ℝ+
ftc1.r ⊢φ→R∈ℝ+
ftc1.fc ⊢φ∧y∈D→y−C<R→F⁡y−F⁡C<E
ftc1.x1 ⊢φ→X∈AB
ftc1.x2 ⊢φ→X−C<R
Assertion ftc1lem5 ⊢φ∧X≠C→H⁡X−F⁡C<E

Proof

Step Hyp Ref Expression
1 ftc1.g ⊢G=x∈AB⟼∫AxF⁡tdt
2 ftc1.a ⊢φ→A∈ℝ
3 ftc1.b ⊢φ→B∈ℝ
4 ftc1.le ⊢φ→A≤B
5 ftc1.s ⊢φ→AB⊆D
6 ftc1.d ⊢φ→D⊆ℝ
7 ftc1.i ⊢φ→F∈𝐿1
8 ftc1.c ⊢φ→C∈AB
9 ftc1.f ⊢φ→F∈KCnPL⁡C
10 ftc1.j ⊢J=L↾𝑡ℝ
11 ftc1.k ⊢K=L↾𝑡D
12 ftc1.l ⊢L=TopOpen⁡ℂfld
13 ftc1.h ⊢H=z∈AB∖C⟼G⁡z−G⁡Cz−C
14 ftc1.e ⊢φ→E∈ℝ+
15 ftc1.r ⊢φ→R∈ℝ+
16 ftc1.fc ⊢φ∧y∈D→y−C<R→F⁡y−F⁡C<E
17 ftc1.x1 ⊢φ→X∈AB
18 ftc1.x2 ⊢φ→X−C<R
19 iccssre ⊢A∈ℝ∧B∈ℝ→AB⊆ℝ
20 2 3 19 syl2anc ⊢φ→AB⊆ℝ
21 20 17 sseldd ⊢φ→X∈ℝ
22 ioossicc ⊢AB⊆AB
23 22 8 sselid ⊢φ→C∈AB
24 20 23 sseldd ⊢φ→C∈ℝ
25 21 24 lttri2d ⊢φ→X≠C↔X<C∨C<X
26 25 biimpa ⊢φ∧X≠C→X<C∨C<X
27 17 adantr ⊢φ∧X<C→X∈AB
28 21 adantr ⊢φ∧X<C→X∈ℝ
29 simpr ⊢φ∧X<C→X<C
30 28 29 ltned ⊢φ∧X<C→X≠C
31 eldifsn ⊢X∈AB∖C↔X∈AB∧X≠C
32 27 30 31 sylanbrc ⊢φ∧X<C→X∈AB∖C
33 fveq2 ⊢z=X→G⁡z=G⁡X
34 33 oveq1d ⊢z=X→G⁡z−G⁡C=G⁡X−G⁡C
35 oveq1 ⊢z=X→z−C=X−C
36 34 35 oveq12d ⊢z=X→G⁡z−G⁡Cz−C=G⁡X−G⁡CX−C
37 ovex ⊢G⁡X−G⁡CX−C∈V
38 36 13 37 fvmpt ⊢X∈AB∖C→H⁡X=G⁡X−G⁡CX−C
39 32 38 syl ⊢φ∧X<C→H⁡X=G⁡X−G⁡CX−C
40 1 2 3 4 5 6 7 8 9 10 11 12 ftc1lem3 ⊢φ→F:D⟶ℂ
41 1 2 3 4 5 6 7 40 ftc1lem2 ⊢φ→G:AB⟶ℂ
42 41 17 ffvelcdmd ⊢φ→G⁡X∈ℂ
43 41 23 ffvelcdmd ⊢φ→G⁡C∈ℂ
44 42 43 subcld ⊢φ→G⁡X−G⁡C∈ℂ
45 44 adantr ⊢φ∧X<C→G⁡X−G⁡C∈ℂ
46 21 recnd ⊢φ→X∈ℂ
47 24 recnd ⊢φ→C∈ℂ
48 46 47 subcld ⊢φ→X−C∈ℂ
49 48 adantr ⊢φ∧X<C→X−C∈ℂ
50 46 47 subeq0ad ⊢φ→X−C=0↔X=C
51 50 necon3bid ⊢φ→X−C≠0↔X≠C
52 51 biimpar ⊢φ∧X≠C→X−C≠0
53 30 52 syldan ⊢φ∧X<C→X−C≠0
54 45 49 53 div2negd ⊢φ∧X<C→−G⁡X−G⁡C−X−C=G⁡X−G⁡CX−C
55 42 43 negsubdi2d ⊢φ→−G⁡X−G⁡C=G⁡C−G⁡X
56 46 47 negsubdi2d ⊢φ→−X−C=C−X
57 55 56 oveq12d ⊢φ→−G⁡X−G⁡C−X−C=G⁡C−G⁡XC−X
58 57 adantr ⊢φ∧X<C→−G⁡X−G⁡C−X−C=G⁡C−G⁡XC−X
59 39 54 58 3eqtr2d ⊢φ∧X<C→H⁡X=G⁡C−G⁡XC−X
60 59 fvoveq1d ⊢φ∧X<C→H⁡X−F⁡C=G⁡C−G⁡XC−X−F⁡C
61 47 subidd ⊢φ→C−C=0
62 61 abs00bd ⊢φ→C−C=0
63 15 rpgt0d ⊢φ→0<R
64 62 63 eqbrtrd ⊢φ→C−C<R
65 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 23 64 ftc1lem4 ⊢φ∧X<C→G⁡C−G⁡XC−X−F⁡C<E
66 60 65 eqbrtrd ⊢φ∧X<C→H⁡X−F⁡C<E
67 17 adantr ⊢φ∧C<X→X∈AB
68 24 adantr ⊢φ∧C<X→C∈ℝ
69 simpr ⊢φ∧C<X→C<X
70 68 69 gtned ⊢φ∧C<X→X≠C
71 67 70 31 sylanbrc ⊢φ∧C<X→X∈AB∖C
72 71 38 syl ⊢φ∧C<X→H⁡X=G⁡X−G⁡CX−C
73 72 fvoveq1d ⊢φ∧C<X→H⁡X−F⁡C=G⁡X−G⁡CX−C−F⁡C
74 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 23 64 17 18 ftc1lem4 ⊢φ∧C<X→G⁡X−G⁡CX−C−F⁡C<E
75 73 74 eqbrtrd ⊢φ∧C<X→H⁡X−F⁡C<E
76 66 75 jaodan ⊢φ∧X<C∨C<X→H⁡X−F⁡C<E
77 26 76 syldan ⊢φ∧X≠C→H⁡X−F⁡C<E