Theorem xrge0iifcv

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

	Ref	Expression
Hypothesis	xrge0iifhmeo.1	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
Assertion	xrge0iifcv	⊢ ( 𝑋 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑋 ) = - ( log ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0iifhmeo.1	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
2		iocssicc	⊢ ( 0 (,] 1 ) ⊆ ( 0 [,] 1 )
3	2	sseli	⊢ ( 𝑋 ∈ ( 0 (,] 1 ) → 𝑋 ∈ ( 0 [,] 1 ) )
4		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 0 ↔ 𝑋 = 0 ) )
5		fveq2	⊢ ( 𝑥 = 𝑋 → ( log ‘ 𝑥 ) = ( log ‘ 𝑋 ) )
6	5	negeqd	⊢ ( 𝑥 = 𝑋 → - ( log ‘ 𝑥 ) = - ( log ‘ 𝑋 ) )
7	4 6	ifbieq2d	⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) )
8		pnfex	⊢ +∞ ∈ V
9		negex	⊢ - ( log ‘ 𝑋 ) ∈ V
10	8 9	ifex	⊢ if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) ∈ V
11	7 1 10	fvmpt	⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 𝑋 ) = if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) )
12	3 11	syl	⊢ ( 𝑋 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑋 ) = if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) )
13		0xr	⊢ 0 ∈ ℝ*
14		1re	⊢ 1 ∈ ℝ
15		elioc2	⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝑋 ∈ ( 0 (,] 1 ) ↔ ( 𝑋 ∈ ℝ ∧ 0 < 𝑋 ∧ 𝑋 ≤ 1 ) ) )
16	13 14 15	mp2an	⊢ ( 𝑋 ∈ ( 0 (,] 1 ) ↔ ( 𝑋 ∈ ℝ ∧ 0 < 𝑋 ∧ 𝑋 ≤ 1 ) )
17	16	simp2bi	⊢ ( 𝑋 ∈ ( 0 (,] 1 ) → 0 < 𝑋 )
18	17	gt0ne0d	⊢ ( 𝑋 ∈ ( 0 (,] 1 ) → 𝑋 ≠ 0 )
19	18	neneqd	⊢ ( 𝑋 ∈ ( 0 (,] 1 ) → ¬ 𝑋 = 0 )
20	19	iffalsed	⊢ ( 𝑋 ∈ ( 0 (,] 1 ) → if ( 𝑋 = 0 , +∞ , - ( log ‘ 𝑋 ) ) = - ( log ‘ 𝑋 ) )
21	12 20	eqtrd	⊢ ( 𝑋 ∈ ( 0 (,] 1 ) → ( 𝐹 ‘ 𝑋 ) = - ( log ‘ 𝑋 ) )