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 eqtrid ⊢ ( 𝜑 → ( ( ∗ ‘ ∫ 𝐴 𝐵 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 eqtrid ⊢ ( 𝜑 → ( ( 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 𝑥 )