Theorem xrsdsreclblem

Description: Lemma for xrsdsreclb . (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypothesis	xrsds.d	⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
Assertion	xrsdsreclblem	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrsds.d	⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
2		necom	⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
3		xrleltne	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴 ) )
4		mnfxr	⊢ -∞ ∈ ℝ*
5	4	a1i	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → -∞ ∈ ℝ* )
6		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → 𝐴 ∈ ℝ* )
7		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → 𝐵 ∈ ℝ* )
8		pnfnre	⊢ +∞ ∉ ℝ
9	8	neli	⊢ ¬ +∞ ∈ ℝ
10		mnfle	⊢ ( 𝐴 ∈ ℝ* → -∞ ≤ 𝐴 )
11	6 10	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → -∞ ≤ 𝐴 )
12		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → 𝐴 < 𝐵 )
13	5 6 7 11 12	xrlelttrd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → -∞ < 𝐵 )
14		xrltne	⊢ ( ( -∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ -∞ < 𝐵 ) → 𝐵 ≠ -∞ )
15	5 7 13 14	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → 𝐵 ≠ -∞ )
16		xaddpnf1	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → ( 𝐵 +e +∞ ) = +∞ )
17	7 15 16	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( 𝐵 +e +∞ ) = +∞ )
18	17	eleq1d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( ( 𝐵 +e +∞ ) ∈ ℝ ↔ +∞ ∈ ℝ ) )
19	9 18	mtbiri	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ¬ ( 𝐵 +e +∞ ) ∈ ℝ )
20		ngtmnft	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )
21	6 20	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )
22		simpr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( 𝐵 +e -e 𝐴 ) ∈ ℝ )
23		xnegeq	⊢ ( 𝐴 = -∞ → -e 𝐴 = -e -∞ )
24		xnegmnf	⊢ -e -∞ = +∞
25	23 24	eqtrdi	⊢ ( 𝐴 = -∞ → -e 𝐴 = +∞ )
26	25	oveq2d	⊢ ( 𝐴 = -∞ → ( 𝐵 +e -e 𝐴 ) = ( 𝐵 +e +∞ ) )
27	26	eleq1d	⊢ ( 𝐴 = -∞ → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ ↔ ( 𝐵 +e +∞ ) ∈ ℝ ) )
28	22 27	syl5ibcom	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( 𝐴 = -∞ → ( 𝐵 +e +∞ ) ∈ ℝ ) )
29	21 28	sylbird	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( ¬ -∞ < 𝐴 → ( 𝐵 +e +∞ ) ∈ ℝ ) )
30	19 29	mt3d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → -∞ < 𝐴 )
31		xrre2	⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( -∞ < 𝐴 ∧ 𝐴 < 𝐵 ) ) → 𝐴 ∈ ℝ )
32	5 6 7 30 12 31	syl32anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → 𝐴 ∈ ℝ )
33		pnfxr	⊢ +∞ ∈ ℝ*
34	33	a1i	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → +∞ ∈ ℝ* )
35	6	xnegcld	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → -e 𝐴 ∈ ℝ* )
36		xnegpnf	⊢ -e +∞ = -∞
37		pnfge	⊢ ( 𝐵 ∈ ℝ* → 𝐵 ≤ +∞ )
38	7 37	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → 𝐵 ≤ +∞ )
39	6 7 34 12 38	xrltletrd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → 𝐴 < +∞ )
40		xltnegi	⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐴 < +∞ ) → -e +∞ < -e 𝐴 )
41	6 34 39 40	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → -e +∞ < -e 𝐴 )
42	36 41	eqbrtrrid	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → -∞ < -e 𝐴 )
43		xrltne	⊢ ( ( -∞ ∈ ℝ* ∧ -e 𝐴 ∈ ℝ* ∧ -∞ < -e 𝐴 ) → -e 𝐴 ≠ -∞ )
44	5 35 42 43	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → -e 𝐴 ≠ -∞ )
45		xaddpnf2	⊢ ( ( -e 𝐴 ∈ ℝ* ∧ -e 𝐴 ≠ -∞ ) → ( +∞ +e -e 𝐴 ) = +∞ )
46	35 44 45	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( +∞ +e -e 𝐴 ) = +∞ )
47	46	eleq1d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( ( +∞ +e -e 𝐴 ) ∈ ℝ ↔ +∞ ∈ ℝ ) )
48	9 47	mtbiri	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ¬ ( +∞ +e -e 𝐴 ) ∈ ℝ )
49		nltpnft	⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 = +∞ ↔ ¬ 𝐵 < +∞ ) )
50	7 49	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( 𝐵 = +∞ ↔ ¬ 𝐵 < +∞ ) )
51		oveq1	⊢ ( 𝐵 = +∞ → ( 𝐵 +e -e 𝐴 ) = ( +∞ +e -e 𝐴 ) )
52	51	eleq1d	⊢ ( 𝐵 = +∞ → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ ↔ ( +∞ +e -e 𝐴 ) ∈ ℝ ) )
53	22 52	syl5ibcom	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( 𝐵 = +∞ → ( +∞ +e -e 𝐴 ) ∈ ℝ ) )
54	50 53	sylbird	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( ¬ 𝐵 < +∞ → ( +∞ +e -e 𝐴 ) ∈ ℝ ) )
55	48 54	mt3d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → 𝐵 < +∞ )
56		xrre2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < +∞ ) ) → 𝐵 ∈ ℝ )
57	6 7 34 12 55 56	syl32anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → 𝐵 ∈ ℝ )
58	32 57	jca	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +e -e 𝐴 ) ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
59	58	ex	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
60	59	3expia	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
61	60	3adant3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
62	3 61	sylbird	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 ≠ 𝐴 → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
63	2 62	biimtrid	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ≠ 𝐵 → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
64	63	3exp	⊢ ( 𝐴 ∈ ℝ* → ( 𝐵 ∈ ℝ* → ( 𝐴 ≤ 𝐵 → ( 𝐴 ≠ 𝐵 → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) ) ) )
65	64	com34	⊢ ( 𝐴 ∈ ℝ* → ( 𝐵 ∈ ℝ* → ( 𝐴 ≠ 𝐵 → ( 𝐴 ≤ 𝐵 → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) ) ) )
66	65	3imp1	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐵 +e -e 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )