This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrleid

Description: 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrleid ( 𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ 𝐴 = 𝐴
2 1 olci ⊢ ( 𝐴 < 𝐴 ∨ 𝐴 = 𝐴 )
3 xrleloe ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ 𝐴 ↔ ( 𝐴 < 𝐴 ∨ 𝐴 = 𝐴 ) ) )
4 2 3 mpbiri ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → 𝐴 ≤ 𝐴 )
5 4 anidms ⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴 )