Metamath Proof Explorer


Theorem itg2i1fseqle

Description: Subject to the conditions coming from mbfi1fseq , the sequence of simple functions are all less than the target function F . (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 ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) )
Assertion itg2i1fseqle ( ( 𝜑𝑀 ∈ ℕ ) → ( 𝑃𝑀 ) ∘r𝐹 )

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 fveq2 ( 𝑛 = 𝑀 → ( 𝑃𝑛 ) = ( 𝑃𝑀 ) )
7 6 fveq1d ( 𝑛 = 𝑀 → ( ( 𝑃𝑛 ) ‘ 𝑦 ) = ( ( 𝑃𝑀 ) ‘ 𝑦 ) )
8 eqid ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) )
9 fvex ( ( 𝑃𝑀 ) ‘ 𝑦 ) ∈ V
10 7 8 9 fvmpt ( 𝑀 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑀 ) = ( ( 𝑃𝑀 ) ‘ 𝑦 ) )
11 10 ad2antlr ( ( ( 𝜑𝑀 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑀 ) = ( ( 𝑃𝑀 ) ‘ 𝑦 ) )
12 nnuz ℕ = ( ℤ ‘ 1 )
13 simplr ( ( ( 𝜑𝑀 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → 𝑀 ∈ ℕ )
14 fveq2 ( 𝑥 = 𝑦 → ( ( 𝑃𝑛 ) ‘ 𝑥 ) = ( ( 𝑃𝑛 ) ‘ 𝑦 ) )
15 14 mpteq2dv ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) )
16 fveq2 ( 𝑥 = 𝑦 → ( 𝐹𝑥 ) = ( 𝐹𝑦 ) )
17 15 16 breq12d ( 𝑥 = 𝑦 → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹𝑦 ) ) )
18 17 rspccva ( ( ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹𝑥 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹𝑦 ) )
19 5 18 sylan ( ( 𝜑𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹𝑦 ) )
20 19 adantlr ( ( ( 𝜑𝑀 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ⇝ ( 𝐹𝑦 ) )
21 fveq2 ( 𝑛 = 𝑘 → ( 𝑃𝑛 ) = ( 𝑃𝑘 ) )
22 21 fveq1d ( 𝑛 = 𝑘 → ( ( 𝑃𝑛 ) ‘ 𝑦 ) = ( ( 𝑃𝑘 ) ‘ 𝑦 ) )
23 fvex ( ( 𝑃𝑘 ) ‘ 𝑦 ) ∈ V
24 22 8 23 fvmpt ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) = ( ( 𝑃𝑘 ) ‘ 𝑦 ) )
25 24 adantl ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) = ( ( 𝑃𝑘 ) ‘ 𝑦 ) )
26 3 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑃𝑘 ) ∈ dom ∫1 )
27 i1ff ( ( 𝑃𝑘 ) ∈ dom ∫1 → ( 𝑃𝑘 ) : ℝ ⟶ ℝ )
28 26 27 syl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑃𝑘 ) : ℝ ⟶ ℝ )
29 28 ffvelrnda ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃𝑘 ) ‘ 𝑦 ) ∈ ℝ )
30 29 an32s ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑃𝑘 ) ‘ 𝑦 ) ∈ ℝ )
31 25 30 eqeltrd ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) ∈ ℝ )
32 31 adantllr ( ( ( ( 𝜑𝑀 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) ∈ ℝ )
33 simpr ( ( 0𝑝r ≤ ( 𝑃𝑛 ) ∧ ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) → ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) )
34 33 ralimi ( ∀ 𝑛 ∈ ℕ ( 0𝑝r ≤ ( 𝑃𝑛 ) ∧ ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) )
35 4 34 syl ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) )
36 fvoveq1 ( 𝑛 = 𝑘 → ( 𝑃 ‘ ( 𝑛 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
37 21 36 breq12d ( 𝑛 = 𝑘 → ( ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝑃𝑘 ) ∘r ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
38 37 rspccva ( ( ∀ 𝑛 ∈ ℕ ( 𝑃𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑃𝑘 ) ∘r ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
39 35 38 sylan ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑃𝑘 ) ∘r ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
40 ffn ( ( 𝑃𝑘 ) : ℝ ⟶ ℝ → ( 𝑃𝑘 ) Fn ℝ )
41 26 27 40 3syl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑃𝑘 ) Fn ℝ )
42 peano2nn ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
43 ffvelrn ( ( 𝑃 : ℕ ⟶ dom ∫1 ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ dom ∫1 )
44 3 42 43 syl2an ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ dom ∫1 )
45 i1ff ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ dom ∫1 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) : ℝ ⟶ ℝ )
46 ffn ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) : ℝ ⟶ ℝ → ( 𝑃 ‘ ( 𝑘 + 1 ) ) Fn ℝ )
47 44 45 46 3syl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) Fn ℝ )
48 reex ℝ ∈ V
49 48 a1i ( ( 𝜑𝑘 ∈ ℕ ) → ℝ ∈ V )
50 inidm ( ℝ ∩ ℝ ) = ℝ
51 eqidd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃𝑘 ) ‘ 𝑦 ) = ( ( 𝑃𝑘 ) ‘ 𝑦 ) )
52 eqidd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) = ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) )
53 41 47 49 49 50 51 52 ofrfval ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑃𝑘 ) ∘r ≤ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ∀ 𝑦 ∈ ℝ ( ( 𝑃𝑘 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) ) )
54 39 53 mpbid ( ( 𝜑𝑘 ∈ ℕ ) → ∀ 𝑦 ∈ ℝ ( ( 𝑃𝑘 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) )
55 54 r19.21bi ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃𝑘 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) )
56 55 an32s ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑃𝑘 ) ‘ 𝑦 ) ≤ ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) )
57 fveq2 ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑃𝑛 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
58 57 fveq1d ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝑃𝑛 ) ‘ 𝑦 ) = ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) )
59 fvex ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) ∈ V
60 58 8 59 fvmpt ( ( 𝑘 + 1 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) )
61 42 60 syl ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) )
62 61 adantl ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) ‘ 𝑦 ) )
63 56 25 62 3brtr4d ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑘 + 1 ) ) )
64 63 adantllr ( ( ( ( 𝜑𝑀 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ ( 𝑘 + 1 ) ) )
65 12 13 20 32 64 climub ( ( ( 𝜑𝑀 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑃𝑛 ) ‘ 𝑦 ) ) ‘ 𝑀 ) ≤ ( 𝐹𝑦 ) )
66 11 65 eqbrtrrd ( ( ( 𝜑𝑀 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃𝑀 ) ‘ 𝑦 ) ≤ ( 𝐹𝑦 ) )
67 66 ralrimiva ( ( 𝜑𝑀 ∈ ℕ ) → ∀ 𝑦 ∈ ℝ ( ( 𝑃𝑀 ) ‘ 𝑦 ) ≤ ( 𝐹𝑦 ) )
68 3 ffvelrnda ( ( 𝜑𝑀 ∈ ℕ ) → ( 𝑃𝑀 ) ∈ dom ∫1 )
69 i1ff ( ( 𝑃𝑀 ) ∈ dom ∫1 → ( 𝑃𝑀 ) : ℝ ⟶ ℝ )
70 ffn ( ( 𝑃𝑀 ) : ℝ ⟶ ℝ → ( 𝑃𝑀 ) Fn ℝ )
71 68 69 70 3syl ( ( 𝜑𝑀 ∈ ℕ ) → ( 𝑃𝑀 ) Fn ℝ )
72 2 ffnd ( 𝜑𝐹 Fn ℝ )
73 72 adantr ( ( 𝜑𝑀 ∈ ℕ ) → 𝐹 Fn ℝ )
74 48 a1i ( ( 𝜑𝑀 ∈ ℕ ) → ℝ ∈ V )
75 eqidd ( ( ( 𝜑𝑀 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃𝑀 ) ‘ 𝑦 ) = ( ( 𝑃𝑀 ) ‘ 𝑦 ) )
76 eqidd ( ( ( 𝜑𝑀 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹𝑦 ) = ( 𝐹𝑦 ) )
77 71 73 74 74 50 75 76 ofrfval ( ( 𝜑𝑀 ∈ ℕ ) → ( ( 𝑃𝑀 ) ∘r𝐹 ↔ ∀ 𝑦 ∈ ℝ ( ( 𝑃𝑀 ) ‘ 𝑦 ) ≤ ( 𝐹𝑦 ) ) )
78 67 77 mpbird ( ( 𝜑𝑀 ∈ ℕ ) → ( 𝑃𝑀 ) ∘r𝐹 )