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 ⊢D=dist⁡ℝ𝑠*
Assertion xrsdsreclb ⊢A∈ℝ*∧B∈ℝ*∧A≠B→ADB∈ℝ↔A∈ℝ∧B∈ℝ

Proof

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