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 23515 |
. 2
⊢ (𝜑 →
(∫2‘𝐻)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) |
12 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫2‘𝐺)
∈ ℝ) |
13 | 5 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) |
14 | | 0e0iccpnf 12283 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]+∞) |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑈) → 0 ∈
(0[,]+∞)) |
16 | 13, 15 | ifclda 4120 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) |
17 | 16, 8 | fmptd 6385 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻:ℝ⟶(0[,]+∞)) |
18 | 9, 10 | readdcld 10069 |
. . . . . . . . 9
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ) |
19 | | itg2lecl 23505 |
. . . . . . . . 9
⊢ ((𝐻:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ ∧
(∫2‘𝐻)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) →
(∫2‘𝐻)
∈ ℝ) |
20 | 17, 18, 11, 19 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 →
(∫2‘𝐻)
∈ ℝ) |
21 | 20 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫2‘𝐻)
∈ ℝ) |
22 | | itg1cl 23452 |
. . . . . . . 8
⊢ (𝑓 ∈ dom ∫1
→ (∫1‘𝑓) ∈ ℝ) |
23 | 22 | ad2antrl 764 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫1‘𝑓)
∈ ℝ) |
24 | | simprll 802 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑓 ∈ dom
∫1) |
25 | | simprrl 804 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑔 ∈ dom
∫1) |
26 | 24, 25 | itg1add 23468 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘(𝑓 ∘𝑓 +
𝑔)) =
((∫1‘𝑓) + (∫1‘𝑔))) |
27 | 17 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝐻:ℝ⟶(0[,]+∞)) |
28 | 24, 25 | i1fadd 23462 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝑓 ∘𝑓 + 𝑔) ∈ dom
∫1) |
29 | | inss1 3833 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
30 | | mblss 23299 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
31 | 1, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
32 | 29, 31 | syl5ss 3614 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ ℝ) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝐴 ∩ 𝐵) ⊆ ℝ) |
34 | 3 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (vol*‘(𝐴 ∩ 𝐵)) = 0) |
35 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥𝜑 |
36 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑓 ∈ dom
∫1 |
37 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝑓 |
38 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥
∘𝑟 ≤ |
39 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
40 | 6, 39 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝐹 |
41 | 37, 38, 40 | nfbr 4699 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑓 ∘𝑟
≤ 𝐹 |
42 | 36, 41 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐹) |
43 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑔 ∈ dom
∫1 |
44 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝑔 |
45 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
46 | 7, 45 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝐺 |
47 | 44, 38, 46 | nfbr 4699 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑔 ∘𝑟
≤ 𝐺 |
48 | 43, 47 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺) |
49 | 42, 48 | nfan 1828 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝑓 ∈ dom ∫1
∧ 𝑓
∘𝑟 ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘𝑟
≤ 𝐺)) |
50 | 35, 49 | nfan 1828 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) |
51 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → 𝑥 ∈ ℝ) |
52 | | i1ff 23443 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
53 | 24, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑓:ℝ⟶ℝ) |
54 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:ℝ⟶ℝ →
𝑓 Fn
ℝ) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑓 Fn ℝ) |
56 | | i1ff 23443 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
57 | 25, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑔:ℝ⟶ℝ) |
58 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔:ℝ⟶ℝ →
𝑔 Fn
ℝ) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑔 Fn ℝ) |
60 | | reex 10027 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℝ
∈ V |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ℝ ∈
V) |
62 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℝ
∩ ℝ) = ℝ |
63 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) = (𝑓‘𝑥)) |
64 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) = (𝑔‘𝑥)) |
65 | 55, 59, 61, 61, 62, 63, 64 | ofval 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) = ((𝑓‘𝑥) + (𝑔‘𝑥))) |
66 | 51, 65 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) = ((𝑓‘𝑥) + (𝑔‘𝑥))) |
67 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓:ℝ⟶ℝ ∧
𝑥 ∈ ℝ) →
(𝑓‘𝑥) ∈ ℝ) |
68 | 53, 51, 67 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑥) ∈ ℝ) |
69 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:ℝ⟶ℝ ∧
𝑥 ∈ ℝ) →
(𝑔‘𝑥) ∈ ℝ) |
70 | 57, 51, 69 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑔‘𝑥) ∈ ℝ) |
71 | 68, 70 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈ ℝ) |
72 | 71 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈
ℝ*) |
73 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈
ℝ*) |
74 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℝ) |
75 | 74 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈
ℝ*) |
76 | | iccssxr 12256 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0[,]+∞) ⊆ ℝ* |
77 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐻:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (𝐻‘𝑥) ∈
(0[,]+∞)) |
78 | 27, 51, 77 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) ∈ (0[,]+∞)) |
79 | 76, 78 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) ∈
ℝ*) |
80 | 79 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℝ*) |
81 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℝ) |
82 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
83 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑔 ∘𝑟 ≤ 𝐺) |
84 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → ℝ ∈
V) |
85 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ V) |
86 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
87 | 86, 4 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
88 | 87 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
89 | 88 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) |
90 | 89, 13 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
91 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → 0 ∈
(0[,]+∞)) |
92 | 90, 91 | ifclda 4120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞)) |
93 | 92 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞)) |
94 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝑔 Fn ℝ) |
95 | | dffn5 6241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑔 Fn ℝ ↔ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔‘𝑥))) |
96 | 94, 95 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔‘𝑥))) |
97 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
98 | 84, 85, 93, 96, 97 | ofrfval2 6915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → (𝑔 ∘𝑟 ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
99 | 59, 98 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝑔 ∘𝑟 ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) |
100 | 83, 99 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
101 | 100 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
102 | 51, 101 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
103 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
104 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) |
105 | 104 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) |
106 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
107 | 105, 106 | sylnib 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
108 | | imnan 438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
109 | 107, 108 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
110 | 109 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ 𝐵) |
111 | 110 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐵, 𝐶, 0) = 0) |
112 | 103, 111 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ 0) |
113 | 81, 82, 74, 112 | leadd2dd 10642 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ ((𝑓‘𝑥) + 0)) |
114 | 74 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℂ) |
115 | 114 | addid1d 10236 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + 0) = (𝑓‘𝑥)) |
116 | 113, 115 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝑓‘𝑥)) |
117 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → 𝑓 ∘𝑟 ≤ 𝐹) |
118 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → ℝ ∈
V) |
119 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ∈ V) |
120 | | ssun1 3776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
121 | 120, 4 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
122 | 121 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
123 | 122 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
124 | 123, 13 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) |
125 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
126 | 124, 125 | ifclda 4120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞)) |
127 | 126 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞)) |
128 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝑓 Fn ℝ) |
129 | | dffn5 6241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 Fn ℝ ↔ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥))) |
130 | 128, 129 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥))) |
131 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
132 | 118, 119,
127, 130, 131 | ofrfval2 6915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → (𝑓 ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
133 | 55, 132 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝑓 ∘𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) |
134 | 117, 133 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
135 | 134 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
136 | 51, 135 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
137 | 136 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
138 | 121 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → 𝐴 ⊆ 𝑈) |
139 | 138 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) |
140 | 139 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = 𝐶) |
141 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
142 | 16 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) |
143 | 8 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
144 | 141, 142,
143 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
145 | 51, 144 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
146 | 145 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
147 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
148 | 147 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) |
149 | 140, 146,
148 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝐴, 𝐶, 0)) |
150 | 137, 149 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ (𝐻‘𝑥)) |
151 | 73, 75, 80, 116, 150 | xrletrd 11993 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥)) |
152 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈
ℝ*) |
153 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℝ) |
154 | 153 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈
ℝ*) |
155 | 79 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℝ*) |
156 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℝ) |
157 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
158 | 136 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) |
159 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) |
160 | 159 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) |
161 | 158, 160 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ 0) |
162 | 156, 157,
153, 161 | leadd1dd 10641 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (0 + (𝑔‘𝑥))) |
163 | 153 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℂ) |
164 | 163 | addid2d 10237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (0 + (𝑔‘𝑥)) = (𝑔‘𝑥)) |
165 | 162, 164 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝑔‘𝑥)) |
166 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) |
167 | 145 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) |
168 | 4 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑈 = (𝐴 ∪ 𝐵)) |
169 | 168 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (𝐴 ∪ 𝐵))) |
170 | | biorf 420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) |
171 | | elun 3753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
172 | 170, 171 | syl6rbbr 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
173 | 172 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) |
174 | 169, 173 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ 𝐵)) |
175 | 174 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = if(𝑥 ∈ 𝐵, 𝐶, 0)) |
176 | 167, 175 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝐵, 𝐶, 0)) |
177 | 166, 176 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ (𝐻‘𝑥)) |
178 | 152, 154,
155, 165, 177 | xrletrd 11993 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥)) |
179 | 151, 178 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥)) |
180 | 66, 179 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥)) |
181 | 180 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥))) |
182 | 50, 181 | ralrimi 2957 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ∀𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥)) |
183 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦((𝑓 ∘𝑓 +
𝑔)‘𝑥) ≤ (𝐻‘𝑥) |
184 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝑓 ∘𝑓 + 𝑔)‘𝑦) |
185 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥
≤ |
186 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) |
187 | 8, 186 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝐻 |
188 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝑦 |
189 | 187, 188 | nffv 6198 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝐻‘𝑦) |
190 | 184, 185,
189 | nfbr 4699 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥((𝑓 ∘𝑓 +
𝑔)‘𝑦) ≤ (𝐻‘𝑦) |
191 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝑓 ∘𝑓 + 𝑔)‘𝑥) = ((𝑓 ∘𝑓 + 𝑔)‘𝑦)) |
192 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
193 | 191, 192 | breq12d 4666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥) ↔ ((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦))) |
194 | 183, 190,
193 | cbvral 3167 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
(ℝ ∖ (𝐴 ∩
𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑥) ≤ (𝐻‘𝑥) ↔ ∀𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)) |
195 | 182, 194 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ∀𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)) |
196 | 195 | r19.21bi 2932 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘𝑓 + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)) |
197 | 27, 28, 33, 34, 196 | itg2uba 23510 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘(𝑓 ∘𝑓 +
𝑔)) ≤
(∫2‘𝐻)) |
198 | 26, 197 | eqbrtrrd 4677 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → ((∫1‘𝑓) +
(∫1‘𝑔)) ≤ (∫2‘𝐻)) |
199 | 23 | adantrr 753 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘𝑓) ∈
ℝ) |
200 | | itg1cl 23452 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘𝑔) ∈ ℝ) |
201 | 25, 200 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘𝑔) ∈
ℝ) |
202 | 20 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫2‘𝐻) ∈
ℝ) |
203 | 199, 201,
202 | leaddsub2d 10629 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (((∫1‘𝑓) +
(∫1‘𝑔)) ≤ (∫2‘𝐻) ↔
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓)))) |
204 | 198, 203 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺))) → (∫1‘𝑔) ≤
((∫2‘𝐻) − (∫1‘𝑓))) |
205 | 204 | anassrs 680 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ 𝐺)) → (∫1‘𝑔) ≤
((∫2‘𝐻) − (∫1‘𝑓))) |
206 | 205 | expr 643 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) ∧ 𝑔 ∈ dom ∫1)
→ (𝑔
∘𝑟 ≤ 𝐺 → (∫1‘𝑔) ≤
((∫2‘𝐻) − (∫1‘𝑓)))) |
207 | 206 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
∀𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ 𝐺 → (∫1‘𝑔) ≤
((∫2‘𝐻) − (∫1‘𝑓)))) |
208 | 92, 7 | fmptd 6385 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞)) |
209 | 208 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) → 𝐺:ℝ⟶(0[,]+∞)) |
210 | 21, 23 | resubcld 10458 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
((∫2‘𝐻) − (∫1‘𝑓)) ∈
ℝ) |
211 | 210 | rexrd 10089 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
((∫2‘𝐻) − (∫1‘𝑓)) ∈
ℝ*) |
212 | | itg2leub 23501 |
. . . . . . . . 9
⊢ ((𝐺:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐻) − (∫1‘𝑓)) ∈ ℝ*)
→ ((∫2‘𝐺) ≤ ((∫2‘𝐻) −
(∫1‘𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟
≤ 𝐺 →
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓))))) |
213 | 209, 211,
212 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
((∫2‘𝐺) ≤ ((∫2‘𝐻) −
(∫1‘𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟
≤ 𝐺 →
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓))))) |
214 | 207, 213 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫2‘𝐺)
≤ ((∫2‘𝐻) − (∫1‘𝑓))) |
215 | 12, 21, 23, 214 | lesubd 10631 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘𝑟
≤ 𝐹)) →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺))) |
216 | 215 | expr 643 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺)))) |
217 | 216 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺)))) |
218 | 126, 6 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) |
219 | 20, 10 | resubcld 10458 |
. . . . . 6
⊢ (𝜑 →
((∫2‘𝐻) − (∫2‘𝐺)) ∈
ℝ) |
220 | 219 | rexrd 10089 |
. . . . 5
⊢ (𝜑 →
((∫2‘𝐻) − (∫2‘𝐺)) ∈
ℝ*) |
221 | | itg2leub 23501 |
. . . . 5
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐻) − (∫2‘𝐺)) ∈ ℝ*)
→ ((∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺))))) |
222 | 218, 220,
221 | syl2anc 693 |
. . . 4
⊢ (𝜑 →
((∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘𝑟
≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺))))) |
223 | 217, 222 | mpbird 247 |
. . 3
⊢ (𝜑 →
(∫2‘𝐹)
≤ ((∫2‘𝐻) − (∫2‘𝐺))) |
224 | | leaddsub 10504 |
. . . 4
⊢
(((∫2‘𝐹) ∈ ℝ ∧
(∫2‘𝐺)
∈ ℝ ∧ (∫2‘𝐻) ∈ ℝ) →
(((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)
↔ (∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)))) |
225 | 9, 10, 20, 224 | syl3anc 1326 |
. . 3
⊢ (𝜑 →
(((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)
↔ (∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)))) |
226 | 223, 225 | mpbird 247 |
. 2
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)) |
227 | | itg2cl 23499 |
. . . 4
⊢ (𝐻:ℝ⟶(0[,]+∞)
→ (∫2‘𝐻) ∈
ℝ*) |
228 | 17, 227 | syl 17 |
. . 3
⊢ (𝜑 →
(∫2‘𝐻)
∈ ℝ*) |
229 | 18 | rexrd 10089 |
. . 3
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ*) |
230 | | xrletri3 11985 |
. . 3
⊢
(((∫2‘𝐻) ∈ ℝ* ∧
((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ*)
→ ((∫2‘𝐻) = ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ ((∫2‘𝐻) ≤
((∫2‘𝐹) + (∫2‘𝐺)) ∧
((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)))) |
231 | 228, 229,
230 | syl2anc 693 |
. 2
⊢ (𝜑 →
((∫2‘𝐻) = ((∫2‘𝐹) +
(∫2‘𝐺)) ↔ ((∫2‘𝐻) ≤
((∫2‘𝐹) + (∫2‘𝐺)) ∧
((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)))) |
232 | 11, 226, 231 | mpbir2and 957 |
1
⊢ (𝜑 →
(∫2‘𝐻)
= ((∫2‘𝐹) + (∫2‘𝐺))) |