Metamath Proof Explorer

Theorem itg2mono

Description: The Monotone Convergence Theorem for nonnegative functions. If { ( Fn ) : n e. NN } is a monotone increasing sequence of positive, measurable, real-valued functions, and G is the pointwise limit of the sequence, then ( S.2G ) is the limit of the sequence { ( S.2( Fn ) ) : n e. NN } . (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 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < )
Assertion itg2mono ( 𝜑 → ( ∫2 ‘ 𝐺 ) = 𝑆 )

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 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
8 fss ⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ℝ )
9 3 7 8 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ℝ )
10 9 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
11 10 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
12 11 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℝ )
13 12 frnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ⊆ ℝ )
14 1nn ⊢ 1 ∈ ℕ
15 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
16 15 11 dmmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ℕ )
17 14 16 eleqtrrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 1 ∈ dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
18 17 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ )
19 dm0rn0 ⊢ ( dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ∅ )
20 19 necon3bii ⊢ ( dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ )
21 18 20 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ )
22 12 ffnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) Fn ℕ )
23 breq1 ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) → ( 𝑧 ≤ 𝑦 ↔ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ) )
24 23 ralrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ) )
25 22 24 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ) )
26 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
27 26 fveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
28 fvex ⊢ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V
29 27 15 28 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
30 29 breq1d ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ 𝑦 ) )
31 30 ralbiia ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ 𝑦 )
32 27 breq1d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ 𝑦 ) )
33 32 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ 𝑦 )
34 31 33 bitr4i ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ↔ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
35 25 34 bitrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) )
36 35 rexbidv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) )
37 5 36 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 )
38 13 21 37 suprcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ℝ )
39 38 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ℝ* )
40 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ )
41 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) )
42 41 feq1d ⊢ ( 𝑛 = 1 → ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,) +∞ ) ) )
43 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) )
44 14 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
45 42 43 44 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,) +∞ ) )
46 45 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
47 elrege0 ⊢ ( ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ) )
48 46 47 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ) )
49 48 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ∈ ℝ )
50 48 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) )
51 41 fveq1d ⊢ ( 𝑛 = 1 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) )
52 fvex ⊢ ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ∈ V
53 51 15 52 fvmpt ⊢ ( 1 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 1 ) = ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) )
54 14 53 ax-mp ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 1 ) = ( ( 𝐹 ‘ 1 ) ‘ 𝑥 )
55 fnfvelrn ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) Fn ℕ ∧ 1 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 1 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
56 22 14 55 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 1 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
57 54 56 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
58 13 21 37 57 suprubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 1 ) ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
59 40 49 38 50 58 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
60 elxrge0 ⊢ ( sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ( 0 [,] +∞ ) ↔ ( sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ℝ* ∧ 0 ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
61 39 59 60 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ( 0 [,] +∞ ) )
62 61 1 fmptd ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
63 itg2cl ⊢ ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
64 62 63 syl ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
65 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
66 fss ⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
67 3 65 66 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
68 itg2cl ⊢ ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
69 67 68 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
70 69 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ* )
71 70 frnd ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* )
72 supxrcl ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
73 71 72 syl ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
74 6 73 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
75 2 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ MblFn )
76 3 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) )
77 4 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
78 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
79 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) → 𝑓 ∈ dom ∫1 )
80 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) → 𝑓 ∘r ≤ 𝐺 )
81 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) → ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 )
82 1 75 76 77 78 6 79 80 81 itg2monolem3 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) → ( ∫1 ‘ 𝑓 ) ≤ 𝑆 )
83 82 expr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ) → ( ¬ ( ∫1 ‘ 𝑓 ) ≤ 𝑆 → ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) )
84 83 pm2.18d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐺 ) ) → ( ∫1 ‘ 𝑓 ) ≤ 𝑆 )
85 84 expr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑓 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) )
86 85 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) )
87 itg2leub ⊢ ( ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑆 ∈ ℝ* ) → ( ( ∫2 ‘ 𝐺 ) ≤ 𝑆 ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) )
88 62 74 87 syl2anc ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐺 ) ≤ 𝑆 ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐺 → ( ∫1 ‘ 𝑓 ) ≤ 𝑆 ) ) )
89 86 88 mpbird ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ≤ 𝑆 )
90 26 feq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐹 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) ) )
91 90 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) )
92 43 91 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) )
93 92 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) )
94 fss ⊢ ( ( ( 𝐹 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( 𝐹 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,] +∞ ) )
95 93 65 94 sylancl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,] +∞ ) )
96 62 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
97 13 21 37 3jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ⊆ ℝ ∧ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ) )
98 97 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ⊆ ℝ ∧ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ) )
99 29 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
100 22 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) Fn ℕ )
101 simplr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑚 ∈ ℕ )
102 fnfvelrn ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) Fn ℕ ∧ 𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
103 100 101 102 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
104 99 103 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
105 suprub ⊢ ( ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ⊆ ℝ ∧ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ) ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
106 98 104 105 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
107 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
108 ltso ⊢ < Or ℝ
109 108 supex ⊢ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ V
110 1 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ V ) → ( 𝐺 ‘ 𝑥 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
111 107 109 110 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
112 106 111 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
113 112 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
114 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
115 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) )
116 114 115 breq12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑧 ) ) )
117 116 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℝ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑧 ∈ ℝ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑧 ) )
118 113 117 sylib ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∀ 𝑧 ∈ ℝ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑧 ) )
119 93 ffnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) Fn ℝ )
120 38 1 fmptd ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
121 120 ffnd ⊢ ( 𝜑 → 𝐺 Fn ℝ )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐺 Fn ℝ )
123 reex ⊢ ℝ ∈ V
124 123 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ℝ ∈ V )
125 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
126 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
127 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑧 ∈ ℝ ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
128 119 122 124 124 125 126 127 ofrfval ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑚 ) ∘r ≤ 𝐺 ↔ ∀ 𝑧 ∈ ℝ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑧 ) ) )
129 118 128 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) ∘r ≤ 𝐺 )
130 itg2le ⊢ ( ( ( 𝐹 ‘ 𝑚 ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝐹 ‘ 𝑚 ) ∘r ≤ 𝐺 ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐺 ) )
131 95 96 129 130 syl3anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐺 ) )
132 131 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐺 ) )
133 70 ffnd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ )
134 breq1 ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑚 ) → ( 𝑧 ≤ ( ∫2 ‘ 𝐺 ) ↔ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐺 ) ) )
135 134 ralrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐺 ) ) )
136 133 135 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐺 ) ) )
137 2fveq3 ⊢ ( 𝑛 = 𝑚 → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ∫2 ‘ ( 𝐹 ‘ 𝑚 ) ) )
138 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) )
139 fvex ⊢ ( ∫2 ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ V
140 137 138 139 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑚 ) = ( ∫2 ‘ ( 𝐹 ‘ 𝑚 ) ) )
141 140 breq1d ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ( ∫2 ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐺 ) ) )
142 141 ralbiia ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑚 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐺 ) )
143 136 142 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑚 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐺 ) ) )
144 132 143 mpbird ⊢ ( 𝜑 → ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐺 ) )
145 supxrleub ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* ∧ ( ∫2 ‘ 𝐺 ) ∈ ℝ* ) → ( sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐺 ) ) )
146 71 64 145 syl2anc ⊢ ( 𝜑 → ( sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐺 ) ) )
147 144 146 mpbird ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ∫2 ‘ 𝐺 ) )
148 6 147 eqbrtrid ⊢ ( 𝜑 → 𝑆 ≤ ( ∫2 ‘ 𝐺 ) )
149 64 74 89 148 xrletrid ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) = 𝑆 )