Metamath Proof Explorer

Theorem itg2monolem3

Description: Lemma for itg2mono . (Contributed by Mario Carneiro, 16-Aug-2014)

Ref Expression
Hypotheses itg2mono.1 ⊢G=x∈ℝ⟼supran⁡n∈ℕ⟼F⁡n⁡xℝ<
itg2mono.2 ⊢φ∧n∈ℕ→F⁡n∈MblFn
itg2mono.3 ⊢φ∧n∈ℕ→F⁡n:ℝ⟶0+∞
itg2mono.4 ⊢φ∧n∈ℕ→F⁡n≤fF⁡n+1
itg2mono.5 ⊢φ∧x∈ℝ→∃y∈ℝ∀n∈ℕF⁡n⁡x≤y
itg2mono.6 ⊢S=supran⁡n∈ℕ⟼∫2⁡F⁡nℝ*<
itg2monolem2.7 ⊢φ→P∈dom⁡∫1
itg2monolem2.8 ⊢φ→P≤fG
itg2monolem2.9 ⊢φ→¬∫1⁡P≤S
Assertion itg2monolem3 ⊢φ→∫1⁡P≤S

Proof

Step Hyp Ref Expression
1 itg2mono.1 ⊢G=x∈ℝ⟼supran⁡n∈ℕ⟼F⁡n⁡xℝ<
2 itg2mono.2 ⊢φ∧n∈ℕ→F⁡n∈MblFn
3 itg2mono.3 ⊢φ∧n∈ℕ→F⁡n:ℝ⟶0+∞
4 itg2mono.4 ⊢φ∧n∈ℕ→F⁡n≤fF⁡n+1
5 itg2mono.5 ⊢φ∧x∈ℝ→∃y∈ℝ∀n∈ℕF⁡n⁡x≤y
6 itg2mono.6 ⊢S=supran⁡n∈ℕ⟼∫2⁡F⁡nℝ*<
7 itg2monolem2.7 ⊢φ→P∈dom⁡∫1
8 itg2monolem2.8 ⊢φ→P≤fG
9 itg2monolem2.9 ⊢φ→¬∫1⁡P≤S
10 1 2 3 4 5 6 7 8 9 itg2monolem2 ⊢φ→S∈ℝ
11 10 adantr ⊢φ∧t∈ℝ+→S∈ℝ
12 11 recnd ⊢φ∧t∈ℝ+→S∈ℂ
13 7 adantr ⊢φ∧t∈ℝ+→P∈dom⁡∫1
14 itg1cl ⊢P∈dom⁡∫1→∫1⁡P∈ℝ
15 13 14 syl ⊢φ∧t∈ℝ+→∫1⁡P∈ℝ
16 15 recnd ⊢φ∧t∈ℝ+→∫1⁡P∈ℂ
17 simpr ⊢φ∧t∈ℝ+→t∈ℝ+
18 17 rpred ⊢φ∧t∈ℝ+→t∈ℝ
19 11 18 readdcld ⊢φ∧t∈ℝ+→S+t∈ℝ
20 19 recnd ⊢φ∧t∈ℝ+→S+t∈ℂ
21 0red ⊢φ∧t∈ℝ+→0∈ℝ
22 0xr ⊢0∈ℝ*
23 22 a1i ⊢φ→0∈ℝ*
24 fveq2 ⊢n=1→F⁡n=F⁡1
25 24 feq1d ⊢n=1→F⁡n:ℝ⟶0+∞↔F⁡1:ℝ⟶0+∞
26 icossicc ⊢0+∞⊆0+∞
27 fss ⊢F⁡n:ℝ⟶0+∞∧0+∞⊆0+∞→F⁡n:ℝ⟶0+∞
28 3 26 27 sylancl ⊢φ∧n∈ℕ→F⁡n:ℝ⟶0+∞
29 28 ralrimiva ⊢φ→∀n∈ℕF⁡n:ℝ⟶0+∞
30 1nn ⊢1∈ℕ
31 30 a1i ⊢φ→1∈ℕ
32 25 29 31 rspcdva ⊢φ→F⁡1:ℝ⟶0+∞
33 itg2cl ⊢F⁡1:ℝ⟶0+∞→∫2⁡F⁡1∈ℝ*
34 32 33 syl ⊢φ→∫2⁡F⁡1∈ℝ*
35 itg2cl ⊢F⁡n:ℝ⟶0+∞→∫2⁡F⁡n∈ℝ*
36 28 35 syl ⊢φ∧n∈ℕ→∫2⁡F⁡n∈ℝ*
37 36 fmpttd ⊢φ→n∈ℕ⟼∫2⁡F⁡n:ℕ⟶ℝ*
38 37 frnd ⊢φ→ran⁡n∈ℕ⟼∫2⁡F⁡n⊆ℝ*
39 supxrcl ⊢ran⁡n∈ℕ⟼∫2⁡F⁡n⊆ℝ*→supran⁡n∈ℕ⟼∫2⁡F⁡nℝ*<∈ℝ*
40 38 39 syl ⊢φ→supran⁡n∈ℕ⟼∫2⁡F⁡nℝ*<∈ℝ*
41 6 40 eqeltrid ⊢φ→S∈ℝ*
42 itg2ge0 ⊢F⁡1:ℝ⟶0+∞→0≤∫2⁡F⁡1
43 32 42 syl ⊢φ→0≤∫2⁡F⁡1
44 2fveq3 ⊢n=1→∫2⁡F⁡n=∫2⁡F⁡1
45 eqid ⊢n∈ℕ⟼∫2⁡F⁡n=n∈ℕ⟼∫2⁡F⁡n
46 fvex ⊢∫2⁡F⁡1∈V
47 44 45 46 fvmpt ⊢1∈ℕ→n∈ℕ⟼∫2⁡F⁡n⁡1=∫2⁡F⁡1
48 30 47 ax-mp ⊢n∈ℕ⟼∫2⁡F⁡n⁡1=∫2⁡F⁡1
49 37 ffnd ⊢φ→n∈ℕ⟼∫2⁡F⁡nFnℕ
50 fnfvelrn ⊢n∈ℕ⟼∫2⁡F⁡nFnℕ∧1∈ℕ→n∈ℕ⟼∫2⁡F⁡n⁡1∈ran⁡n∈ℕ⟼∫2⁡F⁡n
51 49 30 50 sylancl ⊢φ→n∈ℕ⟼∫2⁡F⁡n⁡1∈ran⁡n∈ℕ⟼∫2⁡F⁡n
52 48 51 eqeltrrid ⊢φ→∫2⁡F⁡1∈ran⁡n∈ℕ⟼∫2⁡F⁡n
53 supxrub ⊢ran⁡n∈ℕ⟼∫2⁡F⁡n⊆ℝ*∧∫2⁡F⁡1∈ran⁡n∈ℕ⟼∫2⁡F⁡n→∫2⁡F⁡1≤supran⁡n∈ℕ⟼∫2⁡F⁡nℝ*<
54 38 52 53 syl2anc ⊢φ→∫2⁡F⁡1≤supran⁡n∈ℕ⟼∫2⁡F⁡nℝ*<
55 54 6 breqtrrdi ⊢φ→∫2⁡F⁡1≤S
56 23 34 41 43 55 xrletrd ⊢φ→0≤S
57 56 adantr ⊢φ∧t∈ℝ+→0≤S
58 11 17 ltaddrpd ⊢φ∧t∈ℝ+→S<S+t
59 21 11 19 57 58 lelttrd ⊢φ∧t∈ℝ+→0<S+t
60 59 gt0ne0d ⊢φ∧t∈ℝ+→S+t≠0
61 12 16 20 60 div23d ⊢φ∧t∈ℝ+→S⁢∫1⁡PS+t=SS+t⁢∫1⁡P
62 11 19 60 redivcld ⊢φ∧t∈ℝ+→SS+t∈ℝ
63 62 15 remulcld ⊢φ∧t∈ℝ+→SS+t⁢∫1⁡P∈ℝ
64 halfre ⊢12∈ℝ
65 ifcl ⊢SS+t∈ℝ∧12∈ℝ→if12≤SS+tSS+t12∈ℝ
66 62 64 65 sylancl ⊢φ∧t∈ℝ+→if12≤SS+tSS+t12∈ℝ
67 66 15 remulcld ⊢φ∧t∈ℝ+→if12≤SS+tSS+t12⁢∫1⁡P∈ℝ
68 max2 ⊢12∈ℝ∧SS+t∈ℝ→SS+t≤if12≤SS+tSS+t12
69 64 62 68 sylancr ⊢φ∧t∈ℝ+→SS+t≤if12≤SS+tSS+t12
70 7 14 syl ⊢φ→∫1⁡P∈ℝ
71 70 rexrd ⊢φ→∫1⁡P∈ℝ*
72 xrltnle ⊢S∈ℝ*∧∫1⁡P∈ℝ*→S<∫1⁡P↔¬∫1⁡P≤S
73 41 71 72 syl2anc ⊢φ→S<∫1⁡P↔¬∫1⁡P≤S
74 9 73 mpbird ⊢φ→S<∫1⁡P
75 74 adantr ⊢φ∧t∈ℝ+→S<∫1⁡P
76 21 11 15 57 75 lelttrd ⊢φ∧t∈ℝ+→0<∫1⁡P
77 lemul1 ⊢SS+t∈ℝ∧if12≤SS+tSS+t12∈ℝ∧∫1⁡P∈ℝ∧0<∫1⁡P→SS+t≤if12≤SS+tSS+t12↔SS+t⁢∫1⁡P≤if12≤SS+tSS+t12⁢∫1⁡P
78 62 66 15 76 77 syl112anc ⊢φ∧t∈ℝ+→SS+t≤if12≤SS+tSS+t12↔SS+t⁢∫1⁡P≤if12≤SS+tSS+t12⁢∫1⁡P
79 69 78 mpbid ⊢φ∧t∈ℝ+→SS+t⁢∫1⁡P≤if12≤SS+tSS+t12⁢∫1⁡P
80 2 adantlr ⊢φ∧t∈ℝ+∧n∈ℕ→F⁡n∈MblFn
81 3 adantlr ⊢φ∧t∈ℝ+∧n∈ℕ→F⁡n:ℝ⟶0+∞
82 4 adantlr ⊢φ∧t∈ℝ+∧n∈ℕ→F⁡n≤fF⁡n+1
83 5 adantlr ⊢φ∧t∈ℝ+∧x∈ℝ→∃y∈ℝ∀n∈ℕF⁡n⁡x≤y
84 64 a1i ⊢φ∧t∈ℝ+→12∈ℝ
85 halfgt0 ⊢0<12
86 85 a1i ⊢φ∧t∈ℝ+→0<12
87 max1 ⊢12∈ℝ∧SS+t∈ℝ→12≤if12≤SS+tSS+t12
88 64 62 87 sylancr ⊢φ∧t∈ℝ+→12≤if12≤SS+tSS+t12
89 21 84 66 86 88 ltletrd ⊢φ∧t∈ℝ+→0<if12≤SS+tSS+t12
90 20 mulridd ⊢φ∧t∈ℝ+→S+t⋅1=S+t
91 58 90 breqtrrd ⊢φ∧t∈ℝ+→S<S+t⋅1
92 1red ⊢φ∧t∈ℝ+→1∈ℝ
93 ltdivmul ⊢S∈ℝ∧1∈ℝ∧S+t∈ℝ∧0<S+t→SS+t<1↔S<S+t⋅1
94 11 92 19 59 93 syl112anc ⊢φ∧t∈ℝ+→SS+t<1↔S<S+t⋅1
95 91 94 mpbird ⊢φ∧t∈ℝ+→SS+t<1
96 halflt1 ⊢12<1
97 breq1 ⊢SS+t=if12≤SS+tSS+t12→SS+t<1↔if12≤SS+tSS+t12<1
98 breq1 ⊢12=if12≤SS+tSS+t12→12<1↔if12≤SS+tSS+t12<1
99 97 98 ifboth ⊢SS+t<1∧12<1→if12≤SS+tSS+t12<1
100 95 96 99 sylancl ⊢φ∧t∈ℝ+→if12≤SS+tSS+t12<1
101 1xr ⊢1∈ℝ*
102 elioo2 ⊢0∈ℝ*∧1∈ℝ*→if12≤SS+tSS+t12∈01↔if12≤SS+tSS+t12∈ℝ∧0<if12≤SS+tSS+t12∧if12≤SS+tSS+t12<1
103 22 101 102 mp2an ⊢if12≤SS+tSS+t12∈01↔if12≤SS+tSS+t12∈ℝ∧0<if12≤SS+tSS+t12∧if12≤SS+tSS+t12<1
104 66 89 100 103 syl3anbrc ⊢φ∧t∈ℝ+→if12≤SS+tSS+t12∈01
105 8 adantr ⊢φ∧t∈ℝ+→P≤fG
106 fveq2 ⊢y=x→P⁡y=P⁡x
107 106 oveq2d ⊢y=x→if12≤SS+tSS+t12⁢P⁡y=if12≤SS+tSS+t12⁢P⁡x
108 fveq2 ⊢y=x→F⁡n⁡y=F⁡n⁡x
109 107 108 breq12d ⊢y=x→if12≤SS+tSS+t12⁢P⁡y≤F⁡n⁡y↔if12≤SS+tSS+t12⁢P⁡x≤F⁡n⁡x
110 109 cbvrabv ⊢y∈ℝ|if12≤SS+tSS+t12⁢P⁡y≤F⁡n⁡y=x∈ℝ|if12≤SS+tSS+t12⁢P⁡x≤F⁡n⁡x
111 110 mpteq2i ⊢n∈ℕ⟼y∈ℝ|if12≤SS+tSS+t12⁢P⁡y≤F⁡n⁡y=n∈ℕ⟼x∈ℝ|if12≤SS+tSS+t12⁢P⁡x≤F⁡n⁡x
112 1 80 81 82 83 6 104 13 105 11 111 itg2monolem1 ⊢φ∧t∈ℝ+→if12≤SS+tSS+t12⁢∫1⁡P≤S
113 63 67 11 79 112 letrd ⊢φ∧t∈ℝ+→SS+t⁢∫1⁡P≤S
114 61 113 eqbrtrd ⊢φ∧t∈ℝ+→S⁢∫1⁡PS+t≤S
115 11 15 remulcld ⊢φ∧t∈ℝ+→S⁢∫1⁡P∈ℝ
116 ledivmul2 ⊢S⁢∫1⁡P∈ℝ∧S∈ℝ∧S+t∈ℝ∧0<S+t→S⁢∫1⁡PS+t≤S↔S⁢∫1⁡P≤S⁢S+t
117 115 11 19 59 116 syl112anc ⊢φ∧t∈ℝ+→S⁢∫1⁡PS+t≤S↔S⁢∫1⁡P≤S⁢S+t
118 114 117 mpbid ⊢φ∧t∈ℝ+→S⁢∫1⁡P≤S⁢S+t
119 66 15 89 76 mulgt0d ⊢φ∧t∈ℝ+→0<if12≤SS+tSS+t12⁢∫1⁡P
120 21 67 11 119 112 ltletrd ⊢φ∧t∈ℝ+→0<S
121 lemul2 ⊢∫1⁡P∈ℝ∧S+t∈ℝ∧S∈ℝ∧0<S→∫1⁡P≤S+t↔S⁢∫1⁡P≤S⁢S+t
122 15 19 11 120 121 syl112anc ⊢φ∧t∈ℝ+→∫1⁡P≤S+t↔S⁢∫1⁡P≤S⁢S+t
123 118 122 mpbird ⊢φ∧t∈ℝ+→∫1⁡P≤S+t
124 123 ralrimiva ⊢φ→∀t∈ℝ+∫1⁡P≤S+t
125 alrple ⊢∫1⁡P∈ℝ∧S∈ℝ→∫1⁡P≤S↔∀t∈ℝ+∫1⁡P≤S+t
126 70 10 125 syl2anc ⊢φ→∫1⁡P≤S↔∀t∈ℝ+∫1⁡P≤S+t
127 124 126 mpbird ⊢φ→∫1⁡P≤S