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
|- ( ph -> A e. RR )
iblidicc.b
|- ( ph -> B e. RR )
Assertion iblidicc
|- ( ph -> ( x e. ( A [,] B ) |-> x ) e. L^1 )

Proof

Step Hyp Ref Expression
1 iblidicc.a
 |-  ( ph -> A e. RR )
2 iblidicc.b
 |-  ( ph -> B e. RR )
3 iccssre
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
4 1 2 3 syl2anc
 |-  ( ph -> ( A [,] B ) C_ RR )
5 ax-resscn
 |-  RR C_ CC
6 4 5 sstrdi
 |-  ( ph -> ( A [,] B ) C_ CC )
7 ssid
 |-  CC C_ CC
8 cncfmptid
 |-  ( ( ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) )
9 6 7 8 sylancl
 |-  ( ph -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) )
10 cniccibl
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> x ) e. L^1 )
11 1 2 9 10 syl3anc
 |-  ( ph -> ( x e. ( A [,] B ) |-> x ) e. L^1 )