Step |
Hyp |
Ref |
Expression |
1 |
|
simprrl |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ) |
2 |
1 1
|
jca |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ) ) |
3 |
|
simp11 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ ) |
4 |
|
simp21 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) |
5 |
|
simp23 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) |
6 |
3 4 5
|
cgrrflxd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 〈 𝐶 , 𝑐 〉 Cgr 〈 𝐶 , 𝑐 〉 ) |
7 |
|
simp33 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) |
8 |
3 7 5
|
cgrrflxd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 〈 𝐸 , 𝑐 〉 Cgr 〈 𝐸 , 𝑐 〉 ) |
9 |
6 8
|
jca |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐶 , 𝑐 〉 Cgr 〈 𝐶 , 𝑐 〉 ∧ 〈 𝐸 , 𝑐 〉 Cgr 〈 𝐸 , 𝑐 〉 ) ) |
10 |
9
|
adantr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → ( 〈 𝐶 , 𝑐 〉 Cgr 〈 𝐶 , 𝑐 〉 ∧ 〈 𝐸 , 𝑐 〉 Cgr 〈 𝐸 , 𝑐 〉 ) ) |
11 |
|
simp31 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) |
12 |
|
simp22 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) |
13 |
|
simp2rr |
⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) → 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) |
14 |
13
|
ad2antrl |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) |
15 |
3 4 11 4 12 14
|
cgrcomand |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐶 , 𝑑 〉 ) |
16 |
|
simp2lr |
⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) → 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) |
17 |
16
|
ad2antrl |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) |
18 |
3 12 5 4 12 17
|
cgrcomrand |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐷 , 𝐶 〉 ) |
19 |
|
3simpa |
⊢ ( ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
20 |
19
|
3anim3i |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) |
21 |
|
simpl |
⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ) |
22 |
|
btwnconn1lem4 |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ) → 〈 𝑑 , 𝑐 〉 Cgr 〈 𝐷 , 𝐶 〉 ) |
23 |
20 21 22
|
syl2an |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → 〈 𝑑 , 𝑐 〉 Cgr 〈 𝐷 , 𝐶 〉 ) |
24 |
3 12 5 11 5 12 4 18 23
|
cgrtr3and |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → 〈 𝐷 , 𝑐 〉 Cgr 〈 𝑑 , 𝑐 〉 ) |
25 |
3 12 5 11 5 24
|
cgrcomlrand |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → 〈 𝑐 , 𝐷 〉 Cgr 〈 𝑐 , 𝑑 〉 ) |
26 |
15 25
|
jca |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → ( 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐶 , 𝑑 〉 ∧ 〈 𝑐 , 𝐷 〉 Cgr 〈 𝑐 , 𝑑 〉 ) ) |
27 |
|
brifs |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 〈 𝐶 , 𝐸 〉 , 〈 𝑐 , 𝐷 〉 〉 InnerFiveSeg 〈 〈 𝐶 , 𝐸 〉 , 〈 𝑐 , 𝑑 〉 〉 ↔ ( ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ) ∧ ( 〈 𝐶 , 𝑐 〉 Cgr 〈 𝐶 , 𝑐 〉 ∧ 〈 𝐸 , 𝑐 〉 Cgr 〈 𝐸 , 𝑐 〉 ) ∧ ( 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐶 , 𝑑 〉 ∧ 〈 𝑐 , 𝐷 〉 Cgr 〈 𝑐 , 𝑑 〉 ) ) ) ) |
28 |
|
ifscgr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 〈 𝐶 , 𝐸 〉 , 〈 𝑐 , 𝐷 〉 〉 InnerFiveSeg 〈 〈 𝐶 , 𝐸 〉 , 〈 𝑐 , 𝑑 〉 〉 → 〈 𝐸 , 𝐷 〉 Cgr 〈 𝐸 , 𝑑 〉 ) ) |
29 |
27 28
|
sylbird |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ) ∧ ( 〈 𝐶 , 𝑐 〉 Cgr 〈 𝐶 , 𝑐 〉 ∧ 〈 𝐸 , 𝑐 〉 Cgr 〈 𝐸 , 𝑐 〉 ) ∧ ( 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐶 , 𝑑 〉 ∧ 〈 𝑐 , 𝐷 〉 Cgr 〈 𝑐 , 𝑑 〉 ) ) → 〈 𝐸 , 𝐷 〉 Cgr 〈 𝐸 , 𝑑 〉 ) ) |
30 |
3 4 7 5 12 4 7 5 11 29
|
syl333anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ) ∧ ( 〈 𝐶 , 𝑐 〉 Cgr 〈 𝐶 , 𝑐 〉 ∧ 〈 𝐸 , 𝑐 〉 Cgr 〈 𝐸 , 𝑐 〉 ) ∧ ( 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐶 , 𝑑 〉 ∧ 〈 𝑐 , 𝐷 〉 Cgr 〈 𝑐 , 𝑑 〉 ) ) → 〈 𝐸 , 𝐷 〉 Cgr 〈 𝐸 , 𝑑 〉 ) ) |
31 |
30
|
adantr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → ( ( ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ) ∧ ( 〈 𝐶 , 𝑐 〉 Cgr 〈 𝐶 , 𝑐 〉 ∧ 〈 𝐸 , 𝑐 〉 Cgr 〈 𝐸 , 𝑐 〉 ) ∧ ( 〈 𝐶 , 𝐷 〉 Cgr 〈 𝐶 , 𝑑 〉 ∧ 〈 𝑐 , 𝐷 〉 Cgr 〈 𝑐 , 𝑑 〉 ) ) → 〈 𝐸 , 𝐷 〉 Cgr 〈 𝐸 , 𝑑 〉 ) ) |
32 |
2 10 26 31
|
mp3and |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝑐 ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐵 Btwn 〈 𝐴 , 𝐷 〉 ) ) ∧ ( ( 𝐷 Btwn 〈 𝐴 , 𝑐 〉 ∧ 〈 𝐷 , 𝑐 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ∧ ( 𝐶 Btwn 〈 𝐴 , 𝑑 〉 ∧ 〈 𝐶 , 𝑑 〉 Cgr 〈 𝐶 , 𝐷 〉 ) ) ∧ ( ( 𝑐 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑐 , 𝑏 〉 Cgr 〈 𝐶 , 𝐵 〉 ) ∧ ( 𝑑 Btwn 〈 𝐴 , 𝑏 〉 ∧ 〈 𝑑 , 𝑏 〉 Cgr 〈 𝐷 , 𝐵 〉 ) ) ) ∧ ( 𝐸 Btwn 〈 𝐶 , 𝑐 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑑 〉 ) ) ) → 〈 𝐸 , 𝐷 〉 Cgr 〈 𝐸 , 𝑑 〉 ) |