Metamath Proof Explorer

Theorem itg2i1fseq

Description: Subject to the conditions coming from mbfi1fseq , the integral of the sequence of simple functions converges to the integral of the target function. (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 ‘ ( 𝑃 ‘ 𝑚 ) ) )
Assertion itg2i1fseq ( 𝜑 → ( ∫2 ‘ 𝐹 ) = sup ( ran 𝑆 , ℝ* , < ) )

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 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑃 ‘ 𝑛 ) = ( 𝑃 ‘ 𝑚 ) )
8 7 fveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑥 ) )
9 8 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑥 ) )
10 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) )
11 10 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ) )
12 9 11 eqtrid ⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ) )
13 12 rneqd ⊢ ( 𝑥 = 𝑦 → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ) )
14 13 supeq1d ⊢ ( 𝑥 = 𝑦 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) )
15 14 cbvmptv ⊢ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑦 ∈ ℝ ↦ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) )
16 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ 𝑚 ) ∈ dom ∫1 )
17 i1fmbf ⊢ ( ( 𝑃 ‘ 𝑚 ) ∈ dom ∫1 → ( 𝑃 ‘ 𝑚 ) ∈ MblFn )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ 𝑚 ) ∈ MblFn )
19 i1ff ⊢ ( ( 𝑃 ‘ 𝑚 ) ∈ dom ∫1 → ( 𝑃 ‘ 𝑚 ) : ℝ ⟶ ℝ )
20 16 19 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ 𝑚 ) : ℝ ⟶ ℝ )
21 7 breq2d ⊢ ( 𝑛 = 𝑚 → ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑛 ) ↔ 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑚 ) ) )
22 fvoveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑃 ‘ ( 𝑛 + 1 ) ) = ( 𝑃 ‘ ( 𝑚 + 1 ) ) )
23 7 22 breq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝑃 ‘ 𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ) )
24 21 23 anbi12d ⊢ ( 𝑛 = 𝑚 → ( ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) ↔ ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑚 ) ∧ ( 𝑃 ‘ 𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ) ) )
25 24 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑚 ) ∧ ( 𝑃 ‘ 𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ) )
26 4 25 sylan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑚 ) ∧ ( 𝑃 ‘ 𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ) )
27 26 simpld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑚 ) )
28 0plef ⊢ ( ( 𝑃 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( ( 𝑃 ‘ 𝑚 ) : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑚 ) ) )
29 20 27 28 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) )
30 26 simprd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ 𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) )
31 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
32 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
33 31 32 sselid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
34 1 2 3 4 5 itg2i1fseqle ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ 𝑚 ) ∘r ≤ 𝐹 )
35 20 ffnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ 𝑚 ) Fn ℝ )
36 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐹 Fn ℝ )
38 reex ⊢ ℝ ∈ V
39 38 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ℝ ∈ V )
40 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
41 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) )
42 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
43 35 37 39 39 40 41 42 ofrfval ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑚 ) ∘r ≤ 𝐹 ↔ ∀ 𝑦 ∈ ℝ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
44 34 43 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∀ 𝑦 ∈ ℝ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) )
45 44 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) )
46 45 an32s ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) )
47 46 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∀ 𝑚 ∈ ℕ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) )
48 brralrspcev ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
49 33 47 48 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
50 7 fveq2d ⊢ ( 𝑛 = 𝑚 → ( ∫2 ‘ ( 𝑃 ‘ 𝑛 ) ) = ( ∫2 ‘ ( 𝑃 ‘ 𝑚 ) ) )
51 50 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑛 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑚 ) ) )
52 51 rneqi ⊢ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑛 ) ) ) = ran ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑚 ) ) )
53 52 supeq1i ⊢ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑛 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑚 ) ) ) , ℝ* , < )
54 15 18 29 30 49 53 itg2mono ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑛 ) ) ) , ℝ* , < ) )
55 2 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
56 7 fveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) = ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) )
57 56 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) )
58 57 rneqi ⊢ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) = ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) )
59 58 supeq1i ⊢ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < )
60 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
61 1zzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℤ )
62 20 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ∈ ℝ )
63 62 an32s ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ∈ ℝ )
64 63 57 fmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) : ℕ ⟶ ℝ )
65 peano2nn ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
66 ffvelcdm ⊢ ( ( 𝑃 : ℕ ⟶ dom ∫1 ∧ ( 𝑚 + 1 ) ∈ ℕ ) → ( 𝑃 ‘ ( 𝑚 + 1 ) ) ∈ dom ∫1 )
67 3 65 66 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑚 + 1 ) ) ∈ dom ∫1 )
68 i1ff ⊢ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ∈ dom ∫1 → ( 𝑃 ‘ ( 𝑚 + 1 ) ) : ℝ ⟶ ℝ )
69 67 68 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑚 + 1 ) ) : ℝ ⟶ ℝ )
70 69 ffnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑚 + 1 ) ) Fn ℝ )
71 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
72 35 70 39 39 40 41 71 ofrfval ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑚 ) ∘r ≤ ( 𝑃 ‘ ( 𝑚 + 1 ) ) ↔ ∀ 𝑦 ∈ ℝ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) ) )
73 30 72 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∀ 𝑦 ∈ ℝ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
74 73 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
75 74 an32s ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
76 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) )
77 fvex ⊢ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ∈ V
78 56 76 77 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) = ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) )
79 78 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) = ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) )
80 fveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑃 ‘ 𝑛 ) = ( 𝑃 ‘ ( 𝑚 + 1 ) ) )
81 80 fveq1d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
82 fvex ⊢ ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) ∈ V
83 81 76 82 fvmpt ⊢ ( ( 𝑚 + 1 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
84 65 83 syl ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
85 84 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑚 + 1 ) ) ‘ 𝑦 ) )
86 75 79 85 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑚 + 1 ) ) )
87 78 breq1d ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ 𝑧 ↔ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ 𝑧 ) )
88 87 ralbiia ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ 𝑧 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
89 88 rexbii ⊢ ( ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ 𝑧 ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ≤ 𝑧 )
90 49 89 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ‘ 𝑚 ) ≤ 𝑧 )
91 60 61 64 86 90 climsup ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) )
92 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) )
93 92 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) )
94 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
95 93 94 breq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹 ‘ 𝑦 ) ) )
96 95 rspccva ⊢ ( ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹 ‘ 𝑦 ) )
97 5 96 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹 ‘ 𝑦 ) )
98 climuni ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) ∧ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹 ‘ 𝑦 ) ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) = ( 𝐹 ‘ 𝑦 ) )
99 91 97 98 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) = ( 𝐹 ‘ 𝑦 ) )
100 59 99 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) = ( 𝐹 ‘ 𝑦 ) )
101 100 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
102 55 101 eqtr4d ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ ↦ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑚 ) ‘ 𝑦 ) ) , ℝ , < ) ) )
103 102 15 eqtr4di ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
104 103 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) ) )
105 itg2itg1 ⊢ ( ( ( 𝑃 ‘ 𝑚 ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑚 ) ) → ( ∫2 ‘ ( 𝑃 ‘ 𝑚 ) ) = ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) )
106 16 27 105 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∫2 ‘ ( 𝑃 ‘ 𝑚 ) ) = ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) )
107 106 mpteq2dva ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) ) )
108 6 107 eqtr4id ⊢ ( 𝜑 → 𝑆 = ( 𝑚 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑚 ) ) ) )
109 108 51 eqtr4di ⊢ ( 𝜑 → 𝑆 = ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑛 ) ) ) )
110 109 rneqd ⊢ ( 𝜑 → ran 𝑆 = ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑛 ) ) ) )
111 110 supeq1d ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝑃 ‘ 𝑛 ) ) ) , ℝ* , < ) )
112 54 104 111 3eqtr4d ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) = sup ( ran 𝑆 , ℝ* , < ) )