Step |
Hyp |
Ref |
Expression |
1 |
|
itg10a.1 |
⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 ) |
2 |
|
itg10a.2 |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
3 |
|
itg10a.3 |
⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 ) |
4 |
|
itg1lea.4 |
⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 ) |
5 |
|
itg1lea.5 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) |
6 |
|
i1fsub |
⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐹 ∈ dom ∫1 ) → ( 𝐺 ∘f − 𝐹 ) ∈ dom ∫1 ) |
7 |
4 1 6
|
syl2anc |
⊢ ( 𝜑 → ( 𝐺 ∘f − 𝐹 ) ∈ dom ∫1 ) |
8 |
|
eldifi |
⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 𝑥 ∈ ℝ ) |
9 |
|
i1ff |
⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ ) |
10 |
4 9
|
syl |
⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ ) |
11 |
10
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ ) |
12 |
|
i1ff |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ ) |
13 |
1 12
|
syl |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ ) |
14 |
13
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
15 |
11 14
|
subge0d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) |
16 |
8 15
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 0 ≤ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) |
17 |
5 16
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 0 ≤ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) |
18 |
10
|
ffnd |
⊢ ( 𝜑 → 𝐺 Fn ℝ ) |
19 |
13
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn ℝ ) |
20 |
|
reex |
⊢ ℝ ∈ V |
21 |
20
|
a1i |
⊢ ( 𝜑 → ℝ ∈ V ) |
22 |
|
inidm |
⊢ ( ℝ ∩ ℝ ) = ℝ |
23 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
24 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
25 |
18 19 21 21 22 23 24
|
ofval |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ∘f − 𝐹 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) |
26 |
8 25
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( ( 𝐺 ∘f − 𝐹 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) |
27 |
17 26
|
breqtrrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 0 ≤ ( ( 𝐺 ∘f − 𝐹 ) ‘ 𝑥 ) ) |
28 |
7 2 3 27
|
itg1ge0a |
⊢ ( 𝜑 → 0 ≤ ( ∫1 ‘ ( 𝐺 ∘f − 𝐹 ) ) ) |
29 |
|
itg1sub |
⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐹 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐺 ∘f − 𝐹 ) ) = ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) ) |
30 |
4 1 29
|
syl2anc |
⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐺 ∘f − 𝐹 ) ) = ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) ) |
31 |
28 30
|
breqtrd |
⊢ ( 𝜑 → 0 ≤ ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) ) |
32 |
|
itg1cl |
⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) ∈ ℝ ) |
33 |
4 32
|
syl |
⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) ∈ ℝ ) |
34 |
|
itg1cl |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℝ ) |
35 |
1 34
|
syl |
⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) ∈ ℝ ) |
36 |
33 35
|
subge0d |
⊢ ( 𝜑 → ( 0 ≤ ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) ↔ ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) ) ) |
37 |
31 36
|
mpbid |
⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) ) |