Theorem iblconst

Description: A constant function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

	Ref	Expression
Assertion	iblconst	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		mbfconst	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ MblFn )
3	2	3adant2	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ MblFn )
4	1 3	eqeltrrid	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
5		ifan	⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
6	5	mpteq2i	⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
7	6	fveq2i	⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ) )
8		simpl1	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝐴 ∈ dom vol )
9		simpl2	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( vol ‘ 𝐴 ) ∈ ℝ )
10		simpl3	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝐵 ∈ ℂ )
11		ax-icn	⊢ i ∈ ℂ
12		ine0	⊢ i ≠ 0
13		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
14	13	adantl	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝑘 ∈ ℤ )
15		expclz	⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ∈ ℂ )
16	11 12 14 15	mp3an12i	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( i ↑ 𝑘 ) ∈ ℂ )
17		expne0i	⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
18	11 12 14 17	mp3an12i	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( i ↑ 𝑘 ) ≠ 0 )
19	10 16 18	divcld	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝐵 / ( i ↑ 𝑘 ) ) ∈ ℂ )
20	19	recld	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ ℝ )
21		0re	⊢ 0 ∈ ℝ
22		ifcl	⊢ ( ( ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
23	20 21 22	sylancl	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
24		max1	⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) )
25	21 20 24	sylancr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) )
26		elrege0	⊢ ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) ↔ ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ ∧ 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
27	23 25 26	sylanbrc	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
28		itg2const	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ) ) = ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) · ( vol ‘ 𝐴 ) ) )
29	8 9 27 28	syl3anc	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ) ) = ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) · ( vol ‘ 𝐴 ) ) )
30	7 29	eqtrid	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) · ( vol ‘ 𝐴 ) ) )
31	23 9	remulcld	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) · ( vol ‘ 𝐴 ) ) ∈ ℝ )
32	30 31	eqeltrd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
33	32	ralrimiva	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
34		eqidd	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
35		eqidd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
36		simpl3	⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
37	34 35 36	isibl2	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
38	4 33 37	mpbir2and	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
39	1 38	eqeltrid	⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ 𝐿1 )