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 )