MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iblmulc2 Structured version   Visualization version   GIF version

Theorem iblmulc2 24443
Description: Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.)
Hypotheses
Ref Expression
itgmulc2.1 (𝜑𝐶 ∈ ℂ)
itgmulc2.2 ((𝜑𝑥𝐴) → 𝐵𝑉)
itgmulc2.3 (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
Assertion
Ref Expression
iblmulc2 (𝜑 → (𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥   𝑥,𝑉
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem iblmulc2
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 itgmulc2.1 . . 3 (𝜑𝐶 ∈ ℂ)
2 itgmulc2.2 . . 3 ((𝜑𝑥𝐴) → 𝐵𝑉)
3 itgmulc2.3 . . . 4 (𝜑 → (𝑥𝐴𝐵) ∈ 𝐿1)
4 iblmbf 24380 . . . 4 ((𝑥𝐴𝐵) ∈ 𝐿1 → (𝑥𝐴𝐵) ∈ MblFn)
53, 4syl 17 . . 3 (𝜑 → (𝑥𝐴𝐵) ∈ MblFn)
61, 2, 5mbfmulc2 24276 . 2 (𝜑 → (𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
7 ifan 4501 . . . . . 6 if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) = if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0)
81adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → 𝐶 ∈ ℂ)
95, 2mbfmptcl 24249 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴) → 𝐵 ∈ ℂ)
108, 9mulcld 10661 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴) → (𝐶 · 𝐵) ∈ ℂ)
1110adantlr 714 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (𝐶 · 𝐵) ∈ ℂ)
12 ax-icn 10596 . . . . . . . . . . . . . 14 i ∈ ℂ
13 ine0 11075 . . . . . . . . . . . . . 14 i ≠ 0
14 elfzelz 12913 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...3) → 𝑘 ∈ ℤ)
1514ad2antlr 726 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → 𝑘 ∈ ℤ)
16 expclz 13461 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ∈ ℂ)
1712, 13, 15, 16mp3an12i 1462 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (i↑𝑘) ∈ ℂ)
18 expne0i 13468 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0)
1912, 13, 15, 18mp3an12i 1462 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (i↑𝑘) ≠ 0)
2011, 17, 19divcld 11416 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → ((𝐶 · 𝐵) / (i↑𝑘)) ∈ ℂ)
2120recld 14555 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ)
22 0re 10643 . . . . . . . . . . 11 0 ∈ ℝ
23 ifcl 4494 . . . . . . . . . . 11 (((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ)
2421, 22, 23sylancl 589 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ)
2524rexrd 10691 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ*)
26 max1 12577 . . . . . . . . . 10 ((0 ∈ ℝ ∧ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ) → 0 ≤ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))
2722, 21, 26sylancr 590 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → 0 ≤ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))
28 elxrge0 12846 . . . . . . . . 9 (if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ (0[,]+∞) ↔ (if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ* ∧ 0 ≤ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)))
2925, 27, 28sylanbrc 586 . . . . . . . 8 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ (0[,]+∞))
30 0e0iccpnf 12848 . . . . . . . . 9 0 ∈ (0[,]+∞)
3130a1i 11 . . . . . . . 8 (((𝜑𝑘 ∈ (0...3)) ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
3229, 31ifclda 4484 . . . . . . 7 ((𝜑𝑘 ∈ (0...3)) → if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈ (0[,]+∞))
3332adantr 484 . . . . . 6 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈ (0[,]+∞))
347, 33eqeltrid 2920 . . . . 5 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ (0[,]+∞))
3534fmpttd 6872 . . . 4 ((𝜑𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞))
36 reex 10628 . . . . . . . . . . 11 ℝ ∈ V
3736a1i 11 . . . . . . . . . 10 (𝜑 → ℝ ∈ V)
381abscld 14798 . . . . . . . . . . 11 (𝜑 → (abs‘𝐶) ∈ ℝ)
3938adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → (abs‘𝐶) ∈ ℝ)
409abscld 14798 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (abs‘𝐵) ∈ ℝ)
419absge0d 14806 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 0 ≤ (abs‘𝐵))
42 elrege0 12843 . . . . . . . . . . . . 13 ((abs‘𝐵) ∈ (0[,)+∞) ↔ ((abs‘𝐵) ∈ ℝ ∧ 0 ≤ (abs‘𝐵)))
4340, 41, 42sylanbrc 586 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (abs‘𝐵) ∈ (0[,)+∞))
44 0e0icopnf 12847 . . . . . . . . . . . . 13 0 ∈ (0[,)+∞)
4544a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,)+∞))
4643, 45ifclda 4484 . . . . . . . . . . 11 (𝜑 → if(𝑥𝐴, (abs‘𝐵), 0) ∈ (0[,)+∞))
4746adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, (abs‘𝐵), 0) ∈ (0[,)+∞))
48 fconstmpt 5602 . . . . . . . . . . 11 (ℝ × {(abs‘𝐶)}) = (𝑥 ∈ ℝ ↦ (abs‘𝐶))
4948a1i 11 . . . . . . . . . 10 (𝜑 → (ℝ × {(abs‘𝐶)}) = (𝑥 ∈ ℝ ↦ (abs‘𝐶)))
50 eqidd 2825 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0)))
5137, 39, 47, 49, 50offval2 7422 . . . . . . . . 9 (𝜑 → ((ℝ × {(abs‘𝐶)}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥𝐴, (abs‘𝐵), 0))))
52 ovif2 7247 . . . . . . . . . . 11 ((abs‘𝐶) · if(𝑥𝐴, (abs‘𝐵), 0)) = if(𝑥𝐴, ((abs‘𝐶) · (abs‘𝐵)), ((abs‘𝐶) · 0))
538, 9absmuld 14816 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → (abs‘(𝐶 · 𝐵)) = ((abs‘𝐶) · (abs‘𝐵)))
5453ifeq1da 4480 . . . . . . . . . . . 12 (𝜑 → if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), ((abs‘𝐶) · 0)) = if(𝑥𝐴, ((abs‘𝐶) · (abs‘𝐵)), ((abs‘𝐶) · 0)))
5538recnd 10669 . . . . . . . . . . . . . 14 (𝜑 → (abs‘𝐶) ∈ ℂ)
5655mul01d 10839 . . . . . . . . . . . . 13 (𝜑 → ((abs‘𝐶) · 0) = 0)
5756ifeq2d 4469 . . . . . . . . . . . 12 (𝜑 → if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), ((abs‘𝐶) · 0)) = if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))
5854, 57eqtr3d 2861 . . . . . . . . . . 11 (𝜑 → if(𝑥𝐴, ((abs‘𝐶) · (abs‘𝐵)), ((abs‘𝐶) · 0)) = if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))
5952, 58syl5eq 2871 . . . . . . . . . 10 (𝜑 → ((abs‘𝐶) · if(𝑥𝐴, (abs‘𝐵), 0)) = if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))
6059mpteq2dv 5149 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥𝐴, (abs‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)))
6151, 60eqtrd 2859 . . . . . . . 8 (𝜑 → ((ℝ × {(abs‘𝐶)}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)))
6261fveq2d 6667 . . . . . . 7 (𝜑 → (∫2‘((ℝ × {(abs‘𝐶)}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0)))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))))
6347fmpttd 6872 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0)):ℝ⟶(0[,)+∞))
642, 3iblabs 24441 . . . . . . . . . 10 (𝜑 → (𝑥𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1)
6540, 41iblpos 24405 . . . . . . . . . 10 (𝜑 → ((𝑥𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1 ↔ ((𝑥𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0))) ∈ ℝ)))
6664, 65mpbid 235 . . . . . . . . 9 (𝜑 → ((𝑥𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0))) ∈ ℝ))
6766simprd 499 . . . . . . . 8 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0))) ∈ ℝ)
68 abscl 14640 . . . . . . . . . 10 (𝐶 ∈ ℂ → (abs‘𝐶) ∈ ℝ)
69 absge0 14649 . . . . . . . . . 10 (𝐶 ∈ ℂ → 0 ≤ (abs‘𝐶))
70 elrege0 12843 . . . . . . . . . 10 ((abs‘𝐶) ∈ (0[,)+∞) ↔ ((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶)))
7168, 69, 70sylanbrc 586 . . . . . . . . 9 (𝐶 ∈ ℂ → (abs‘𝐶) ∈ (0[,)+∞))
721, 71syl 17 . . . . . . . 8 (𝜑 → (abs‘𝐶) ∈ (0[,)+∞))
7363, 67, 72itg2mulc 24360 . . . . . . 7 (𝜑 → (∫2‘((ℝ × {(abs‘𝐶)}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0)))) = ((abs‘𝐶) · (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0)))))
7462, 73eqtr3d 2861 . . . . . 6 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))) = ((abs‘𝐶) · (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0)))))
7538, 67remulcld 10671 . . . . . 6 (𝜑 → ((abs‘𝐶) · (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘𝐵), 0)))) ∈ ℝ)
7674, 75eqeltrd 2916 . . . . 5 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))) ∈ ℝ)
7776adantr 484 . . . 4 ((𝜑𝑘 ∈ (0...3)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))) ∈ ℝ)
7810abscld 14798 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℝ)
7978rexrd 10691 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℝ*)
8010absge0d 14806 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 0 ≤ (abs‘(𝐶 · 𝐵)))
81 elxrge0 12846 . . . . . . . . . 10 ((abs‘(𝐶 · 𝐵)) ∈ (0[,]+∞) ↔ ((abs‘(𝐶 · 𝐵)) ∈ ℝ* ∧ 0 ≤ (abs‘(𝐶 · 𝐵))))
8279, 80, 81sylanbrc 586 . . . . . . . . 9 ((𝜑𝑥𝐴) → (abs‘(𝐶 · 𝐵)) ∈ (0[,]+∞))
8330a1i 11 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝑥𝐴) → 0 ∈ (0[,]+∞))
8482, 83ifclda 4484 . . . . . . . 8 (𝜑 → if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0) ∈ (0[,]+∞))
8584adantr 484 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0) ∈ (0[,]+∞))
8685fmpttd 6872 . . . . . 6 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)):ℝ⟶(0[,]+∞))
8786adantr 484 . . . . 5 ((𝜑𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)):ℝ⟶(0[,]+∞))
8820releabsd 14813 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘((𝐶 · 𝐵) / (i↑𝑘))))
8911, 17, 19absdivd 14817 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘))))
90 elfznn0 13006 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (0...3) → 𝑘 ∈ ℕ0)
9190ad2antlr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → 𝑘 ∈ ℕ0)
92 absexp 14666 . . . . . . . . . . . . . . . . 17 ((i ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘))
9312, 91, 92sylancr 590 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘))
94 absi 14648 . . . . . . . . . . . . . . . . . 18 (abs‘i) = 1
9594oveq1i 7161 . . . . . . . . . . . . . . . . 17 ((abs‘i)↑𝑘) = (1↑𝑘)
96 1exp 13465 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → (1↑𝑘) = 1)
9715, 96syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (1↑𝑘) = 1)
9895, 97syl5eq 2871 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → ((abs‘i)↑𝑘) = 1)
9993, 98eqtrd 2859 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (abs‘(i↑𝑘)) = 1)
10099oveq2d 7167 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / 1))
10178recnd 10669 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ)
102101adantlr 714 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ)
103102div1d 11408 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → ((abs‘(𝐶 · 𝐵)) / 1) = (abs‘(𝐶 · 𝐵)))
10489, 100, 1033eqtrd 2863 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = (abs‘(𝐶 · 𝐵)))
10588, 104breqtrd 5079 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘(𝐶 · 𝐵)))
10680adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → 0 ≤ (abs‘(𝐶 · 𝐵)))
107 breq1 5056 . . . . . . . . . . . . 13 ((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → ((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘(𝐶 · 𝐵)) ↔ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵))))
108 breq1 5056 . . . . . . . . . . . . 13 (0 = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → (0 ≤ (abs‘(𝐶 · 𝐵)) ↔ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵))))
109107, 108ifboth 4488 . . . . . . . . . . . 12 (((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘(𝐶 · 𝐵)) ∧ 0 ≤ (abs‘(𝐶 · 𝐵))) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵)))
110105, 106, 109syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵)))
111 iftrue 4456 . . . . . . . . . . . 12 (𝑥𝐴 → if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))
112111adantl 485 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))
113 iftrue 4456 . . . . . . . . . . . 12 (𝑥𝐴 → if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0) = (abs‘(𝐶 · 𝐵)))
114113adantl 485 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0) = (abs‘(𝐶 · 𝐵)))
115110, 112, 1143brtr4d 5085 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥𝐴) → if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))
116115ex 416 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...3)) → (𝑥𝐴 → if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)))
117 0le0 11737 . . . . . . . . . . 11 0 ≤ 0
118117a1i 11 . . . . . . . . . 10 𝑥𝐴 → 0 ≤ 0)
119 iffalse 4459 . . . . . . . . . 10 𝑥𝐴 → if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = 0)
120 iffalse 4459 . . . . . . . . . 10 𝑥𝐴 → if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0) = 0)
121118, 119, 1203brtr4d 5085 . . . . . . . . 9 𝑥𝐴 → if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))
122116, 121pm2.61d1 183 . . . . . . . 8 ((𝜑𝑘 ∈ (0...3)) → if(𝑥𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))
1237, 122eqbrtrid 5088 . . . . . . 7 ((𝜑𝑘 ∈ (0...3)) → if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))
124123ralrimivw 3178 . . . . . 6 ((𝜑𝑘 ∈ (0...3)) → ∀𝑥 ∈ ℝ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))
12536a1i 11 . . . . . . 7 ((𝜑𝑘 ∈ (0...3)) → ℝ ∈ V)
12685adantlr 714 . . . . . . 7 (((𝜑𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0) ∈ (0[,]+∞))
127 eqidd 2825 . . . . . . 7 ((𝜑𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)))
128 eqidd 2825 . . . . . . 7 ((𝜑𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)))
129125, 34, 126, 127, 128ofrfval2 7423 . . . . . 6 ((𝜑𝑘 ∈ (0...3)) → ((𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)))
130124, 129mpbird 260 . . . . 5 ((𝜑𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)))
131 itg2le 24352 . . . . 5 (((𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))))
13235, 87, 130, 131syl3anc 1368 . . . 4 ((𝜑𝑘 ∈ (0...3)) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))))
133 itg2lecl 24351 . . . 4 (((𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥𝐴, (abs‘(𝐶 · 𝐵)), 0)))) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ)
13435, 77, 132, 133syl3anc 1368 . . 3 ((𝜑𝑘 ∈ (0...3)) → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ)
135134ralrimiva 3177 . 2 (𝜑 → ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ)
136 eqidd 2825 . . 3 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)))
137 eqidd 2825 . . 3 ((𝜑𝑥𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) = (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))))
138136, 137, 10isibl2 24379 . 2 (𝜑 → ((𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1 ↔ ((𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ)))
1396, 135, 138mpbir2and 712 1 (𝜑 → (𝑥𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1538  wcel 2115  wne 3014  wral 3133  Vcvv 3480  ifcif 4450  {csn 4550   class class class wbr 5053  cmpt 5133   × cxp 5541  wf 6341  cfv 6345  (class class class)co 7151  f cof 7403  r cofr 7404  cc 10535  cr 10536  0cc0 10537  1c1 10538  ici 10539   · cmul 10542  +∞cpnf 10672  *cxr 10674  cle 10676   / cdiv 11297  3c3 11692  0cn0 11896  cz 11980  [,)cico 12739  [,]cicc 12740  ...cfz 12896  cexp 13436  cre 14458  abscabs 14595  MblFncmbf 24227  2citg2 24229  𝐿1cibl 24230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-inf2 9103  ax-cc 9857  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615  ax-addf 10616  ax-mulf 10617
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-disj 5019  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-isom 6354  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7405  df-ofr 7406  df-om 7577  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-2o 8101  df-oadd 8104  df-omul 8105  df-er 8287  df-map 8406  df-pm 8407  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fsupp 8833  df-fi 8874  df-sup 8905  df-inf 8906  df-oi 8973  df-dju 9329  df-card 9367  df-acn 9370  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11637  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705  df-9 11706  df-n0 11897  df-z 11981  df-dec 12098  df-uz 12243  df-q 12348  df-rp 12389  df-xneg 12506  df-xadd 12507  df-xmul 12508  df-ioo 12741  df-ioc 12742  df-ico 12743  df-icc 12744  df-fz 12897  df-fzo 13040  df-fl 13168  df-seq 13376  df-exp 13437  df-hash 13698  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-clim 14847  df-rlim 14848  df-sum 15045  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-starv 16582  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-unif 16590  df-hom 16591  df-cco 16592  df-rest 16698  df-topn 16699  df-0g 16717  df-gsum 16718  df-topgen 16719  df-pt 16720  df-prds 16723  df-xrs 16777  df-qtop 16782  df-imas 16783  df-xps 16785  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-submnd 17959  df-mulg 18227  df-cntz 18449  df-cmn 18910  df-psmet 20092  df-xmet 20093  df-met 20094  df-bl 20095  df-mopn 20096  df-cnfld 20101  df-top 21508  df-topon 21525  df-topsp 21547  df-bases 21560  df-cn 21841  df-cnp 21842  df-cmp 22001  df-tx 22176  df-hmeo 22369  df-xms 22936  df-ms 22937  df-tms 22938  df-cncf 23492  df-ovol 24077  df-vol 24078  df-mbf 24232  df-itg1 24233  df-itg2 24234  df-ibl 24235  df-0p 24283
This theorem is referenced by:  itgmulc2lem1  24444  itgmulc2lem2  24445  itgmulc2  24446  itgabs  24447  circlemeth  31996  3factsumint1  39284  fourierdlem83  42784  fourierdlem95  42796  sqwvfoura  42823  sqwvfourb  42824
  Copyright terms: Public domain W3C validator