xrsdsreclblem

		Ref	Expression
	Hypothesis	xrsds.d	$⊢ D = dist (ℝ_{𝑠}^{*})$
	Assertion	xrsdsreclblem	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \land A \leq B) \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ))$

Proof

Step	Hyp	Ref	Expression
1		xrsds.d	$⊢ D = dist (ℝ_{𝑠}^{*})$
2		necom	$⊢ A \neq B \leftrightarrow B \neq A$
3		xrleltne	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A < B \leftrightarrow B \neq A)$
4		mnfxr	$⊢ −∞ \in ℝ^{*}$
5	4	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to −∞ \in ℝ^{*}$
6		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to A \in ℝ^{*}$
7		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to B \in ℝ^{*}$
8		pnfnre	$⊢ +∞ \notin ℝ$
9	8	neli	$⊢ \neg +∞ \in ℝ$
10		mnfle	$⊢ A \in ℝ^{*} \to −∞ \leq A$
11	6 10	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to −∞ \leq A$
12		simpl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to A < B$
13	5 6 7 11 12	xrlelttrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to −∞ < B$
14		xrltne	$⊢ (−∞ \in ℝ^{} \land B \in ℝ^{} \land −∞ < B) \to B \neq −∞$
15	5 7 13 14	syl3anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to B \neq −∞$
16		xaddpnf1	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to B +_{𝑒} +∞ = +∞$
17	7 15 16	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to B +_{𝑒} +∞ = +∞$
18	17	eleq1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to (B +_{𝑒} +∞ \in ℝ \leftrightarrow +∞ \in ℝ)$
19	9 18	mtbiri	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to \neg B +_{𝑒} +∞ \in ℝ$
20		ngtmnft	$⊢ A \in ℝ^{*} \to (A = −∞ \leftrightarrow \neg −∞ < A)$
21	6 20	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to (A = −∞ \leftrightarrow \neg −∞ < A)$
22		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to B +_{𝑒} (- A) \in ℝ$
23		xnegeq	$⊢ A = −∞ \to - A = - −∞$
24		xnegmnf	$⊢ - −∞ = +∞$
25	23 24	eqtrdi	$⊢ A = −∞ \to - A = +∞$
26	25	oveq2d	$⊢ A = −∞ \to B +_{𝑒} (- A) = B +_{𝑒} +∞$
27	26	eleq1d	$⊢ A = −∞ \to (B +_{𝑒} (- A) \in ℝ \leftrightarrow B +_{𝑒} +∞ \in ℝ)$
28	22 27	syl5ibcom	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to (A = −∞ \to B +_{𝑒} +∞ \in ℝ)$
29	21 28	sylbird	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to (\neg −∞ < A \to B +_{𝑒} +∞ \in ℝ)$
30	19 29	mt3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to −∞ < A$
31		xrre2	$⊢ ((−∞ \in ℝ^{} \land A \in ℝ^{} \land B \in ℝ^{*}) \land (−∞ < A \land A < B)) \to A \in ℝ$
32	5 6 7 30 12 31	syl32anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to A \in ℝ$
33		pnfxr	$⊢ +∞ \in ℝ^{*}$
34	33	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to +∞ \in ℝ^{*}$
35	6	xnegcld	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to - A \in ℝ^{*}$
36		xnegpnf	$⊢ - +∞ = −∞$
37		pnfge	$⊢ B \in ℝ^{*} \to B \leq +∞$
38	7 37	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to B \leq +∞$
39	6 7 34 12 38	xrltletrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to A < +∞$
40		xltnegi	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{} \land A < +∞) \to - +∞ < - A$
41	6 34 39 40	syl3anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to - +∞ < - A$
42	36 41	eqbrtrrid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to −∞ < - A$
43		xrltne	$⊢ (−∞ \in ℝ^{} \land - A \in ℝ^{} \land −∞ < - A) \to - A \neq −∞$
44	5 35 42 43	syl3anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to - A \neq −∞$
45		xaddpnf2	$⊢ (- A \in ℝ^{*} \land - A \neq −∞) \to +∞ +_{𝑒} (- A) = +∞$
46	35 44 45	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to +∞ +_{𝑒} (- A) = +∞$
47	46	eleq1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to (+∞ +_{𝑒} (- A) \in ℝ \leftrightarrow +∞ \in ℝ)$
48	9 47	mtbiri	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to \neg +∞ +_{𝑒} (- A) \in ℝ$
49		nltpnft	$⊢ B \in ℝ^{*} \to (B = +∞ \leftrightarrow \neg B < +∞)$
50	7 49	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to (B = +∞ \leftrightarrow \neg B < +∞)$
51		oveq1	$⊢ B = +∞ \to B +_{𝑒} (- A) = +∞ +_{𝑒} (- A)$
52	51	eleq1d	$⊢ B = +∞ \to (B +_{𝑒} (- A) \in ℝ \leftrightarrow +∞ +_{𝑒} (- A) \in ℝ)$
53	22 52	syl5ibcom	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to (B = +∞ \to +∞ +_{𝑒} (- A) \in ℝ)$
54	50 53	sylbird	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to (\neg B < +∞ \to +∞ +_{𝑒} (- A) \in ℝ)$
55	48 54	mt3d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to B < +∞$
56		xrre2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land +∞ \in ℝ^{*}) \land (A < B \land B < +∞)) \to B \in ℝ$
57	6 7 34 12 55 56	syl32anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to B \in ℝ$
58	32 57	jca	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A < B) \land B +_{𝑒} (- A) \in ℝ) \to (A \in ℝ \land B \in ℝ)$
59	58	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ))$
60	59	3expia	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ)))$
61	60	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A < B \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ)))$
62	3 61	sylbird	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (B \neq A \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ)))$
63	2 62	syl5bi	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A \neq B \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ)))$
64	63	3exp	$⊢ A \in ℝ^{} \to (B \in ℝ^{} \to (A \leq B \to (A \neq B \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ)))))$
65	64	com34	$⊢ A \in ℝ^{} \to (B \in ℝ^{} \to (A \neq B \to (A \leq B \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ)))))$
66	65	3imp1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \land A \leq B) \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ))$

Metamath Proof Explorer

Theorem xrsdsreclblem

Proof