Metamath Proof Explorer


Theorem ltord2

Description: Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Hypotheses ltord.1 ( 𝑥 = 𝑦𝐴 = 𝐵 )
ltord.2 ( 𝑥 = 𝐶𝐴 = 𝑀 )
ltord.3 ( 𝑥 = 𝐷𝐴 = 𝑁 )
ltord.4 𝑆 ⊆ ℝ
ltord.5 ( ( 𝜑𝑥𝑆 ) → 𝐴 ∈ ℝ )
ltord2.6 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 < 𝑦𝐵 < 𝐴 ) )
Assertion ltord2 ( ( 𝜑 ∧ ( 𝐶𝑆𝐷𝑆 ) ) → ( 𝐶 < 𝐷𝑁 < 𝑀 ) )

Proof

Step Hyp Ref Expression
1 ltord.1 ( 𝑥 = 𝑦𝐴 = 𝐵 )
2 ltord.2 ( 𝑥 = 𝐶𝐴 = 𝑀 )
3 ltord.3 ( 𝑥 = 𝐷𝐴 = 𝑁 )
4 ltord.4 𝑆 ⊆ ℝ
5 ltord.5 ( ( 𝜑𝑥𝑆 ) → 𝐴 ∈ ℝ )
6 ltord2.6 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 < 𝑦𝐵 < 𝐴 ) )
7 1 negeqd ( 𝑥 = 𝑦 → - 𝐴 = - 𝐵 )
8 2 negeqd ( 𝑥 = 𝐶 → - 𝐴 = - 𝑀 )
9 3 negeqd ( 𝑥 = 𝐷 → - 𝐴 = - 𝑁 )
10 5 renegcld ( ( 𝜑𝑥𝑆 ) → - 𝐴 ∈ ℝ )
11 5 ralrimiva ( 𝜑 → ∀ 𝑥𝑆 𝐴 ∈ ℝ )
12 1 eleq1d ( 𝑥 = 𝑦 → ( 𝐴 ∈ ℝ ↔ 𝐵 ∈ ℝ ) )
13 12 rspccva ( ( ∀ 𝑥𝑆 𝐴 ∈ ℝ ∧ 𝑦𝑆 ) → 𝐵 ∈ ℝ )
14 11 13 sylan ( ( 𝜑𝑦𝑆 ) → 𝐵 ∈ ℝ )
15 14 adantrl ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝐵 ∈ ℝ )
16 5 adantrr ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → 𝐴 ∈ ℝ )
17 ltneg ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ - 𝐴 < - 𝐵 ) )
18 15 16 17 syl2anc ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝐵 < 𝐴 ↔ - 𝐴 < - 𝐵 ) )
19 6 18 sylibd ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 < 𝑦 → - 𝐴 < - 𝐵 ) )
20 7 8 9 4 10 19 ltord1 ( ( 𝜑 ∧ ( 𝐶𝑆𝐷𝑆 ) ) → ( 𝐶 < 𝐷 ↔ - 𝑀 < - 𝑁 ) )
21 3 eleq1d ( 𝑥 = 𝐷 → ( 𝐴 ∈ ℝ ↔ 𝑁 ∈ ℝ ) )
22 21 rspccva ( ( ∀ 𝑥𝑆 𝐴 ∈ ℝ ∧ 𝐷𝑆 ) → 𝑁 ∈ ℝ )
23 11 22 sylan ( ( 𝜑𝐷𝑆 ) → 𝑁 ∈ ℝ )
24 23 adantrl ( ( 𝜑 ∧ ( 𝐶𝑆𝐷𝑆 ) ) → 𝑁 ∈ ℝ )
25 2 eleq1d ( 𝑥 = 𝐶 → ( 𝐴 ∈ ℝ ↔ 𝑀 ∈ ℝ ) )
26 25 rspccva ( ( ∀ 𝑥𝑆 𝐴 ∈ ℝ ∧ 𝐶𝑆 ) → 𝑀 ∈ ℝ )
27 11 26 sylan ( ( 𝜑𝐶𝑆 ) → 𝑀 ∈ ℝ )
28 27 adantrr ( ( 𝜑 ∧ ( 𝐶𝑆𝐷𝑆 ) ) → 𝑀 ∈ ℝ )
29 ltneg ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑁 < 𝑀 ↔ - 𝑀 < - 𝑁 ) )
30 24 28 29 syl2anc ( ( 𝜑 ∧ ( 𝐶𝑆𝐷𝑆 ) ) → ( 𝑁 < 𝑀 ↔ - 𝑀 < - 𝑁 ) )
31 20 30 bitr4d ( ( 𝜑 ∧ ( 𝐶𝑆𝐷𝑆 ) ) → ( 𝐶 < 𝐷𝑁 < 𝑀 ) )