| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xrex 13030 | . . . 4
⊢
ℝ* ∈ V | 
| 2 | 1 | a1i 11 | . . 3
⊢ (⊤
→ ℝ* ∈ V) | 
| 3 |  | id 22 | . . . . . . . 8
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ∈
ℝ*) | 
| 4 |  | xnegcl 13256 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ*
→ -𝑒𝑥 ∈ ℝ*) | 
| 5 |  | xaddcl 13282 | . . . . . . . 8
⊢ ((𝑦 ∈ ℝ*
∧ -𝑒𝑥 ∈ ℝ*) → (𝑦 +𝑒
-𝑒𝑥)
∈ ℝ*) | 
| 6 | 3, 4, 5 | syl2anr 597 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑦 +𝑒
-𝑒𝑥)
∈ ℝ*) | 
| 7 |  | xnegcl 13256 | . . . . . . . 8
⊢ (𝑦 ∈ ℝ*
→ -𝑒𝑦 ∈ ℝ*) | 
| 8 |  | xaddcl 13282 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ*
∧ -𝑒𝑦 ∈ ℝ*) → (𝑥 +𝑒
-𝑒𝑦)
∈ ℝ*) | 
| 9 | 7, 8 | sylan2 593 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥 +𝑒
-𝑒𝑦)
∈ ℝ*) | 
| 10 | 6, 9 | ifcld 4571 | . . . . . 6
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))
∈ ℝ*) | 
| 11 | 10 | rgen2 3198 | . . . . 5
⊢
∀𝑥 ∈
ℝ* ∀𝑦 ∈ ℝ* if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))
∈ ℝ* | 
| 12 |  | xrsxmet.1 | . . . . . . 7
⊢ 𝐷 =
(dist‘ℝ*𝑠) | 
| 13 | 12 | xrsds 21428 | . . . . . 6
⊢ 𝐷 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))) | 
| 14 | 13 | fmpo 8094 | . . . . 5
⊢
(∀𝑥 ∈
ℝ* ∀𝑦 ∈ ℝ* if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))
∈ ℝ* ↔ 𝐷:(ℝ* ×
ℝ*)⟶ℝ*) | 
| 15 | 11, 14 | mpbi 230 | . . . 4
⊢ 𝐷:(ℝ* ×
ℝ*)⟶ℝ* | 
| 16 | 15 | a1i 11 | . . 3
⊢ (⊤
→ 𝐷:(ℝ* ×
ℝ*)⟶ℝ*) | 
| 17 |  | breq2 5146 | . . . . . 6
⊢ ((𝑦 +𝑒
-𝑒𝑥) =
if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))
→ (0 ≤ (𝑦
+𝑒 -𝑒𝑥) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)))) | 
| 18 |  | breq2 5146 | . . . . . 6
⊢ ((𝑥 +𝑒
-𝑒𝑦) =
if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))
→ (0 ≤ (𝑥
+𝑒 -𝑒𝑦) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)))) | 
| 19 |  | xsubge0 13304 | . . . . . . . 8
⊢ ((𝑦 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (0 ≤ (𝑦 +𝑒
-𝑒𝑥)
↔ 𝑥 ≤ 𝑦)) | 
| 20 | 19 | ancoms 458 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (0 ≤ (𝑦 +𝑒
-𝑒𝑥)
↔ 𝑥 ≤ 𝑦)) | 
| 21 | 20 | biimpar 477 | . . . . . 6
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≤ 𝑦) → 0 ≤ (𝑦 +𝑒
-𝑒𝑥)) | 
| 22 |  | xrletri 13196 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)) | 
| 23 | 22 | orcanai 1004 | . . . . . . 7
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑦 ≤ 𝑥) | 
| 24 |  | xsubge0 13304 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (0 ≤ (𝑥 +𝑒
-𝑒𝑦)
↔ 𝑦 ≤ 𝑥)) | 
| 25 | 24 | biimpar 477 | . . . . . . 7
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑦 ≤ 𝑥) → 0 ≤ (𝑥 +𝑒
-𝑒𝑦)) | 
| 26 | 23, 25 | syldan 591 | . . . . . 6
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ ¬ 𝑥 ≤ 𝑦) → 0 ≤ (𝑥 +𝑒
-𝑒𝑦)) | 
| 27 | 17, 18, 21, 26 | ifbothda 4563 | . . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))) | 
| 28 | 12 | xrsdsval 21429 | . . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))) | 
| 29 | 27, 28 | breqtrrd 5170 | . . . 4
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → 0 ≤ (𝑥𝐷𝑦)) | 
| 30 | 29 | adantl 481 | . . 3
⊢
((⊤ ∧ (𝑥
∈ ℝ* ∧ 𝑦 ∈ ℝ*)) → 0 ≤
(𝑥𝐷𝑦)) | 
| 31 | 29 | biantrud 531 | . . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦)))) | 
| 32 | 28, 10 | eqeltrd 2840 | . . . . . 6
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥𝐷𝑦) ∈
ℝ*) | 
| 33 |  | 0xr 11309 | . . . . . 6
⊢ 0 ∈
ℝ* | 
| 34 |  | xrletri3 13197 | . . . . . 6
⊢ (((𝑥𝐷𝑦) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦)))) | 
| 35 | 32, 33, 34 | sylancl 586 | . . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦)))) | 
| 36 |  | simpr 484 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦) | 
| 37 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = 0) | 
| 38 |  | 0re 11264 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℝ | 
| 39 | 37, 38 | eqeltrdi 2848 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) ∈ ℝ) | 
| 40 | 12 | xrsdsreclb 21432 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑥
≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))) | 
| 41 | 40 | ad4ant124 1173 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))) | 
| 42 | 39, 41 | mpbid 232 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) | 
| 43 | 42 | simpld 494 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℝ) | 
| 44 | 43 | recnd 11290 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℂ) | 
| 45 | 42 | simprd 495 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℝ) | 
| 46 | 45 | recnd 11290 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℂ) | 
| 47 |  | rexsub 13276 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 +𝑒
-𝑒𝑦) =
(𝑥 − 𝑦)) | 
| 48 | 42, 47 | syl 17 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +𝑒
-𝑒𝑦) =
(𝑥 − 𝑦)) | 
| 49 | 28 | eqeq1d 2738 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑥𝐷𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
0)) | 
| 50 | 49 | biimpa 476 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) → if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
0) | 
| 51 | 50 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
0) | 
| 52 |  | xneg11 13258 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 +𝑒
-𝑒𝑥)
∈ ℝ* ∧ 0 ∈ ℝ*) →
(-𝑒(𝑦
+𝑒 -𝑒𝑥) = -𝑒0 ↔ (𝑦 +𝑒
-𝑒𝑥) =
0)) | 
| 53 | 6, 33, 52 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (-𝑒(𝑦 +𝑒
-𝑒𝑥) =
-𝑒0 ↔ (𝑦 +𝑒
-𝑒𝑥) =
0)) | 
| 54 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → 𝑦 ∈ ℝ*) | 
| 55 | 4 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → -𝑒𝑥 ∈ ℝ*) | 
| 56 |  | xnegdi 13291 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ*
∧ -𝑒𝑥 ∈ ℝ*) →
-𝑒(𝑦
+𝑒 -𝑒𝑥) = (-𝑒𝑦 +𝑒
-𝑒-𝑒𝑥)) | 
| 57 | 54, 55, 56 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → -𝑒(𝑦 +𝑒
-𝑒𝑥) =
(-𝑒𝑦
+𝑒 -𝑒-𝑒𝑥)) | 
| 58 |  | xnegneg 13257 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ*
→ -𝑒-𝑒𝑥 = 𝑥) | 
| 59 | 58 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → -𝑒-𝑒𝑥 = 𝑥) | 
| 60 | 59 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (-𝑒𝑦 +𝑒
-𝑒-𝑒𝑥) = (-𝑒𝑦 +𝑒 𝑥)) | 
| 61 | 7 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → -𝑒𝑦 ∈ ℝ*) | 
| 62 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → 𝑥 ∈ ℝ*) | 
| 63 |  | xaddcom 13283 | . . . . . . . . . . . . . . . . 17
⊢
((-𝑒𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ*)
→ (-𝑒𝑦 +𝑒 𝑥) = (𝑥 +𝑒
-𝑒𝑦)) | 
| 64 | 61, 62, 63 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (-𝑒𝑦 +𝑒 𝑥) = (𝑥 +𝑒
-𝑒𝑦)) | 
| 65 | 57, 60, 64 | 3eqtrd 2780 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → -𝑒(𝑦 +𝑒
-𝑒𝑥) =
(𝑥 +𝑒
-𝑒𝑦)) | 
| 66 |  | xneg0 13255 | . . . . . . . . . . . . . . . 16
⊢
-𝑒0 = 0 | 
| 67 | 66 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → -𝑒0 = 0) | 
| 68 | 65, 67 | eqeq12d 2752 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (-𝑒(𝑦 +𝑒
-𝑒𝑥) =
-𝑒0 ↔ (𝑥 +𝑒
-𝑒𝑦) =
0)) | 
| 69 | 53, 68 | bitr3d 281 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑦 +𝑒
-𝑒𝑥) = 0
↔ (𝑥
+𝑒 -𝑒𝑦) = 0)) | 
| 70 | 69 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑦 +𝑒
-𝑒𝑥) = 0
↔ (𝑥
+𝑒 -𝑒𝑦) = 0)) | 
| 71 |  | biidd 262 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥 +𝑒
-𝑒𝑦) = 0
↔ (𝑥
+𝑒 -𝑒𝑦) = 0)) | 
| 72 |  | eqeq1 2740 | . . . . . . . . . . . . . 14
⊢ ((𝑦 +𝑒
-𝑒𝑥) =
if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))
→ ((𝑦
+𝑒 -𝑒𝑥) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
0)) | 
| 73 | 72 | bibi1d 343 | . . . . . . . . . . . . 13
⊢ ((𝑦 +𝑒
-𝑒𝑥) =
if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))
→ (((𝑦
+𝑒 -𝑒𝑥) = 0 ↔ (𝑥 +𝑒
-𝑒𝑦) =
0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
0 ↔ (𝑥
+𝑒 -𝑒𝑦) = 0))) | 
| 74 |  | eqeq1 2740 | . . . . . . . . . . . . . 14
⊢ ((𝑥 +𝑒
-𝑒𝑦) =
if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))
→ ((𝑥
+𝑒 -𝑒𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
0)) | 
| 75 | 74 | bibi1d 343 | . . . . . . . . . . . . 13
⊢ ((𝑥 +𝑒
-𝑒𝑦) =
if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))
→ (((𝑥
+𝑒 -𝑒𝑦) = 0 ↔ (𝑥 +𝑒
-𝑒𝑦) =
0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
0 ↔ (𝑥
+𝑒 -𝑒𝑦) = 0))) | 
| 76 | 73, 75 | ifboth 4564 | . . . . . . . . . . . 12
⊢ ((((𝑦 +𝑒
-𝑒𝑥) = 0
↔ (𝑥
+𝑒 -𝑒𝑦) = 0) ∧ ((𝑥 +𝑒
-𝑒𝑦) = 0
↔ (𝑥
+𝑒 -𝑒𝑦) = 0)) → (if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
0 ↔ (𝑥
+𝑒 -𝑒𝑦) = 0)) | 
| 77 | 70, 71, 76 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
0 ↔ (𝑥
+𝑒 -𝑒𝑦) = 0)) | 
| 78 | 51, 77 | mpbid 232 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +𝑒
-𝑒𝑦) =
0) | 
| 79 | 48, 78 | eqtr3d 2778 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 − 𝑦) = 0) | 
| 80 | 44, 46, 79 | subeq0d 11629 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 = 𝑦) | 
| 81 | 36, 80 | pm2.61dane 3028 | . . . . . . 7
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑥𝐷𝑦) = 0) → 𝑥 = 𝑦) | 
| 82 | 81 | ex 412 | . . . . . 6
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑥𝐷𝑦) = 0 → 𝑥 = 𝑦)) | 
| 83 | 12 | xrsdsval 21429 | . . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑦))) | 
| 84 | 83 | anidms 566 | . . . . . . . . 9
⊢ (𝑦 ∈ ℝ*
→ (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑦))) | 
| 85 |  | xrleid 13194 | . . . . . . . . . 10
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤ 𝑦) | 
| 86 | 85 | iftrued 4532 | . . . . . . . . 9
⊢ (𝑦 ∈ ℝ*
→ if(𝑦 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑦)) =
(𝑦 +𝑒
-𝑒𝑦)) | 
| 87 |  | xnegid 13281 | . . . . . . . . 9
⊢ (𝑦 ∈ ℝ*
→ (𝑦
+𝑒 -𝑒𝑦) = 0) | 
| 88 | 84, 86, 87 | 3eqtrd 2780 | . . . . . . . 8
⊢ (𝑦 ∈ ℝ*
→ (𝑦𝐷𝑦) = 0) | 
| 89 | 88 | adantl 481 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑦𝐷𝑦) = 0) | 
| 90 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑦)) | 
| 91 | 90 | eqeq1d 2738 | . . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥𝐷𝑦) = 0 ↔ (𝑦𝐷𝑦) = 0)) | 
| 92 | 89, 91 | syl5ibrcom 247 | . . . . . 6
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥 = 𝑦 → (𝑥𝐷𝑦) = 0)) | 
| 93 | 82, 92 | impbid 212 | . . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) | 
| 94 | 31, 35, 93 | 3bitr2d 307 | . . . 4
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦)) | 
| 95 | 94 | adantl 481 | . . 3
⊢
((⊤ ∧ (𝑥
∈ ℝ* ∧ 𝑦 ∈ ℝ*)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦)) | 
| 96 |  | simplrr 777 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℝ) | 
| 97 | 96 | leidd 11830 | . . . . . 6
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ≤ (𝑧𝐷𝑦)) | 
| 98 |  | simpr 484 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑧 = 𝑥) | 
| 99 | 98 | oveq1d 7447 | . . . . . 6
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = (𝑥𝐷𝑦)) | 
| 100 | 98 | oveq1d 7447 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = (𝑥𝐷𝑥)) | 
| 101 |  | simpll1 1212 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑥 ∈ ℝ*) | 
| 102 |  | oveq12 7441 | . . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑥 ∧ 𝑦 = 𝑥) → (𝑦𝐷𝑦) = (𝑥𝐷𝑥)) | 
| 103 | 102 | anidms 566 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑦𝐷𝑦) = (𝑥𝐷𝑥)) | 
| 104 | 103 | eqeq1d 2738 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ((𝑦𝐷𝑦) = 0 ↔ (𝑥𝐷𝑥) = 0)) | 
| 105 | 104, 88 | vtoclga 3576 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
→ (𝑥𝐷𝑥) = 0) | 
| 106 | 101, 105 | syl 17 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑥) = 0) | 
| 107 | 100, 106 | eqtrd 2776 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = 0) | 
| 108 | 107 | oveq1d 7447 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (0 + (𝑧𝐷𝑦))) | 
| 109 | 96 | recnd 11290 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℂ) | 
| 110 | 109 | addlidd 11463 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (0 + (𝑧𝐷𝑦)) = (𝑧𝐷𝑦)) | 
| 111 | 108, 110 | eqtr2d 2777 | . . . . . 6
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) | 
| 112 | 97, 99, 111 | 3brtr3d 5173 | . . . . 5
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) | 
| 113 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑧 = 𝑦) | 
| 114 | 113 | oveq1d 7447 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) = (𝑦𝐷𝑥)) | 
| 115 |  | simplrl 776 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) ∈ ℝ) | 
| 116 | 114, 115 | eqeltrrd 2841 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℝ) | 
| 117 | 116 | leidd 11830 | . . . . . 6
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ≤ (𝑦𝐷𝑥)) | 
| 118 |  | simpll1 1212 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑥 ∈ ℝ*) | 
| 119 |  | simpll2 1213 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑦 ∈ ℝ*) | 
| 120 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑦𝐷𝑥) = (𝑦𝐷𝑦)) | 
| 121 | 90, 120 | eqtr4d 2779 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) | 
| 122 | 121 | adantl 481 | . . . . . . . 8
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) | 
| 123 |  | eqeq2 2748 | . . . . . . . . . 10
⊢ ((𝑥 +𝑒
-𝑒𝑦) =
if(𝑦 ≤ 𝑥, (𝑥 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑥))
→ (if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
(𝑥 +𝑒
-𝑒𝑦)
↔ if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
if(𝑦 ≤ 𝑥, (𝑥 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑥)))) | 
| 124 |  | eqeq2 2748 | . . . . . . . . . 10
⊢ ((𝑦 +𝑒
-𝑒𝑥) =
if(𝑦 ≤ 𝑥, (𝑥 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑥))
→ (if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
(𝑦 +𝑒
-𝑒𝑥)
↔ if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
if(𝑦 ≤ 𝑥, (𝑥 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑥)))) | 
| 125 |  | xrleloe 13187 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))) | 
| 126 | 125 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))) | 
| 127 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦) | 
| 128 | 127 | neneqd 2944 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → ¬ 𝑥 = 𝑦) | 
| 129 |  | biorf 936 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 = 𝑦 ∨ 𝑥 < 𝑦))) | 
| 130 |  | orcom 870 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑦 ∨ 𝑥 < 𝑦) ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)) | 
| 131 | 129, 130 | bitrdi 287 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))) | 
| 132 | 128, 131 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))) | 
| 133 |  | xrltnle 11329 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥)) | 
| 134 | 133 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥)) | 
| 135 | 126, 132,
134 | 3bitr2d 307 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑥)) | 
| 136 | 135 | con2bid 354 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → (𝑦 ≤ 𝑥 ↔ ¬ 𝑥 ≤ 𝑦)) | 
| 137 | 136 | biimpa 476 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → ¬ 𝑥 ≤ 𝑦) | 
| 138 | 137 | iffalsed 4535 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
(𝑥 +𝑒
-𝑒𝑦)) | 
| 139 | 135 | biimpar 477 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦) | 
| 140 | 139 | iftrued 4532 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
(𝑦 +𝑒
-𝑒𝑥)) | 
| 141 | 123, 124,
138, 140 | ifbothda 4563 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦)) =
if(𝑦 ≤ 𝑥, (𝑥 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑥))) | 
| 142 | 28 | adantr 480 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +𝑒
-𝑒𝑥),
(𝑥 +𝑒
-𝑒𝑦))) | 
| 143 | 12 | xrsdsval 21429 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑥))) | 
| 144 | 143 | ancoms 458 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑥))) | 
| 145 | 144 | adantr 480 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +𝑒
-𝑒𝑦),
(𝑦 +𝑒
-𝑒𝑥))) | 
| 146 | 141, 142,
145 | 3eqtr4d 2786 | . . . . . . . 8
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) | 
| 147 | 122, 146 | pm2.61dane 3028 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) | 
| 148 | 118, 119,
147 | syl2anc 584 | . . . . . 6
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥)) | 
| 149 | 113 | oveq1d 7447 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = (𝑦𝐷𝑦)) | 
| 150 | 119, 88 | syl 17 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑦) = 0) | 
| 151 | 149, 150 | eqtrd 2776 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = 0) | 
| 152 | 114, 151 | oveq12d 7450 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((𝑦𝐷𝑥) + 0)) | 
| 153 | 116 | recnd 11290 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℂ) | 
| 154 | 153 | addridd 11462 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑦𝐷𝑥) + 0) = (𝑦𝐷𝑥)) | 
| 155 | 152, 154 | eqtrd 2776 | . . . . . 6
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (𝑦𝐷𝑥)) | 
| 156 | 117, 148,
155 | 3brtr4d 5174 | . . . . 5
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) | 
| 157 |  | simplrl 776 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) ∈ ℝ) | 
| 158 |  | simpll3 1214 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ*) | 
| 159 |  | simpll1 1212 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ*) | 
| 160 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑥) | 
| 161 | 12 | xrsdsreclb 21432 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ 𝑧
≠ 𝑥) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ))) | 
| 162 | 158, 159,
160, 161 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ))) | 
| 163 | 157, 162 | mpbid 232 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)) | 
| 164 | 163 | simprd 495 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ) | 
| 165 | 164 | recnd 11290 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℂ) | 
| 166 |  | simplrr 777 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) ∈ ℝ) | 
| 167 |  | simpll2 1213 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ*) | 
| 168 |  | simprr 772 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑦) | 
| 169 | 12 | xrsdsreclb 21432 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
≠ 𝑦) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ))) | 
| 170 | 158, 167,
168, 169 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ))) | 
| 171 | 166, 170 | mpbid 232 | . . . . . . . . 9
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)) | 
| 172 | 171 | simprd 495 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ) | 
| 173 | 172 | recnd 11290 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℂ) | 
| 174 | 163 | simpld 494 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ) | 
| 175 | 174 | recnd 11290 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℂ) | 
| 176 | 165, 173,
175 | abs3difd 15500 | . . . . . 6
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑥 − 𝑦)) ≤ ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦)))) | 
| 177 | 12 | xrsdsreval 21430 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦))) | 
| 178 | 164, 172,
177 | syl2anc 584 | . . . . . 6
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦))) | 
| 179 | 12 | xrsdsreval 21430 | . . . . . . . . 9
⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥))) | 
| 180 | 163, 179 | syl 17 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥))) | 
| 181 | 175, 165 | abssubd 15493 | . . . . . . . 8
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑧 − 𝑥)) = (abs‘(𝑥 − 𝑧))) | 
| 182 | 180, 181 | eqtrd 2776 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑥 − 𝑧))) | 
| 183 | 12 | xrsdsreval 21430 | . . . . . . . 8
⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦))) | 
| 184 | 171, 183 | syl 17 | . . . . . . 7
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦))) | 
| 185 | 182, 184 | oveq12d 7450 | . . . . . 6
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦)))) | 
| 186 | 176, 178,
185 | 3brtr4d 5174 | . . . . 5
⊢ ((((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) | 
| 187 | 112, 156,
186 | pm2.61da2ne 3029 | . . . 4
⊢ (((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑧
∈ ℝ*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) | 
| 188 | 187 | 3adant1 1130 | . . 3
⊢
((⊤ ∧ (𝑥
∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) | 
| 189 | 2, 16, 30, 95, 188 | isxmet2d 24338 | . 2
⊢ (⊤
→ 𝐷 ∈
(∞Met‘ℝ*)) | 
| 190 | 189 | mptru 1546 | 1
⊢ 𝐷 ∈
(∞Met‘ℝ*) |