Metamath Proof Explorer

Theorem itg2mulc

Description: The integral of a nonnegative constant times a function is the constant times the integral of the original function. (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses itg2mulc.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2mulc.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
itg2mulc.4 ⊢ ( 𝜑 → 𝐴 ∈ ( 0 [,) +∞ ) )
Assertion itg2mulc ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 itg2mulc.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
2 itg2mulc.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
3 itg2mulc.4 ⊢ ( 𝜑 → 𝐴 ∈ ( 0 [,) +∞ ) )
4 1 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
5 2 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
6 elrege0 ⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
7 3 6 sylib ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
8 7 simpld ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
9 8 anim1i ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
10 elrp ⊢ ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
11 9 10 sylibr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ+ )
12 4 5 11 itg2mulclem ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) )
13 ge0mulcl ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ ) )
15 fconst6g ⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) → ( ℝ × { 𝐴 } ) : ℝ ⟶ ( 0 [,) +∞ ) )
16 3 15 syl ⊢ ( 𝜑 → ( ℝ × { 𝐴 } ) : ℝ ⟶ ( 0 [,) +∞ ) )
17 reex ⊢ ℝ ∈ V
18 17 a1i ⊢ ( 𝜑 → ℝ ∈ V )
19 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
20 14 16 1 18 18 19 off ⊢ ( 𝜑 → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,) +∞ ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,) +∞ ) )
22 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
23 fss ⊢ ( ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,] +∞ ) )
24 20 22 23 sylancl ⊢ ( 𝜑 → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,] +∞ ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,] +∞ ) )
26 8 2 remulcld ⊢ ( 𝜑 → ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∈ ℝ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∈ ℝ )
28 itg2lecl ⊢ ( ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∈ ℝ ∧ ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ) → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ∈ ℝ )
29 25 27 12 28 syl3anc ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ∈ ℝ )
30 11 rpreccld ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ+ )
31 21 29 30 itg2mulclem ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ∫2 ‘ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ) ≤ ( ( 1 / 𝐴 ) · ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ) )
32 4 feqmptd ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
33 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
34 ax-resscn ⊢ ℝ ⊆ ℂ
35 33 34 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
36 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → 𝐹 : ℝ ⟶ ℂ )
37 1 35 36 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
38 37 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐹 : ℝ ⟶ ℂ )
39 38 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 0 < 𝐴 ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
40 39 mulid2d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐴 ) ∧ 𝑦 ∈ ℝ ) → ( 1 · ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ 𝑦 ) )
41 40 mpteq2dva ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 𝑦 ∈ ℝ ↦ ( 1 · ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
42 32 41 eqtr4d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 1 · ( 𝐹 ‘ 𝑦 ) ) ) )
43 17 a1i ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ℝ ∈ V )
44 1red ⊢ ( ( ( 𝜑 ∧ 0 < 𝐴 ) ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℝ )
45 43 30 11 ofc12 ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · ( ℝ × { 𝐴 } ) ) = ( ℝ × { ( ( 1 / 𝐴 ) · 𝐴 ) } ) )
46 fconstmpt ⊢ ( ℝ × { ( ( 1 / 𝐴 ) · 𝐴 ) } ) = ( 𝑦 ∈ ℝ ↦ ( ( 1 / 𝐴 ) · 𝐴 ) )
47 45 46 eqtrdi ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · ( ℝ × { 𝐴 } ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 1 / 𝐴 ) · 𝐴 ) ) )
48 8 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
49 48 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐴 ∈ ℂ )
50 11 rpne0d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
51 49 50 recid2d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( 1 / 𝐴 ) · 𝐴 ) = 1 )
52 51 mpteq2dv ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 𝑦 ∈ ℝ ↦ ( ( 1 / 𝐴 ) · 𝐴 ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) )
53 47 52 eqtrd ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · ( ℝ × { 𝐴 } ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) )
54 43 44 39 53 32 offval2 ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · ( ℝ × { 𝐴 } ) ) ∘f · 𝐹 ) = ( 𝑦 ∈ ℝ ↦ ( 1 · ( 𝐹 ‘ 𝑦 ) ) ) )
55 30 rpcnd ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℂ )
56 fconst6g ⊢ ( ( 1 / 𝐴 ) ∈ ℂ → ( ℝ × { ( 1 / 𝐴 ) } ) : ℝ ⟶ ℂ )
57 55 56 syl ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ℝ × { ( 1 / 𝐴 ) } ) : ℝ ⟶ ℂ )
58 fconst6g ⊢ ( 𝐴 ∈ ℂ → ( ℝ × { 𝐴 } ) : ℝ ⟶ ℂ )
59 49 58 syl ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ℝ × { 𝐴 } ) : ℝ ⟶ ℂ )
60 mulass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
61 60 adantl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐴 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
62 43 57 59 38 61 caofass ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · ( ℝ × { 𝐴 } ) ) ∘f · 𝐹 ) = ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) )
63 42 54 62 3eqtr2d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐹 = ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) )
64 63 fveq2d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ∫2 ‘ 𝐹 ) = ( ∫2 ‘ ( ( ℝ × { ( 1 / 𝐴 ) } ) ∘f · ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ) )
65 29 recnd ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ∈ ℂ )
66 65 49 50 divrec2d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) / 𝐴 ) = ( ( 1 / 𝐴 ) · ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ) )
67 31 64 66 3brtr4d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) / 𝐴 ) )
68 5 29 11 lemuldiv2d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ≤ ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ↔ ( ∫2 ‘ 𝐹 ) ≤ ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) / 𝐴 ) ) )
69 67 68 mpbird ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ≤ ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) )
70 itg2cl ⊢ ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ∈ ℝ* )
71 24 70 syl ⊢ ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ∈ ℝ* )
72 26 rexrd ⊢ ( 𝜑 → ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∈ ℝ* )
73 xrletri3 ⊢ ( ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ∈ ℝ* ∧ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∈ ℝ* ) → ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ↔ ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∧ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ≤ ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ) ) )
74 71 72 73 syl2anc ⊢ ( 𝜑 → ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ↔ ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∧ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ≤ ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ) ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ↔ ( ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ≤ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ∧ ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) ≤ ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) ) ) )
76 12 69 75 mpbir2and ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) )
77 17 a1i ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ℝ ∈ V )
78 37 adantr ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → 𝐹 : ℝ ⟶ ℂ )
79 8 adantr ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → 𝐴 ∈ ℝ )
80 0re ⊢ 0 ∈ ℝ
81 80 a1i ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → 0 ∈ ℝ )
82 simplr ⊢ ( ( ( 𝜑 ∧ 0 = 𝐴 ) ∧ 𝑥 ∈ ℂ ) → 0 = 𝐴 )
83 82 oveq1d ⊢ ( ( ( 𝜑 ∧ 0 = 𝐴 ) ∧ 𝑥 ∈ ℂ ) → ( 0 · 𝑥 ) = ( 𝐴 · 𝑥 ) )
84 mul02 ⊢ ( 𝑥 ∈ ℂ → ( 0 · 𝑥 ) = 0 )
85 84 adantl ⊢ ( ( ( 𝜑 ∧ 0 = 𝐴 ) ∧ 𝑥 ∈ ℂ ) → ( 0 · 𝑥 ) = 0 )
86 83 85 eqtr3d ⊢ ( ( ( 𝜑 ∧ 0 = 𝐴 ) ∧ 𝑥 ∈ ℂ ) → ( 𝐴 · 𝑥 ) = 0 )
87 77 78 79 81 86 caofid2 ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) = ( ℝ × { 0 } ) )
88 87 fveq2d ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ∫2 ‘ ( ℝ × { 0 } ) ) )
89 itg20 ⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0
90 88 89 eqtrdi ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = 0 )
91 2 adantr ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
92 91 recnd ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( ∫2 ‘ 𝐹 ) ∈ ℂ )
93 92 mul02d ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( 0 · ( ∫2 ‘ 𝐹 ) ) = 0 )
94 simpr ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → 0 = 𝐴 )
95 94 oveq1d ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( 0 · ( ∫2 ‘ 𝐹 ) ) = ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) )
96 90 93 95 3eqtr2d ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) )
97 7 simprd ⊢ ( 𝜑 → 0 ≤ 𝐴 )
98 leloe ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
99 80 8 98 sylancr ⊢ ( 𝜑 → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
100 97 99 mpbid ⊢ ( 𝜑 → ( 0 < 𝐴 ∨ 0 = 𝐴 ) )
101 76 96 100 mpjaodan ⊢ ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( 𝐴 · ( ∫2 ‘ 𝐹 ) ) )