This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgabs

Description: The triangle inequality for integrals. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgabs.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgabs.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
Assertion itgabs ( 𝜑 → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgabs.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 itgabs.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 1 2 itgcl ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
4 3 cjcld ⊢ ( 𝜑 → ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℂ )
5 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
6 2 5 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
7 6 1 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
8 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℂ )
9 nfv ⊢ Ⅎ 𝑦 𝐵 ∈ ℂ
10 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
11 10 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ
12 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
13 12 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
14 9 11 13 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℂ ↔ ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ )
15 8 14 sylib ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ )
16 15 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ )
17 nfcv ⊢ Ⅎ 𝑦 𝐵
18 17 10 12 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
19 18 2 eqeltrrid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ 𝐿1 )
20 4 16 19 iblmulc2 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ∈ 𝐿1 )
21 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℂ )
22 21 16 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
23 22 iblcn ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐴 ↦ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑦 ∈ 𝐴 ↦ ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ) ∈ 𝐿1 ∧ ( 𝑦 ∈ 𝐴 ↦ ( ℑ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ) ∈ 𝐿1 ) ) )
24 20 23 mpbid ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐴 ↦ ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ) ∈ 𝐿1 ∧ ( 𝑦 ∈ 𝐴 ↦ ( ℑ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ) ∈ 𝐿1 ) )
25 24 simpld ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ) ∈ 𝐿1 )
26 ovexd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ V )
27 26 20 iblabs ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ) ∈ 𝐿1 )
28 22 recld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ∈ ℝ )
29 22 abscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ∈ ℝ )
30 22 releabsd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ≤ ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) )
31 25 27 28 29 30 itgle ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 ≤ ∫ 𝐴 ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 )
32 3 abscld ⊢ ( 𝜑 → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ )
33 32 recnd ⊢ ( 𝜑 → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℂ )
34 33 sqvald ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) )
35 3 absvalsqd ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) = ( ∫ 𝐴 𝐵 d 𝑥 · ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) )
36 3 4 mulcomd ⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 · ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) = ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 𝐵 d 𝑥 ) )
37 12 17 10 cbvitg ⊢ ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 d 𝑦
38 37 oveq2i ⊢ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 d 𝑦 )
39 4 16 19 itgmulc2 ⊢ ( 𝜑 → ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 d 𝑦 ) = ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 )
40 38 39 eqtrid ⊢ ( 𝜑 → ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 )
41 35 36 40 3eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) = ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 )
42 41 fveq2d ⊢ ( 𝜑 → ( ℜ ‘ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) ) = ( ℜ ‘ ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 ) )
43 32 resqcld ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) ∈ ℝ )
44 43 rered ⊢ ( 𝜑 → ( ℜ ‘ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) )
45 26 20 itgre ⊢ ( 𝜑 → ( ℜ ‘ ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 ) = ∫ 𝐴 ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 )
46 42 44 45 3eqtr3d ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) = ∫ 𝐴 ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 )
47 34 46 eqtr3d ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) = ∫ 𝐴 ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 )
48 12 fveq2d ⊢ ( 𝑥 = 𝑦 → ( abs ‘ 𝐵 ) = ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
49 nfcv ⊢ Ⅎ 𝑦 ( abs ‘ 𝐵 )
50 nfcv ⊢ Ⅎ 𝑥 abs
51 50 10 nffv ⊢ Ⅎ 𝑥 ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
52 48 49 51 cbvitg ⊢ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 = ∫ 𝐴 ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦
53 52 oveq2i ⊢ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 )
54 16 abscld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
55 16 19 iblabs ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ∈ 𝐿1 )
56 33 54 55 itgmulc2 ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 ) = ∫ 𝐴 ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 )
57 21 16 absmuld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) = ( ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) · ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) )
58 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
59 58 abscjd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) )
60 59 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) · ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) )
61 57 60 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) )
62 61 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 = ∫ 𝐴 ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 )
63 56 62 eqtr4d ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) d 𝑦 ) = ∫ 𝐴 ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 )
64 53 63 eqtrid ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) d 𝑦 )
65 31 47 64 3brtr4d ⊢ ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ≤ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
66 65 adantr ⊢ ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ≤ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
67 32 adantr ⊢ ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ )
68 7 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
69 1 2 iblabs ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )
70 68 69 itgrecl ⊢ ( 𝜑 → ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ∈ ℝ )
71 70 adantr ⊢ ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ∈ ℝ )
72 simpr ⊢ ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) )
73 lemul2 ⊢ ( ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ ∧ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ∈ ℝ ∧ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ) → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ↔ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ≤ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) ) )
74 67 71 67 72 73 syl112anc ⊢ ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ↔ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ≤ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) ) )
75 66 74 mpbird ⊢ ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 )
76 75 ex ⊢ ( 𝜑 → ( 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
77 7 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( abs ‘ 𝐵 ) )
78 69 68 77 itgge0 ⊢ ( 𝜑 → 0 ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 )
79 breq1 ⊢ ( 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) → ( 0 ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ↔ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
80 78 79 syl5ibcom ⊢ ( 𝜑 → ( 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
81 3 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) )
82 0re ⊢ 0 ∈ ℝ
83 leloe ⊢ ( ( 0 ∈ ℝ ∧ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ ) → ( 0 ≤ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↔ ( 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∨ 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ) )
84 82 32 83 sylancr ⊢ ( 𝜑 → ( 0 ≤ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↔ ( 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∨ 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ) )
85 81 84 mpbid ⊢ ( 𝜑 → ( 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∨ 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) )
86 76 80 85 mpjaod ⊢ ( 𝜑 → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 )