Step | Hyp | Ref
| Expression |
1 | | itg2mono.1 |
. . . . . . . . . 10
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < )) |
2 | | itg2mono.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) |
3 | | itg2mono.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) |
4 | | itg2mono.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1))) |
5 | | itg2mono.5 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
6 | | itg2mono.6 |
. . . . . . . . . 10
⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
) |
7 | | itg2monolem2.7 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ dom
∫1) |
8 | | itg2monolem2.8 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∘𝑟 ≤ 𝐺) |
9 | | itg2monolem2.9 |
. . . . . . . . . 10
⊢ (𝜑 → ¬
(∫1‘𝑃)
≤ 𝑆) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | itg2monolem2 23324 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℝ) |
11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑆 ∈
ℝ) |
12 | 11 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑆 ∈
ℂ) |
13 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑃 ∈ dom
∫1) |
14 | | itg1cl 23258 |
. . . . . . . . 9
⊢ (𝑃 ∈ dom ∫1
→ (∫1‘𝑃) ∈ ℝ) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(∫1‘𝑃)
∈ ℝ) |
16 | 15 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(∫1‘𝑃)
∈ ℂ) |
17 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑡 ∈
ℝ+) |
18 | 17 | rpred 11748 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑡 ∈
ℝ) |
19 | 11, 18 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑆 + 𝑡) ∈ ℝ) |
20 | 19 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑆 + 𝑡) ∈ ℂ) |
21 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 0 ∈
ℝ) |
22 | | 0xr 9965 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
23 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ*) |
24 | | 1nn 10908 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
25 | | icossicc 12131 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
26 | | fss 5969 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑛):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ (0[,]+∞)) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
27 | 3, 25, 26 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
28 | 27 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞)) |
29 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → (𝐹‘𝑛) = (𝐹‘1)) |
30 | 29 | feq1d 5943 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → ((𝐹‘𝑛):ℝ⟶(0[,]+∞) ↔ (𝐹‘1):ℝ⟶(0[,]+∞))) |
31 | 30 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℕ → (∀𝑛
∈ ℕ (𝐹‘𝑛):ℝ⟶(0[,]+∞) → (𝐹‘1):ℝ⟶(0[,]+∞))) |
32 | 24, 28, 31 | mpsyl 66 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘1):ℝ⟶(0[,]+∞)) |
33 | | itg2cl 23305 |
. . . . . . . . . . . 12
⊢ ((𝐹‘1):ℝ⟶(0[,]+∞)
→ (∫2‘(𝐹‘1)) ∈
ℝ*) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ∈
ℝ*) |
35 | | itg2cl 23305 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛):ℝ⟶(0[,]+∞) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
36 | 27, 35 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(∫2‘(𝐹‘𝑛)) ∈
ℝ*) |
37 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) |
38 | 36, 37 | fmptd 6292 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ*) |
39 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ* →
ran (𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆
ℝ*) |
41 | | supxrcl 12017 |
. . . . . . . . . . . . 13
⊢ (ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ* →
sup(ran (𝑛 ∈ ℕ
↦ (∫2‘(𝐹‘𝑛))), ℝ*, < ) ∈
ℝ*) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, < ) ∈
ℝ*) |
43 | 6, 42 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
44 | | itg2ge0 23308 |
. . . . . . . . . . . 12
⊢ ((𝐹‘1):ℝ⟶(0[,]+∞)
→ 0 ≤ (∫2‘(𝐹‘1))) |
45 | 32, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤
(∫2‘(𝐹‘1))) |
46 | 29 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 →
(∫2‘(𝐹‘𝑛)) = (∫2‘(𝐹‘1))) |
47 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(∫2‘(𝐹‘1)) ∈ V |
48 | 46, 37, 47 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℕ → ((𝑛 ∈
ℕ ↦ (∫2‘(𝐹‘𝑛)))‘1) =
(∫2‘(𝐹‘1))) |
49 | 24, 48 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘1) =
(∫2‘(𝐹‘1)) |
50 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))):ℕ⟶ℝ* →
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ) |
51 | 38, 50 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ) |
52 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) Fn ℕ ∧ 1 ∈ ℕ) →
((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘1) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
53 | 51, 24, 52 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))‘1) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
54 | 49, 53 | syl5eqelr 2693 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) |
55 | | supxrub 12026 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))) ⊆ ℝ* ∧
(∫2‘(𝐹‘1)) ∈ ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛)))) → (∫2‘(𝐹‘1)) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
)) |
56 | 40, 54, 55 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ≤ sup(ran (𝑛 ∈ ℕ ↦
(∫2‘(𝐹‘𝑛))), ℝ*, <
)) |
57 | 56, 6 | syl6breqr 4625 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∫2‘(𝐹‘1)) ≤ 𝑆) |
58 | 23, 34, 43, 45, 57 | xrletrd 11869 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝑆) |
59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 0 ≤
𝑆) |
60 | 11, 17 | ltaddrpd 11781 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑆 < (𝑆 + 𝑡)) |
61 | 21, 11, 19, 59, 60 | lelttrd 10074 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 0 <
(𝑆 + 𝑡)) |
62 | 61 | gt0ne0d 10471 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑆 + 𝑡) ≠ 0) |
63 | 12, 16, 20, 62 | div23d 10717 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝑆 ·
(∫1‘𝑃)) / (𝑆 + 𝑡)) = ((𝑆 / (𝑆 + 𝑡)) · (∫1‘𝑃))) |
64 | 11, 19, 62 | redivcld 10732 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑆 / (𝑆 + 𝑡)) ∈ ℝ) |
65 | 64, 15 | remulcld 9949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝑆 / (𝑆 + 𝑡)) · (∫1‘𝑃)) ∈
ℝ) |
66 | | halfre 11123 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
67 | | ifcl 4080 |
. . . . . . . . 9
⊢ (((𝑆 / (𝑆 + 𝑡)) ∈ ℝ ∧ (1 / 2) ∈
ℝ) → if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ∈ ℝ) |
68 | 64, 66, 67 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → if((1 /
2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ∈ ℝ) |
69 | 68, 15 | remulcld 9949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (if((1 /
2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ·
(∫1‘𝑃)) ∈ ℝ) |
70 | | max2 11892 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ (𝑆 /
(𝑆 + 𝑡)) ∈ ℝ) → (𝑆 / (𝑆 + 𝑡)) ≤ if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2))) |
71 | 66, 64, 70 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑆 / (𝑆 + 𝑡)) ≤ if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2))) |
72 | 7, 14 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(∫1‘𝑃)
∈ ℝ) |
73 | 72 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(∫1‘𝑃)
∈ ℝ*) |
74 | | xrltnle 9984 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℝ*
∧ (∫1‘𝑃) ∈ ℝ*) → (𝑆 <
(∫1‘𝑃)
↔ ¬ (∫1‘𝑃) ≤ 𝑆)) |
75 | 43, 73, 74 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 < (∫1‘𝑃) ↔ ¬
(∫1‘𝑃)
≤ 𝑆)) |
76 | 9, 75 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 < (∫1‘𝑃)) |
77 | 76 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑆 <
(∫1‘𝑃)) |
78 | 21, 11, 15, 59, 77 | lelttrd 10074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 0 <
(∫1‘𝑃)) |
79 | | lemul1 10754 |
. . . . . . . . 9
⊢ (((𝑆 / (𝑆 + 𝑡)) ∈ ℝ ∧ if((1 / 2) ≤
(𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ∈ ℝ ∧
((∫1‘𝑃) ∈ ℝ ∧ 0 <
(∫1‘𝑃))) → ((𝑆 / (𝑆 + 𝑡)) ≤ if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ↔ ((𝑆 / (𝑆 + 𝑡)) · (∫1‘𝑃)) ≤ (if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ·
(∫1‘𝑃)))) |
80 | 64, 68, 15, 78, 79 | syl112anc 1322 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝑆 / (𝑆 + 𝑡)) ≤ if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ↔ ((𝑆 / (𝑆 + 𝑡)) · (∫1‘𝑃)) ≤ (if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ·
(∫1‘𝑃)))) |
81 | 71, 80 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝑆 / (𝑆 + 𝑡)) · (∫1‘𝑃)) ≤ (if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ·
(∫1‘𝑃))) |
82 | 2 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn) |
83 | 3 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞)) |
84 | 4 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1))) |
85 | 5 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) →
∃𝑦 ∈ ℝ
∀𝑛 ∈ ℕ
((𝐹‘𝑛)‘𝑥) ≤ 𝑦) |
86 | 66 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 / 2)
∈ ℝ) |
87 | | halfgt0 11125 |
. . . . . . . . . . 11
⊢ 0 < (1
/ 2) |
88 | 87 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 0 < (1
/ 2)) |
89 | | max1 11890 |
. . . . . . . . . . 11
⊢ (((1 / 2)
∈ ℝ ∧ (𝑆 /
(𝑆 + 𝑡)) ∈ ℝ) → (1 / 2) ≤ if((1
/ 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2))) |
90 | 66, 64, 89 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 / 2)
≤ if((1 / 2) ≤ (𝑆 /
(𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2))) |
91 | 21, 86, 68, 88, 90 | ltletrd 10076 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 0 <
if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2))) |
92 | 20 | mulid1d 9936 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝑆 + 𝑡) · 1) = (𝑆 + 𝑡)) |
93 | 60, 92 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑆 < ((𝑆 + 𝑡) · 1)) |
94 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 1 ∈
ℝ) |
95 | | ltdivmul 10777 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℝ ∧ 1 ∈
ℝ ∧ ((𝑆 + 𝑡) ∈ ℝ ∧ 0 <
(𝑆 + 𝑡))) → ((𝑆 / (𝑆 + 𝑡)) < 1 ↔ 𝑆 < ((𝑆 + 𝑡) · 1))) |
96 | 11, 94, 19, 61, 95 | syl112anc 1322 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝑆 / (𝑆 + 𝑡)) < 1 ↔ 𝑆 < ((𝑆 + 𝑡) · 1))) |
97 | 93, 96 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑆 / (𝑆 + 𝑡)) < 1) |
98 | | halflt1 11127 |
. . . . . . . . . 10
⊢ (1 / 2)
< 1 |
99 | | breq1 4586 |
. . . . . . . . . . 11
⊢ ((𝑆 / (𝑆 + 𝑡)) = if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) → ((𝑆 / (𝑆 + 𝑡)) < 1 ↔ if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) < 1)) |
100 | | breq1 4586 |
. . . . . . . . . . 11
⊢ ((1 / 2)
= if((1 / 2) ≤ (𝑆 /
(𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) → ((1 / 2) < 1 ↔
if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) < 1)) |
101 | 99, 100 | ifboth 4074 |
. . . . . . . . . 10
⊢ (((𝑆 / (𝑆 + 𝑡)) < 1 ∧ (1 / 2) < 1) → if((1
/ 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) < 1) |
102 | 97, 98, 101 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → if((1 /
2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) < 1) |
103 | | 1re 9918 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
104 | 103 | rexri 9976 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ* |
105 | | elioo2 12087 |
. . . . . . . . . 10
⊢ ((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))) |
106 | 22, 104, 105 | mp2an 704 |
. . . . . . . . 9
⊢ (if((1 /
2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ∈ (0(,)1) ↔ (if((1 /
2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ∈ ℝ ∧ 0 <
if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ∧ if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) < 1)) |
107 | 68, 91, 102, 106 | syl3anbrc 1239 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → if((1 /
2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ∈ (0(,)1)) |
108 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑃 ∘𝑟
≤ 𝐺) |
109 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑃‘𝑦) = (𝑃‘𝑥)) |
110 | 109 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) · (𝑃‘𝑦)) = (if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) · (𝑃‘𝑥))) |
111 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((𝐹‘𝑛)‘𝑦) = ((𝐹‘𝑛)‘𝑥)) |
112 | 110, 111 | breq12d 4596 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) · (𝑃‘𝑦)) ≤ ((𝐹‘𝑛)‘𝑦) ↔ (if((1 / 2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) · (𝑃‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥))) |
113 | 112 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑦 ∈ ℝ ∣ (if((1 /
2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) · (𝑃‘𝑦)) ≤ ((𝐹‘𝑛)‘𝑦)} = {𝑥 ∈ ℝ ∣ (if((1 / 2) ≤
(𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) · (𝑃‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)} |
114 | 113 | mpteq2i 4669 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ {𝑦 ∈ ℝ ∣ (if((1 /
2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) · (𝑃‘𝑦)) ≤ ((𝐹‘𝑛)‘𝑦)}) = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (if((1 / 2) ≤
(𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) · (𝑃‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)}) |
115 | 1, 82, 83, 84, 85, 6, 107, 13, 108, 11, 114 | itg2monolem1 23323 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (if((1 /
2) ≤ (𝑆 / (𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ·
(∫1‘𝑃)) ≤ 𝑆) |
116 | 65, 69, 11, 81, 115 | letrd 10073 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝑆 / (𝑆 + 𝑡)) · (∫1‘𝑃)) ≤ 𝑆) |
117 | 63, 116 | eqbrtrd 4605 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ((𝑆 ·
(∫1‘𝑃)) / (𝑆 + 𝑡)) ≤ 𝑆) |
118 | 11, 15 | remulcld 9949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑆 ·
(∫1‘𝑃)) ∈ ℝ) |
119 | | ledivmul2 10781 |
. . . . . 6
⊢ (((𝑆 ·
(∫1‘𝑃)) ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ((𝑆 + 𝑡) ∈ ℝ ∧ 0 < (𝑆 + 𝑡))) → (((𝑆 · (∫1‘𝑃)) / (𝑆 + 𝑡)) ≤ 𝑆 ↔ (𝑆 · (∫1‘𝑃)) ≤ (𝑆 · (𝑆 + 𝑡)))) |
120 | 118, 11, 19, 61, 119 | syl112anc 1322 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (((𝑆 ·
(∫1‘𝑃)) / (𝑆 + 𝑡)) ≤ 𝑆 ↔ (𝑆 · (∫1‘𝑃)) ≤ (𝑆 · (𝑆 + 𝑡)))) |
121 | 117, 120 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑆 ·
(∫1‘𝑃)) ≤ (𝑆 · (𝑆 + 𝑡))) |
122 | 68, 15, 91, 78 | mulgt0d 10071 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 0 <
(if((1 / 2) ≤ (𝑆 /
(𝑆 + 𝑡)), (𝑆 / (𝑆 + 𝑡)), (1 / 2)) ·
(∫1‘𝑃))) |
123 | 21, 69, 11, 122, 115 | ltletrd 10076 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 0 <
𝑆) |
124 | | lemul2 10755 |
. . . . 5
⊢
(((∫1‘𝑃) ∈ ℝ ∧ (𝑆 + 𝑡) ∈ ℝ ∧ (𝑆 ∈ ℝ ∧ 0 < 𝑆)) →
((∫1‘𝑃) ≤ (𝑆 + 𝑡) ↔ (𝑆 · (∫1‘𝑃)) ≤ (𝑆 · (𝑆 + 𝑡)))) |
125 | 15, 19, 11, 123, 124 | syl112anc 1322 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
((∫1‘𝑃) ≤ (𝑆 + 𝑡) ↔ (𝑆 · (∫1‘𝑃)) ≤ (𝑆 · (𝑆 + 𝑡)))) |
126 | 121, 125 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(∫1‘𝑃)
≤ (𝑆 + 𝑡)) |
127 | 126 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ ℝ+
(∫1‘𝑃)
≤ (𝑆 + 𝑡)) |
128 | | alrple 11911 |
. . 3
⊢
(((∫1‘𝑃) ∈ ℝ ∧ 𝑆 ∈ ℝ) →
((∫1‘𝑃) ≤ 𝑆 ↔ ∀𝑡 ∈ ℝ+
(∫1‘𝑃)
≤ (𝑆 + 𝑡))) |
129 | 72, 10, 128 | syl2anc 691 |
. 2
⊢ (𝜑 →
((∫1‘𝑃) ≤ 𝑆 ↔ ∀𝑡 ∈ ℝ+
(∫1‘𝑃)
≤ (𝑆 + 𝑡))) |
130 | 127, 129 | mpbird 246 |
1
⊢ (𝜑 →
(∫1‘𝑃)
≤ 𝑆) |