Metamath Proof Explorer


Theorem itgabsnc

Description: Choice-free analogue of itgabs . (Contributed by Brendan Leahy, 19-Nov-2017) (Revised by Brendan Leahy, 19-Jun-2018)

Ref Expression
Hypotheses itgabsnc.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
itgabsnc.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )
itgabsnc.m1 ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn )
itgabsnc.m2 ( 𝜑 → ( 𝑦𝐴 ↦ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ∈ MblFn )
Assertion itgabsnc ( 𝜑 → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgabsnc.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
2 itgabsnc.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )
3 itgabsnc.m1 ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn )
4 itgabsnc.m2 ( 𝜑 → ( 𝑦𝐴 ↦ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ∈ MblFn )
5 1 2 itgcl ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
6 5 cjcld ( 𝜑 → ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℂ )
7 iblmbf ( ( 𝑥𝐴𝐵 ) ∈ 𝐿1 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
8 2 7 syl ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
9 8 1 mbfmptcl ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
10 9 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 𝐵 ∈ ℂ )
11 nfv 𝑦 𝐵 ∈ ℂ
12 nfcsb1v 𝑥 𝑦 / 𝑥 𝐵
13 12 nfel1 𝑥 𝑦 / 𝑥 𝐵 ∈ ℂ
14 csbeq1a ( 𝑥 = 𝑦𝐵 = 𝑦 / 𝑥 𝐵 )
15 14 eleq1d ( 𝑥 = 𝑦 → ( 𝐵 ∈ ℂ ↔ 𝑦 / 𝑥 𝐵 ∈ ℂ ) )
16 11 13 15 cbvralw ( ∀ 𝑥𝐴 𝐵 ∈ ℂ ↔ ∀ 𝑦𝐴 𝑦 / 𝑥 𝐵 ∈ ℂ )
17 10 16 sylib ( 𝜑 → ∀ 𝑦𝐴 𝑦 / 𝑥 𝐵 ∈ ℂ )
18 17 r19.21bi ( ( 𝜑𝑦𝐴 ) → 𝑦 / 𝑥 𝐵 ∈ ℂ )
19 nfcv 𝑦 𝐵
20 19 12 14 cbvmpt ( 𝑥𝐴𝐵 ) = ( 𝑦𝐴 𝑦 / 𝑥 𝐵 )
21 20 2 eqeltrrid ( 𝜑 → ( 𝑦𝐴 𝑦 / 𝑥 𝐵 ) ∈ 𝐿1 )
22 6 18 21 4 iblmulc2nc ( 𝜑 → ( 𝑦𝐴 ↦ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ∈ 𝐿1 )
23 6 adantr ( ( 𝜑𝑦𝐴 ) → ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℂ )
24 23 18 mulcld ( ( 𝜑𝑦𝐴 ) → ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ∈ ℂ )
25 24 iblcn ( 𝜑 → ( ( 𝑦𝐴 ↦ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑦𝐴 ↦ ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ) ∈ 𝐿1 ∧ ( 𝑦𝐴 ↦ ( ℑ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ) ∈ 𝐿1 ) ) )
26 22 25 mpbid ( 𝜑 → ( ( 𝑦𝐴 ↦ ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ) ∈ 𝐿1 ∧ ( 𝑦𝐴 ↦ ( ℑ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ) ∈ 𝐿1 ) )
27 26 simpld ( 𝜑 → ( 𝑦𝐴 ↦ ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ) ∈ 𝐿1 )
28 23 18 absmuld ( ( 𝜑𝑦𝐴 ) → ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) = ( ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) )
29 28 mpteq2dva ( 𝜑 → ( 𝑦𝐴 ↦ ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ) = ( 𝑦𝐴 ↦ ( ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) ) )
30 8 1 mbfdm2 ( 𝜑𝐴 ∈ dom vol )
31 23 abscld ( ( 𝜑𝑦𝐴 ) → ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ∈ ℝ )
32 18 abscld ( ( 𝜑𝑦𝐴 ) → ( abs ‘ 𝑦 / 𝑥 𝐵 ) ∈ ℝ )
33 fconstmpt ( 𝐴 × { ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) } ) = ( 𝑦𝐴 ↦ ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) )
34 33 a1i ( 𝜑 → ( 𝐴 × { ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) } ) = ( 𝑦𝐴 ↦ ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ) )
35 nfcv 𝑦 ( abs ‘ 𝐵 )
36 nfcv 𝑥 abs
37 36 12 nffv 𝑥 ( abs ‘ 𝑦 / 𝑥 𝐵 )
38 14 fveq2d ( 𝑥 = 𝑦 → ( abs ‘ 𝐵 ) = ( abs ‘ 𝑦 / 𝑥 𝐵 ) )
39 35 37 38 cbvmpt ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) = ( 𝑦𝐴 ↦ ( abs ‘ 𝑦 / 𝑥 𝐵 ) )
40 39 a1i ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) = ( 𝑦𝐴 ↦ ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) )
41 30 31 32 34 40 offval2 ( 𝜑 → ( ( 𝐴 × { ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) } ) ∘f · ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ) = ( 𝑦𝐴 ↦ ( ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) ) )
42 29 41 eqtr4d ( 𝜑 → ( 𝑦𝐴 ↦ ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ) = ( ( 𝐴 × { ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) } ) ∘f · ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ) )
43 6 abscld ( 𝜑 → ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ∈ ℝ )
44 9 abscld ( ( 𝜑𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
45 44 recnd ( ( 𝜑𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℂ )
46 45 fmpttd ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
47 3 43 46 mbfmulc2re ( 𝜑 → ( ( 𝐴 × { ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) } ) ∘f · ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ) ∈ MblFn )
48 42 47 eqeltrd ( 𝜑 → ( 𝑦𝐴 ↦ ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ) ∈ MblFn )
49 24 22 48 iblabsnc ( 𝜑 → ( 𝑦𝐴 ↦ ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ) ∈ 𝐿1 )
50 24 recld ( ( 𝜑𝑦𝐴 ) → ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ∈ ℝ )
51 24 abscld ( ( 𝜑𝑦𝐴 ) → ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ∈ ℝ )
52 24 releabsd ( ( 𝜑𝑦𝐴 ) → ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) ≤ ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) )
53 27 49 50 51 52 itgle ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) d 𝑦 ≤ ∫ 𝐴 ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) d 𝑦 )
54 5 abscld ( 𝜑 → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ )
55 54 recnd ( 𝜑 → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℂ )
56 55 sqvald ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) )
57 5 absvalsqd ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) = ( ∫ 𝐴 𝐵 d 𝑥 · ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) )
58 5 6 mulcomd ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 · ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) = ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 𝐵 d 𝑥 ) )
59 14 19 12 cbvitg 𝐴 𝐵 d 𝑥 = ∫ 𝐴 𝑦 / 𝑥 𝐵 d 𝑦
60 59 oveq2i ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 𝑦 / 𝑥 𝐵 d 𝑦 )
61 6 18 21 4 itgmulc2nc ( 𝜑 → ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 𝑦 / 𝑥 𝐵 d 𝑦 ) = ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) d 𝑦 )
62 60 61 syl5eq ( 𝜑 → ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) d 𝑦 )
63 57 58 62 3eqtrd ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) = ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) d 𝑦 )
64 63 fveq2d ( 𝜑 → ( ℜ ‘ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) ) = ( ℜ ‘ ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) d 𝑦 ) )
65 54 resqcld ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) ∈ ℝ )
66 65 rered ( 𝜑 → ( ℜ ‘ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) )
67 ovexd ( ( 𝜑𝑦𝐴 ) → ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ∈ V )
68 67 22 itgre ( 𝜑 → ( ℜ ‘ ∫ 𝐴 ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) d 𝑦 ) = ∫ 𝐴 ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) d 𝑦 )
69 64 66 68 3eqtr3d ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↑ 2 ) = ∫ 𝐴 ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) d 𝑦 )
70 56 69 eqtr3d ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) = ∫ 𝐴 ( ℜ ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) d 𝑦 )
71 38 35 37 cbvitg 𝐴 ( abs ‘ 𝐵 ) d 𝑥 = ∫ 𝐴 ( abs ‘ 𝑦 / 𝑥 𝐵 ) d 𝑦
72 71 oveq2i ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝑦 / 𝑥 𝐵 ) d 𝑦 )
73 1 2 3 iblabsnc ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )
74 39 73 eqeltrrid ( 𝜑 → ( 𝑦𝐴 ↦ ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) ∈ 𝐿1 )
75 54 adantr ( ( 𝜑𝑦𝐴 ) → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ )
76 fconstmpt ( 𝐴 × { ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) } ) = ( 𝑦𝐴 ↦ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) )
77 76 a1i ( 𝜑 → ( 𝐴 × { ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) } ) = ( 𝑦𝐴 ↦ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) )
78 30 75 32 77 40 offval2 ( 𝜑 → ( ( 𝐴 × { ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) } ) ∘f · ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ) = ( 𝑦𝐴 ↦ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) ) )
79 3 54 46 mbfmulc2re ( 𝜑 → ( ( 𝐴 × { ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) } ) ∘f · ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ) ∈ MblFn )
80 78 79 eqeltrrd ( 𝜑 → ( 𝑦𝐴 ↦ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) ) ∈ MblFn )
81 55 32 74 80 itgmulc2nc ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝑦 / 𝑥 𝐵 ) d 𝑦 ) = ∫ 𝐴 ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) d 𝑦 )
82 5 adantr ( ( 𝜑𝑦𝐴 ) → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
83 82 abscjd ( ( 𝜑𝑦𝐴 ) → ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) )
84 83 oveq1d ( ( 𝜑𝑦𝐴 ) → ( ( abs ‘ ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) )
85 28 84 eqtrd ( ( 𝜑𝑦𝐴 ) → ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) = ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) )
86 85 itgeq2dv ( 𝜑 → ∫ 𝐴 ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) d 𝑦 = ∫ 𝐴 ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ 𝑦 / 𝑥 𝐵 ) ) d 𝑦 )
87 81 86 eqtr4d ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝑦 / 𝑥 𝐵 ) d 𝑦 ) = ∫ 𝐴 ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) d 𝑦 )
88 72 87 syl5eq ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( abs ‘ ( ( ∗ ‘ ∫ 𝐴 𝐵 d 𝑥 ) · 𝑦 / 𝑥 𝐵 ) ) d 𝑦 )
89 53 70 88 3brtr4d ( 𝜑 → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ≤ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
90 89 adantr ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ≤ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
91 54 adantr ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ )
92 44 73 itgrecl ( 𝜑 → ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ∈ ℝ )
93 92 adantr ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ∈ ℝ )
94 simpr ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) )
95 lemul2 ( ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ ∧ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ∈ ℝ ∧ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ) → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ↔ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ≤ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) ) )
96 91 93 91 94 95 syl112anc ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ↔ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ≤ ( ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) · ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) ) )
97 90 96 mpbird ( ( 𝜑 ∧ 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 )
98 97 ex ( 𝜑 → ( 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
99 9 absge0d ( ( 𝜑𝑥𝐴 ) → 0 ≤ ( abs ‘ 𝐵 ) )
100 73 44 99 itgge0 ( 𝜑 → 0 ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 )
101 breq1 ( 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) → ( 0 ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ↔ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
102 100 101 syl5ibcom ( 𝜑 → ( 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 ) )
103 5 absge0d ( 𝜑 → 0 ≤ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) )
104 0re 0 ∈ ℝ
105 leloe ( ( 0 ∈ ℝ ∧ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∈ ℝ ) → ( 0 ≤ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↔ ( 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∨ 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ) )
106 104 54 105 sylancr ( 𝜑 → ( 0 ≤ ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ↔ ( 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∨ 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) ) )
107 103 106 mpbid ( 𝜑 → ( 0 < ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ∨ 0 = ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ) )
108 98 102 107 mpjaod ( 𝜑 → ( abs ‘ ∫ 𝐴 𝐵 d 𝑥 ) ≤ ∫ 𝐴 ( abs ‘ 𝐵 ) d 𝑥 )