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

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢ F = x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x
2 iocssicc ⊢ 0 1 ⊆ 0 1
3 2 sseli ⊢ X ∈ 0 1 → X ∈ 0 1
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 → if x = 0 +∞ − log ⁡ x = if X = 0 +∞ − log ⁡ X
8 pnfex ⊢ +∞ ∈ V
9 negex ⊢ − log ⁡ X ∈ V
10 8 9 ifex ⊢ if X = 0 +∞ − log ⁡ X ∈ V
11 7 1 10 fvmpt ⊢ X ∈ 0 1 → F ⁡ X = if X = 0 +∞ − log ⁡ X
12 3 11 syl ⊢ X ∈ 0 1 → F ⁡ X = if X = 0 +∞ − log ⁡ X
13 0xr ⊢ 0 ∈ ℝ *
14 1re ⊢ 1 ∈ ℝ
15 elioc2 ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ → X ∈ 0 1 ↔ X ∈ ℝ ∧ 0 < X ∧ X ≤ 1
16 13 14 15 mp2an ⊢ X ∈ 0 1 ↔ X ∈ ℝ ∧ 0 < X ∧ X ≤ 1
17 16 simp2bi ⊢ X ∈ 0 1 → 0 < X
18 17 gt0ne0d ⊢ X ∈ 0 1 → X ≠ 0
19 18 neneqd ⊢ X ∈ 0 1 → ¬ X = 0
20 19 iffalsed ⊢ X ∈ 0 1 → if X = 0 +∞ − log ⁡ X = − log ⁡ X
21 12 20 eqtrd ⊢ X ∈ 0 1 → F ⁡ X = − log ⁡ X