Theorem leord2

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	leord2	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 ≤ 𝐷 ↔ 𝑁 ≤ 𝑀 ) )

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	leord1	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 ≤ 𝐷 ↔ - 𝑀 ≤ - 𝑁 ) )
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		leneg	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑁 ≤ 𝑀 ↔ - 𝑀 ≤ - 𝑁 ) )
30	24 28 29	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝑁 ≤ 𝑀 ↔ - 𝑀 ≤ - 𝑁 ) )
31	20 30	bitr4d	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 ≤ 𝐷 ↔ 𝑁 ≤ 𝑀 ) )