Metamath Proof Explorer

Theorem 5segofs

Description: Rephrase ax5seg using the outer five segment predicate. Theorem 2.10 of Schwabhauser p. 28. (Contributed by Scott Fenton, 21-Sep-2013)

		Ref	Expression
	Assertion	5segofs	$⊢ ((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, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land A \neq B) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$

Proof

Step	Hyp	Ref	Expression
1		brofs	$⊢ ((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, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow ((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⟩)))$
2	1	anbi1d	$⊢ ((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, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land A \neq B) \leftrightarrow (((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⟩)) \land A \neq B))$
3		simpr	$⊢ (((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⟩)) \land A \neq B) \to A \neq B$
4		simpl1l	$⊢ (((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⟩)) \land A \neq B) \to B Btwn ⟨A, C⟩$
5		simpl1r	$⊢ (((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⟩)) \land A \neq B) \to F Btwn ⟨E, G⟩$
6	3 4 5	3jca	$⊢ (((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⟩)) \land A \neq B) \to (A \neq B \land B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩)$
7		simpl2	$⊢ (((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⟩)) \land A \neq B) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
8		simpl3	$⊢ (((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⟩)) \land A \neq B) \to (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)$
9	6 7 8	3jca	$⊢ (((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⟩)) \land A \neq B) \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⟩))$
10	2 9	syl6bi	$⊢ ((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, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land A \neq B) \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⟩)))$
11		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⟩)$
12	10 11	syld	$⊢ ((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, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land A \neq B) \to ⟨C, D⟩ Cgr ⟨G, H⟩)$