This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg2monolem2

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

Ref Expression
Hypotheses itg2mono.1 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
itg2mono.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ MblFn )
itg2mono.3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) )
itg2mono.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
itg2mono.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
itg2mono.6 ⊢ 𝑆 = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < )
itg2monolem2.7 ⊢ ( 𝜑 → 𝑃 ∈ dom ∫1 )
itg2monolem2.8 ⊢ ( 𝜑 → 𝑃 ∘r ≤ 𝐺 )
itg2monolem2.9 ⊢ ( 𝜑 → ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 )
Assertion itg2monolem2 ( 𝜑 → 𝑆 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 itg2mono.1 ⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
2 itg2mono.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ MblFn )
3 itg2mono.3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) )
4 itg2mono.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
5 itg2mono.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
6 itg2mono.6 ⊢ 𝑆 = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < )
7 itg2monolem2.7 ⊢ ( 𝜑 → 𝑃 ∈ dom ∫1 )
8 itg2monolem2.8 ⊢ ( 𝜑 → 𝑃 ∘r ≤ 𝐺 )
9 itg2monolem2.9 ⊢ ( 𝜑 → ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 )
10 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
11 fss ⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
12 3 10 11 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
13 itg2cl ⊢ ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
14 12 13 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
15 14 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ* )
16 15 frnd ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* )
17 supxrcl ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
18 16 17 syl ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
19 6 18 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
20 itg1cl ⊢ ( 𝑃 ∈ dom ∫1 → ( ∫1 ‘ 𝑃 ) ∈ ℝ )
21 7 20 syl ⊢ ( 𝜑 → ( ∫1 ‘ 𝑃 ) ∈ ℝ )
22 mnfxr ⊢ -∞ ∈ ℝ*
23 22 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
24 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) )
25 24 feq1d ⊢ ( 𝑛 = 1 → ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) ↔ ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) ) )
26 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
27 1nn ⊢ 1 ∈ ℕ
28 27 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
29 25 26 28 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) )
30 itg2cl ⊢ ( ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ℝ* )
31 29 30 syl ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ℝ* )
32 itg2ge0 ⊢ ( ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) → 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
33 29 32 syl ⊢ ( 𝜑 → 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
34 mnflt0 ⊢ -∞ < 0
35 0xr ⊢ 0 ∈ ℝ*
36 xrltletr ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) → -∞ < ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) )
37 22 35 31 36 mp3an12i ⊢ ( 𝜑 → ( ( -∞ < 0 ∧ 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) → -∞ < ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) )
38 34 37 mpani ⊢ ( 𝜑 → ( 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) → -∞ < ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) )
39 33 38 mpd ⊢ ( 𝜑 → -∞ < ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
40 2fveq3 ⊢ ( 𝑛 = 1 → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
41 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) )
42 fvex ⊢ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ V
43 40 41 42 fvmpt ⊢ ( 1 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) = ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
44 27 43 ax-mp ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) = ( ∫2 ‘ ( 𝐹 ‘ 1 ) )
45 15 ffnd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ )
46 fnfvelrn ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ ∧ 1 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
47 45 27 46 sylancl ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
48 44 47 eqeltrrid ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
49 supxrub ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* ∧ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) )
50 16 48 49 syl2anc ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) )
51 50 6 breqtrrdi ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ≤ 𝑆 )
52 23 31 19 39 51 xrltletrd ⊢ ( 𝜑 → -∞ < 𝑆 )
53 21 rexrd ⊢ ( 𝜑 → ( ∫1 ‘ 𝑃 ) ∈ ℝ* )
54 xrltnle ⊢ ( ( 𝑆 ∈ ℝ* ∧ ( ∫1 ‘ 𝑃 ) ∈ ℝ* ) → ( 𝑆 < ( ∫1 ‘ 𝑃 ) ↔ ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 ) )
55 19 53 54 syl2anc ⊢ ( 𝜑 → ( 𝑆 < ( ∫1 ‘ 𝑃 ) ↔ ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 ) )
56 9 55 mpbird ⊢ ( 𝜑 → 𝑆 < ( ∫1 ‘ 𝑃 ) )
57 19 53 56 xrltled ⊢ ( 𝜑 → 𝑆 ≤ ( ∫1 ‘ 𝑃 ) )
58 xrre ⊢ ( ( ( 𝑆 ∈ ℝ* ∧ ( ∫1 ‘ 𝑃 ) ∈ ℝ ) ∧ ( -∞ < 𝑆 ∧ 𝑆 ≤ ( ∫1 ‘ 𝑃 ) ) ) → 𝑆 ∈ ℝ )
59 19 21 52 57 58 syl22anc ⊢ ( 𝜑 → 𝑆 ∈ ℝ )