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	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ∧ 𝐴 ≠ 𝐵 ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		brofs	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ) )
2	1	anbi1d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ∧ 𝐴 ≠ 𝐵 ) ↔ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) ) )
3		simpr	⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
4		simpl1l	⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
5		simpl1r	⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) → 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ )
6	3 4 5	3jca	⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) )
7		simpl2	⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) )
8		simpl3	⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) → ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) )
9	6 7 8	3jca	⊢ ( ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) )
10	2 9	syl6bi	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) ) )
11		ax5seg	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐹 Btwn ⟨ 𝐸 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐹 , 𝐺 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐸 , 𝐻 ⟩ ∧ ⟨ 𝐵 , 𝐷 ⟩ Cgr ⟨ 𝐹 , 𝐻 ⟩ ) ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )
12	10 11	syld	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ OuterFiveSeg ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐺 , 𝐻 ⟩ ⟩ ∧ 𝐴 ≠ 𝐵 ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐺 , 𝐻 ⟩ ) )