Step |
Hyp |
Ref |
Expression |
1 |
|
brofs |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 〈 𝐴 , 𝐵 〉 , 〈 𝐶 , 𝐷 〉 〉 OuterFiveSeg 〈 〈 𝐸 , 𝐹 〉 , 〈 𝐺 , 𝐻 〉 〉 ↔ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) ) |
2 |
|
simpr1l |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ) |
3 |
|
simpr2l |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ) |
4 |
|
simpr1 |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ) |
5 |
|
simpr2 |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) |
6 |
4 5
|
jca |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) ) |
7 |
6
|
ex |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) → ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) ) ) |
8 |
|
simp11 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ ) |
9 |
|
simp12 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) |
10 |
|
simp13 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) |
11 |
|
simp21 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) |
12 |
|
simp23 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) |
13 |
|
simp31 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) |
14 |
|
simp32 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ) |
15 |
|
cgrextend |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) → 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐸 , 𝐺 〉 ) ) |
16 |
8 9 10 11 12 13 14 15
|
syl133anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) → 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐸 , 𝐺 〉 ) ) |
17 |
7 16
|
syld |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) → 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐸 , 𝐺 〉 ) ) |
18 |
17
|
imp |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐸 , 𝐺 〉 ) |
19 |
|
simpr2r |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) |
20 |
3 18 19
|
3jca |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐸 , 𝐺 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) |
21 |
20
|
ex |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐸 , 𝐺 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) ) |
22 |
|
brcgr3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ↔ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐸 , 𝐺 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) ) |
23 |
8 9 10 11 12 13 14 22
|
syl133anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ↔ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐸 , 𝐺 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) ) |
24 |
21 23
|
sylibrd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) → 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ) ) |
25 |
24
|
imp |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ) |
26 |
|
simpr3 |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) |
27 |
2 25 26
|
3jca |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) |
28 |
|
simpr1 |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ) |
29 |
|
3simpa |
⊢ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) → ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ) ) |
30 |
|
btwnxfr |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ) → 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ) |
31 |
8 9 10 11 12 13 14 30
|
syl133anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ) → 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ) |
32 |
29 31
|
syl5 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) → 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ) |
33 |
32
|
imp |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) |
34 |
28 33
|
jca |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ) |
35 |
|
3simpb |
⊢ ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐸 , 𝐺 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) |
36 |
23 35
|
syl6bi |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) ) |
37 |
36
|
imp |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) |
38 |
37
|
3ad2antr2 |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ) |
39 |
|
simpr3 |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) |
40 |
34 38 39
|
3jca |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) → ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) |
41 |
27 40
|
impbida |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐹 Btwn 〈 𝐸 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐸 , 𝐹 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐹 , 𝐺 〉 ) ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ↔ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) ) |
42 |
1 41
|
bitrd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐺 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐻 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 〈 𝐴 , 𝐵 〉 , 〈 𝐶 , 𝐷 〉 〉 OuterFiveSeg 〈 〈 𝐸 , 𝐹 〉 , 〈 𝐺 , 𝐻 〉 〉 ↔ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐸 , 〈 𝐹 , 𝐺 〉 〉 ∧ ( 〈 𝐴 , 𝐷 〉 Cgr 〈 𝐸 , 𝐻 〉 ∧ 〈 𝐵 , 𝐷 〉 Cgr 〈 𝐹 , 𝐻 〉 ) ) ) ) |