axsegcon

Description: Any segment A B can be extended to a point x such that B x is congruent to C D . Axiom A4 of Schwabhauser p. 11. (Contributed by Scott Fenton, 4-Jun-2013)

		Ref	Expression
	Assertion	axsegcon	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨B, x⟩ Cgr ⟨C, D⟩)$

Proof

Step	Hyp	Ref	Expression
1		axsegconlem1	$⊢ (A = B \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
2	1	ex	$⊢ A = B \to (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
3		simprll	$⊢ (A \neq B \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to A \in 𝔼 (N)$
4		simprlr	$⊢ (A \neq B \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to B \in 𝔼 (N)$
5		simpl	$⊢ (A \neq B \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to A \neq B$
6		simprr	$⊢ (A \neq B \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to (C \in 𝔼 (N) \land D \in 𝔼 (N))$
7		eqid	$⊢ \sum_{p = 1}^{N} {(A (p) - B (p))}^{2} = \sum_{p = 1}^{N} {(A (p) - B (p))}^{2}$
8		eqid	$⊢ \sum_{p = 1}^{N} {(C (p) - D (p))}^{2} = \sum_{p = 1}^{N} {(C (p) - D (p))}^{2}$
9		eqid	$⊢ (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}})$
10	7 8 9	axsegconlem8	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \in 𝔼 (N)$
11	7 8	axsegconlem7	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}} \in [0, 1]$
12	7 8 9	axsegconlem10	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \forall i \in (1 \dots N) B (i) = (1 - (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}})) A (i) + (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}}) (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i)$
13	7 8 9	axsegconlem9	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \sum_{i = 1}^{N} {(B (i) - (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}$
14		fveq1	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to x (i) = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i)$
15	14	oveq2d	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to t x (i) = t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i)$
16	15	oveq2d	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to (1 - t) A (i) + t x (i) = (1 - t) A (i) + t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i)$
17	16	eqeq2d	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to (B (i) = (1 - t) A (i) + t x (i) \leftrightarrow B (i) = (1 - t) A (i) + t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))$
18	17	ralbidv	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \leftrightarrow \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))$
19	14	oveq2d	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to B (i) - x (i) = B (i) - (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i)$
20	19	oveq1d	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to {(B (i) - x (i))}^{2} = {(B (i) - (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))}^{2}$
21	20	sumeq2sdv	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(B (i) - (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))}^{2}$
22	21	eqeq1d	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to (\sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} \leftrightarrow \sum_{i = 1}^{N} {(B (i) - (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
23	18 22	anbi12d	$⊢ x = (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \to ((\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}) \leftrightarrow (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i) \land \sum_{i = 1}^{N} {(B (i) - (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
24		oveq2	$⊢ t = \frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}} \to 1 - t = 1 - (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}})$
25	24	oveq1d	$⊢ t = \frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}} \to (1 - t) A (i) = (1 - (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}})) A (i)$
26		oveq1	$⊢ t = \frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}} \to t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i) = (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}}) (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i)$
27	25 26	oveq12d	$⊢ t = \frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}} \to (1 - t) A (i) + t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i) = (1 - (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}})) A (i) + (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}}) (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i)$
28	27	eqeq2d	$⊢ t = \frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}} \to (B (i) = (1 - t) A (i) + t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i) \leftrightarrow B (i) = (1 - (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}})) A (i) + (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}}) (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))$
29	28	ralbidv	$⊢ t = \frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}} \to (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i) \leftrightarrow \forall i \in (1 \dots N) B (i) = (1 - (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}})) A (i) + (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}}) (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))$
30	29	anbi1d	$⊢ t = \frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}} \to ((\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i) \land \sum_{i = 1}^{N} {(B (i) - (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}) \leftrightarrow (\forall i \in (1 \dots N) B (i) = (1 - (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}})) A (i) + (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}}) (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i) \land \sum_{i = 1}^{N} {(B (i) - (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
31	23 30	rspc2ev	$⊢ ((k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) \in 𝔼 (N) \land \frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}} \in [0, 1] \land (\forall i \in (1 \dots N) B (i) = (1 - (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}})) A (i) + (\frac{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}}) (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i) \land \sum_{i = 1}^{N} {(B (i) - (k \in (1 \dots N) ⟼ \frac{(\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}} + \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}}) B (k) - \sqrt{\sum_{p = 1}^{N} {(C (p) - D (p))}^{2}} A (k)}{\sqrt{\sum_{p = 1}^{N} {(A (p) - B (p))}^{2}}}) (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
32	10 11 12 13 31	syl112anc	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land A \neq B) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
33	3 4 5 6 32	syl31anc	$⊢ (A \neq B \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
34	33	ex	$⊢ A \neq B \to (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
35	2 34	pm2.61ine	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
36		simpllr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to B \in 𝔼 (N)$
37		simplll	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to A \in 𝔼 (N)$
38		simpr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to x \in 𝔼 (N)$
39		brbtwn	$⊢ (B \in 𝔼 (N) \land A \in 𝔼 (N) \land x \in 𝔼 (N)) \to (B Btwn ⟨A, x⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i))$
40	36 37 38 39	syl3anc	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (B Btwn ⟨A, x⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i))$
41		simplrl	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to C \in 𝔼 (N)$
42		simplrr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to D \in 𝔼 (N)$
43		brcgr	$⊢ ((B \in 𝔼 (N) \land x \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨B, x⟩ Cgr ⟨C, D⟩ \leftrightarrow \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
44	36 38 41 42 43	syl22anc	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (⟨B, x⟩ Cgr ⟨C, D⟩ \leftrightarrow \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
45	40 44	anbi12d	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to ((B Btwn ⟨A, x⟩ \land ⟨B, x⟩ Cgr ⟨C, D⟩) \leftrightarrow (\exists t \in [0, 1] \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
46		r19.41v	$⊢ \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}) \leftrightarrow (\exists t \in [0, 1] \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
47	45 46	syl6bbr	$⊢ (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to ((B Btwn ⟨A, x⟩ \land ⟨B, x⟩ Cgr ⟨C, D⟩) \leftrightarrow \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
48	47	rexbidva	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨B, x⟩ Cgr ⟨C, D⟩) \leftrightarrow \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
49	35 48	mpbird	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨B, x⟩ Cgr ⟨C, D⟩)$
50	49	3adant1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨B, x⟩ Cgr ⟨C, D⟩)$

Metamath Proof Explorer

Theorem axsegcon

Proof