| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | itg2split.c | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) | 
| 2 | 1 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞)) | 
| 3 |  | 0e0iccpnf 13500 | . . . . . 6
⊢ 0 ∈
(0[,]+∞) | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝑈) → 0 ∈
(0[,]+∞)) | 
| 5 | 2, 4 | ifclda 4560 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) | 
| 6 |  | itg2split.h | . . . 4
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) | 
| 7 | 5, 6 | fmptd 7133 | . . 3
⊢ (𝜑 → 𝐻:ℝ⟶(0[,]+∞)) | 
| 8 |  | itg2cl 25768 | . . 3
⊢ (𝐻:ℝ⟶(0[,]+∞)
→ (∫2‘𝐻) ∈
ℝ*) | 
| 9 | 7, 8 | syl 17 | . 2
⊢ (𝜑 →
(∫2‘𝐻)
∈ ℝ*) | 
| 10 |  | itg2split.sf | . . . 4
⊢ (𝜑 →
(∫2‘𝐹)
∈ ℝ) | 
| 11 |  | itg2split.sg | . . . 4
⊢ (𝜑 →
(∫2‘𝐺)
∈ ℝ) | 
| 12 | 10, 11 | readdcld 11291 | . . 3
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ) | 
| 13 | 12 | rexrd 11312 | . 2
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ∈
ℝ*) | 
| 14 |  | itg2split.a | . . 3
⊢ (𝜑 → 𝐴 ∈ dom vol) | 
| 15 |  | itg2split.b | . . 3
⊢ (𝜑 → 𝐵 ∈ dom vol) | 
| 16 |  | itg2split.i | . . 3
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0) | 
| 17 |  | itg2split.u | . . 3
⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵)) | 
| 18 |  | itg2split.f | . . 3
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) | 
| 19 |  | itg2split.g | . . 3
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)) | 
| 20 | 14, 15, 16, 17, 1, 18, 19, 6, 10, 11 | itg2splitlem 25784 | . 2
⊢ (𝜑 →
(∫2‘𝐻)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) | 
| 21 | 11 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) →
(∫2‘𝐺)
∈ ℝ) | 
| 22 |  | itg2lecl 25774 | . . . . . . . . 9
⊢ ((𝐻:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐹) + (∫2‘𝐺)) ∈ ℝ ∧
(∫2‘𝐻)
≤ ((∫2‘𝐹) + (∫2‘𝐺))) →
(∫2‘𝐻)
∈ ℝ) | 
| 23 | 7, 12, 20, 22 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 →
(∫2‘𝐻)
∈ ℝ) | 
| 24 | 23 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) →
(∫2‘𝐻)
∈ ℝ) | 
| 25 |  | itg1cl 25721 | . . . . . . . 8
⊢ (𝑓 ∈ dom ∫1
→ (∫1‘𝑓) ∈ ℝ) | 
| 26 | 25 | ad2antrl 728 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) →
(∫1‘𝑓)
∈ ℝ) | 
| 27 |  | simprll 778 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → 𝑓 ∈ dom
∫1) | 
| 28 |  | simprrl 780 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → 𝑔 ∈ dom
∫1) | 
| 29 | 27, 28 | itg1add 25737 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) →
(∫1‘(𝑓
∘f + 𝑔)) =
((∫1‘𝑓) + (∫1‘𝑔))) | 
| 30 | 7 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → 𝐻:ℝ⟶(0[,]+∞)) | 
| 31 | 27, 28 | i1fadd 25731 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → (𝑓 ∘f + 𝑔) ∈ dom
∫1) | 
| 32 |  | inss1 4236 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | 
| 33 |  | mblss 25567 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) | 
| 34 | 14, 33 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 35 | 32, 34 | sstrid 3994 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ ℝ) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → (𝐴 ∩ 𝐵) ⊆ ℝ) | 
| 37 | 16 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → (vol*‘(𝐴 ∩ 𝐵)) = 0) | 
| 38 |  | nfv 1913 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥𝜑 | 
| 39 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑓 ∈ dom
∫1 | 
| 40 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝑓 | 
| 41 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥
∘r ≤ | 
| 42 |  | nfmpt1 5249 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0)) | 
| 43 | 18, 42 | nfcxfr 2902 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝐹 | 
| 44 | 40, 41, 43 | nfbr 5189 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑓 ∘r ≤ 𝐹 | 
| 45 | 39, 44 | nfan 1898 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑓 ∈ dom ∫1
∧ 𝑓 ∘r
≤ 𝐹) | 
| 46 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑔 ∈ dom
∫1 | 
| 47 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝑔 | 
| 48 |  | nfmpt1 5249 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0)) | 
| 49 | 19, 48 | nfcxfr 2902 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝐺 | 
| 50 | 47, 41, 49 | nfbr 5189 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑔 ∘r ≤ 𝐺 | 
| 51 | 46, 50 | nfan 1898 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑔 ∈ dom ∫1
∧ 𝑔 ∘r
≤ 𝐺) | 
| 52 | 45, 51 | nfan 1898 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝑓 ∈ dom ∫1
∧ 𝑓 ∘r
≤ 𝐹) ∧ (𝑔 ∈ dom ∫1
∧ 𝑔 ∘r
≤ 𝐺)) | 
| 53 | 38, 52 | nfan 1898 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) | 
| 54 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → 𝑥 ∈ ℝ) | 
| 55 |  | i1ff 25712 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) | 
| 56 | 27, 55 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → 𝑓:ℝ⟶ℝ) | 
| 57 | 56 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → 𝑓 Fn ℝ) | 
| 58 |  | i1ff 25712 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) | 
| 59 | 28, 58 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → 𝑔:ℝ⟶ℝ) | 
| 60 | 59 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → 𝑔 Fn ℝ) | 
| 61 |  | reex 11247 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ℝ
∈ V | 
| 62 | 61 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → ℝ ∈
V) | 
| 63 |  | inidm 4226 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (ℝ
∩ ℝ) = ℝ | 
| 64 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) = (𝑓‘𝑥)) | 
| 65 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) = (𝑔‘𝑥)) | 
| 66 | 57, 60, 62, 62, 63, 64, 65 | ofval 7709 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → ((𝑓 ∘f + 𝑔)‘𝑥) = ((𝑓‘𝑥) + (𝑔‘𝑥))) | 
| 67 | 54, 66 | sylan2 593 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘f + 𝑔)‘𝑥) = ((𝑓‘𝑥) + (𝑔‘𝑥))) | 
| 68 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓:ℝ⟶ℝ ∧
𝑥 ∈ ℝ) →
(𝑓‘𝑥) ∈ ℝ) | 
| 69 | 56, 54, 68 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑥) ∈ ℝ) | 
| 70 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:ℝ⟶ℝ ∧
𝑥 ∈ ℝ) →
(𝑔‘𝑥) ∈ ℝ) | 
| 71 | 59, 54, 70 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑔‘𝑥) ∈ ℝ) | 
| 72 | 69, 71 | readdcld 11291 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈ ℝ) | 
| 73 | 72 | rexrd 11312 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈
ℝ*) | 
| 74 | 73 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈
ℝ*) | 
| 75 | 69 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℝ) | 
| 76 | 75 | rexrd 11312 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈
ℝ*) | 
| 77 |  | iccssxr 13471 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0[,]+∞) ⊆ ℝ* | 
| 78 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐻:ℝ⟶(0[,]+∞)
∧ 𝑥 ∈ ℝ)
→ (𝐻‘𝑥) ∈
(0[,]+∞)) | 
| 79 | 30, 54, 78 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) ∈ (0[,]+∞)) | 
| 80 | 77, 79 | sselid 3980 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) ∈
ℝ*) | 
| 81 | 80 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℝ*) | 
| 82 | 71 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℝ) | 
| 83 |  | 0red 11265 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) | 
| 84 |  | simprrr 781 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → 𝑔 ∘r ≤ 𝐺) | 
| 85 | 61 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → ℝ ∈
V) | 
| 86 |  | fvexd 6920 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ∈ V) | 
| 87 |  | ssun2 4178 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) | 
| 88 | 87, 17 | sseqtrrid 4026 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → 𝐵 ⊆ 𝑈) | 
| 89 | 88 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) | 
| 90 | 89 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈) | 
| 91 | 90, 2 | syldan 591 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) | 
| 92 | 3 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → 0 ∈
(0[,]+∞)) | 
| 93 | 91, 92 | ifclda 4560 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞)) | 
| 94 | 93 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑔 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, 𝐶, 0) ∈ (0[,]+∞)) | 
| 95 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝑔 Fn ℝ) | 
| 96 |  | dffn5 6966 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑔 Fn ℝ ↔ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔‘𝑥))) | 
| 97 | 95, 96 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔‘𝑥))) | 
| 98 | 19 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0))) | 
| 99 | 85, 86, 94, 97, 98 | ofrfval2 7719 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑔 Fn ℝ) → (𝑔 ∘r ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) | 
| 100 | 60, 99 | syldan 591 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → (𝑔 ∘r ≤ 𝐺 ↔ ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0))) | 
| 101 | 84, 100 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → ∀𝑥 ∈ ℝ (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) | 
| 102 | 101 | r19.21bi 3250 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) | 
| 103 | 54, 102 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) | 
| 104 | 103 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) | 
| 105 |  | eldifn 4131 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) | 
| 106 | 105 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) | 
| 107 |  | elin 3966 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | 
| 108 | 106, 107 | sylnib 328 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | 
| 109 |  | imnan 399 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | 
| 110 | 108, 109 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | 
| 111 | 110 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ 𝐵) | 
| 112 | 111 | iffalsed 4535 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐵, 𝐶, 0) = 0) | 
| 113 | 104, 112 | breqtrd 5168 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ 0) | 
| 114 | 82, 83, 75, 113 | leadd2dd 11879 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ ((𝑓‘𝑥) + 0)) | 
| 115 | 75 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℂ) | 
| 116 | 115 | addridd 11462 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + 0) = (𝑓‘𝑥)) | 
| 117 | 114, 116 | breqtrd 5168 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝑓‘𝑥)) | 
| 118 |  | simprlr 779 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → 𝑓 ∘r ≤ 𝐹) | 
| 119 | 61 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → ℝ ∈
V) | 
| 120 |  | fvexd 6920 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ∈ V) | 
| 121 |  | ssun1 4177 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) | 
| 122 | 121, 17 | sseqtrrid 4026 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐴 ⊆ 𝑈) | 
| 123 | 122 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) | 
| 124 | 123 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) | 
| 125 | 124, 2 | syldan 591 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) | 
| 126 | 3 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) | 
| 127 | 125, 126 | ifclda 4560 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞)) | 
| 128 | 127 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓 Fn ℝ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, 𝐶, 0) ∈ (0[,]+∞)) | 
| 129 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝑓 Fn ℝ) | 
| 130 |  | dffn5 6966 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 Fn ℝ ↔ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥))) | 
| 131 | 129, 130 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥))) | 
| 132 | 18 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))) | 
| 133 | 119, 120,
128, 131, 132 | ofrfval2 7719 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑓 Fn ℝ) → (𝑓 ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) | 
| 134 | 57, 133 | syldan 591 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → (𝑓 ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0))) | 
| 135 | 118, 134 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → ∀𝑥 ∈ ℝ (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) | 
| 136 | 135 | r19.21bi 3250 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) | 
| 137 | 54, 136 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) | 
| 138 | 137 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) | 
| 139 | 122 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → 𝐴 ⊆ 𝑈) | 
| 140 | 139 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈) | 
| 141 | 140 | iftrued 4532 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = 𝐶) | 
| 142 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) | 
| 143 | 5 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) | 
| 144 | 6 | fvmpt2 7026 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ 𝑈, 𝐶, 0) ∈ (0[,]+∞)) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) | 
| 145 | 142, 143,
144 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ ℝ) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) | 
| 146 | 54, 145 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) | 
| 147 | 146 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) | 
| 148 |  | iftrue 4530 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) | 
| 149 | 148 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 𝐶) | 
| 150 | 141, 147,
149 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝐴, 𝐶, 0)) | 
| 151 | 138, 150 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ (𝐻‘𝑥)) | 
| 152 | 74, 76, 81, 117, 151 | xrletrd 13205 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥)) | 
| 153 | 73 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ∈
ℝ*) | 
| 154 | 71 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℝ) | 
| 155 | 154 | rexrd 11312 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈
ℝ*) | 
| 156 | 80 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈
ℝ*) | 
| 157 | 69 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ℝ) | 
| 158 |  | 0red 11265 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) | 
| 159 | 137 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ if(𝑥 ∈ 𝐴, 𝐶, 0)) | 
| 160 |  | iffalse 4533 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) | 
| 161 | 160 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, 𝐶, 0) = 0) | 
| 162 | 159, 161 | breqtrd 5168 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ≤ 0) | 
| 163 | 157, 158,
154, 162 | leadd1dd 11878 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (0 + (𝑔‘𝑥))) | 
| 164 | 154 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ℂ) | 
| 165 | 164 | addlidd 11463 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (0 + (𝑔‘𝑥)) = (𝑔‘𝑥)) | 
| 166 | 163, 165 | breqtrd 5168 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝑔‘𝑥)) | 
| 167 | 103 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ if(𝑥 ∈ 𝐵, 𝐶, 0)) | 
| 168 | 146 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝑈, 𝐶, 0)) | 
| 169 | 17 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑈 = (𝐴 ∪ 𝐵)) | 
| 170 | 169 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (𝐴 ∪ 𝐵))) | 
| 171 |  | elun 4152 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | 
| 172 |  | biorf 936 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))) | 
| 173 | 171, 172 | bitr4id 290 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) | 
| 174 | 173 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵)) | 
| 175 | 170, 174 | bitrd 279 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ 𝐵)) | 
| 176 | 175 | ifbid 4548 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑈, 𝐶, 0) = if(𝑥 ∈ 𝐵, 𝐶, 0)) | 
| 177 | 168, 176 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = if(𝑥 ∈ 𝐵, 𝐶, 0)) | 
| 178 | 167, 177 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ≤ (𝐻‘𝑥)) | 
| 179 | 153, 155,
156, 166, 178 | xrletrd 13205 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥)) | 
| 180 | 152, 179 | pm2.61dan 812 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓‘𝑥) + (𝑔‘𝑥)) ≤ (𝐻‘𝑥)) | 
| 181 | 67, 180 | eqbrtrd 5164 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘f + 𝑔)‘𝑥) ≤ (𝐻‘𝑥)) | 
| 182 | 181 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → (𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵)) → ((𝑓 ∘f + 𝑔)‘𝑥) ≤ (𝐻‘𝑥))) | 
| 183 | 53, 182 | ralrimi 3256 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → ∀𝑥 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘f + 𝑔)‘𝑥) ≤ (𝐻‘𝑥)) | 
| 184 |  | nfv 1913 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦((𝑓 ∘f + 𝑔)‘𝑥) ≤ (𝐻‘𝑥) | 
| 185 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝑓 ∘f + 𝑔)‘𝑦) | 
| 186 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥
≤ | 
| 187 |  | nfmpt1 5249 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0)) | 
| 188 | 6, 187 | nfcxfr 2902 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝐻 | 
| 189 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝑦 | 
| 190 | 188, 189 | nffv 6915 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝐻‘𝑦) | 
| 191 | 185, 186,
190 | nfbr 5189 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥((𝑓 ∘f + 𝑔)‘𝑦) ≤ (𝐻‘𝑦) | 
| 192 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝑓 ∘f + 𝑔)‘𝑥) = ((𝑓 ∘f + 𝑔)‘𝑦)) | 
| 193 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) | 
| 194 | 192, 193 | breq12d 5155 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (((𝑓 ∘f + 𝑔)‘𝑥) ≤ (𝐻‘𝑥) ↔ ((𝑓 ∘f + 𝑔)‘𝑦) ≤ (𝐻‘𝑦))) | 
| 195 | 184, 191,
194 | cbvralw 3305 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
(ℝ ∖ (𝐴 ∩
𝐵))((𝑓 ∘f + 𝑔)‘𝑥) ≤ (𝐻‘𝑥) ↔ ∀𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘f + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)) | 
| 196 | 183, 195 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) → ∀𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))((𝑓 ∘f + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)) | 
| 197 | 196 | r19.21bi 3250 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) ∧ 𝑦 ∈ (ℝ ∖ (𝐴 ∩ 𝐵))) → ((𝑓 ∘f + 𝑔)‘𝑦) ≤ (𝐻‘𝑦)) | 
| 198 | 30, 31, 36, 37, 197 | itg2uba 25779 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) →
(∫1‘(𝑓
∘f + 𝑔))
≤ (∫2‘𝐻)) | 
| 199 | 29, 198 | eqbrtrrd 5166 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) →
((∫1‘𝑓) + (∫1‘𝑔)) ≤
(∫2‘𝐻)) | 
| 200 | 26 | adantrr 717 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) →
(∫1‘𝑓)
∈ ℝ) | 
| 201 |  | itg1cl 25721 | . . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘𝑔) ∈ ℝ) | 
| 202 | 28, 201 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) →
(∫1‘𝑔)
∈ ℝ) | 
| 203 | 23 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) →
(∫2‘𝐻)
∈ ℝ) | 
| 204 | 200, 202,
203 | leaddsub2d 11866 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) →
(((∫1‘𝑓) + (∫1‘𝑔)) ≤
(∫2‘𝐻)
↔ (∫1‘𝑔) ≤ ((∫2‘𝐻) −
(∫1‘𝑓)))) | 
| 205 | 199, 204 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺))) →
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓))) | 
| 206 | 205 | anassrs 467 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐺)) →
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓))) | 
| 207 | 206 | expr 456 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) ∧ 𝑔 ∈ dom ∫1) → (𝑔 ∘r ≤ 𝐺 →
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓)))) | 
| 208 | 207 | ralrimiva 3145 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) → ∀𝑔 ∈ dom
∫1(𝑔
∘r ≤ 𝐺
→ (∫1‘𝑔) ≤ ((∫2‘𝐻) −
(∫1‘𝑓)))) | 
| 209 | 93, 19 | fmptd 7133 | . . . . . . . . . 10
⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞)) | 
| 210 | 209 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) → 𝐺:ℝ⟶(0[,]+∞)) | 
| 211 | 24, 26 | resubcld 11692 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) →
((∫2‘𝐻) − (∫1‘𝑓)) ∈
ℝ) | 
| 212 | 211 | rexrd 11312 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) →
((∫2‘𝐻) − (∫1‘𝑓)) ∈
ℝ*) | 
| 213 |  | itg2leub 25770 | . . . . . . . . 9
⊢ ((𝐺:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐻) − (∫1‘𝑓)) ∈ ℝ*)
→ ((∫2‘𝐺) ≤ ((∫2‘𝐻) −
(∫1‘𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐺 →
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓))))) | 
| 214 | 210, 212,
213 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) →
((∫2‘𝐺) ≤ ((∫2‘𝐻) −
(∫1‘𝑓)) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐺 →
(∫1‘𝑔)
≤ ((∫2‘𝐻) − (∫1‘𝑓))))) | 
| 215 | 208, 214 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) →
(∫2‘𝐺)
≤ ((∫2‘𝐻) − (∫1‘𝑓))) | 
| 216 | 21, 24, 26, 215 | lesubd 11868 | . . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹)) →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺))) | 
| 217 | 216 | expr 456 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑓 ∘r ≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺)))) | 
| 218 | 217 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺)))) | 
| 219 | 127, 18 | fmptd 7133 | . . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞)) | 
| 220 | 23, 11 | resubcld 11692 | . . . . . 6
⊢ (𝜑 →
((∫2‘𝐻) − (∫2‘𝐺)) ∈
ℝ) | 
| 221 | 220 | rexrd 11312 | . . . . 5
⊢ (𝜑 →
((∫2‘𝐻) − (∫2‘𝐺)) ∈
ℝ*) | 
| 222 |  | itg2leub 25770 | . . . . 5
⊢ ((𝐹:ℝ⟶(0[,]+∞)
∧ ((∫2‘𝐻) − (∫2‘𝐺)) ∈ ℝ*)
→ ((∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺))))) | 
| 223 | 219, 221,
222 | syl2anc 584 | . . . 4
⊢ (𝜑 →
((∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)) ↔ ∀𝑓 ∈ dom ∫1(𝑓 ∘r ≤ 𝐹 →
(∫1‘𝑓)
≤ ((∫2‘𝐻) − (∫2‘𝐺))))) | 
| 224 | 218, 223 | mpbird 257 | . . 3
⊢ (𝜑 →
(∫2‘𝐹)
≤ ((∫2‘𝐻) − (∫2‘𝐺))) | 
| 225 |  | leaddsub 11740 | . . . 4
⊢
(((∫2‘𝐹) ∈ ℝ ∧
(∫2‘𝐺)
∈ ℝ ∧ (∫2‘𝐻) ∈ ℝ) →
(((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)
↔ (∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)))) | 
| 226 | 10, 11, 23, 225 | syl3anc 1372 | . . 3
⊢ (𝜑 →
(((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)
↔ (∫2‘𝐹) ≤ ((∫2‘𝐻) −
(∫2‘𝐺)))) | 
| 227 | 224, 226 | mpbird 257 | . 2
⊢ (𝜑 →
((∫2‘𝐹) + (∫2‘𝐺)) ≤
(∫2‘𝐻)) | 
| 228 | 9, 13, 20, 227 | xrletrid 13198 | 1
⊢ (𝜑 →
(∫2‘𝐻)
= ((∫2‘𝐹) + (∫2‘𝐺))) |