Metamath Proof Explorer

Theorem itg2i1fseq2

Description: In an extension to the results of itg2i1fseq , if there is an upper bound on the integrals of the simple functions approaching F , then S.2 F is real and the standard limit relation applies. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itg2i1fseq.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
itg2i1fseq.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2i1fseq.3 ⊢ ( 𝜑 → 𝑃 : ℕ ⟶ dom ∫1 )
itg2i1fseq.4 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) )
itg2i1fseq.5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) )
itg2i1fseq.6 ⊢ 𝑆 = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) )
itg2i1fseq2.7 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
itg2i1fseq2.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) ≤ 𝑀 )
Assertion itg2i1fseq2 ( 𝜑 → 𝑆 ⇝ ( ∫2 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 itg2i1fseq.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 itg2i1fseq.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
3 itg2i1fseq.3 ⊢ ( 𝜑 → 𝑃 : ℕ ⟶ dom ∫1 )
4 itg2i1fseq.4 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) )
5 itg2i1fseq.5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) )
6 itg2i1fseq.6 ⊢ 𝑆 = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) )
7 itg2i1fseq2.7 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
8 itg2i1fseq2.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) ≤ 𝑀 )
9 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
10 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
11 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ 𝑚 ) ∈ dom ∫1 )
12 itg1cl ⊢ ( ( 𝑃 ‘ 𝑚 ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) ∈ ℝ )
13 11 12 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) ∈ ℝ )
14 13 6 fmptd ⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ℝ )
15 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ‘ 𝑘 ) ∈ dom ∫1 )
16 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
17 ffvelcdm ⊢ ( ( 𝑃 : ℕ ⟶ dom ∫1 ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ dom ∫1 )
18 3 16 17 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ dom ∫1 )
19 simpr ⊢ ( ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) → ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) )
20 19 ralimi ⊢ ( ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) )
21 4 20 syl ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) )
22 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑃 ‘ 𝑛 ) = ( 𝑃 ‘ 𝑘 ) )
23 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑃 ‘ ( 𝑛 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
24 22 23 breq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝑃 ‘ 𝑘 ) ∘r ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
25 24 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ‘ 𝑘 ) ∘r ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
26 21 25 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ‘ 𝑘 ) ∘r ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
27 itg1le ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ dom ∫1 ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ dom ∫1 ∧ ( 𝑃 ‘ 𝑘 ) ∘r ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) → ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) ≤ ( ∫1 ‘ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
28 15 18 26 27 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) ≤ ( ∫1 ‘ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
29 2fveq3 ⊢ ( 𝑚 = 𝑘 → ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) = ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) )
30 fvex ⊢ ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) ∈ V
31 29 6 30 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝑆 ‘ 𝑘 ) = ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) = ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) )
33 2fveq3 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) = ( ∫1 ‘ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
34 fvex ⊢ ( ∫1 ‘ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ∈ V
35 33 6 34 fvmpt ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ∫1 ‘ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
36 16 35 syl ⊢ ( 𝑘 ∈ ℕ → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ∫1 ‘ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ∫1 ‘ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
38 28 32 37 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ≤ ( 𝑆 ‘ ( 𝑘 + 1 ) ) )
39 32 8 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ≤ 𝑀 )
40 39 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑀 )
41 brralrspcev ⊢ ( ( 𝑀 ∈ ℝ ∧ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑀 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑧 )
42 7 40 41 syl2anc ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑧 )
43 9 10 14 38 42 climsup ⊢ ( 𝜑 → 𝑆 ⇝ sup ( ran 𝑆 , ℝ , < ) )
44 1 2 3 4 5 6 itg2i1fseq ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) = sup ( ran 𝑆 , ℝ* , < ) )
45 14 frnd ⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ )
46 6 13 dmmptd ⊢ ( 𝜑 → dom 𝑆 = ℕ )
47 1nn ⊢ 1 ∈ ℕ
48 ne0i ⊢ ( 1 ∈ ℕ → ℕ ≠ ∅ )
49 47 48 mp1i ⊢ ( 𝜑 → ℕ ≠ ∅ )
50 46 49 eqnetrd ⊢ ( 𝜑 → dom 𝑆 ≠ ∅ )
51 dm0rn0 ⊢ ( dom 𝑆 = ∅ ↔ ran 𝑆 = ∅ )
52 51 necon3bii ⊢ ( dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅ )
53 50 52 sylib ⊢ ( 𝜑 → ran 𝑆 ≠ ∅ )
54 ffn ⊢ ( 𝑆 : ℕ ⟶ ℝ → 𝑆 Fn ℕ )
55 breq1 ⊢ ( 𝑦 = ( 𝑆 ‘ 𝑘 ) → ( 𝑦 ≤ 𝑧 ↔ ( 𝑆 ‘ 𝑘 ) ≤ 𝑧 ) )
56 55 ralrn ⊢ ( 𝑆 Fn ℕ → ( ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧 ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑧 ) )
57 14 54 56 3syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧 ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑧 ) )
58 57 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ℝ ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧 ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ 𝑧 ) )
59 42 58 mpbird ⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧 )
60 supxrre ⊢ ( ( ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧 ) → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran 𝑆 , ℝ , < ) )
61 45 53 59 60 syl3anc ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran 𝑆 , ℝ , < ) )
62 44 61 eqtrd ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) = sup ( ran 𝑆 , ℝ , < ) )
63 43 62 breqtrrd ⊢ ( 𝜑 → 𝑆 ⇝ ( ∫2 ‘ 𝐹 ) )