Step | Hyp | Ref
| Expression |
1 | | itg2split.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ dom vol) |
2 | | itg2split.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ dom vol) |
3 | | itg2split.i |
. . 3
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
4 | | itg2split.u |
. . 3
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) |
5 | | itg2split.c |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) |
6 | | itg2split.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
7 | | itg2split.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
8 | | itg2split.h |
. . 3
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
9 | | itg2split.sf |
. . 3
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) |
10 | | itg2split.sg |
. . 3
⊢ (𝜑 →
(∫2‘𝐺)
∈ ℝ) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | itg2splitlem 23321 |
. 2
⊢ (𝜑 →
(∫2‘𝐻)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) |
12 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫2‘𝐺)
∈ ℝ) |
13 | 5 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) |
14 | | 0e0iccpnf 12154 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]+∞) |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑈) → 0 ∈
(0[,]+∞)) |
16 | 13, 15 | ifclda 4070 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) |
17 | 16, 8 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:ℝ⟶(0[,]+∞)) |
18 | 9, 10 | readdcld 9948 |
. . . . . . . . 9
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ) |
19 | | itg2lecl 23311 |
. . . . . . . . 9
⊢ ((𝐻:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ ∧
(∫2‘𝐻)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) →
(∫2‘𝐻)
∈ ℝ) |
20 | 17, 18, 11, 19 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 →
(∫2‘𝐻)
∈ ℝ) |
21 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫2‘𝐻)
∈ ℝ) |
22 | | itg1cl 23258 |
. . . . . . . 8
⊢ (𝑓 ∈ dom ∫1
→ (∫1‘𝑓) ∈ ℝ) |
23 | 22 | ad2antrl 760 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫1‘𝑓)
∈ ℝ) |
24 | | simprll 798 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑓 ∈ dom
∫1) |
25 | | simprrl 800 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑔 ∈ dom
∫1) |
26 | 24, 25 | itg1add 23274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘(𝑓 ∘𝑓 +
𝑔)) =
((∫1‘𝑓) + (∫1‘𝑔))) |
27 | 17 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝐻:ℝ⟶(0[,]+∞)) |
28 | 24, 25 | i1fadd 23268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝑓 ∘𝑓 + 𝑔) ∈ dom
∫1) |
29 | | inss1 3795 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
30 | | mblss 23106 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
31 | 1, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
32 | 29, 31 | syl5ss 3579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ ℝ) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝐴 ∩ 𝐵) ⊆ ℝ) |
34 | 3 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
35 | | nfv 1830 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥𝜑 |
36 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑓 ∈ dom
∫1 |
37 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝑓 |
38 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥
∘𝑟 ≤ |
39 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
40 | 6, 39 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝐹 |
41 | 37, 38, 40 | nfbr 4629 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑓 ∘𝑟
≤ 𝐹 |
42 | 36, 41 | nfan 1816 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐹) |
43 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑔 ∈ dom
∫1 |
44 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝑔 |
45 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
46 | 7, 45 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝐺 |
47 | 44, 38, 46 | nfbr 4629 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑔 ∘𝑟
≤ 𝐺 |
48 | 43, 47 | nfan 1816 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺) |
49 | 42, 48 | nfan 1816 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟
≤ 𝐺)) |
50 | 35, 49 | nfan 1816 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) |
51 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → 𝑥 ∈ ℝ) |
52 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
53 | 24, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑓:ℝ⟶ℝ) |
54 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:ℝ⟶ℝ →
𝑓 Fn
ℝ) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑓 Fn ℝ) |
56 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
57 | 25, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑔:ℝ⟶ℝ) |
58 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔:ℝ⟶ℝ →
𝑔 Fn
ℝ) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑔 Fn ℝ) |
60 | | reex 9906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℝ
∈ V |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ℝ ∈
V) |
62 | | inidm 3784 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℝ
∩ ℝ) = ℝ |
63 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
64 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) = (𝑔‘𝑥)) |
65 | 55, 59, 61, 61, 62, 63, 64 | ofval 6804 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) = ((𝑓‘𝑥) + (𝑔‘𝑥))) |
66 | 51, 65 | sylan2 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) = ((𝑓‘𝑥) + (𝑔‘𝑥))) |
67 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓:ℝ⟶ℝ ∧
𝑥 ∈ ℝ) →
(𝑓‘𝑥) ∈ ℝ) |
68 | 53, 51, 67 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑥) ∈ ℝ) |
69 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:ℝ⟶ℝ ∧
𝑥 ∈ ℝ) →
(𝑔‘𝑥) ∈ ℝ) |
70 | 57, 51, 69 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑔‘𝑥) ∈ ℝ) |
71 | 68, 70 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈ ℝ) |
72 | 71 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈
ℝ*) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈
ℝ*) |
74 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℝ) |
75 | 74 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈
ℝ*) |
76 | | iccssxr 12127 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0[,]+∞) ⊆ ℝ* |
77 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐻:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (𝐻‘𝑥) ∈
(0[,]+∞)) |
78 | 27, 51, 77 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) ∈ (0[,]+∞)) |
79 | 76, 78 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) ∈
ℝ*) |
80 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℝ*) |
81 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℝ) |
82 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
83 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑔 ∘𝑟 ≤ 𝐺) |
84 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → ℝ ∈
V) |
85 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑔‘𝑥) ∈ V |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ V) |
87 | | ssun2 3739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
88 | 87, 4 | syl5sseqr 3617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
89 | 88 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
90 | 89 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
91 | 90, 13 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
92 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → 0 ∈
(0[,]+∞)) |
93 | 91, 92 | ifclda 4070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞)) |
94 | 93 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞)) |
95 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝑔 Fn ℝ) |
96 | | dffn5 6151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑔 Fn ℝ ↔ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔‘𝑥))) |
97 | 95, 96 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔‘𝑥))) |
98 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
99 | 84, 86, 94, 97, 98 | ofrfval2 6813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → (𝑔 ∘𝑟 ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
100 | 59, 99 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝑔 ∘𝑟 ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
101 | 83, 100 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
102 | 101 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
103 | 51, 102 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
104 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
105 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) |
106 | 105 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) |
107 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
108 | 106, 107 | sylnib 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
109 | | imnan 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
110 | 108, 109 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
111 | 110 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ 𝐵) |
112 | 111 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐵, 𝐶, 0) = 0) |
113 | 104, 112 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ 0) |
114 | 81, 82, 74, 113 | leadd2dd 10521 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ ((𝑓‘𝑥) + 0)) |
115 | 74 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℂ) |
116 | 115 | addid1d 10115 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + 0) = (𝑓‘𝑥)) |
117 | 114, 116 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝑓‘𝑥)) |
118 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑓 ∘𝑟 ≤ 𝐹) |
119 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → ℝ ∈
V) |
120 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓‘𝑥) ∈ V |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ∈ V) |
122 | | ssun1 3738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
123 | 122, 4 | syl5sseqr 3617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
124 | 123 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
125 | 124 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
126 | 125, 13 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) |
127 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
128 | 126, 127 | ifclda 4070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞)) |
129 | 128 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞)) |
130 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝑓 Fn ℝ) |
131 | | dffn5 6151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 Fn ℝ ↔ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥))) |
132 | 130, 131 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥))) |
133 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
134 | 119, 121,
129, 132, 133 | ofrfval2 6813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → (𝑓 ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
135 | 55, 134 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝑓 ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
136 | 118, 135 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
137 | 136 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
138 | 51, 137 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
139 | 138 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
140 | 123 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → 𝐴 ⊆ 𝑈) |
141 | 140 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
142 | 141 | iftrued 4044 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = 𝐶) |
143 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
144 | 16 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) |
145 | 8 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
146 | 143, 144,
145 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
147 | 51, 146 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
148 | 147 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
149 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
150 | 149 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
151 | 142, 148,
150 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝐴, 𝐶, 0)) |
152 | 139, 151 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ (𝐻‘𝑥)) |
153 | 73, 75, 80, 117, 152 | xrletrd 11869 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥)) |
154 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈
ℝ*) |
155 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℝ) |
156 | 155 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈
ℝ*) |
157 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℝ*) |
158 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℝ) |
159 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
160 | 138 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
161 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) |
162 | 161 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) |
163 | 160, 162 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ 0) |
164 | 158, 159,
155, 163 | leadd1dd 10520 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (0 + (𝑔‘𝑥))) |
165 | 155 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℂ) |
166 | 165 | addid2d 10116 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (0 + (𝑔‘𝑥)) = (𝑔‘𝑥)) |
167 | 164, 166 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝑔‘𝑥)) |
168 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
169 | 147 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
170 | 4 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑈 = (𝐴 ∪ 𝐵)) |
171 | 170 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (𝐴 ∪ 𝐵))) |
172 | | biorf 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) |
173 | | elun 3715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
174 | 172, 173 | syl6rbbr 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
175 | 174 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
176 | 171, 175 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ 𝐵)) |
177 | 176 | ifbid 4058 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = if(𝑥 ∈ 𝐵, 𝐶, 0)) |
178 | 169, 177 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝐵, 𝐶, 0)) |
179 | 168, 178 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ (𝐻‘𝑥)) |
180 | 154, 156,
157, 167, 179 | xrletrd 11869 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥)) |
181 | 153, 180 | pm2.61dan 828 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥)) |
182 | 66, 181 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥)) |
183 | 182 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥))) |
184 | 50, 183 | ralrimi 2940 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ∀𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥)) |
185 | | nfv 1830 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦((𝑓 ∘𝑓 +
𝑔)‘𝑥) ≤ (𝐻‘𝑥) |
186 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝑓 ∘𝑓 + 𝑔)‘𝑦) |
187 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥
≤ |
188 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
189 | 8, 188 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝐻 |
190 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝑦 |
191 | 189, 190 | nffv 6110 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝐻‘𝑦) |
192 | 186, 187,
191 | nfbr 4629 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥((𝑓 ∘𝑓 +
𝑔)‘𝑦) ≤ (𝐻‘𝑦) |
193 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) = ((𝑓 ∘𝑓 + 𝑔)‘𝑦)) |
194 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
195 | 193, 194 | breq12d 4596 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥) ↔ ((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦))) |
196 | 185, 192,
195 | cbvral 3143 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
(ℝ ∖ (𝐴 ∩
𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥) ↔ ∀𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)) |
197 | 184, 196 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ∀𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)) |
198 | 197 | r19.21bi 2916 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)) |
199 | 27, 28, 33, 34, 198 | itg2uba 23316 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘(𝑓 ∘𝑓 +
𝑔)) ≤
(∫2‘𝐻)) |
200 | 26, 199 | eqbrtrrd 4607 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ((∫1‘𝑓) +
(∫1‘𝑔)) ≤ (∫2‘𝐻)) |
201 | 23 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘𝑓) ∈
ℝ) |
202 | | itg1cl 23258 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘𝑔) ∈ ℝ) |
203 | 25, 202 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘𝑔) ∈
ℝ) |
204 | 20 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫2‘𝐻) ∈
ℝ) |
205 | 201, 203,
204 | leaddsub2d 10508 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (((∫1‘𝑓) +
(∫1‘𝑔)) ≤ (∫2‘𝐻) ↔
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓)))) |
206 | 200, 205 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘𝑔) ≤
((∫2‘𝐻) − (∫1‘𝑓))) |
207 | 206 | anassrs 678 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺)) → (∫1‘𝑔) ≤
((∫2‘𝐻) − (∫1‘𝑓))) |
208 | 207 | expr 641 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) ∧ 𝑔 ∈ dom ∫1)
→ (𝑔
∘𝑟 ≤ 𝐺 → (∫1‘𝑔) ≤
((∫2‘𝐻) − (∫1‘𝑓)))) |
209 | 208 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
∀𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ 𝐺 → (∫1‘𝑔) ≤
((∫2‘𝐻) − (∫1‘𝑓)))) |
210 | 93, 7 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞)) |
211 | 210 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) → 𝐺:ℝ⟶(0[,]+∞)) |
212 | 21, 23 | resubcld 10337 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
((∫2‘𝐻) − (∫1‘𝑓)) ∈
ℝ) |
213 | 212 | rexrd 9968 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
((∫2‘𝐻) − (∫1‘𝑓)) ∈
ℝ*) |
214 | | itg2leub 23307 |
. . . . . . . . 9
⊢ ((𝐺:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐻) − (∫1‘𝑓)) ∈ ℝ*)
→ ((∫2‘𝐺) ≤ ((∫2‘𝐻) −
(∫1‘𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟
≤ 𝐺 →
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓))))) |
215 | 211, 213,
214 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
((∫2‘𝐺) ≤ ((∫2‘𝐻) −
(∫1‘𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟
≤ 𝐺 →
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓))))) |
216 | 209, 215 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫2‘𝐺)
≤ ((∫2‘𝐻) − (∫1‘𝑓))) |
217 | 12, 21, 23, 216 | lesubd 10510 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺))) |
218 | 217 | expr 641 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺)))) |
219 | 218 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺)))) |
220 | 128, 6 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
221 | 20, 10 | resubcld 10337 |
. . . . . 6
⊢ (𝜑 →
((∫2‘𝐻) − (∫2‘𝐺)) ∈
ℝ) |
222 | 221 | rexrd 9968 |
. . . . 5
⊢ (𝜑 →
((∫2‘𝐻) − (∫2‘𝐺)) ∈
ℝ*) |
223 | | itg2leub 23307 |
. . . . 5
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐻) − (∫2‘𝐺)) ∈ ℝ*)
→ ((∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺))))) |
224 | 220, 222,
223 | syl2anc 691 |
. . . 4
⊢ (𝜑 →
((∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺))))) |
225 | 219, 224 | mpbird 246 |
. . 3
⊢ (𝜑 →
(∫2‘𝐹)
≤ ((∫2‘𝐻) − (∫2‘𝐺))) |
226 | | leaddsub 10383 |
. . . 4
⊢
(((∫2‘𝐹) ∈ ℝ ∧
(∫2‘𝐺)
∈ ℝ ∧ (∫2‘𝐻) ∈ ℝ) →
(((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)
↔ (∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)))) |
227 | 9, 10, 20, 226 | syl3anc 1318 |
. . 3
⊢ (𝜑 →
(((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)
↔ (∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)))) |
228 | 225, 227 | mpbird 246 |
. 2
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)) |
229 | | itg2cl 23305 |
. . . 4
⊢ (𝐻:ℝ⟶(0[,]+∞)
→ (∫2‘𝐻) ∈
ℝ*) |
230 | 17, 229 | syl 17 |
. . 3
⊢ (𝜑 →
(∫2‘𝐻)
∈ ℝ*) |
231 | 18 | rexrd 9968 |
. . 3
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ*) |
232 | | xrletri3 11861 |
. . 3
⊢
(((∫2‘𝐻) ∈ ℝ* ∧
((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ*)
→ ((∫2‘𝐻) = ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ ((∫2‘𝐻) ≤
((∫2‘𝐹) + (∫2‘𝐺)) ∧
((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)))) |
233 | 230, 231,
232 | syl2anc 691 |
. 2
⊢ (𝜑 →
((∫2‘𝐻) = ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ ((∫2‘𝐻) ≤
((∫2‘𝐹) + (∫2‘𝐺)) ∧
((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)))) |
234 | 11, 228, 233 | mpbir2and 959 |
1
⊢ (𝜑 →
(∫2‘𝐻)
= ((∫2‘𝐹) + (∫2‘𝐺))) |