Metamath Proof Explorer


Theorem ftc1anclem4

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 17-Jun-2018)

Ref Expression
Assertion ftc1anclem4 Fdom1G𝐿1G:2tGtFt

Proof

Step Hyp Ref Expression
1 ffvelrn G:tGt
2 1 recnd G:tGt
3 i1ff Fdom1F:
4 3 ffvelrnda Fdom1tFt
5 4 recnd Fdom1tFt
6 subcl GtFtGtFt
7 2 5 6 syl2anr Fdom1tG:tGtFt
8 7 anandirs Fdom1G:tGtFt
9 8 abscld Fdom1G:tGtFt
10 9 rexrd Fdom1G:tGtFt*
11 8 absge0d Fdom1G:t0GtFt
12 elxrge0 GtFt0+∞GtFt*0GtFt
13 10 11 12 sylanbrc Fdom1G:tGtFt0+∞
14 13 fmpttd Fdom1G:tGtFt:0+∞
15 14 3adant2 Fdom1G𝐿1G:tGtFt:0+∞
16 reex V
17 16 a1i Fdom1G𝐿1G:V
18 fvexd Fdom1G𝐿1G:tGtV
19 fvexd Fdom1G𝐿1G:tFtV
20 eqidd Fdom1G𝐿1G:tGt=tGt
21 eqidd Fdom1G𝐿1G:tFt=tFt
22 17 18 19 20 21 offval2 Fdom1G𝐿1G:tGt+ftFt=tGt+Ft
23 22 fveq2d Fdom1G𝐿1G:2tGt+ftFt=2tGt+Ft
24 id G:G:
25 24 feqmptd G:G=tGt
26 absf abs:
27 26 a1i G:abs:
28 27 feqmptd G:abs=xx
29 fveq2 x=Gtx=Gt
30 2 25 28 29 fmptco G:absG=tGt
31 30 adantl G𝐿1G:absG=tGt
32 iblmbf G𝐿1GMblFn
33 ftc1anclem1 G:GMblFnabsGMblFn
34 32 33 sylan2 G:G𝐿1absGMblFn
35 34 ancoms G𝐿1G:absGMblFn
36 31 35 eqeltrrd G𝐿1G:tGtMblFn
37 36 3adant1 Fdom1G𝐿1G:tGtMblFn
38 2 abscld G:tGt
39 2 absge0d G:t0Gt
40 elrege0 Gt0+∞Gt0Gt
41 38 39 40 sylanbrc G:tGt0+∞
42 41 fmpttd G:tGt:0+∞
43 42 3ad2ant3 Fdom1G𝐿1G:tGt:0+∞
44 iftrue tiftGt0=Gt
45 44 mpteq2ia tiftGt0=tGt
46 45 fveq2i 2tiftGt0=2tGt
47 1 adantll G𝐿1G:tGt
48 simpr G𝐿1G:G:
49 48 feqmptd G𝐿1G:G=tGt
50 simpl G𝐿1G:G𝐿1
51 49 50 eqeltrrd G𝐿1G:tGt𝐿1
52 47 51 36 iblabsnc G𝐿1G:tGt𝐿1
53 38 adantll G𝐿1G:tGt
54 39 adantll G𝐿1G:t0Gt
55 53 54 iblpos G𝐿1G:tGt𝐿1tGtMblFn2tiftGt0
56 52 55 mpbid G𝐿1G:tGtMblFn2tiftGt0
57 56 simprd G𝐿1G:2tiftGt0
58 46 57 eqeltrrid G𝐿1G:2tGt
59 58 3adant1 Fdom1G𝐿1G:2tGt
60 5 abscld Fdom1tFt
61 5 absge0d Fdom1t0Ft
62 elrege0 Ft0+∞Ft0Ft
63 60 61 62 sylanbrc Fdom1tFt0+∞
64 63 fmpttd Fdom1tFt:0+∞
65 64 3ad2ant1 Fdom1G𝐿1G:tFt:0+∞
66 iftrue tiftFt0=Ft
67 66 mpteq2ia tiftFt0=tFt
68 67 fveq2i 2tiftFt0=2tFt
69 3 feqmptd Fdom1F=tFt
70 i1fibl Fdom1F𝐿1
71 69 70 eqeltrrd Fdom1tFt𝐿1
72 26 a1i Fdom1abs:
73 72 feqmptd Fdom1abs=xx
74 fveq2 x=Ftx=Ft
75 5 69 73 74 fmptco Fdom1absF=tFt
76 i1fmbf Fdom1FMblFn
77 ftc1anclem1 F:FMblFnabsFMblFn
78 3 76 77 syl2anc Fdom1absFMblFn
79 75 78 eqeltrrd Fdom1tFtMblFn
80 4 71 79 iblabsnc Fdom1tFt𝐿1
81 60 61 iblpos Fdom1tFt𝐿1tFtMblFn2tiftFt0
82 80 81 mpbid Fdom1tFtMblFn2tiftFt0
83 82 simprd Fdom12tiftFt0
84 68 83 eqeltrrid Fdom12tFt
85 84 3ad2ant1 Fdom1G𝐿1G:2tFt
86 37 43 59 65 85 itg2addnc Fdom1G𝐿1G:2tGt+ftFt=2tGt+2tFt
87 23 86 eqtr3d Fdom1G𝐿1G:2tGt+Ft=2tGt+2tFt
88 59 85 readdcld Fdom1G𝐿1G:2tGt+2tFt
89 87 88 eqeltrd Fdom1G𝐿1G:2tGt+Ft
90 readdcl GtFtGt+Ft
91 38 60 90 syl2anr Fdom1tG:tGt+Ft
92 91 anandirs Fdom1G:tGt+Ft
93 92 rexrd Fdom1G:tGt+Ft*
94 38 adantll Fdom1G:tGt
95 60 adantlr Fdom1G:tFt
96 39 adantll Fdom1G:t0Gt
97 61 adantlr Fdom1G:t0Ft
98 94 95 96 97 addge0d Fdom1G:t0Gt+Ft
99 elxrge0 Gt+Ft0+∞Gt+Ft*0Gt+Ft
100 93 98 99 sylanbrc Fdom1G:tGt+Ft0+∞
101 100 fmpttd Fdom1G:tGt+Ft:0+∞
102 101 3adant2 Fdom1G𝐿1G:tGt+Ft:0+∞
103 abs2dif2 GtFtGtFtGt+Ft
104 2 5 103 syl2anr Fdom1tG:tGtFtGt+Ft
105 104 anandirs Fdom1G:tGtFtGt+Ft
106 105 ralrimiva Fdom1G:tGtFtGt+Ft
107 16 a1i Fdom1G:V
108 eqidd Fdom1G:tGtFt=tGtFt
109 eqidd Fdom1G:tGt+Ft=tGt+Ft
110 107 9 92 108 109 ofrfval2 Fdom1G:tGtFtftGt+FttGtFtGt+Ft
111 106 110 mpbird Fdom1G:tGtFtftGt+Ft
112 111 3adant2 Fdom1G𝐿1G:tGtFtftGt+Ft
113 itg2le tGtFt:0+∞tGt+Ft:0+∞tGtFtftGt+Ft2tGtFt2tGt+Ft
114 15 102 112 113 syl3anc Fdom1G𝐿1G:2tGtFt2tGt+Ft
115 itg2lecl tGtFt:0+∞2tGt+Ft2tGtFt2tGt+Ft2tGtFt
116 15 89 114 115 syl3anc Fdom1G𝐿1G:2tGtFt