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∈01⟼ifx=0+∞−log⁡x
Assertion xrge0iifcv ⊢X∈01→F⁡X=−log⁡X

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢F=x∈01⟼ifx=0+∞−log⁡x
2 iocssicc ⊢01⊆01
3 2 sseli ⊢X∈01→X∈01
4 eqeq1 ⊢x=X→x=0↔X=0
5 fveq2 ⊢x=X→log⁡x=log⁡X
6 5 negeqd ⊢x=X→−log⁡x=−log⁡X
7 4 6 ifbieq2d ⊢x=X→ifx=0+∞−log⁡x=ifX=0+∞−log⁡X
8 pnfex ⊢+∞∈V
9 negex ⊢−log⁡X∈V
10 8 9 ifex ⊢ifX=0+∞−log⁡X∈V
11 7 1 10 fvmpt ⊢X∈01→F⁡X=ifX=0+∞−log⁡X
12 3 11 syl ⊢X∈01→F⁡X=ifX=0+∞−log⁡X
13 0xr ⊢0∈ℝ*
14 1re ⊢1∈ℝ
15 elioc2 ⊢0∈ℝ*∧1∈ℝ→X∈01↔X∈ℝ∧0<X∧X≤1
16 13 14 15 mp2an ⊢X∈01↔X∈ℝ∧0<X∧X≤1
17 16 simp2bi ⊢X∈01→0<X
18 17 gt0ne0d ⊢X∈01→X≠0
19 18 neneqd ⊢X∈01→¬X=0
20 19 iffalsed ⊢X∈01→ifX=0+∞−log⁡X=−log⁡X
21 12 20 eqtrd ⊢X∈01→F⁡X=−log⁡X