Step | Hyp | Ref
| Expression |
1 | | simpr3 1198 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → (𝑅 +𝑒 𝑆) ≤ (𝑃𝐷𝑄)) |
2 | | simpr1 1196 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → 𝑅 ∈
ℝ*) |
3 | | simpr2 1197 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → 𝑆 ∈
ℝ*) |
4 | 2, 3 | xaddcld 12891 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → (𝑅 +𝑒 𝑆) ∈
ℝ*) |
5 | | xmetcl 23229 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) → (𝑃𝐷𝑄) ∈
ℝ*) |
6 | 5 | adantr 484 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → (𝑃𝐷𝑄) ∈
ℝ*) |
7 | 4, 6 | xrlenltd 10899 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → ((𝑅 +𝑒 𝑆) ≤ (𝑃𝐷𝑄) ↔ ¬ (𝑃𝐷𝑄) < (𝑅 +𝑒 𝑆))) |
8 | 1, 7 | mpbid 235 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → ¬ (𝑃𝐷𝑄) < (𝑅 +𝑒 𝑆)) |
9 | | elin 3882 |
. . . 4
⊢ (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑄(ball‘𝐷)𝑆)) ↔ (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ (𝑄(ball‘𝐷)𝑆))) |
10 | | simpl1 1193 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → 𝐷 ∈ (∞Met‘𝑋)) |
11 | | simpl2 1194 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → 𝑃 ∈ 𝑋) |
12 | | elbl 23286 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
13 | 10, 11, 2, 12 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → (𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))) |
14 | | simpl3 1195 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → 𝑄 ∈ 𝑋) |
15 | | elbl 23286 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑄 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑥 ∈ (𝑄(ball‘𝐷)𝑆) ↔ (𝑥 ∈ 𝑋 ∧ (𝑄𝐷𝑥) < 𝑆))) |
16 | 10, 14, 3, 15 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → (𝑥 ∈ (𝑄(ball‘𝐷)𝑆) ↔ (𝑥 ∈ 𝑋 ∧ (𝑄𝐷𝑥) < 𝑆))) |
17 | 13, 16 | anbi12d 634 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → ((𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ (𝑄(ball‘𝐷)𝑆)) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ (𝑥 ∈ 𝑋 ∧ (𝑄𝐷𝑥) < 𝑆)))) |
18 | | anandi 676 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ ((𝑃𝐷𝑥) < 𝑅 ∧ (𝑄𝐷𝑥) < 𝑆)) ↔ ((𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) ∧ (𝑥 ∈ 𝑋 ∧ (𝑄𝐷𝑥) < 𝑆))) |
19 | 17, 18 | bitr4di 292 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → ((𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ (𝑄(ball‘𝐷)𝑆)) ↔ (𝑥 ∈ 𝑋 ∧ ((𝑃𝐷𝑥) < 𝑅 ∧ (𝑄𝐷𝑥) < 𝑆)))) |
20 | 10 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
21 | 11 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → 𝑃 ∈ 𝑋) |
22 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
23 | | xmetcl 23229 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷𝑥) ∈
ℝ*) |
24 | 20, 21, 22, 23 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷𝑥) ∈
ℝ*) |
25 | 14 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → 𝑄 ∈ 𝑋) |
26 | | xmetcl 23229 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑄𝐷𝑥) ∈
ℝ*) |
27 | 20, 25, 22, 26 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → (𝑄𝐷𝑥) ∈
ℝ*) |
28 | 2 | adantr 484 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → 𝑅 ∈
ℝ*) |
29 | 3 | adantr 484 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → 𝑆 ∈
ℝ*) |
30 | | xlt2add 12850 |
. . . . . . . 8
⊢ ((((𝑃𝐷𝑥) ∈ ℝ* ∧ (𝑄𝐷𝑥) ∈ ℝ*) ∧ (𝑅 ∈ ℝ*
∧ 𝑆 ∈
ℝ*)) → (((𝑃𝐷𝑥) < 𝑅 ∧ (𝑄𝐷𝑥) < 𝑆) → ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥)) < (𝑅 +𝑒 𝑆))) |
31 | 24, 27, 28, 29, 30 | syl22anc 839 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → (((𝑃𝐷𝑥) < 𝑅 ∧ (𝑄𝐷𝑥) < 𝑆) → ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥)) < (𝑅 +𝑒 𝑆))) |
32 | | xmettri3 23251 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑃𝐷𝑄) ≤ ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥))) |
33 | 20, 21, 25, 22, 32 | syl13anc 1374 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷𝑄) ≤ ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥))) |
34 | 6 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷𝑄) ∈
ℝ*) |
35 | 24, 27 | xaddcld 12891 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥)) ∈
ℝ*) |
36 | 4 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → (𝑅 +𝑒 𝑆) ∈
ℝ*) |
37 | | xrlelttr 12746 |
. . . . . . . . 9
⊢ (((𝑃𝐷𝑄) ∈ ℝ* ∧ ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥)) ∈ ℝ* ∧ (𝑅 +𝑒 𝑆) ∈ ℝ*)
→ (((𝑃𝐷𝑄) ≤ ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥)) ∧ ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥)) < (𝑅 +𝑒 𝑆)) → (𝑃𝐷𝑄) < (𝑅 +𝑒 𝑆))) |
38 | 34, 35, 36, 37 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → (((𝑃𝐷𝑄) ≤ ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥)) ∧ ((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥)) < (𝑅 +𝑒 𝑆)) → (𝑃𝐷𝑄) < (𝑅 +𝑒 𝑆))) |
39 | 33, 38 | mpand 695 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → (((𝑃𝐷𝑥) +𝑒 (𝑄𝐷𝑥)) < (𝑅 +𝑒 𝑆) → (𝑃𝐷𝑄) < (𝑅 +𝑒 𝑆))) |
40 | 31, 39 | syld 47 |
. . . . . 6
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) ∧ 𝑥 ∈ 𝑋) → (((𝑃𝐷𝑥) < 𝑅 ∧ (𝑄𝐷𝑥) < 𝑆) → (𝑃𝐷𝑄) < (𝑅 +𝑒 𝑆))) |
41 | 40 | expimpd 457 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → ((𝑥 ∈ 𝑋 ∧ ((𝑃𝐷𝑥) < 𝑅 ∧ (𝑄𝐷𝑥) < 𝑆)) → (𝑃𝐷𝑄) < (𝑅 +𝑒 𝑆))) |
42 | 19, 41 | sylbid 243 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → ((𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ∧ 𝑥 ∈ (𝑄(ball‘𝐷)𝑆)) → (𝑃𝐷𝑄) < (𝑅 +𝑒 𝑆))) |
43 | 9, 42 | syl5bi 245 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → (𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑄(ball‘𝐷)𝑆)) → (𝑃𝐷𝑄) < (𝑅 +𝑒 𝑆))) |
44 | 8, 43 | mtod 201 |
. 2
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → ¬ 𝑥 ∈ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑄(ball‘𝐷)𝑆))) |
45 | 44 | eq0rdv 4319 |
1
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → ((𝑃(ball‘𝐷)𝑅) ∩ (𝑄(ball‘𝐷)𝑆)) = ∅) |