Step | Hyp | Ref
| Expression |
1 | | itg2mulc.2 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
2 | | icossicc 12131 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
3 | | fss 5969 |
. . . . . . 7
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞)) |
4 | 1, 2, 3 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
5 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝐹:ℝ⟶(0[,]+∞)) |
6 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝑓 ∈ dom
∫1) |
7 | | itg2mulclem.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
8 | 7 | rpreccld 11758 |
. . . . . . . 8
⊢ (𝜑 → (1 / 𝐴) ∈
ℝ+) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (1 /
𝐴) ∈
ℝ+) |
10 | 9 | rpred 11748 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (1 /
𝐴) ∈
ℝ) |
11 | 6, 10 | i1fmulc 23276 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓) ∈ dom
∫1) |
12 | | itg2ub 23306 |
. . . . . 6
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ ((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓) ∈ dom
∫1 ∧ ((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓)
∘𝑟 ≤ 𝐹) → (∫1‘((ℝ
× {(1 / 𝐴)})
∘𝑓 · 𝑓)) ≤ (∫2‘𝐹)) |
13 | 12 | 3expia 1259 |
. . . . 5
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ ((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓) ∈ dom
∫1) → (((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓)
∘𝑟 ≤ 𝐹 → (∫1‘((ℝ
× {(1 / 𝐴)})
∘𝑓 · 𝑓)) ≤ (∫2‘𝐹))) |
14 | 5, 11, 13 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓)
∘𝑟 ≤ 𝐹 → (∫1‘((ℝ
× {(1 / 𝐴)})
∘𝑓 · 𝑓)) ≤ (∫2‘𝐹))) |
15 | | i1ff 23249 |
. . . . . . . . . 10
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
16 | 15 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ) |
17 | 16 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → (𝑓‘𝑦) ∈ ℝ) |
18 | | rge0ssre 12151 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℝ |
19 | | fss 5969 |
. . . . . . . . . . 11
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ) |
20 | 1, 18, 19 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
21 | 20 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝐹:ℝ⟶ℝ) |
22 | 21 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
23 | 7 | rpred 11748 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
24 | 23 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → 𝐴 ∈
ℝ) |
25 | 7 | rpgt0d 11751 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝐴) |
26 | 25 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → 0 <
𝐴) |
27 | | ledivmul 10778 |
. . . . . . . 8
⊢ (((𝑓‘𝑦) ∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (((𝑓‘𝑦) / 𝐴) ≤ (𝐹‘𝑦) ↔ (𝑓‘𝑦) ≤ (𝐴 · (𝐹‘𝑦)))) |
28 | 17, 22, 24, 26, 27 | syl112anc 1322 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → (((𝑓‘𝑦) / 𝐴) ≤ (𝐹‘𝑦) ↔ (𝑓‘𝑦) ≤ (𝐴 · (𝐹‘𝑦)))) |
29 | 17 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → (𝑓‘𝑦) ∈ ℂ) |
30 | 24 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → 𝐴 ∈
ℂ) |
31 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝐴 ∈
ℝ+) |
32 | 31 | rpne0d 11753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝐴 ≠ 0) |
33 | 32 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → 𝐴 ≠ 0) |
34 | 29, 30, 33 | divrec2d 10684 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑦) / 𝐴) = ((1 / 𝐴) · (𝑓‘𝑦))) |
35 | 34 | breq1d 4593 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → (((𝑓‘𝑦) / 𝐴) ≤ (𝐹‘𝑦) ↔ ((1 / 𝐴) · (𝑓‘𝑦)) ≤ (𝐹‘𝑦))) |
36 | 28, 35 | bitr3d 269 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑦) ≤ (𝐴 · (𝐹‘𝑦)) ↔ ((1 / 𝐴) · (𝑓‘𝑦)) ≤ (𝐹‘𝑦))) |
37 | 36 | ralbidva 2968 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∀𝑦 ∈ ℝ
(𝑓‘𝑦) ≤ (𝐴 · (𝐹‘𝑦)) ↔ ∀𝑦 ∈ ℝ ((1 / 𝐴) · (𝑓‘𝑦)) ≤ (𝐹‘𝑦))) |
38 | | reex 9906 |
. . . . . . 7
⊢ ℝ
∈ V |
39 | 38 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ℝ
∈ V) |
40 | | ovex 6577 |
. . . . . . 7
⊢ (𝐴 · (𝐹‘𝑦)) ∈ V |
41 | 40 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → (𝐴 · (𝐹‘𝑦)) ∈ V) |
42 | 16 | feqmptd 6159 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝑓 = (𝑦 ∈ ℝ ↦ (𝑓‘𝑦))) |
43 | 7 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → 𝐴 ∈
ℝ+) |
44 | | fconstmpt 5085 |
. . . . . . . 8
⊢ (ℝ
× {𝐴}) = (𝑦 ∈ ℝ ↦ 𝐴) |
45 | 44 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(ℝ × {𝐴}) =
(𝑦 ∈ ℝ ↦
𝐴)) |
46 | 1 | feqmptd 6159 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦))) |
47 | 46 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝐹 = (𝑦 ∈ ℝ ↦ (𝐹‘𝑦))) |
48 | 39, 43, 22, 45, 47 | offval2 6812 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
((ℝ × {𝐴})
∘𝑓 · 𝐹) = (𝑦 ∈ ℝ ↦ (𝐴 · (𝐹‘𝑦)))) |
49 | 39, 17, 41, 42, 48 | ofrfval2 6813 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟
≤ ((ℝ × {𝐴})
∘𝑓 · 𝐹) ↔ ∀𝑦 ∈ ℝ (𝑓‘𝑦) ≤ (𝐴 · (𝐹‘𝑦)))) |
50 | | ovex 6577 |
. . . . . . 7
⊢ ((1 /
𝐴) · (𝑓‘𝑦)) ∈ V |
51 | 50 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → ((1 /
𝐴) · (𝑓‘𝑦)) ∈ V) |
52 | 8 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑦 ∈ ℝ) → (1 /
𝐴) ∈
ℝ+) |
53 | | fconstmpt 5085 |
. . . . . . . 8
⊢ (ℝ
× {(1 / 𝐴)}) = (𝑦 ∈ ℝ ↦ (1 /
𝐴)) |
54 | 53 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(ℝ × {(1 / 𝐴)})
= (𝑦 ∈ ℝ ↦
(1 / 𝐴))) |
55 | 39, 52, 17, 54, 42 | offval2 6812 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓) = (𝑦 ∈ ℝ ↦ ((1 / 𝐴) · (𝑓‘𝑦)))) |
56 | 39, 51, 22, 55, 47 | ofrfval2 6813 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓)
∘𝑟 ≤ 𝐹 ↔ ∀𝑦 ∈ ℝ ((1 / 𝐴) · (𝑓‘𝑦)) ≤ (𝐹‘𝑦))) |
57 | 37, 49, 56 | 3bitr4d 299 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟
≤ ((ℝ × {𝐴})
∘𝑓 · 𝐹) ↔ ((ℝ × {(1 / 𝐴)}) ∘𝑓
· 𝑓)
∘𝑟 ≤ 𝐹)) |
58 | 6, 10 | itg1mulc 23277 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∫1‘((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓)) = ((1 / 𝐴) ·
(∫1‘𝑓))) |
59 | | itg1cl 23258 |
. . . . . . . . . 10
⊢ (𝑓 ∈ dom ∫1
→ (∫1‘𝑓) ∈ ℝ) |
60 | 59 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∫1‘𝑓)
∈ ℝ) |
61 | 60 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∫1‘𝑓)
∈ ℂ) |
62 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝐴 ∈
ℝ) |
63 | 62 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 𝐴 ∈
ℂ) |
64 | 61, 63, 32 | divrec2d 10684 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
((∫1‘𝑓) / 𝐴) = ((1 / 𝐴) · (∫1‘𝑓))) |
65 | 58, 64 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∫1‘((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓)) =
((∫1‘𝑓) / 𝐴)) |
66 | 65 | breq1d 4593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
((∫1‘((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓)) ≤
(∫2‘𝐹)
↔ ((∫1‘𝑓) / 𝐴) ≤ (∫2‘𝐹))) |
67 | | itg2mulc.3 |
. . . . . . 7
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) |
68 | 67 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∫2‘𝐹)
∈ ℝ) |
69 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → 0 <
𝐴) |
70 | | ledivmul 10778 |
. . . . . 6
⊢
(((∫1‘𝑓) ∈ ℝ ∧
(∫2‘𝐹)
∈ ℝ ∧ (𝐴
∈ ℝ ∧ 0 < 𝐴)) → (((∫1‘𝑓) / 𝐴) ≤ (∫2‘𝐹) ↔
(∫1‘𝑓)
≤ (𝐴 ·
(∫2‘𝐹)))) |
71 | 60, 68, 62, 69, 70 | syl112anc 1322 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(((∫1‘𝑓) / 𝐴) ≤ (∫2‘𝐹) ↔
(∫1‘𝑓)
≤ (𝐴 ·
(∫2‘𝐹)))) |
72 | 66, 71 | bitr2d 268 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
((∫1‘𝑓) ≤ (𝐴 · (∫2‘𝐹)) ↔
(∫1‘((ℝ × {(1 / 𝐴)}) ∘𝑓 ·
𝑓)) ≤
(∫2‘𝐹))) |
73 | 14, 57, 72 | 3imtr4d 282 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟
≤ ((ℝ × {𝐴})
∘𝑓 · 𝐹) → (∫1‘𝑓) ≤ (𝐴 · (∫2‘𝐹)))) |
74 | 73 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ ((ℝ × {𝐴})
∘𝑓 · 𝐹) → (∫1‘𝑓) ≤ (𝐴 · (∫2‘𝐹)))) |
75 | | ge0mulcl 12156 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 · 𝑦) ∈
(0[,)+∞)) |
76 | 75 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) →
(𝑥 · 𝑦) ∈
(0[,)+∞)) |
77 | | fconstg 6005 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (ℝ × {𝐴}):ℝ⟶{𝐴}) |
78 | 7, 77 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶{𝐴}) |
79 | | rpre 11715 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
80 | | rpge0 11721 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ 0 ≤ 𝐴) |
81 | | elrege0 12149 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0[,)+∞) ↔
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
82 | 79, 80, 81 | sylanbrc 695 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
(0[,)+∞)) |
83 | 7, 82 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (0[,)+∞)) |
84 | 83 | snssd 4281 |
. . . . . 6
⊢ (𝜑 → {𝐴} ⊆ (0[,)+∞)) |
85 | 78, 84 | fssd 5970 |
. . . . 5
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶(0[,)+∞)) |
86 | 38 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈
V) |
87 | | inidm 3784 |
. . . . 5
⊢ (ℝ
∩ ℝ) = ℝ |
88 | 76, 85, 1, 86, 86, 87 | off 6810 |
. . . 4
⊢ (𝜑 → ((ℝ × {𝐴}) ∘𝑓
· 𝐹):ℝ⟶(0[,)+∞)) |
89 | | fss 5969 |
. . . 4
⊢
((((ℝ × {𝐴}) ∘𝑓 ·
𝐹):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ (0[,]+∞)) → ((ℝ × {𝐴}) ∘𝑓
· 𝐹):ℝ⟶(0[,]+∞)) |
90 | 88, 2, 89 | sylancl 693 |
. . 3
⊢ (𝜑 → ((ℝ × {𝐴}) ∘𝑓
· 𝐹):ℝ⟶(0[,]+∞)) |
91 | 23, 67 | remulcld 9949 |
. . . 4
⊢ (𝜑 → (𝐴 · (∫2‘𝐹)) ∈
ℝ) |
92 | 91 | rexrd 9968 |
. . 3
⊢ (𝜑 → (𝐴 · (∫2‘𝐹)) ∈
ℝ*) |
93 | | itg2leub 23307 |
. . 3
⊢
((((ℝ × {𝐴}) ∘𝑓 ·
𝐹):ℝ⟶(0[,]+∞) ∧ (𝐴 ·
(∫2‘𝐹)) ∈ ℝ*) →
((∫2‘((ℝ × {𝐴}) ∘𝑓 ·
𝐹)) ≤ (𝐴 · (∫2‘𝐹)) ↔ ∀𝑓 ∈ dom
∫1(𝑓
∘𝑟 ≤ ((ℝ × {𝐴}) ∘𝑓 ·
𝐹) →
(∫1‘𝑓)
≤ (𝐴 ·
(∫2‘𝐹))))) |
94 | 90, 92, 93 | syl2anc 691 |
. 2
⊢ (𝜑 →
((∫2‘((ℝ × {𝐴}) ∘𝑓 ·
𝐹)) ≤ (𝐴 · (∫2‘𝐹)) ↔ ∀𝑓 ∈ dom
∫1(𝑓
∘𝑟 ≤ ((ℝ × {𝐴}) ∘𝑓 ·
𝐹) →
(∫1‘𝑓)
≤ (𝐴 ·
(∫2‘𝐹))))) |
95 | 74, 94 | mpbird 246 |
1
⊢ (𝜑 →
(∫2‘((ℝ × {𝐴}) ∘𝑓 ·
𝐹)) ≤ (𝐴 · (∫2‘𝐹))) |