This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg2monolem1

Description: Lemma for itg2mono . We show that for any constant t less than one, t x. S.1 H is less than S , and so S.1 H <_ S , which is one half of the equality in itg2mono . Consider the sequence A ( n ) = { x | t x. H <_ F ( n ) } . This is an increasing sequence of measurable sets whose union is RR , and so ` H |`A ( n ) has an integral which equals S.1 H in the limit, by itg1climres . Then by taking the limit in ` ( t x. H ) |`A ( n ) <_ F ( n ) , we get t x. S.1 H <_ S as desired. (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-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 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < )
itg2mono.7 ⊢ ( 𝜑 → 𝑇 ∈ ( 0 (,) 1 ) )
itg2mono.8 ⊢ ( 𝜑 → 𝐻 ∈ dom ∫1 )
itg2mono.9 ⊢ ( 𝜑 → 𝐻 ∘r ≤ 𝐺 )
itg2mono.10 ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
itg2mono.11 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
Assertion itg2monolem1 ( 𝜑 → ( 𝑇 · ( ∫1 ‘ 𝐻 ) ) ≤ 𝑆 )

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 itg2mono.7 ⊢ ( 𝜑 → 𝑇 ∈ ( 0 (,) 1 ) )
8 itg2mono.8 ⊢ ( 𝜑 → 𝐻 ∈ dom ∫1 )
9 itg2mono.9 ⊢ ( 𝜑 → 𝐻 ∘r ≤ 𝐺 )
10 itg2mono.10 ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
11 itg2mono.11 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
12 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
13 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
14 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
15 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
16 15 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
17 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
18 fss ⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ℝ )
19 3 17 18 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ℝ )
20 0xr ⊢ 0 ∈ ℝ*
21 1xr ⊢ 1 ∈ ℝ*
22 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝑇 ∈ ( 0 (,) 1 ) ↔ ( 𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1 ) ) )
23 20 21 22 mp2an ⊢ ( 𝑇 ∈ ( 0 (,) 1 ) ↔ ( 𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1 ) )
24 7 23 sylib ⊢ ( 𝜑 → ( 𝑇 ∈ ℝ ∧ 0 < 𝑇 ∧ 𝑇 < 1 ) )
25 24 simp1d ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
26 25 renegcld ⊢ ( 𝜑 → - 𝑇 ∈ ℝ )
27 8 26 i1fmulc ⊢ ( 𝜑 → ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ∈ dom ∫1 )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ∈ dom ∫1 )
29 i1ff ⊢ ( ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ∈ dom ∫1 → ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) : ℝ ⟶ ℝ )
30 28 29 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) : ℝ ⟶ ℝ )
31 reex ⊢ ℝ ∈ V
32 31 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ℝ ∈ V )
33 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
34 16 19 30 32 32 33 off ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) : ℝ ⟶ ℝ )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) : ℝ ⟶ ℝ )
36 35 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) Fn ℝ )
37 elpreima ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) Fn ℝ → ( 𝑥 ∈ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 0 ) ) ) )
38 36 37 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 0 ) ) ) )
39 14 38 mpbirand ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ↔ ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 0 ) ) )
40 elioomnf ⊢ ( 0 ∈ ℝ* → ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 0 ) ↔ ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) < 0 ) ) )
41 20 40 ax-mp ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 0 ) ↔ ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) < 0 ) )
42 34 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ℝ )
43 42 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) < 0 ↔ ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) < 0 ) ) )
44 41 43 bitr4id ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 0 ) ↔ ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) < 0 ) )
45 3 ffnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) Fn ℝ )
46 30 ffnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) Fn ℝ )
47 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
48 26 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → - 𝑇 ∈ ℝ )
49 i1ff ⊢ ( 𝐻 ∈ dom ∫1 → 𝐻 : ℝ ⟶ ℝ )
50 8 49 syl ⊢ ( 𝜑 → 𝐻 : ℝ ⟶ ℝ )
51 50 ffnd ⊢ ( 𝜑 → 𝐻 Fn ℝ )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐻 Fn ℝ )
53 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
54 32 48 52 53 ofc1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ‘ 𝑥 ) = ( - 𝑇 · ( 𝐻 ‘ 𝑥 ) ) )
55 25 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℂ )
57 50 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ )
58 57 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ )
59 58 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ 𝑥 ) ∈ ℂ )
60 56 59 mulneg1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( - 𝑇 · ( 𝐻 ‘ 𝑥 ) ) = - ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) )
61 54 60 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ‘ 𝑥 ) = - ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) )
62 45 46 32 32 33 47 61 ofval ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) + - ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) )
63 19 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
64 63 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ )
65 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
66 65 57 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ )
67 66 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ )
68 67 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℂ )
69 64 68 negsubd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) + - ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) )
70 62 69 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) )
71 70 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) < 0 ↔ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) < 0 ) )
72 0red ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ )
73 63 67 72 ltsubaddd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) < 0 ↔ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < ( 0 + ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) ) )
74 68 addlidd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 0 + ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) )
75 74 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < ( 0 + ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) ↔ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) )
76 71 73 75 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ‘ 𝑥 ) < 0 ↔ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) )
77 39 44 76 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ↔ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) )
78 77 notbid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑥 ∈ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ↔ ¬ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) )
79 eldif ⊢ ( 𝑥 ∈ ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) )
80 79 baib ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ↔ ¬ 𝑥 ∈ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) )
81 80 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ↔ ¬ 𝑥 ∈ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) )
82 67 63 lenltd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ¬ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ) )
83 78 81 82 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
84 83 rabbi2dva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ℝ ∩ ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ) = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
85 rembl ⊢ ℝ ∈ dom vol
86 i1fmbf ⊢ ( ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ∈ dom ∫1 → ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ∈ MblFn )
87 28 86 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ∈ MblFn )
88 2 87 mbfadd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ∈ MblFn )
89 mbfima ⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) ∈ MblFn ∧ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) : ℝ ⟶ ℝ ) → ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ∈ dom vol )
90 88 34 89 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ∈ dom vol )
91 cmmbl ⊢ ( ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ∈ dom vol → ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ∈ dom vol )
92 90 91 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ∈ dom vol )
93 inmbl ⊢ ( ( ℝ ∈ dom vol ∧ ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ∈ dom vol ) → ( ℝ ∩ ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ) ∈ dom vol )
94 85 92 93 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ℝ ∩ ( ℝ ∖ ( ◡ ( ( 𝐹 ‘ 𝑛 ) ∘f + ( ( ℝ × { - 𝑇 } ) ∘f · 𝐻 ) ) “ ( -∞ (,) 0 ) ) ) ) ∈ dom vol )
95 84 94 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ∈ dom vol )
96 95 11 fmptd ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ dom vol )
97 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
98 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) )
99 fvoveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
100 98 99 breq12d ⊢ ( 𝑛 = 𝑗 → ( ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐹 ‘ 𝑗 ) ∘r ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
101 100 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ∘r ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
102 97 101 sylib ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ∘r ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
103 102 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∘r ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
104 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) )
105 98 feq1d ⊢ ( 𝑛 = 𝑗 → ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐹 ‘ 𝑗 ) : ℝ ⟶ ( 0 [,) +∞ ) ) )
106 105 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) : ℝ ⟶ ( 0 [,) +∞ ) )
107 104 106 sylib ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) : ℝ ⟶ ( 0 [,) +∞ ) )
108 107 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) : ℝ ⟶ ( 0 [,) +∞ ) )
109 108 ffnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) Fn ℝ )
110 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
111 fveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
112 111 feq1d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐹 ‘ ( 𝑗 + 1 ) ) : ℝ ⟶ ( 0 [,) +∞ ) ) )
113 112 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 𝑗 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
114 104 110 113 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
115 114 ffnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) Fn ℝ )
116 31 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ℝ ∈ V )
117 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
118 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) = ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) )
119 109 115 116 116 33 117 118 ofrfval ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ∘r ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ↔ ∀ 𝑥 ∈ ℝ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) ) )
120 103 119 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) )
121 120 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) )
122 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
123 50 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐻 : ℝ ⟶ ℝ )
124 123 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ )
125 122 124 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ )
126 fss ⊢ ( ( ( 𝐹 ‘ 𝑗 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → ( 𝐹 ‘ 𝑗 ) : ℝ ⟶ ℝ )
127 108 17 126 sylancl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) : ℝ ⟶ ℝ )
128 127 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℝ )
129 fss ⊢ ( ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) : ℝ ⟶ ℝ )
130 114 17 129 sylancl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) : ℝ ⟶ ℝ )
131 130 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) ∈ ℝ )
132 letr ⊢ ( ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℝ ∧ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) ∈ ℝ ) → ( ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) ) )
133 125 128 131 132 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∧ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) ) )
134 121 133 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) ) )
135 134 ss2rabdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } ⊆ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) } )
136 98 fveq1d ⊢ ( 𝑛 = 𝑗 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
137 136 breq2d ⊢ ( 𝑛 = 𝑗 → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
138 137 rabbidv ⊢ ( 𝑛 = 𝑗 → { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } )
139 31 rabex ⊢ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } ∈ V
140 138 11 139 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( 𝐴 ‘ 𝑗 ) = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } )
141 140 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐴 ‘ 𝑗 ) = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } )
142 110 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℕ )
143 111 fveq1d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) )
144 143 breq2d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) ) )
145 144 rabbidv ⊢ ( 𝑛 = ( 𝑗 + 1 ) → { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) } )
146 31 rabex ⊢ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) } ∈ V
147 145 11 146 fvmpt ⊢ ( ( 𝑗 + 1 ) ∈ ℕ → ( 𝐴 ‘ ( 𝑗 + 1 ) ) = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) } )
148 142 147 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐴 ‘ ( 𝑗 + 1 ) ) = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ ( 𝑗 + 1 ) ) ‘ 𝑥 ) } )
149 135 141 148 3sstr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐴 ‘ 𝑗 ) ⊆ ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
150 66 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ )
151 57 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ )
152 63 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
153 152 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) : ℕ ⟶ ℝ )
154 153 frnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ⊆ ℝ )
155 1nn ⊢ 1 ∈ ℕ
156 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
157 156 152 dmmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ℕ )
158 155 157 eleqtrrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 1 ∈ dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
159 158 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ )
160 dm0rn0 ⊢ ( dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ∅ )
161 160 necon3bii ⊢ ( dom ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ )
162 159 161 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ )
163 153 ffnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) Fn ℕ )
164 breq1 ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) → ( 𝑧 ≤ 𝑦 ↔ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ) )
165 164 ralrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ) )
166 163 165 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ) )
167 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
168 167 fveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
169 fvex ⊢ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ∈ V
170 168 156 169 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) )
171 170 breq1d ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ 𝑦 ) )
172 171 ralbiia ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ 𝑦 )
173 168 breq1d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ 𝑦 ) )
174 173 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ ℕ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ≤ 𝑦 )
175 172 174 bitr4i ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑚 ) ≤ 𝑦 ↔ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
176 166 175 bitrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) )
177 176 rexbidv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) )
178 5 177 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 )
179 154 162 178 suprcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ℝ )
180 179 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ℝ )
181 24 simp3d ⊢ ( 𝜑 → 𝑇 < 1 )
182 181 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → 𝑇 < 1 )
183 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → 𝑇 ∈ ℝ )
184 1red ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
185 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → 0 < ( 𝐻 ‘ 𝑥 ) )
186 ltmul1 ⊢ ( ( 𝑇 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝐻 ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑇 < 1 ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( 1 · ( 𝐻 ‘ 𝑥 ) ) ) )
187 183 184 151 185 186 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑇 < 1 ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( 1 · ( 𝐻 ‘ 𝑥 ) ) ) )
188 182 187 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( 1 · ( 𝐻 ‘ 𝑥 ) ) )
189 151 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ℂ )
190 189 mullidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 1 · ( 𝐻 ‘ 𝑥 ) ) = ( 𝐻 ‘ 𝑥 ) )
191 188 190 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( 𝐻 ‘ 𝑥 ) )
192 179 1 fmptd ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
193 192 ffnd ⊢ ( 𝜑 → 𝐺 Fn ℝ )
194 31 a1i ⊢ ( 𝜑 → ℝ ∈ V )
195 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
196 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) )
197 196 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) )
198 197 rneqd ⊢ ( 𝑥 = 𝑦 → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) )
199 198 supeq1d ⊢ ( 𝑥 = 𝑦 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) )
200 ltso ⊢ < Or ℝ
201 200 supex ⊢ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) ∈ V
202 199 1 201 fvmpt ⊢ ( 𝑦 ∈ ℝ → ( 𝐺 ‘ 𝑦 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) )
203 202 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐺 ‘ 𝑦 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) )
204 51 193 194 194 33 195 203 ofrfval ⊢ ( 𝜑 → ( 𝐻 ∘r ≤ 𝐺 ↔ ∀ 𝑦 ∈ ℝ ( 𝐻 ‘ 𝑦 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) ) )
205 9 204 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ( 𝐻 ‘ 𝑦 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) )
206 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) )
207 206 199 breq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐻 ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ↔ ( 𝐻 ‘ 𝑦 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) ) )
208 207 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℝ ( 𝐻 ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ↔ ∀ 𝑦 ∈ ℝ ( 𝐻 ‘ 𝑦 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ) , ℝ , < ) )
209 205 208 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝐻 ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
210 209 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
211 210 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝐻 ‘ 𝑥 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
212 150 151 180 191 211 ltletrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
213 154 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ⊆ ℝ )
214 162 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ )
215 178 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 )
216 suprlub ⊢ ( ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ⊆ ℝ ∧ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) 𝑧 ≤ 𝑦 ) ∧ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ ) → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ↔ ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < 𝑤 ) )
217 213 214 215 150 216 syl31anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ↔ ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < 𝑤 ) )
218 212 217 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < 𝑤 )
219 163 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) Fn ℕ )
220 breq2 ⊢ ( 𝑤 = ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑗 ) → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < 𝑤 ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑗 ) ) )
221 220 rexrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) Fn ℕ → ( ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < 𝑤 ↔ ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑗 ) ) )
222 219 221 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < 𝑤 ↔ ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑗 ) ) )
223 fvex ⊢ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ V
224 136 156 223 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
225 224 breq2d ⊢ ( 𝑗 ∈ ℕ → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑗 ) ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
226 225 rexbiia ⊢ ( ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
227 222 226 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < 𝑤 ↔ ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
228 218 227 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
229 183 151 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ )
230 108 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) : ℝ ⟶ ( 0 [,) +∞ ) )
231 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑥 ∈ ℝ )
232 230 231 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
233 elrege0 ⊢ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
234 232 233 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
235 234 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℝ )
236 235 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℝ )
237 ltle ⊢ ( ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
238 229 236 237 syl2an2r ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
239 238 reximdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ( ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) < ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) → ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
240 228 239 mpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) ) → ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
241 240 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 0 < ( 𝐻 ‘ 𝑥 ) ) → ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
242 155 ne0ii ⊢ ℕ ≠ ∅
243 66 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ )
244 243 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ ℝ )
245 0red ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → 0 ∈ ℝ )
246 234 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
247 246 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℝ )
248 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝐻 ‘ 𝑥 ) ≤ 0 )
249 57 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ )
250 249 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝐻 ‘ 𝑥 ) ∈ ℝ )
251 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → 𝑇 ∈ ℝ )
252 24 simp2d ⊢ ( 𝜑 → 0 < 𝑇 )
253 252 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → 0 < 𝑇 )
254 lemul2 ⊢ ( ( ( 𝐻 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ ( 𝑇 ∈ ℝ ∧ 0 < 𝑇 ) ) → ( ( 𝐻 ‘ 𝑥 ) ≤ 0 ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( 𝑇 · 0 ) ) )
255 250 245 251 253 254 syl112anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑥 ) ≤ 0 ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( 𝑇 · 0 ) ) )
256 248 255 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( 𝑇 · 0 ) )
257 251 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → 𝑇 ∈ ℂ )
258 257 mul01d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝑇 · 0 ) = 0 )
259 256 258 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ 0 )
260 246 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
261 244 245 247 259 260 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
262 261 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) → ∀ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
263 r19.2z ⊢ ( ( ℕ ≠ ∅ ∧ ∀ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) → ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
264 242 262 263 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) ) → ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
265 264 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐻 ‘ 𝑥 ) ≤ 0 ) → ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
266 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ )
267 241 265 266 57 ltlecasei ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
268 267 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
269 rabid2 ⊢ ( ℝ = { 𝑥 ∈ ℝ ∣ ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) )
270 268 269 sylibr ⊢ ( 𝜑 → ℝ = { 𝑥 ∈ ℝ ∣ ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } )
271 iunrab ⊢ ∪ 𝑗 ∈ ℕ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } = { 𝑥 ∈ ℝ ∣ ∃ 𝑗 ∈ ℕ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) }
272 270 271 eqtr4di ⊢ ( 𝜑 → ℝ = ∪ 𝑗 ∈ ℕ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } )
273 141 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( 𝐴 ‘ 𝑗 ) = ∪ 𝑗 ∈ ℕ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) } )
274 96 ffnd ⊢ ( 𝜑 → 𝐴 Fn ℕ )
275 fniunfv ⊢ ( 𝐴 Fn ℕ → ∪ 𝑗 ∈ ℕ ( 𝐴 ‘ 𝑗 ) = ∪ ran 𝐴 )
276 274 275 syl ⊢ ( 𝜑 → ∪ 𝑗 ∈ ℕ ( 𝐴 ‘ 𝑗 ) = ∪ ran 𝐴 )
277 272 273 276 3eqtr2rd ⊢ ( 𝜑 → ∪ ran 𝐴 = ℝ )
278 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) )
279 96 149 277 8 278 itg1climres ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ⇝ ( ∫1 ‘ 𝐻 ) )
280 nnex ⊢ ℕ ∈ V
281 280 mptex ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ∈ V
282 281 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ∈ V )
283 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐴 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑘 ) )
284 283 eleq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) ↔ 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ) )
285 284 ifbid ⊢ ( 𝑗 = 𝑘 → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) = if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) )
286 285 mpteq2dv ⊢ ( 𝑗 = 𝑘 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) )
287 286 fveq2d ⊢ ( 𝑗 = 𝑘 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) )
288 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) )
289 fvex ⊢ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ∈ V
290 287 288 289 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑘 ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) )
291 290 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑘 ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) )
292 96 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ‘ 𝑘 ) ∈ dom vol )
293 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) )
294 293 i1fres ⊢ ( ( 𝐻 ∈ dom ∫1 ∧ ( 𝐴 ‘ 𝑘 ) ∈ dom vol ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
295 8 292 294 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
296 itg1cl ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
297 295 296 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
298 291 297 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑘 ) ∈ ℝ )
299 298 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑘 ) ∈ ℂ )
300 287 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) = ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) )
301 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) )
302 ovex ⊢ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ∈ V
303 300 301 302 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ‘ 𝑘 ) = ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) )
304 290 oveq2d ⊢ ( 𝑘 ∈ ℕ → ( 𝑇 · ( ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑘 ) ) = ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) )
305 303 304 eqtr4d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ‘ 𝑘 ) = ( 𝑇 · ( ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑘 ) ) )
306 305 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ‘ 𝑘 ) = ( 𝑇 · ( ( 𝑗 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ‘ 𝑘 ) ) )
307 12 13 279 55 282 299 306 climmulc2 ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ⇝ ( 𝑇 · ( ∫1 ‘ 𝐻 ) ) )
308 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
309 fss ⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
310 3 308 309 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
311 10 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑆 ∈ ℝ )
312 itg2cl ⊢ ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
313 310 312 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
314 313 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ* )
315 314 frnd ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* )
316 fvex ⊢ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ V
317 316 elabrex ⊢ ( 𝑛 ∈ ℕ → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) } )
318 317 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) } )
319 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) )
320 319 rnmpt ⊢ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) = { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) }
321 318 320 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
322 supxrub ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* ∧ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) )
323 315 321 322 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) )
324 323 6 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑆 )
325 itg2lecl ⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑆 ∈ ℝ ∧ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑆 ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
326 310 311 324 325 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
327 326 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ )
328 310 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
329 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
330 329 feq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) ↔ ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,] +∞ ) ) )
331 330 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) ↔ ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,] +∞ ) )
332 328 331 sylib ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,] +∞ ) )
333 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
334 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
335 334 feq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,] +∞ ) ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) )
336 335 rspccva ⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
337 332 333 336 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
338 itg2le ⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
339 310 337 4 338 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
340 339 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
341 2fveq3 ⊢ ( 𝑛 = 𝑘 → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) )
342 fvex ⊢ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V
343 341 319 342 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) )
344 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
345 2fveq3 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ∫2 ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
346 fvex ⊢ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ V
347 345 319 346 fvmpt ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ∫2 ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
348 344 347 syl ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ∫2 ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
349 343 348 breq12d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ↔ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
350 349 ralbiia ⊢ ( ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ↔ ∀ 𝑘 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
351 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
352 351 fveq2d ⊢ ( 𝑛 = 𝑘 → ( ∫2 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ∫2 ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
353 341 352 breq12d ⊢ ( 𝑛 = 𝑘 → ( ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ↔ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
354 353 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ↔ ∀ 𝑘 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
355 350 354 bitr4i ⊢ ( ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ↔ ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
356 340 355 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) )
357 356 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) )
358 324 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑆 )
359 343 breq1d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 ↔ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) )
360 359 ralbiia ⊢ ( ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
361 341 breq1d ⊢ ( 𝑛 = 𝑘 → ( ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) )
362 361 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
363 360 362 bitr4i ⊢ ( ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 )
364 breq2 ⊢ ( 𝑥 = 𝑆 → ( ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑆 ) )
365 364 ralbidv ⊢ ( 𝑥 = 𝑆 → ( ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑆 ) )
366 363 365 bitrid ⊢ ( 𝑥 = 𝑆 → ( ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑆 ) )
367 366 rspcev ⊢ ( ( 𝑆 ∈ ℝ ∧ ∀ 𝑛 ∈ ℕ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑆 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 )
368 10 358 367 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 )
369 12 13 327 357 368 climsup ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⇝ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ , < ) )
370 327 frnd ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ )
371 319 313 dmmptd ⊢ ( 𝜑 → dom ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ℕ )
372 242 a1i ⊢ ( 𝜑 → ℕ ≠ ∅ )
373 371 372 eqnetrd ⊢ ( 𝜑 → dom ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ≠ ∅ )
374 dm0rn0 ⊢ ( dom ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ∅ )
375 374 necon3bii ⊢ ( dom ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ≠ ∅ ↔ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ≠ ∅ )
376 373 375 sylib ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ≠ ∅ )
377 316 319 fnmpti ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ
378 breq1 ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) → ( 𝑧 ≤ 𝑥 ↔ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 ) )
379 378 ralrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 ) )
380 377 379 mp1i ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 ) )
381 380 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ≤ 𝑥 ) )
382 368 381 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ 𝑥 )
383 supxrre ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ ∧ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) 𝑧 ≤ 𝑥 ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ , < ) )
384 370 376 382 383 syl3anc ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ , < ) )
385 6 384 eqtr2id ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ , < ) = 𝑆 )
386 369 385 breqtrd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⇝ 𝑆 )
387 25 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑇 ∈ ℝ )
388 96 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐴 ‘ 𝑗 ) ∈ dom vol )
389 278 i1fres ⊢ ( ( 𝐻 ∈ dom ∫1 ∧ ( 𝐴 ‘ 𝑗 ) ∈ dom vol ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
390 8 388 389 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
391 itg1cl ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
392 390 391 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
393 387 392 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ∈ ℝ )
394 393 fmpttd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) : ℕ ⟶ ℝ )
395 394 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ‘ 𝑘 ) ∈ ℝ )
396 327 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) ∈ ℝ )
397 329 feq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,) +∞ ) ) )
398 397 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,) +∞ ) )
399 104 398 sylib ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,) +∞ ) )
400 399 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,) +∞ ) )
401 fss ⊢ ( ( ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,] +∞ ) )
402 400 308 401 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,] +∞ ) )
403 31 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ℝ ∈ V )
404 25 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑇 ∈ ℝ )
405 404 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
406 fvex ⊢ ( 𝐻 ‘ 𝑥 ) ∈ V
407 c0ex ⊢ 0 ∈ V
408 406 407 ifex ⊢ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ∈ V
409 408 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ∈ V )
410 fconstmpt ⊢ ( ℝ × { 𝑇 } ) = ( 𝑥 ∈ ℝ ↦ 𝑇 )
411 410 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ℝ × { 𝑇 } ) = ( 𝑥 ∈ ℝ ↦ 𝑇 ) )
412 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) )
413 403 405 409 411 412 offval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ℝ × { 𝑇 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑇 · if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) )
414 ovif2 ⊢ ( 𝑇 · if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) = if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , ( 𝑇 · 0 ) )
415 55 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑇 ∈ ℂ )
416 415 mul01d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 · 0 ) = 0 )
417 416 ifeq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , ( 𝑇 · 0 ) ) = if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) )
418 414 417 eqtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 · if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) = if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) )
419 418 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ ( 𝑇 · if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) )
420 413 419 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ℝ × { 𝑇 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) )
421 295 404 i1fmulc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ℝ × { 𝑇 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ∈ dom ∫1 )
422 420 421 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) ∈ dom ∫1 )
423 iftrue ⊢ ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) = ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) )
424 423 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) = ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) )
425 329 fveq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
426 425 breq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) )
427 426 rabbidv ⊢ ( 𝑛 = 𝑘 → { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) } )
428 31 rabex ⊢ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) } ∈ V
429 427 11 428 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) } )
430 429 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 ‘ 𝑘 ) = { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) } )
431 430 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ↔ 𝑥 ∈ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) } ) )
432 431 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ) → 𝑥 ∈ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) } )
433 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) } ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) )
434 433 simprbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ ℝ ∣ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) } → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
435 432 434 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ) → ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
436 424 435 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
437 iffalse ⊢ ( ¬ 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) = 0 )
438 437 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) = 0 )
439 400 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
440 elrege0 ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) )
441 440 simprbi ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
442 439 441 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
443 442 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ) → 0 ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
444 438 443 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
445 436 444 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
446 445 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
447 ovex ⊢ ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) ∈ V
448 447 407 ifex ⊢ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ∈ V
449 448 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ∈ V )
450 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ∈ V )
451 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) )
452 400 feqmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) )
453 403 449 450 451 452 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) ∘r ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ≤ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) )
454 446 453 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) ∘r ≤ ( 𝐹 ‘ 𝑘 ) )
455 itg2ub ⊢ ( ( ( 𝐹 ‘ 𝑘 ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) ∘r ≤ ( 𝐹 ‘ 𝑘 ) ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) )
456 402 422 454 455 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) )
457 303 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ‘ 𝑘 ) = ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) )
458 295 404 itg1mulc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∫1 ‘ ( ( ℝ × { 𝑇 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) = ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) )
459 420 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∫1 ‘ ( ( ℝ × { 𝑇 } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) ) )
460 457 458 459 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ‘ 𝑘 ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) , ( 𝑇 · ( 𝐻 ‘ 𝑥 ) ) , 0 ) ) ) )
461 343 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ∫2 ‘ ( 𝐹 ‘ 𝑘 ) ) )
462 456 460 461 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑇 · ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝐴 ‘ 𝑗 ) , ( 𝐻 ‘ 𝑥 ) , 0 ) ) ) ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑘 ) )
463 12 13 307 386 395 396 462 climle ⊢ ( 𝜑 → ( 𝑇 · ( ∫1 ‘ 𝐻 ) ) ≤ 𝑆 )