Proof of Theorem metdcnlem
Step | Hyp | Ref
| Expression |
1 | | xmetdcn2.2 |
. . . . 5
⊢ 𝐶 =
(dist‘ℝ*𝑠) |
2 | 1 | xrsxmet 22612 |
. . . 4
⊢ 𝐶 ∈
(∞Met‘ℝ*) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐶 ∈
(∞Met‘ℝ*)) |
4 | | metdcn.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
5 | | metdcn.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
6 | | metdcn.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑋) |
7 | | xmetcl 22136 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
8 | 4, 5, 6, 7 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (𝐴𝐷𝐵) ∈
ℝ*) |
9 | | metdcn.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑋) |
10 | | metdcn.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑋) |
11 | | xmetcl 22136 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) → (𝑌𝐷𝑍) ∈
ℝ*) |
12 | 4, 9, 10, 11 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (𝑌𝐷𝑍) ∈
ℝ*) |
13 | | xmetcl 22136 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑌𝐷𝐵) ∈
ℝ*) |
14 | 4, 9, 6, 13 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝑌𝐷𝐵) ∈
ℝ*) |
15 | | metdcn.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
16 | 15 | rphalfcld 11884 |
. . . . . 6
⊢ (𝜑 → (𝑅 / 2) ∈
ℝ+) |
17 | 16 | rpred 11872 |
. . . . 5
⊢ (𝜑 → (𝑅 / 2) ∈ ℝ) |
18 | | xmetcl 22136 |
. . . . . . . 8
⊢ ((𝐶 ∈
(∞Met‘ℝ*) ∧ (𝐴𝐷𝐵) ∈ ℝ* ∧ (𝑌𝐷𝐵) ∈ ℝ*) → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ∈
ℝ*) |
19 | 3, 8, 14, 18 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ∈
ℝ*) |
20 | | xmetcl 22136 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐴𝐷𝑌) ∈
ℝ*) |
21 | 4, 5, 9, 20 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝐴𝐷𝑌) ∈
ℝ*) |
22 | 16 | rpxrd 11873 |
. . . . . . 7
⊢ (𝜑 → (𝑅 / 2) ∈
ℝ*) |
23 | 1 | xmetrtri2 22161 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ≤ (𝐴𝐷𝑌)) |
24 | 4, 5, 9, 6, 23 | syl13anc 1328 |
. . . . . . 7
⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ≤ (𝐴𝐷𝑌)) |
25 | | metdcn.4 |
. . . . . . 7
⊢ (𝜑 → (𝐴𝐷𝑌) < (𝑅 / 2)) |
26 | 19, 21, 22, 24, 25 | xrlelttrd 11991 |
. . . . . 6
⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) < (𝑅 / 2)) |
27 | | xrltle 11982 |
. . . . . . 7
⊢ ((((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ∈ ℝ* ∧ (𝑅 / 2) ∈
ℝ*) → (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) < (𝑅 / 2) → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ≤ (𝑅 / 2))) |
28 | 19, 22, 27 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) < (𝑅 / 2) → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ≤ (𝑅 / 2))) |
29 | 26, 28 | mpd 15 |
. . . . 5
⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ≤ (𝑅 / 2)) |
30 | | xmetlecl 22151 |
. . . . 5
⊢ ((𝐶 ∈
(∞Met‘ℝ*) ∧ ((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝑌𝐷𝐵) ∈ ℝ*) ∧ ((𝑅 / 2) ∈ ℝ ∧
((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ≤ (𝑅 / 2))) → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ∈ ℝ) |
31 | 3, 8, 14, 17, 29, 30 | syl122anc 1335 |
. . . 4
⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ∈ ℝ) |
32 | | xmetcl 22136 |
. . . . . . . 8
⊢ ((𝐶 ∈
(∞Met‘ℝ*) ∧ (𝑌𝐷𝐵) ∈ ℝ* ∧ (𝑌𝐷𝑍) ∈ ℝ*) → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ∈
ℝ*) |
33 | 3, 14, 12, 32 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ∈
ℝ*) |
34 | | xmetcl 22136 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) → (𝐵𝐷𝑍) ∈
ℝ*) |
35 | 4, 6, 10, 34 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝐵𝐷𝑍) ∈
ℝ*) |
36 | | xmetsym 22152 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑌𝐷𝐵) = (𝐵𝐷𝑌)) |
37 | 4, 9, 6, 36 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌𝐷𝐵) = (𝐵𝐷𝑌)) |
38 | | xmetsym 22152 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋) → (𝑌𝐷𝑍) = (𝑍𝐷𝑌)) |
39 | 4, 9, 10, 38 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌𝐷𝑍) = (𝑍𝐷𝑌)) |
40 | 37, 39 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝜑 → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) = ((𝐵𝐷𝑌)𝐶(𝑍𝐷𝑌))) |
41 | 1 | xmetrtri2 22161 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐵 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋)) → ((𝐵𝐷𝑌)𝐶(𝑍𝐷𝑌)) ≤ (𝐵𝐷𝑍)) |
42 | 4, 6, 10, 9, 41 | syl13anc 1328 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵𝐷𝑌)𝐶(𝑍𝐷𝑌)) ≤ (𝐵𝐷𝑍)) |
43 | 40, 42 | eqbrtrd 4675 |
. . . . . . 7
⊢ (𝜑 → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ≤ (𝐵𝐷𝑍)) |
44 | | metdcn.5 |
. . . . . . 7
⊢ (𝜑 → (𝐵𝐷𝑍) < (𝑅 / 2)) |
45 | 33, 35, 22, 43, 44 | xrlelttrd 11991 |
. . . . . 6
⊢ (𝜑 → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) < (𝑅 / 2)) |
46 | | xrltle 11982 |
. . . . . . 7
⊢ ((((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ∈ ℝ* ∧ (𝑅 / 2) ∈
ℝ*) → (((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) < (𝑅 / 2) → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ≤ (𝑅 / 2))) |
47 | 33, 22, 46 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) < (𝑅 / 2) → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ≤ (𝑅 / 2))) |
48 | 45, 47 | mpd 15 |
. . . . 5
⊢ (𝜑 → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ≤ (𝑅 / 2)) |
49 | | xmetlecl 22151 |
. . . . 5
⊢ ((𝐶 ∈
(∞Met‘ℝ*) ∧ ((𝑌𝐷𝐵) ∈ ℝ* ∧ (𝑌𝐷𝑍) ∈ ℝ*) ∧ ((𝑅 / 2) ∈ ℝ ∧
((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ≤ (𝑅 / 2))) → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ∈ ℝ) |
50 | 3, 14, 12, 17, 48, 49 | syl122anc 1335 |
. . . 4
⊢ (𝜑 → ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ∈ ℝ) |
51 | 31, 50 | readdcld 10069 |
. . 3
⊢ (𝜑 → (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) + ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍))) ∈ ℝ) |
52 | | xmettri 22156 |
. . . . 5
⊢ ((𝐶 ∈
(∞Met‘ℝ*) ∧ ((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝑌𝐷𝑍) ∈ ℝ* ∧ (𝑌𝐷𝐵) ∈ ℝ*)) →
((𝐴𝐷𝐵)𝐶(𝑌𝐷𝑍)) ≤ (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) +𝑒 ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)))) |
53 | 3, 8, 12, 14, 52 | syl13anc 1328 |
. . . 4
⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝑍)) ≤ (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) +𝑒 ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)))) |
54 | | rexadd 12063 |
. . . . 5
⊢ ((((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) ∈ ℝ ∧ ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)) ∈ ℝ) → (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) +𝑒 ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍))) = (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) + ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)))) |
55 | 31, 50, 54 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) +𝑒 ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍))) = (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) + ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)))) |
56 | 53, 55 | breqtrd 4679 |
. . 3
⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝑍)) ≤ (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) + ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍)))) |
57 | | xmetlecl 22151 |
. . 3
⊢ ((𝐶 ∈
(∞Met‘ℝ*) ∧ ((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝑌𝐷𝑍) ∈ ℝ*) ∧
((((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) + ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍))) ∈ ℝ ∧ ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝑍)) ≤ (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) + ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍))))) → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝑍)) ∈ ℝ) |
58 | 3, 8, 12, 51, 56, 57 | syl122anc 1335 |
. 2
⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝑍)) ∈ ℝ) |
59 | 15 | rpred 11872 |
. 2
⊢ (𝜑 → 𝑅 ∈ ℝ) |
60 | 31, 50, 59, 26, 45 | lt2halvesd 11280 |
. 2
⊢ (𝜑 → (((𝐴𝐷𝐵)𝐶(𝑌𝐷𝐵)) + ((𝑌𝐷𝐵)𝐶(𝑌𝐷𝑍))) < 𝑅) |
61 | 58, 51, 59, 56, 60 | lelttrd 10195 |
1
⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝑍)) < 𝑅) |