midofsegid

Description: If two points fall in the same place in the middle of a segment, then they are identical. (Contributed by Scott Fenton, 16-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	midofsegid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \to D = E)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to N \in ℕ$
2		simp2l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to A \in 𝔼 (N)$
3		simp3r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to E \in 𝔼 (N)$
4		simp3l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to D \in 𝔼 (N)$
5		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \land D Btwn ⟨A, E⟩)) \to D Btwn ⟨A, E⟩$
6		simprl3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \land D Btwn ⟨A, E⟩)) \to ⟨A, D⟩ Cgr ⟨A, E⟩$
7	1 2 4 2 3 6	cgrcomand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \land D Btwn ⟨A, E⟩)) \to ⟨A, E⟩ Cgr ⟨A, D⟩$
8	1 2 3 4 5 7	endofsegidand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \land D Btwn ⟨A, E⟩)) \to E = D$
9	8	eqcomd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \land D Btwn ⟨A, E⟩)) \to D = E$
10	9	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land (D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩)) \to (D Btwn ⟨A, E⟩ \to D = E)$
11		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \land E Btwn ⟨A, D⟩)) \to E Btwn ⟨A, D⟩$
12		simprl3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \land E Btwn ⟨A, D⟩)) \to ⟨A, D⟩ Cgr ⟨A, E⟩$
13	1 2 4 3 11 12	endofsegidand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \land E Btwn ⟨A, D⟩)) \to D = E$
14	13	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land (D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩)) \to (E Btwn ⟨A, D⟩ \to D = E)$
15		3simpa	$⊢ (D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \to (D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩)$
16	15	adantl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land (D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩)) \to (D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩)$
17		simp2r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to B \in 𝔼 (N)$
18		btwnconn3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land B \in 𝔼 (N))) \to ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩) \to (D Btwn ⟨A, E⟩ \lor E Btwn ⟨A, D⟩))$
19	1 2 4 3 17 18	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩) \to (D Btwn ⟨A, E⟩ \lor E Btwn ⟨A, D⟩))$
20	19	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land (D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩)) \to ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩) \to (D Btwn ⟨A, E⟩ \lor E Btwn ⟨A, D⟩))$
21	16 20	mpd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land (D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩)) \to (D Btwn ⟨A, E⟩ \lor E Btwn ⟨A, D⟩)$
22	10 14 21	mpjaod	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \land (D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩)) \to D = E$
23	22	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to ((D Btwn ⟨A, B⟩ \land E Btwn ⟨A, B⟩ \land ⟨A, D⟩ Cgr ⟨A, E⟩) \to D = E)$

Metamath Proof Explorer

Theorem midofsegid

Proof