Metamath Proof Explorer

Theorem itg2seq

Description: Definitional property of the S.2 integral: for any function F there is a countable sequence g of simple functions less than F whose integrals converge to the integral of F . (This theorem is for the most part unnecessary in lieu of itg2i1fseq , but unlike that theorem this one doesn't require F to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014)

Ref Expression
Assertion itg2seq ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ ( ∫2 ‘ 𝐹 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ) )

Proof

Step Hyp Ref Expression
1 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
2 1 ad2antlr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → 𝑛 ∈ ℝ )
3 2 ltpnfd ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → 𝑛 < +∞ )
4 iftrue ⊢ ( ( ∫2 ‘ 𝐹 ) = +∞ → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) = 𝑛 )
5 4 adantl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) = 𝑛 )
6 simpr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( ∫2 ‘ 𝐹 ) = +∞ )
7 3 5 6 3brtr4d ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫2 ‘ 𝐹 ) )
8 iffalse ⊢ ( ¬ ( ∫2 ‘ 𝐹 ) = +∞ → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) = ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) )
9 8 adantl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) = ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) )
10 itg2cl ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
11 xrrebnd ⊢ ( ( ∫2 ‘ 𝐹 ) ∈ ℝ* → ( ( ∫2 ‘ 𝐹 ) ∈ ℝ ↔ ( -∞ < ( ∫2 ‘ 𝐹 ) ∧ ( ∫2 ‘ 𝐹 ) < +∞ ) ) )
12 10 11 syl ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ( ∫2 ‘ 𝐹 ) ∈ ℝ ↔ ( -∞ < ( ∫2 ‘ 𝐹 ) ∧ ( ∫2 ‘ 𝐹 ) < +∞ ) ) )
13 itg2ge0 ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → 0 ≤ ( ∫2 ‘ 𝐹 ) )
14 mnflt0 ⊢ -∞ < 0
15 mnfxr ⊢ -∞ ∈ ℝ*
16 0xr ⊢ 0 ∈ ℝ*
17 xrltletr ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 ≤ ( ∫2 ‘ 𝐹 ) ) → -∞ < ( ∫2 ‘ 𝐹 ) ) )
18 15 16 10 17 mp3an12i ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ( -∞ < 0 ∧ 0 ≤ ( ∫2 ‘ 𝐹 ) ) → -∞ < ( ∫2 ‘ 𝐹 ) ) )
19 14 18 mpani ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( 0 ≤ ( ∫2 ‘ 𝐹 ) → -∞ < ( ∫2 ‘ 𝐹 ) ) )
20 13 19 mpd ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → -∞ < ( ∫2 ‘ 𝐹 ) )
21 20 biantrurd ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ( ∫2 ‘ 𝐹 ) < +∞ ↔ ( -∞ < ( ∫2 ‘ 𝐹 ) ∧ ( ∫2 ‘ 𝐹 ) < +∞ ) ) )
22 nltpnft ⊢ ( ( ∫2 ‘ 𝐹 ) ∈ ℝ* → ( ( ∫2 ‘ 𝐹 ) = +∞ ↔ ¬ ( ∫2 ‘ 𝐹 ) < +∞ ) )
23 10 22 syl ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ( ∫2 ‘ 𝐹 ) = +∞ ↔ ¬ ( ∫2 ‘ 𝐹 ) < +∞ ) )
24 23 con2bid ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ( ∫2 ‘ 𝐹 ) < +∞ ↔ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) )
25 12 21 24 3bitr2rd ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ¬ ( ∫2 ‘ 𝐹 ) = +∞ ↔ ( ∫2 ‘ 𝐹 ) ∈ ℝ ) )
26 25 biimpa ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
27 26 adantlr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
28 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
29 28 rpreccld ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
30 29 ad2antlr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
31 27 30 ltsubrpd ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) < ( ∫2 ‘ 𝐹 ) )
32 9 31 eqbrtrd ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫2 ‘ 𝐹 ) )
33 7 32 pm2.61dan ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫2 ‘ 𝐹 ) )
34 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
35 34 ad2antlr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( 1 / 𝑛 ) ∈ ℝ )
36 27 35 resubcld ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ∈ ℝ )
37 2 36 ifclda ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ )
38 37 rexrd ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* )
39 10 adantr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
40 xrltnle ⊢ ( ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ* ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫2 ‘ 𝐹 ) ↔ ¬ ( ∫2 ‘ 𝐹 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
41 38 39 40 syl2anc ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫2 ‘ 𝐹 ) ↔ ¬ ( ∫2 ‘ 𝐹 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
42 33 41 mpbid ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ¬ ( ∫2 ‘ 𝐹 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) )
43 itg2leub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) ) )
44 38 43 syldan ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( ( ∫2 ‘ 𝐹 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) ) )
45 42 44 mtbid ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ¬ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
46 rexanali ⊢ ( ∃ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) ↔ ¬ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
47 45 46 sylibr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ∃ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
48 itg1cl ⊢ ( 𝑓 ∈ dom ∫1 → ( ∫1 ‘ 𝑓 ) ∈ ℝ )
49 ltnle ⊢ ( ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ ∧ ( ∫1 ‘ 𝑓 ) ∈ ℝ ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ 𝑓 ) ↔ ¬ ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
50 37 48 49 syl2an ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ dom ∫1 ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ 𝑓 ) ↔ ¬ ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
51 50 anbi2d ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ dom ∫1 ) → ( ( 𝑓 ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ 𝑓 ) ) ↔ ( 𝑓 ∘r ≤ 𝐹 ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) ) )
52 51 rexbidva ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ( ∃ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ 𝑓 ) ) ↔ ∃ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 ∧ ¬ ( ∫1 ‘ 𝑓 ) ≤ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) ) )
53 47 52 mpbird ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → ∃ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ 𝑓 ) ) )
54 53 ralrimiva ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ∀ 𝑛 ∈ ℕ ∃ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ 𝑓 ) ) )
55 ovex ⊢ ( ℝ ↑m ℝ ) ∈ V
56 i1ff ⊢ ( 𝑥 ∈ dom ∫1 → 𝑥 : ℝ ⟶ ℝ )
57 reex ⊢ ℝ ∈ V
58 57 57 elmap ⊢ ( 𝑥 ∈ ( ℝ ↑m ℝ ) ↔ 𝑥 : ℝ ⟶ ℝ )
59 56 58 sylibr ⊢ ( 𝑥 ∈ dom ∫1 → 𝑥 ∈ ( ℝ ↑m ℝ ) )
60 59 ssriv ⊢ dom ∫1 ⊆ ( ℝ ↑m ℝ )
61 55 60 ssexi ⊢ dom ∫1 ∈ V
62 nnenom ⊢ ℕ ≈ ω
63 breq1 ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ( 𝑓 ∘r ≤ 𝐹 ↔ ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ) )
64 fveq2 ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ( ∫1 ‘ 𝑓 ) = ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) )
65 64 breq2d ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ 𝑓 ) ↔ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) )
66 63 65 anbi12d ⊢ ( 𝑓 = ( 𝑔 ‘ 𝑛 ) → ( ( 𝑓 ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ 𝑓 ) ) ↔ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) )
67 61 62 66 axcc4 ⊢ ( ∀ 𝑛 ∈ ℕ ∃ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ 𝑓 ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) )
68 54 67 syl ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) )
69 simprl ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → 𝑔 : ℕ ⟶ dom ∫1 )
70 simpl ⊢ ( ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) → ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 )
71 70 ralimi ⊢ ( ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 )
72 71 ad2antll ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 )
73 10 adantr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
74 ffvelcdm ⊢ ( ( 𝑔 : ℕ ⟶ dom ∫1 ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ∈ dom ∫1 )
75 itg1cl ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ ℝ )
76 74 75 syl ⊢ ( ( 𝑔 : ℕ ⟶ dom ∫1 ∧ 𝑛 ∈ ℕ ) → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ ℝ )
77 76 fmpttd ⊢ ( 𝑔 : ℕ ⟶ dom ∫1 → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ )
78 77 ad2antrl ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ )
79 78 frnd ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ⊆ ℝ )
80 ressxr ⊢ ℝ ⊆ ℝ*
81 79 80 sstrdi ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ⊆ ℝ* )
82 supxrcl ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ⊆ ℝ* → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
83 81 82 syl ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
84 38 adantlr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* )
85 76 adantll ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ ℝ )
86 85 rexrd ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ ℝ* )
87 xrltle ⊢ ( ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* ∧ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ ℝ* ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) )
88 84 86 87 syl2anc ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) )
89 2fveq3 ⊢ ( 𝑛 = 𝑚 → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) = ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) )
90 89 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) )
91 90 rneqi ⊢ ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) )
92 77 adantl ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ )
93 92 frnd ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) → ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ⊆ ℝ )
94 93 80 sstrdi ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) → ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ⊆ ℝ* )
95 94 adantr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ⊆ ℝ* )
96 91 95 eqsstrrid ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) ⊆ ℝ* )
97 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) = ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) )
98 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) )
99 fvex ⊢ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ V
100 97 98 99 fvmpt ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) ‘ 𝑛 ) = ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) )
101 fvex ⊢ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ∈ V
102 101 98 fnmpti ⊢ ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) Fn ℕ
103 fnfvelrn ⊢ ( ( ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) Fn ℕ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) ‘ 𝑛 ) ∈ ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) )
104 102 103 mpan ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) ‘ 𝑛 ) ∈ ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) )
105 100 104 eqeltrrd ⊢ ( 𝑛 ∈ ℕ → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) )
106 105 adantl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) )
107 supxrub ⊢ ( ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) ⊆ ℝ* ∧ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) ) → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) )
108 96 106 107 syl2anc ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) )
109 91 supeq1i ⊢ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < )
110 95 82 syl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
111 109 110 eqeltrrid ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ∈ ℝ* )
112 xrletr ⊢ ( ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* ∧ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∈ ℝ* ∧ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ∈ ℝ* ) → ( ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∧ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
113 84 86 111 112 syl3anc ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ∧ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
114 108 113 mpan2d ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
115 88 114 syld ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
116 115 adantld ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
117 116 ralimdva ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) → ( ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) → ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
118 117 impr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) )
119 breq2 ⊢ ( 𝑥 = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ↔ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
120 119 ralbidv ⊢ ( 𝑥 = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) → ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
121 breq2 ⊢ ( 𝑥 = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) → ( ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ↔ ( ∫2 ‘ 𝐹 ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
122 120 121 imbi12d ⊢ ( 𝑥 = sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) → ( ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) ↔ ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) → ( ∫2 ‘ 𝐹 ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) ) )
123 elxr ⊢ ( 𝑥 ∈ ℝ* ↔ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) )
124 simplrl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → 𝑥 ∈ ℝ )
125 arch ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 )
126 124 125 syl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 )
127 4 adantl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) = 𝑛 )
128 127 breq2d ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ 𝑥 < 𝑛 ) )
129 128 rexbidv ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( ∃ 𝑛 ∈ ℕ 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 ) )
130 126 129 mpbird ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ( ∫2 ‘ 𝐹 ) = +∞ ) → ∃ 𝑛 ∈ ℕ 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) )
131 26 adantlr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
132 simplrl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → 𝑥 ∈ ℝ )
133 131 132 resubcld ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) ∈ ℝ )
134 simplrr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → 𝑥 < ( ∫2 ‘ 𝐹 ) )
135 132 131 posdifd ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( 𝑥 < ( ∫2 ‘ 𝐹 ) ↔ 0 < ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) ) )
136 134 135 mpbid ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → 0 < ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) )
137 nnrecl ⊢ ( ( ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) ∈ ℝ ∧ 0 < ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) ) → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) )
138 133 136 137 syl2anc ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) )
139 34 adantl ⊢ ( ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
140 131 adantr ⊢ ( ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
141 132 adantr ⊢ ( ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ )
142 ltsub13 ⊢ ( ( ( 1 / 𝑛 ) ∈ ℝ ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 1 / 𝑛 ) < ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) ↔ 𝑥 < ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) )
143 139 140 141 142 syl3anc ⊢ ( ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1 / 𝑛 ) < ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) ↔ 𝑥 < ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) )
144 8 ad2antlr ⊢ ( ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) ∧ 𝑛 ∈ ℕ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) = ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) )
145 144 breq2d ⊢ ( ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ 𝑥 < ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) )
146 143 145 bitr4d ⊢ ( ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1 / 𝑛 ) < ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) ↔ 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
147 146 rexbidva ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ( ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < ( ( ∫2 ‘ 𝐹 ) − 𝑥 ) ↔ ∃ 𝑛 ∈ ℕ 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
148 138 147 mpbid ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) ∧ ¬ ( ∫2 ‘ 𝐹 ) = +∞ ) → ∃ 𝑛 ∈ ℕ 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) )
149 130 148 pm2.61dan ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( ∫2 ‘ 𝐹 ) ) ) → ∃ 𝑛 ∈ ℕ 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) )
150 149 expr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < ( ∫2 ‘ 𝐹 ) → ∃ 𝑛 ∈ ℕ 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ) )
151 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
152 xrltnle ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ* ) → ( 𝑥 < ( ∫2 ‘ 𝐹 ) ↔ ¬ ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
153 151 10 152 syl2anr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < ( ∫2 ‘ 𝐹 ) ↔ ¬ ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
154 151 ad2antlr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℝ* )
155 38 adantlr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* )
156 xrltnle ⊢ ( ( 𝑥 ∈ ℝ* ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* ) → ( 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ ¬ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ) )
157 154 155 156 syl2anc ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ ¬ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ) )
158 157 rexbidva ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑛 ∈ ℕ 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ ∃ 𝑛 ∈ ℕ ¬ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ) )
159 rexnal ⊢ ( ∃ 𝑛 ∈ ℕ ¬ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ↔ ¬ ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 )
160 158 159 bitrdi ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑛 ∈ ℕ 𝑥 < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ ¬ ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ) )
161 150 153 160 3imtr3d ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( ¬ ( ∫2 ‘ 𝐹 ) ≤ 𝑥 → ¬ ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ) )
162 161 con4d ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
163 10 adantr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
164 pnfge ⊢ ( ( ∫2 ‘ 𝐹 ) ∈ ℝ* → ( ∫2 ‘ 𝐹 ) ≤ +∞ )
165 163 164 syl ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = +∞ ) → ( ∫2 ‘ 𝐹 ) ≤ +∞ )
166 simpr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = +∞ ) → 𝑥 = +∞ )
167 165 166 breqtrrd ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = +∞ ) → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 )
168 167 a1d ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = +∞ ) → ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
169 1nn ⊢ 1 ∈ ℕ
170 169 ne0ii ⊢ ℕ ≠ ∅
171 r19.2z ⊢ ( ( ℕ ≠ ∅ ∧ ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ) → ∃ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 )
172 170 171 mpan ⊢ ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ∃ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 )
173 37 adantlr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = -∞ ) ∧ 𝑛 ∈ ℕ ) → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ )
174 mnflt ⊢ ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ → -∞ < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) )
175 rexr ⊢ ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ → if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* )
176 xrltnle ⊢ ( ( -∞ ∈ ℝ* ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ* ) → ( -∞ < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ ¬ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ -∞ ) )
177 15 175 176 sylancr ⊢ ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ → ( -∞ < if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ↔ ¬ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ -∞ ) )
178 174 177 mpbid ⊢ ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ∈ ℝ → ¬ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ -∞ )
179 173 178 syl ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = -∞ ) ∧ 𝑛 ∈ ℕ ) → ¬ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ -∞ )
180 simplr ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = -∞ ) ∧ 𝑛 ∈ ℕ ) → 𝑥 = -∞ )
181 180 breq2d ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = -∞ ) ∧ 𝑛 ∈ ℕ ) → ( if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 ↔ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ -∞ ) )
182 179 181 mtbird ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = -∞ ) ∧ 𝑛 ∈ ℕ ) → ¬ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 )
183 182 nrexdv ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = -∞ ) → ¬ ∃ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 )
184 183 pm2.21d ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = -∞ ) → ( ∃ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
185 172 184 syl5 ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 = -∞ ) → ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
186 162 168 185 3jaodan ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) ) → ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
187 123 186 sylan2b ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ* ) → ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
188 187 ralrimiva ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ∀ 𝑥 ∈ ℝ* ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
189 188 adantr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ∀ 𝑥 ∈ ℝ* ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ 𝑥 → ( ∫2 ‘ 𝐹 ) ≤ 𝑥 ) )
190 109 83 eqeltrrid ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ∈ ℝ* )
191 122 189 190 rspcdva ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ( ∀ 𝑛 ∈ ℕ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) → ( ∫2 ‘ 𝐹 ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) ) )
192 118 191 mpd ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ( ∫2 ‘ 𝐹 ) ≤ sup ( ran ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ) , ℝ* , < ) )
193 192 109 breqtrrdi ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ( ∫2 ‘ 𝐹 ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) )
194 itg2ub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 ‘ 𝑛 ) ∈ dom ∫1 ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ) → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) )
195 194 3expia ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 ‘ 𝑛 ) ∈ dom ∫1 ) → ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
196 74 195 sylan2 ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
197 196 anassrs ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
198 197 adantrd ⊢ ( ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) → ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
199 198 ralimdva ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑔 : ℕ ⟶ dom ∫1 ) → ( ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) → ∀ 𝑛 ∈ ℕ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
200 199 impr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) )
201 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) )
202 89 201 101 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ‘ 𝑚 ) = ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) )
203 202 breq1d ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
204 203 ralbiia ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ∀ 𝑚 ∈ ℕ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐹 ) )
205 89 breq1d ⊢ ( 𝑛 = 𝑚 → ( ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐹 ) ) )
206 205 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ∀ 𝑚 ∈ ℕ ( ∫1 ‘ ( 𝑔 ‘ 𝑚 ) ) ≤ ( ∫2 ‘ 𝐹 ) )
207 204 206 bitr4i ⊢ ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ∀ 𝑛 ∈ ℕ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ≤ ( ∫2 ‘ 𝐹 ) )
208 200 207 sylibr ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐹 ) )
209 ffn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ → ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) Fn ℕ )
210 breq1 ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ‘ 𝑚 ) → ( 𝑧 ≤ ( ∫2 ‘ 𝐹 ) ↔ ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐹 ) ) )
211 210 ralrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐹 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐹 ) ) )
212 78 209 211 3syl ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐹 ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≤ ( ∫2 ‘ 𝐹 ) ) )
213 208 212 mpbird ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐹 ) )
214 supxrleub ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ⊆ ℝ* ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ* ) → ( sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐹 ) ) )
215 81 73 214 syl2anc ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ( sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ∫2 ‘ 𝐹 ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) 𝑧 ≤ ( ∫2 ‘ 𝐹 ) ) )
216 213 215 mpbird ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ≤ ( ∫2 ‘ 𝐹 ) )
217 73 83 193 216 xrletrid ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ( ∫2 ‘ 𝐹 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) )
218 69 72 217 3jca ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) ) → ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ ( ∫2 ‘ 𝐹 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ) )
219 218 ex ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) → ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ ( ∫2 ‘ 𝐹 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ) ) )
220 219 eximdv ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ if ( ( ∫2 ‘ 𝐹 ) = +∞ , 𝑛 , ( ( ∫2 ‘ 𝐹 ) − ( 1 / 𝑛 ) ) ) < ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ ( ∫2 ‘ 𝐹 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ) ) )
221 68 220 mpd ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∘r ≤ 𝐹 ∧ ( ∫2 ‘ 𝐹 ) = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑔 ‘ 𝑛 ) ) ) , ℝ* , < ) ) )