bldisj

Description: Two balls are disjoint if the center-to-center distance is more than the sum of the radii. (Contributed by Mario Carneiro, 30-Dec-2013)

		Ref	Expression
	Assertion	bldisj	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		simpr3	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) )
2		simpr1	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑅 ∈ ℝ^* )
3		simpr2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑆 ∈ ℝ^* )
4	2 3	xaddcld	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑅 +_𝑒 𝑆 ) ∈ ℝ^* )
5		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ^* )
6	5	adantr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ^* )
7	4 6	xrlenltd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ↔ ¬ ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +_𝑒 𝑆 ) ) )
8	1 7	mpbid	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ¬ ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +_𝑒 𝑆 ) )
9		elin	⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) )
10		simpl1	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
11		simpl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑃 ∈ 𝑋 )
12		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
13	10 11 2 12	syl3anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
14		simpl3	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑄 ∈ 𝑋 )
15		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑄 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
16	10 14 3 15	syl3anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
17	13 16	anbi12d	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) ) )
18		anandi	⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
19	17 18	bitr4di	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) ) )
20	10	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
21	11	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
22		simpr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
23		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ^* )
24	20 21 22 23	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ^* )
25	14	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑄 ∈ 𝑋 )
26		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ^* )
27	20 25 22 26	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ^* )
28	2	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ^* )
29	3	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ ℝ^* )
30		xlt2add	⊢ ( ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ^* ∧ ( 𝑄 𝐷 𝑥 ) ∈ ℝ^* ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) → ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +_𝑒 𝑆 ) ) )
31	24 27 28 29 30	syl22anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) → ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +_𝑒 𝑆 ) ) )
32		xmettri3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) )
33	20 21 25 22 32	syl13anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) )
34	6	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ^* )
35	24 27	xaddcld	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) ∈ ℝ^* )
36	4	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑅 +_𝑒 𝑆 ) ∈ ℝ^* )
37		xrlelttr	⊢ ( ( ( 𝑃 𝐷 𝑄 ) ∈ ℝ^* ∧ ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ∈ ℝ^* ) → ( ( ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) ∧ ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +_𝑒 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +_𝑒 𝑆 ) ) )
38	34 35 36 37	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) ∧ ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +_𝑒 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +_𝑒 𝑆 ) ) )
39	33 38	mpand	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) +_𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +_𝑒 𝑆 ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +_𝑒 𝑆 ) ) )
40	31 39	syld	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +_𝑒 𝑆 ) ) )
41	40	expimpd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +_𝑒 𝑆 ) ) )
42	19 41	sylbid	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +_𝑒 𝑆 ) ) )
43	9 42	biimtrid	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +_𝑒 𝑆 ) ) )
44	8 43	mtod	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ¬ 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) )
45	44	eq0rdv	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ ( 𝑅 +_𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) = ∅ )

Metamath Proof Explorer

Theorem bldisj

Proof