ax5seg

Description: The five segment axiom. Take two triangles A D C and E H G , a point B on A C , and a point F on E G . If all corresponding line segments except for C D and G H are congruent, then so are C D and G H . Axiom A5 of Schwabhauser p. 11. (Contributed by Scott Fenton, 12-Jun-2013)

		Ref	Expression
	Assertion	ax5seg	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((A \neq B \land B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (1 \dots N) \in Fin$
2		simpl21	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to C \in 𝔼 (N)$
3		fveere	$⊢ (C \in 𝔼 (N) \land j \in (1 \dots N)) \to C (j) \in ℝ$
4	2 3	sylancom	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to C (j) \in ℝ$
5		simpl22	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to D \in 𝔼 (N)$
6		fveere	$⊢ (D \in 𝔼 (N) \land j \in (1 \dots N)) \to D (j) \in ℝ$
7	5 6	sylancom	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to D (j) \in ℝ$
8	4 7	resubcld	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to C (j) - D (j) \in ℝ$
9	8	resqcld	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to {(C (j) - D (j))}^{2} \in ℝ$
10	1 9	fsumrecl	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} \in ℝ$
11	10	recnd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} \in ℂ$
12	11	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} \in ℂ$
13		simpl32	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to G \in 𝔼 (N)$
14		fveere	$⊢ (G \in 𝔼 (N) \land j \in (1 \dots N)) \to G (j) \in ℝ$
15	13 14	sylancom	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to G (j) \in ℝ$
16		simpl33	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to H \in 𝔼 (N)$
17		fveere	$⊢ (H \in 𝔼 (N) \land j \in (1 \dots N)) \to H (j) \in ℝ$
18	16 17	sylancom	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to H (j) \in ℝ$
19	15 18	resubcld	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to G (j) - H (j) \in ℝ$
20	19	resqcld	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land j \in (1 \dots N)) \to {(G (j) - H (j))}^{2} \in ℝ$
21	1 20	fsumrecl	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to \sum_{j = 1}^{N} {(G (j) - H (j))}^{2} \in ℝ$
22	21	recnd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to \sum_{j = 1}^{N} {(G (j) - H (j))}^{2} \in ℂ$
23	22	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to \sum_{j = 1}^{N} {(G (j) - H (j))}^{2} \in ℂ$
24		elicc01	$⊢ t \in [0, 1] \leftrightarrow (t \in ℝ \land 0 \leq t \land t \leq 1)$
25	24	simp1bi	$⊢ t \in [0, 1] \to t \in ℝ$
26	25	recnd	$⊢ t \in [0, 1] \to t \in ℂ$
27	26	ad2antrr	$⊢ ((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \to t \in ℂ$
28	27	3ad2ant1	$⊢ (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to t \in ℂ$
29	28	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t \in ℂ$
30		simpl11	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to N \in ℕ$
31		simp12	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to A \in 𝔼 (N)$
32		simp13	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to B \in 𝔼 (N)$
33		simp21	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to C \in 𝔼 (N)$
34	31 32 33	3jca	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))$
35	34	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))$
36		simprrl	$⊢ ((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \to \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i)$
37	36	3ad2ant1	$⊢ (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i)$
38	37	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i)$
39		simp1rl	$⊢ (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to A \neq B$
40	39	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to A \neq B$
41		ax5seglem4	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \land \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land A \neq B) \to t \neq 0$
42	30 35 38 40 41	syl211anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t \neq 0$
43		simpr3r	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ⟨B, D⟩ Cgr ⟨F, H⟩$
44		simpl13	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to B \in 𝔼 (N)$
45		simpl22	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to D \in 𝔼 (N)$
46		simpl31	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to F \in 𝔼 (N)$
47		simpl33	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to H \in 𝔼 (N)$
48		brcgr	$⊢ ((B \in 𝔼 (N) \land D \in 𝔼 (N)) \land (F \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨B, D⟩ Cgr ⟨F, H⟩ \leftrightarrow \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(F (j) - H (j))}^{2})$
49	44 45 46 47 48	syl22anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (⟨B, D⟩ Cgr ⟨F, H⟩ \leftrightarrow \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(F (j) - H (j))}^{2})$
50	43 49	mpbid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(F (j) - H (j))}^{2}$
51		simp23	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to E \in 𝔼 (N)$
52		simp31	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to F \in 𝔼 (N)$
53		simp32	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to G \in 𝔼 (N)$
54	51 52 53	3jca	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N))$
55	34 54	jca	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N)))$
56	55	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N)))$
57		simpr1l	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (t \in [0, 1] \land s \in [0, 1])$
58		simprrr	$⊢ ((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \to \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)$
59	58	3ad2ant1	$⊢ (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)$
60	59	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)$
61	38 60	jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))$
62		simpr2l	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ⟨A, B⟩ Cgr ⟨E, F⟩$
63		simpr2r	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ⟨B, C⟩ Cgr ⟨F, G⟩$
64		ax5seglem6	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N)))) \land (A \neq B \land (t \in [0, 1] \land s \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)) \to t = s$
65	30 56 40 57 61 62 63 64	syl232anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t = s$
66	65	oveq2d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to 1 - t = 1 - s$
67	54	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N))$
68		ax5seglem3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N))) \land ((t \in [0, 1] \land s \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)) \to \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(E (j) - G (j))}^{2}$
69	30 35 67 57 61 62 63 68	syl322anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(E (j) - G (j))}^{2}$
70	65 69	oveq12d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = s \sum_{j = 1}^{N} {(E (j) - G (j))}^{2}$
71		simpr3l	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ⟨A, D⟩ Cgr ⟨E, H⟩$
72		simpl12	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to A \in 𝔼 (N)$
73		simpl23	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to E \in 𝔼 (N)$
74		brcgr	$⊢ ((A \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨A, D⟩ Cgr ⟨E, H⟩ \leftrightarrow \sum_{j = 1}^{N} {(A (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(E (j) - H (j))}^{2})$
75	72 45 73 47 74	syl22anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (⟨A, D⟩ Cgr ⟨E, H⟩ \leftrightarrow \sum_{j = 1}^{N} {(A (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(E (j) - H (j))}^{2})$
76	71 75	mpbid	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to \sum_{j = 1}^{N} {(A (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(E (j) - H (j))}^{2}$
77	70 76	oveq12d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2} = s \sum_{j = 1}^{N} {(E (j) - G (j))}^{2} - \sum_{j = 1}^{N} {(E (j) - H (j))}^{2}$
78	66 77	oveq12d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (1 - t) (t \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2}) = (1 - s) (s \sum_{j = 1}^{N} {(E (j) - G (j))}^{2} - \sum_{j = 1}^{N} {(E (j) - H (j))}^{2})$
79	50 78	oveq12d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} + (1 - t) (t \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2}) = \sum_{j = 1}^{N} {(F (j) - H (j))}^{2} + (1 - s) (s \sum_{j = 1}^{N} {(E (j) - G (j))}^{2} - \sum_{j = 1}^{N} {(E (j) - H (j))}^{2})$
80	31 32	jca	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (A \in 𝔼 (N) \land B \in 𝔼 (N))$
81		simp22	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to D \in 𝔼 (N)$
82	80 33 81	jca32	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))$
83	82	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))$
84		simp1ll	$⊢ (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to t \in [0, 1]$
85	84	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t \in [0, 1]$
86		ax5seglem9	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (t \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i))) \to t \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} + (1 - t) (t \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2})$
87	30 83 85 38 86	syl22anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} + (1 - t) (t \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2})$
88		3simpc	$⊢ (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N)) \to (G \in 𝔼 (N) \land H \in 𝔼 (N))$
89	88	3ad2ant3	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (G \in 𝔼 (N) \land H \in 𝔼 (N))$
90	51 52 89	jca31	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((E \in 𝔼 (N) \land F \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N)))$
91	90	adantr	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ((E \in 𝔼 (N) \land F \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N)))$
92		simp1lr	$⊢ (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to s \in [0, 1]$
93	92	adantl	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to s \in [0, 1]$
94		ax5seglem9	$⊢ ((N \in ℕ \land ((E \in 𝔼 (N) \land F \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N)))) \land (s \in [0, 1] \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \to s \sum_{j = 1}^{N} {(G (j) - H (j))}^{2} = \sum_{j = 1}^{N} {(F (j) - H (j))}^{2} + (1 - s) (s \sum_{j = 1}^{N} {(E (j) - G (j))}^{2} - \sum_{j = 1}^{N} {(E (j) - H (j))}^{2})$
95	30 91 93 60 94	syl22anc	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to s \sum_{j = 1}^{N} {(G (j) - H (j))}^{2} = \sum_{j = 1}^{N} {(F (j) - H (j))}^{2} + (1 - s) (s \sum_{j = 1}^{N} {(E (j) - G (j))}^{2} - \sum_{j = 1}^{N} {(E (j) - H (j))}^{2})$
96	79 87 95	3eqtr4d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = s \sum_{j = 1}^{N} {(G (j) - H (j))}^{2}$
97	65	oveq1d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t \sum_{j = 1}^{N} {(G (j) - H (j))}^{2} = s \sum_{j = 1}^{N} {(G (j) - H (j))}^{2}$
98	96 97	eqtr4d	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to t \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = t \sum_{j = 1}^{N} {(G (j) - H (j))}^{2}$
99	12 23 29 42 98	mulcanad	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(G (j) - H (j))}^{2}$
100	99	3exp2	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((t \in [0, 1] \land s \in [0, 1]) \land (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))) \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \to ((⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \to \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(G (j) - H (j))}^{2})))$
101	100	expd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((t \in [0, 1] \land s \in [0, 1]) \to ((A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \to ((⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \to \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(G (j) - H (j))}^{2}))))$
102	101	rexlimdvv	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (\exists t \in [0, 1] \exists s \in [0, 1] (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \to ((⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩) \to \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(G (j) - H (j))}^{2})))$
103	102	3impd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((\exists t \in [0, 1] \exists s \in [0, 1] (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(G (j) - H (j))}^{2})$
104		brbtwn	$⊢ (B \in 𝔼 (N) \land A \in 𝔼 (N) \land C \in 𝔼 (N)) \to (B Btwn ⟨A, C⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i))$
105	32 31 33 104	syl3anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (B Btwn ⟨A, C⟩ \leftrightarrow \exists t \in [0, 1] \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i))$
106		brbtwn	$⊢ (F \in 𝔼 (N) \land E \in 𝔼 (N) \land G \in 𝔼 (N)) \to (F Btwn ⟨E, G⟩ \leftrightarrow \exists s \in [0, 1] \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))$
107	52 51 53 106	syl3anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (F Btwn ⟨E, G⟩ \leftrightarrow \exists s \in [0, 1] \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))$
108	105 107	anbi12d	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \leftrightarrow (\exists t \in [0, 1] \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \exists s \in [0, 1] \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))$
109		reeanv	$⊢ \exists t \in [0, 1] \exists s \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)) \leftrightarrow (\exists t \in [0, 1] \forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \exists s \in [0, 1] \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))$
110	108 109	bitr4di	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \leftrightarrow \exists t \in [0, 1] \exists s \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))$
111	110	anbi2d	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((A \neq B \land (B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩)) \leftrightarrow (A \neq B \land \exists t \in [0, 1] \exists s \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))))$
112		3anass	$⊢ (A \neq B \land B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \leftrightarrow (A \neq B \land (B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩))$
113		r19.42v	$⊢ \exists s \in [0, 1] (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \leftrightarrow (A \neq B \land \exists s \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))$
114	113	rexbii	$⊢ \exists t \in [0, 1] \exists s \in [0, 1] (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \leftrightarrow \exists t \in [0, 1] (A \neq B \land \exists s \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))$
115		r19.42v	$⊢ \exists t \in [0, 1] (A \neq B \land \exists s \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \leftrightarrow (A \neq B \land \exists t \in [0, 1] \exists s \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))$
116	114 115	bitri	$⊢ \exists t \in [0, 1] \exists s \in [0, 1] (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \leftrightarrow (A \neq B \land \exists t \in [0, 1] \exists s \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i)))$
117	111 112 116	3bitr4g	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((A \neq B \land B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \leftrightarrow \exists t \in [0, 1] \exists s \in [0, 1] (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))))$
118	117	3anbi1d	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((A \neq B \land B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \leftrightarrow (\exists t \in [0, 1] \exists s \in [0, 1] (A \neq B \land (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t C (i) \land \forall i \in (1 \dots N) F (i) = (1 - s) E (i) + s G (i))) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
119		simp33	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to H \in 𝔼 (N)$
120		brcgr	$⊢ ((C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨C, D⟩ Cgr ⟨G, H⟩ \leftrightarrow \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(G (j) - H (j))}^{2})$
121	33 81 53 119 120	syl22anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨C, D⟩ Cgr ⟨G, H⟩ \leftrightarrow \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(G (j) - H (j))}^{2})$
122	103 118 121	3imtr4d	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((A \neq B \land B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$

Metamath Proof Explorer

Theorem ax5seg

Proof