Description: If a number is less than another number, and the other number is less than or equal to a third number, the first number is less than the third number. (Contributed by Alexander van der Vekens, 24-Mar-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lelttrdi.r | ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) | |
| lelttrdi.l | ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 ) | ||
| Assertion | lelttrdi | ⊢ ( 𝜑 → ( 𝐴 < 𝐵 → 𝐴 < 𝐶 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lelttrdi.r | ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) | |
| 2 | lelttrdi.l | ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 ) | |
| 3 | 1 | simp1d | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
| 4 | 3 | adantr | ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ ) |
| 5 | 1 | simp2d | ⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
| 6 | 5 | adantr | ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ ) |
| 7 | 1 | simp3d | ⊢ ( 𝜑 → 𝐶 ∈ ℝ ) |
| 8 | 7 | adantr | ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐶 ∈ ℝ ) |
| 9 | simpr | ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 ) | |
| 10 | 2 | adantr | ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐵 ≤ 𝐶 ) |
| 11 | 4 6 8 9 10 | ltletrd | ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐶 ) |
| 12 | 11 | ex | ⊢ ( 𝜑 → ( 𝐴 < 𝐵 → 𝐴 < 𝐶 ) ) |