Metamath Proof Explorer

Theorem itg2monolem3

Description: Lemma for itg2mono . (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 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < )
itg2monolem2.7 ⊢ ( 𝜑 → 𝑃 ∈ dom ∫1 )
itg2monolem2.8 ⊢ ( 𝜑 → 𝑃 ∘r ≤ 𝐺 )
itg2monolem2.9 ⊢ ( 𝜑 → ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 )
Assertion itg2monolem3 ( 𝜑 → ( ∫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 itg2monolem2.7 ⊢ ( 𝜑 → 𝑃 ∈ dom ∫1 )
8 itg2monolem2.8 ⊢ ( 𝜑 → 𝑃 ∘r ≤ 𝐺 )
9 itg2monolem2.9 ⊢ ( 𝜑 → ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 )
10 1 2 3 4 5 6 7 8 9 itg2monolem2 ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑆 ∈ ℝ )
12 11 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑆 ∈ ℂ )
13 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑃 ∈ dom ∫1 )
14 itg1cl ⊢ ( 𝑃 ∈ dom ∫1 → ( ∫1 ‘ 𝑃 ) ∈ ℝ )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ∫1 ‘ 𝑃 ) ∈ ℝ )
16 15 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ∫1 ‘ 𝑃 ) ∈ ℂ )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑡 ∈ ℝ+ )
18 17 rpred ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑡 ∈ ℝ )
19 11 18 readdcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑆 + 𝑡 ) ∈ ℝ )
20 19 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑆 + 𝑡 ) ∈ ℂ )
21 0red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 0 ∈ ℝ )
22 0xr ⊢ 0 ∈ ℝ*
23 22 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
24 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) )
25 24 feq1d ⊢ ( 𝑛 = 1 → ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) ↔ ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) ) )
26 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
27 fss ⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
28 3 26 27 sylancl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
30 1nn ⊢ 1 ∈ ℕ
31 30 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
32 25 29 31 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) )
33 itg2cl ⊢ ( ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ℝ* )
34 32 33 syl ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ℝ* )
35 itg2cl ⊢ ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
36 28 35 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
37 36 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ* )
38 37 frnd ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* )
39 supxrcl ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
40 38 39 syl ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
41 6 40 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
42 itg2ge0 ⊢ ( ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) → 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
43 32 42 syl ⊢ ( 𝜑 → 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
44 2fveq3 ⊢ ( 𝑛 = 1 → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
45 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) )
46 fvex ⊢ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ V
47 44 45 46 fvmpt ⊢ ( 1 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) = ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
48 30 47 ax-mp ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) = ( ∫2 ‘ ( 𝐹 ‘ 1 ) )
49 37 ffnd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ )
50 fnfvelrn ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ ∧ 1 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
51 49 30 50 sylancl ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
52 48 51 eqeltrrid ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
53 supxrub ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* ∧ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) )
54 38 52 53 syl2anc ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) )
55 54 6 breqtrrdi ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ≤ 𝑆 )
56 23 34 41 43 55 xrletrd ⊢ ( 𝜑 → 0 ≤ 𝑆 )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 0 ≤ 𝑆 )
58 11 17 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑆 < ( 𝑆 + 𝑡 ) )
59 21 11 19 57 58 lelttrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 0 < ( 𝑆 + 𝑡 ) )
60 59 gt0ne0d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑆 + 𝑡 ) ≠ 0 )
61 12 16 20 60 div23d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) / ( 𝑆 + 𝑡 ) ) = ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) · ( ∫1 ‘ 𝑃 ) ) )
62 11 19 60 redivcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑆 / ( 𝑆 + 𝑡 ) ) ∈ ℝ )
63 62 15 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) · ( ∫1 ‘ 𝑃 ) ) ∈ ℝ )
64 halfre ⊢ ( 1 / 2 ) ∈ ℝ
65 ifcl ⊢ ( ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∈ ℝ )
66 62 64 65 sylancl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∈ ℝ )
67 66 15 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( ∫1 ‘ 𝑃 ) ) ∈ ℝ )
68 max2 ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( 𝑆 / ( 𝑆 + 𝑡 ) ) ∈ ℝ ) → ( 𝑆 / ( 𝑆 + 𝑡 ) ) ≤ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) )
69 64 62 68 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑆 / ( 𝑆 + 𝑡 ) ) ≤ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) )
70 7 14 syl ⊢ ( 𝜑 → ( ∫1 ‘ 𝑃 ) ∈ ℝ )
71 70 rexrd ⊢ ( 𝜑 → ( ∫1 ‘ 𝑃 ) ∈ ℝ* )
72 xrltnle ⊢ ( ( 𝑆 ∈ ℝ* ∧ ( ∫1 ‘ 𝑃 ) ∈ ℝ* ) → ( 𝑆 < ( ∫1 ‘ 𝑃 ) ↔ ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 ) )
73 41 71 72 syl2anc ⊢ ( 𝜑 → ( 𝑆 < ( ∫1 ‘ 𝑃 ) ↔ ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 ) )
74 9 73 mpbird ⊢ ( 𝜑 → 𝑆 < ( ∫1 ‘ 𝑃 ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑆 < ( ∫1 ‘ 𝑃 ) )
76 21 11 15 57 75 lelttrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 0 < ( ∫1 ‘ 𝑃 ) )
77 lemul1 ⊢ ( ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) ∈ ℝ ∧ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∈ ℝ ∧ ( ( ∫1 ‘ 𝑃 ) ∈ ℝ ∧ 0 < ( ∫1 ‘ 𝑃 ) ) ) → ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) ≤ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ↔ ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) · ( ∫1 ‘ 𝑃 ) ) ≤ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( ∫1 ‘ 𝑃 ) ) ) )
78 62 66 15 76 77 syl112anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) ≤ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ↔ ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) · ( ∫1 ‘ 𝑃 ) ) ≤ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( ∫1 ‘ 𝑃 ) ) ) )
79 69 78 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) · ( ∫1 ‘ 𝑃 ) ) ≤ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( ∫1 ‘ 𝑃 ) ) )
80 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ MblFn )
81 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) )
82 4 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
83 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
84 64 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 1 / 2 ) ∈ ℝ )
85 halfgt0 ⊢ 0 < ( 1 / 2 )
86 85 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 0 < ( 1 / 2 ) )
87 max1 ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( 𝑆 / ( 𝑆 + 𝑡 ) ) ∈ ℝ ) → ( 1 / 2 ) ≤ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) )
88 64 62 87 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 1 / 2 ) ≤ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) )
89 21 84 66 86 88 ltletrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 0 < if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) )
90 20 mulid1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝑆 + 𝑡 ) · 1 ) = ( 𝑆 + 𝑡 ) )
91 58 90 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑆 < ( ( 𝑆 + 𝑡 ) · 1 ) )
92 1red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 1 ∈ ℝ )
93 ltdivmul ⊢ ( ( 𝑆 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝑆 + 𝑡 ) ∈ ℝ ∧ 0 < ( 𝑆 + 𝑡 ) ) ) → ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) < 1 ↔ 𝑆 < ( ( 𝑆 + 𝑡 ) · 1 ) ) )
94 11 92 19 59 93 syl112anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) < 1 ↔ 𝑆 < ( ( 𝑆 + 𝑡 ) · 1 ) ) )
95 91 94 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑆 / ( 𝑆 + 𝑡 ) ) < 1 )
96 halflt1 ⊢ ( 1 / 2 ) < 1
97 breq1 ⊢ ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) = if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) → ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) < 1 ↔ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) < 1 ) )
98 breq1 ⊢ ( ( 1 / 2 ) = if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) → ( ( 1 / 2 ) < 1 ↔ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) < 1 ) )
99 97 98 ifboth ⊢ ( ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) < 1 ∧ ( 1 / 2 ) < 1 ) → if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) < 1 )
100 95 96 99 sylancl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) < 1 )
101 1xr ⊢ 1 ∈ ℝ*
102 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∈ ( 0 (,) 1 ) ↔ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∈ ℝ ∧ 0 < if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∧ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) < 1 ) ) )
103 22 101 102 mp2an ⊢ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∈ ( 0 (,) 1 ) ↔ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∈ ℝ ∧ 0 < if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∧ if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) < 1 ) )
104 66 89 100 103 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) ∈ ( 0 (,) 1 ) )
105 8 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 𝑃 ∘r ≤ 𝐺 )
106 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑃 ‘ 𝑦 ) = ( 𝑃 ‘ 𝑥 ) )
107 106 oveq2d ⊢ ( 𝑦 = 𝑥 → ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( 𝑃 ‘ 𝑦 ) ) = ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( 𝑃 ‘ 𝑥 ) ) )
108 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
109 107 108 breq12d ⊢ ( 𝑦 = 𝑥 → ( ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( 𝑃 ‘ 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) ↔ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( 𝑃 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
110 109 cbvrabv ⊢ { 𝑦 ∈ ℝ ∣ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( 𝑃 ‘ 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) } = { 𝑥 ∈ ℝ ∣ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( 𝑃 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
111 110 mpteq2i ⊢ ( 𝑛 ∈ ℕ ↦ { 𝑦 ∈ ℝ ∣ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( 𝑃 ‘ 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑦 ) } ) = ( 𝑛 ∈ ℕ ↦ { 𝑥 ∈ ℝ ∣ ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( 𝑃 ‘ 𝑥 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
112 1 80 81 82 83 6 104 13 105 11 111 itg2monolem1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( ∫1 ‘ 𝑃 ) ) ≤ 𝑆 )
113 63 67 11 79 112 letrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝑆 / ( 𝑆 + 𝑡 ) ) · ( ∫1 ‘ 𝑃 ) ) ≤ 𝑆 )
114 61 113 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) / ( 𝑆 + 𝑡 ) ) ≤ 𝑆 )
115 11 15 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) ∈ ℝ )
116 ledivmul2 ⊢ ( ( ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( ( 𝑆 + 𝑡 ) ∈ ℝ ∧ 0 < ( 𝑆 + 𝑡 ) ) ) → ( ( ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) / ( 𝑆 + 𝑡 ) ) ≤ 𝑆 ↔ ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) ≤ ( 𝑆 · ( 𝑆 + 𝑡 ) ) ) )
117 115 11 19 59 116 syl112anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) / ( 𝑆 + 𝑡 ) ) ≤ 𝑆 ↔ ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) ≤ ( 𝑆 · ( 𝑆 + 𝑡 ) ) ) )
118 114 117 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) ≤ ( 𝑆 · ( 𝑆 + 𝑡 ) ) )
119 66 15 89 76 mulgt0d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 0 < ( if ( ( 1 / 2 ) ≤ ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 𝑆 / ( 𝑆 + 𝑡 ) ) , ( 1 / 2 ) ) · ( ∫1 ‘ 𝑃 ) ) )
120 21 67 11 119 112 ltletrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → 0 < 𝑆 )
121 lemul2 ⊢ ( ( ( ∫1 ‘ 𝑃 ) ∈ ℝ ∧ ( 𝑆 + 𝑡 ) ∈ ℝ ∧ ( 𝑆 ∈ ℝ ∧ 0 < 𝑆 ) ) → ( ( ∫1 ‘ 𝑃 ) ≤ ( 𝑆 + 𝑡 ) ↔ ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) ≤ ( 𝑆 · ( 𝑆 + 𝑡 ) ) ) )
122 15 19 11 120 121 syl112anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ( ∫1 ‘ 𝑃 ) ≤ ( 𝑆 + 𝑡 ) ↔ ( 𝑆 · ( ∫1 ‘ 𝑃 ) ) ≤ ( 𝑆 · ( 𝑆 + 𝑡 ) ) ) )
123 118 122 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ+ ) → ( ∫1 ‘ 𝑃 ) ≤ ( 𝑆 + 𝑡 ) )
124 123 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ ℝ+ ( ∫1 ‘ 𝑃 ) ≤ ( 𝑆 + 𝑡 ) )
125 alrple ⊢ ( ( ( ∫1 ‘ 𝑃 ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( ( ∫1 ‘ 𝑃 ) ≤ 𝑆 ↔ ∀ 𝑡 ∈ ℝ+ ( ∫1 ‘ 𝑃 ) ≤ ( 𝑆 + 𝑡 ) ) )
126 70 10 125 syl2anc ⊢ ( 𝜑 → ( ( ∫1 ‘ 𝑃 ) ≤ 𝑆 ↔ ∀ 𝑡 ∈ ℝ+ ( ∫1 ‘ 𝑃 ) ≤ ( 𝑆 + 𝑡 ) ) )
127 124 126 mpbird ⊢ ( 𝜑 → ( ∫1 ‘ 𝑃 ) ≤ 𝑆 )