iblconst

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

		Ref	Expression
	Assertion	iblconst	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to A \times \{B\} \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		fconstmpt	$⊢ A \times \{B\} = (x \in A ⟼ B)$
2		mbfconst	$⊢ (A \in dom vol \land B \in ℂ) \to A \times \{B\} \in MblFn$
3	2	3adant2	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to A \times \{B\} \in MblFn$
4	1 3	eqeltrrid	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to (x \in A ⟼ B) \in MblFn$
5		ifan	$⊢ if ((x \in A \land 0 \leq ℜ (\frac{B}{i^{k}})), ℜ (\frac{B}{i^{k}}), 0) = if (x \in A, if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0), 0)$
6	5	mpteq2i	$⊢ (x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{B}{i^{k}})), ℜ (\frac{B}{i^{k}}), 0)) = (x \in ℝ ⟼ if (x \in A, if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0), 0))$
7	6	fveq2i	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{B}{i^{k}})), ℜ (\frac{B}{i^{k}}), 0))) = \int^{2} ((x \in ℝ ⟼ if (x \in A, if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0), 0)))$
8		simpl1	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to A \in dom vol$
9		simpl2	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to vol (A) \in ℝ$
10		simpl3	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to B \in ℂ$
11		ax-icn	$⊢ i \in ℂ$
12		ine0	$⊢ i \neq 0$
13		elfzelz	$⊢ k \in (0 \dots 3) \to k \in ℤ$
14	13	adantl	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to k \in ℤ$
15		expclz	$⊢ (i \in ℂ \land i \neq 0 \land k \in ℤ) \to i^{k} \in ℂ$
16	11 12 14 15	mp3an12i	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to i^{k} \in ℂ$
17		expne0i	$⊢ (i \in ℂ \land i \neq 0 \land k \in ℤ) \to i^{k} \neq 0$
18	11 12 14 17	mp3an12i	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to i^{k} \neq 0$
19	10 16 18	divcld	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to \frac{B}{i^{k}} \in ℂ$
20	19	recld	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to ℜ (\frac{B}{i^{k}}) \in ℝ$
21		0re	$⊢ 0 \in ℝ$
22		ifcl	$⊢ (ℜ (\frac{B}{i^{k}}) \in ℝ \land 0 \in ℝ) \to if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) \in ℝ$
23	20 21 22	sylancl	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) \in ℝ$
24		max1	$⊢ (0 \in ℝ \land ℜ (\frac{B}{i^{k}}) \in ℝ) \to 0 \leq if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0)$
25	21 20 24	sylancr	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to 0 \leq if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0)$
26		elrege0	$⊢ if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) \in [0, +∞) \leftrightarrow (if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) \in ℝ \land 0 \leq if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0))$
27	23 25 26	sylanbrc	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) \in [0, +∞)$
28		itg2const	$⊢ (A \in dom vol \land vol (A) \in ℝ \land if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0), 0))) = if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) vol (A)$
29	8 9 27 28	syl3anc	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to \int^{2} ((x \in ℝ ⟼ if (x \in A, if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0), 0))) = if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) vol (A)$
30	7 29	eqtrid	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{B}{i^{k}})), ℜ (\frac{B}{i^{k}}), 0))) = if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) vol (A)$
31	23 9	remulcld	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to if (0 \leq ℜ (\frac{B}{i^{k}}), ℜ (\frac{B}{i^{k}}), 0) vol (A) \in ℝ$
32	30 31	eqeltrd	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land k \in (0 \dots 3)) \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{B}{i^{k}})), ℜ (\frac{B}{i^{k}}), 0))) \in ℝ$
33	32	ralrimiva	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to \forall k \in (0 \dots 3) \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{B}{i^{k}})), ℜ (\frac{B}{i^{k}}), 0))) \in ℝ$
34		eqidd	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to (x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{B}{i^{k}})), ℜ (\frac{B}{i^{k}}), 0)) = (x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{B}{i^{k}})), ℜ (\frac{B}{i^{k}}), 0))$
35		eqidd	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land x \in A) \to ℜ (\frac{B}{i^{k}}) = ℜ (\frac{B}{i^{k}})$
36		simpl3	$⊢ ((A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \land x \in A) \to B \in ℂ$
37	34 35 36	isibl2	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to ((x \in A ⟼ B) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ B) \in MblFn \land \forall k \in (0 \dots 3) \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (\frac{B}{i^{k}})), ℜ (\frac{B}{i^{k}}), 0))) \in ℝ))$
38	4 33 37	mpbir2and	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to (x \in A ⟼ B) \in 𝐿^{1}$
39	1 38	eqeltrid	$⊢ (A \in dom vol \land vol (A) \in ℝ \land B \in ℂ) \to A \times \{B\} \in 𝐿^{1}$

Metamath Proof Explorer

Theorem iblconst

Proof