This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnicciblnc

Description: Choice-free proof of cniccibl . (Contributed by Brendan Leahy, 2-Nov-2017)

		Ref	Expression
	Assertion	cnicciblnc	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to F \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		iccmbl	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \in dom vol$
2		cnmbf	$⊢ ([A, B] \in dom vol \land F : [A, B] \underset{cn}{⟶} ℂ) \to F \in MblFn$
3	1 2	stoic3	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to F \in MblFn$
4		simp3	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to F : [A, B] \underset{cn}{⟶} ℂ$
5		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to F : [A, B] ⟶ ℂ$
6		fdm	$⊢ F : [A, B] ⟶ ℂ \to dom F = [A, B]$
7	4 5 6	3syl	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to dom F = [A, B]$
8	7	fveq2d	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to vol (dom F) = vol ([A, B])$
9		iccvolcl	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B]) \in ℝ$
10	9	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to vol ([A, B]) \in ℝ$
11	8 10	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to vol (dom F) \in ℝ$
12		cniccbdd	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x$
13	7	raleqdv	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to (\forall y \in dom F \|F (y)\| \leq x \leftrightarrow \forall y \in [A, B] \|F (y)\| \leq x)$
14	13	rexbidv	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to (\exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x \leftrightarrow \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x)$
15	12 14	mpbird	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x$
16		bddiblnc	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \in 𝐿^{1}$
17	3 11 15 16	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to F \in 𝐿^{1}$