xrsdsreclb

Description: The metric of the extended real number structure is only real when both arguments are real. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		xrsds.d	$⊢ D = dist (ℝ_{𝑠}^{*})$
2	1	xrsdsval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A D B = if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B))$
3	2	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \to A D B = if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B))$
4	3	eleq1d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \to (A D B \in ℝ \leftrightarrow if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \in ℝ)$
5		eleq1	$⊢ B +_{𝑒} (- A) = if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \to (B +_{𝑒} (- A) \in ℝ \leftrightarrow if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \in ℝ)$
6	5	imbi1d	$⊢ B +_{𝑒} (- A) = if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \to ((B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ)) \leftrightarrow (if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \in ℝ \to (A \in ℝ \land B \in ℝ)))$
7		eleq1	$⊢ A +_{𝑒} (- B) = if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \to (A +_{𝑒} (- B) \in ℝ \leftrightarrow if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \in ℝ)$
8	7	imbi1d	$⊢ A +_{𝑒} (- B) = if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \to ((A +_{𝑒} (- B) \in ℝ \to (A \in ℝ \land B \in ℝ)) \leftrightarrow (if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \in ℝ \to (A \in ℝ \land B \in ℝ)))$
9	1	xrsdsreclblem	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \land A \leq B) \to (B +_{𝑒} (- A) \in ℝ \to (A \in ℝ \land B \in ℝ))$
10		xrletri	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \lor B \leq A)$
11	10	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \to (A \leq B \lor B \leq A)$
12	11	orcanai	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \land \neg A \leq B) \to B \leq A$
13		necom	$⊢ A \neq B \leftrightarrow B \neq A$
14	13	3anbi3i	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \leftrightarrow (A \in ℝ^{} \land B \in ℝ^{} \land B \neq A)$
15		3ancoma	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land B \neq A) \leftrightarrow (B \in ℝ^{} \land A \in ℝ^{} \land B \neq A)$
16	14 15	bitri	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \leftrightarrow (B \in ℝ^{} \land A \in ℝ^{} \land B \neq A)$
17	1	xrsdsreclblem	$⊢ ((B \in ℝ^{} \land A \in ℝ^{} \land B \neq A) \land B \leq A) \to (A +_{𝑒} (- B) \in ℝ \to (B \in ℝ \land A \in ℝ))$
18	16 17	sylanb	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \land B \leq A) \to (A +_{𝑒} (- B) \in ℝ \to (B \in ℝ \land A \in ℝ))$
19		ancom	$⊢ (B \in ℝ \land A \in ℝ) \leftrightarrow (A \in ℝ \land B \in ℝ)$
20	18 19	syl6ib	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \land B \leq A) \to (A +_{𝑒} (- B) \in ℝ \to (A \in ℝ \land B \in ℝ))$
21	12 20	syldan	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \land \neg A \leq B) \to (A +_{𝑒} (- B) \in ℝ \to (A \in ℝ \land B \in ℝ))$
22	6 8 9 21	ifbothda	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \to (if (A \leq B, B +_{𝑒} (- A), A +_{𝑒} (- B)) \in ℝ \to (A \in ℝ \land B \in ℝ))$
23	4 22	sylbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \to (A D B \in ℝ \to (A \in ℝ \land B \in ℝ))$
24	1	xrsdsreval	$⊢ (A \in ℝ \land B \in ℝ) \to A D B = \|A - B\|$
25		recn	$⊢ A \in ℝ \to A \in ℂ$
26		recn	$⊢ B \in ℝ \to B \in ℂ$
27		subcl	$⊢ (A \in ℂ \land B \in ℂ) \to A - B \in ℂ$
28	25 26 27	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to A - B \in ℂ$
29	28	abscld	$⊢ (A \in ℝ \land B \in ℝ) \to \|A - B\| \in ℝ$
30	24 29	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ) \to A D B \in ℝ$
31	23 30	impbid1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \neq B) \to (A D B \in ℝ \leftrightarrow (A \in ℝ \land B \in ℝ))$

Metamath Proof Explorer

Theorem xrsdsreclb

Proof