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 ≤ 𝐹 )