Metamath Proof Explorer

Theorem xrletr

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

Ref Expression
Assertion xrletr ⊢ 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 2 adantr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A ≤ B → B ≤ C ↔ B < C ∨ B = C
4 xrlelttr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A ≤ B ∧ B < C → A < C
5 xrltle ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → A < C → A ≤ C
6 5 3adant2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < C → A ≤ C
7 4 6 syld ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A ≤ B ∧ B < C → A ≤ C
8 7 expdimp ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A ≤ B → B < C → A ≤ C
9 breq2 ⊢ B = C → A ≤ B ↔ A ≤ C
10 9 biimpcd ⊢ A ≤ B → B = C → A ≤ C
11 10 adantl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A ≤ B → B = C → A ≤ C
12 8 11 jaod ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A ≤ B → B < C ∨ B = C → A ≤ C
13 3 12 sylbid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A ≤ B → B ≤ C → A ≤ C
14 13 expimpd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A ≤ B ∧ B ≤ C → A ≤ C