Metamath Proof Explorer

Theorem xrge0iifcv

Description: The defined function's value in the real. (Contributed by Thierry Arnoux, 1-Apr-2017)

Ref Expression
Hypothesis xrge0iifhmeo.1 
|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
Assertion xrge0iifcv 
|- ( X e. ( 0 (,] 1 ) -> ( F ` X ) = -u ( log ` X ) )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 
 |-  F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
2 iocssicc 
 |-  ( 0 (,] 1 ) C_ ( 0 [,] 1 )
3 2 sseli 
 |-  ( X e. ( 0 (,] 1 ) -> X e. ( 0 [,] 1 ) )
4 eqeq1 
 |-  ( x = X -> ( x = 0 <-> X = 0 ) )
5 fveq2 
 |-  ( x = X -> ( log ` x ) = ( log ` X ) )
6 5 negeqd 
 |-  ( x = X -> -u ( log ` x ) = -u ( log ` X ) )
7 4 6 ifbieq2d 
 |-  ( x = X -> if ( x = 0 , +oo , -u ( log ` x ) ) = if ( X = 0 , +oo , -u ( log ` X ) ) )
8 pnfex 
 |-  +oo e. _V
9 negex 
 |-  -u ( log ` X ) e. _V
10 8 9 ifex 
 |-  if ( X = 0 , +oo , -u ( log ` X ) ) e. _V
11 7 1 10 fvmpt 
 |-  ( X e. ( 0 [,] 1 ) -> ( F ` X ) = if ( X = 0 , +oo , -u ( log ` X ) ) )
12 3 11 syl 
 |-  ( X e. ( 0 (,] 1 ) -> ( F ` X ) = if ( X = 0 , +oo , -u ( log ` X ) ) )
13 0xr 
 |-  0 e. RR*
14 1re 
 |-  1 e. RR
15 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( X e. ( 0 (,] 1 ) <-> ( X e. RR /\ 0 < X /\ X <_ 1 ) ) )
16 13 14 15 mp2an 
 |-  ( X e. ( 0 (,] 1 ) <-> ( X e. RR /\ 0 < X /\ X <_ 1 ) )
17 16 simp2bi 
 |-  ( X e. ( 0 (,] 1 ) -> 0 < X )
18 17 gt0ne0d 
 |-  ( X e. ( 0 (,] 1 ) -> X =/= 0 )
19 18 neneqd 
 |-  ( X e. ( 0 (,] 1 ) -> -. X = 0 )
20 19 iffalsed 
 |-  ( X e. ( 0 (,] 1 ) -> if ( X = 0 , +oo , -u ( log ` X ) ) = -u ( log ` X ) )
21 12 20 eqtrd 
 |-  ( X e. ( 0 (,] 1 ) -> ( F ` X ) = -u ( log ` X ) )