Metamath Proof Explorer


Theorem iblidicc

Description: The identity function is integrable on any closed interval. (Contributed by Thierry Arnoux, 13-Dec-2021)

Ref Expression
Hypotheses iblidicc.a ( 𝜑𝐴 ∈ ℝ )
iblidicc.b ( 𝜑𝐵 ∈ ℝ )
Assertion iblidicc ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑥 ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 iblidicc.a ( 𝜑𝐴 ∈ ℝ )
2 iblidicc.b ( 𝜑𝐵 ∈ ℝ )
3 iccssre ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
4 1 2 3 syl2anc ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
5 ax-resscn ℝ ⊆ ℂ
6 4 5 sstrdi ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
7 ssid ℂ ⊆ ℂ
8 cncfmptid ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
9 6 7 8 sylancl ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
10 cniccibl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑥 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑥 ) ∈ 𝐿1 )
11 1 2 9 10 syl3anc ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑥 ) ∈ 𝐿1 )