Theorem 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	⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
Assertion	xrsdsreclb	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ↔ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrsds.d	⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
2	1	xrsdsval	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 𝐷 𝐵 ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) )
3	2	3adant3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 𝐷 𝐵 ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) )
4	3	eleq1d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ↔ if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) ∈ ℝ ) )
5		eleq1	⊢ ( ( 𝐵 +𝑒 -𝑒 𝐴 ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ↔ if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) ∈ ℝ ) )
6	5	imbi1d	⊢ ( ( 𝐵 +𝑒 -𝑒 𝐴 ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) → ( ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ↔ ( if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
7		eleq1	⊢ ( ( 𝐴 +𝑒 -𝑒 𝐵 ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ ↔ if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) ∈ ℝ ) )
8	7	imbi1d	⊢ ( ( 𝐴 +𝑒 -𝑒 𝐵 ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) → ( ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ↔ ( if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
9	1	xrsdsreclblem	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
10		xrletri	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴 ) )
11	10	3adant3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴 ) )
12	11	orcanai	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ ¬ 𝐴 ≤ 𝐵 ) → 𝐵 ≤ 𝐴 )
13		necom	⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
14	13	3anbi3i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≠ 𝐴 ) )
15		3ancoma	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≠ 𝐴 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ≠ 𝐴 ) )
16	14 15	bitri	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ≠ 𝐴 ) )
17	1	xrsdsreclblem	⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ → ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) )
18	16 17	sylanb	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ → ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) )
19		ancom	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ↔ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
20	18 19	syl6ib	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
21	12 20	syldan	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
22	6 8 9 21	ifbothda	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) → ( if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
23	4 22	sylbid	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
24	1	xrsdsreval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 𝐷 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )
25		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
26		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
27		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
28	25 26 27	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
29	28	abscld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
30	24 29	eqeltrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ )
31	23 30	impbid1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ↔ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )