This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrdi ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
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 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ↔ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )