Metamath Proof Explorer

Theorem areacirclem3

Description: Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017) (Revised by Brendan Leahy, 11-Jul-2018)

Ref Expression
Assertion areacirclem3 
|- ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. L^1 )

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( R e. RR -> -u R e. RR )
2 1 adantr 
 |-  ( ( R e. RR /\ 0 <_ R ) -> -u R e. RR )
3 simpl 
 |-  ( ( R e. RR /\ 0 <_ R ) -> R e. RR )
4 2cnd 
 |-  ( ( R e. RR /\ 0 <_ R ) -> 2 e. CC )
5 iccssre 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( -u R [,] R ) C_ RR )
6 2 3 5 syl2anc 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( -u R [,] R ) C_ RR )
7 ax-resscn 
 |-  RR C_ CC
8 6 7 sstrdi 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( -u R [,] R ) C_ CC )
9 ssidd 
 |-  ( ( R e. RR /\ 0 <_ R ) -> CC C_ CC )
10 cncfmptc 
 |-  ( ( 2 e. CC /\ ( -u R [,] R ) C_ CC /\ CC C_ CC ) -> ( t e. ( -u R [,] R ) |-> 2 ) e. ( ( -u R [,] R ) -cn-> CC ) )
11 4 8 9 10 syl3anc 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> 2 ) e. ( ( -u R [,] R ) -cn-> CC ) )
12 areacirclem2 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
13 11 12 mulcncf 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) )
14 cnicciblnc 
 |-  ( ( -u R e. RR /\ R e. RR /\ ( t e. ( -u R [,] R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. ( ( -u R [,] R ) -cn-> CC ) ) -> ( t e. ( -u R [,] R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. L^1 )
15 2 3 13 14 syl3anc 
 |-  ( ( R e. RR /\ 0 <_ R ) -> ( t e. ( -u R [,] R ) |-> ( 2 x. ( sqrt ` ( ( R ^ 2 ) - ( t ^ 2 ) ) ) ) ) e. L^1 )