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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐹 ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 iccmbl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ dom vol )
2 cnmbf ⊢ ( ( ( 𝐴 [,] 𝐵 ) ∈ dom vol ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐹 ∈ MblFn )
3 1 2 stoic3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐹 ∈ MblFn )
4 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
5 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
6 fdm ⊢ ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ → dom 𝐹 = ( 𝐴 [,] 𝐵 ) )
7 4 5 6 3syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → dom 𝐹 = ( 𝐴 [,] 𝐵 ) )
8 7 fveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( vol ‘ dom 𝐹 ) = ( vol ‘ ( 𝐴 [,] 𝐵 ) ) )
9 iccvolcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ )
10 9 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ )
11 8 10 eqeltrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( vol ‘ dom 𝐹 ) ∈ ℝ )
12 cniccbdd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
13 7 raleqdv ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) )
14 13 rexbidv ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) )
15 12 14 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
16 bddiblnc ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 𝐹 ∈ 𝐿1 )
17 3 11 15 16 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → 𝐹 ∈ 𝐿1 )