Metamath Proof Explorer

Theorem xrltletr

Description: Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion xrltletr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < B ∧ B ≤ C → A < C

Proof

Step Hyp Ref Expression
1 xrleloe ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B ≤ C ↔ B < C ∨ B = C
2 1 3adant1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → B ≤ C ↔ B < C ∨ B = C
3 xrlttr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < B ∧ B < C → A < C
4 3 expcomd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → B < C → A < B → A < C
5 breq2 ⊢ B = C → A < B ↔ A < C
6 5 biimpd ⊢ B = C → A < B → A < C
7 6 a1i ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → B = C → A < B → A < C
8 4 7 jaod ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → B < C ∨ B = C → A < B → A < C
9 2 8 sylbid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → B ≤ C → A < B → A < C
10 9 impcomd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < B ∧ B ≤ C → A < C