Step |
Hyp |
Ref |
Expression |
1 |
|
3ancomb |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) |
2 |
|
xmettri |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) ) |
3 |
1 2
|
sylan2b |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) ) |
4 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ ℝ* ) |
5 |
4
|
3adant3r2 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ∈ ℝ* ) |
6 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐶 ) ∈ ℝ* ) |
7 |
6
|
3adant3r1 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) ∈ ℝ* ) |
8 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
9 |
8
|
3adant3r3 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
10 |
|
xmetge0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐶 ) ) |
11 |
10
|
3adant3r2 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 0 ≤ ( 𝐴 𝐷 𝐶 ) ) |
12 |
|
xmetge0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 0 ≤ ( 𝐵 𝐷 𝐶 ) ) |
13 |
12
|
3adant3r1 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 0 ≤ ( 𝐵 𝐷 𝐶 ) ) |
14 |
|
ge0nemnf |
⊢ ( ( ( 𝐵 𝐷 𝐶 ) ∈ ℝ* ∧ 0 ≤ ( 𝐵 𝐷 𝐶 ) ) → ( 𝐵 𝐷 𝐶 ) ≠ -∞ ) |
15 |
7 13 14
|
syl2anc |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) ≠ -∞ ) |
16 |
|
xmetge0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) ) |
17 |
16
|
3adant3r3 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) ) |
18 |
|
xlesubadd |
⊢ ( ( ( ( 𝐴 𝐷 𝐶 ) ∈ ℝ* ∧ ( 𝐵 𝐷 𝐶 ) ∈ ℝ* ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) ∧ ( 0 ≤ ( 𝐴 𝐷 𝐶 ) ∧ ( 𝐵 𝐷 𝐶 ) ≠ -∞ ∧ 0 ≤ ( 𝐴 𝐷 𝐵 ) ) ) → ( ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) ) ) |
19 |
5 7 9 11 15 17 18
|
syl33anc |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) ) ) |
20 |
3 19
|
mpbird |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ) |