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 )