Step |
Hyp |
Ref |
Expression |
1 |
|
brcolinear |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear 〈 𝐵 , 𝐶 〉 ↔ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∨ 𝐵 Btwn 〈 𝐶 , 𝐴 〉 ∨ 𝐶 Btwn 〈 𝐴 , 𝐵 〉 ) ) ) |
2 |
1
|
3adant3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear 〈 𝐵 , 𝐶 〉 ↔ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∨ 𝐵 Btwn 〈 𝐶 , 𝐴 〉 ∨ 𝐶 Btwn 〈 𝐴 , 𝐵 〉 ) ) ) |
3 |
2
|
anbi1d |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Colinear 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ↔ ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∨ 𝐵 Btwn 〈 𝐶 , 𝐴 〉 ∨ 𝐶 Btwn 〈 𝐴 , 𝐵 〉 ) ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) ) |
4 |
|
simp1 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ ) |
5 |
|
simp3r |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) |
6 |
|
simp3l |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) |
7 |
5 6
|
jca |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
8 |
|
simp21 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) |
9 |
|
simp23 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) |
10 |
8 9
|
jca |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
11 |
4 7 10
|
3jca |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) |
12 |
11
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) |
13 |
|
axsegcon |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐷 , 𝑓 〉 Cgr 〈 𝐴 , 𝐶 〉 ) ) |
14 |
12 13
|
syl |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐷 , 𝑓 〉 Cgr 〈 𝐴 , 𝐶 〉 ) ) |
15 |
|
simprlr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ∧ ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ) → 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) |
16 |
|
simprrr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ∧ ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ) → 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) |
17 |
|
an4 |
⊢ ( ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ∧ ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ↔ ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ) |
18 |
|
simpl1 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ ) |
19 |
|
simpl21 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) |
20 |
|
simpl22 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) |
21 |
|
simpl3l |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) |
22 |
|
simpl3r |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) |
23 |
|
cgrcomlr |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ↔ 〈 𝐵 , 𝐴 〉 Cgr 〈 𝐸 , 𝐷 〉 ) ) |
24 |
18 19 20 21 22 23
|
syl122anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ↔ 〈 𝐵 , 𝐴 〉 Cgr 〈 𝐸 , 𝐷 〉 ) ) |
25 |
24
|
anbi1d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ↔ ( 〈 𝐵 , 𝐴 〉 Cgr 〈 𝐸 , 𝐷 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ) |
26 |
25
|
anbi2d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ↔ ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ) ∧ ( 〈 𝐵 , 𝐴 〉 Cgr 〈 𝐸 , 𝐷 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ) ) |
27 |
|
simpl23 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) |
28 |
|
simpr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) |
29 |
|
cgrextend |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ) ∧ ( 〈 𝐵 , 𝐴 〉 Cgr 〈 𝐸 , 𝐷 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) → 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) |
30 |
18 20 19 27 22 21 28 29
|
syl133anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ) ∧ ( 〈 𝐵 , 𝐴 〉 Cgr 〈 𝐸 , 𝐷 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) → 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) |
31 |
26 30
|
sylbid |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) → 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) |
32 |
17 31
|
syl5bi |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ∧ ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) → 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) |
33 |
32
|
imp |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ∧ ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ) → 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) |
34 |
15 16 33
|
3jca |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ∧ ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) |
35 |
34
|
expr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ( ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) |
36 |
|
cgrcom |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐷 , 𝑓 〉 Cgr 〈 𝐴 , 𝐶 〉 ↔ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) |
37 |
18 21 28 19 27 36
|
syl122anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 〈 𝐷 , 𝑓 〉 Cgr 〈 𝐴 , 𝐶 〉 ↔ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) |
38 |
37
|
anbi2d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐷 , 𝑓 〉 Cgr 〈 𝐴 , 𝐶 〉 ) ↔ ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ) |
39 |
38
|
adantr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ( ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐷 , 𝑓 〉 Cgr 〈 𝐴 , 𝐶 〉 ) ↔ ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) ) |
40 |
|
simpl2 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
41 |
|
brcgr3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ↔ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) |
42 |
18 40 21 22 28 41
|
syl113anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ↔ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) |
43 |
42
|
adantr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ( 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ↔ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) |
44 |
35 39 43
|
3imtr4d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ( ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐷 , 𝑓 〉 Cgr 〈 𝐴 , 𝐶 〉 ) → 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
45 |
44
|
an32s |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐷 , 𝑓 〉 Cgr 〈 𝐴 , 𝐶 〉 ) → 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
46 |
45
|
reximdva |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ( ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn 〈 𝐸 , 𝑓 〉 ∧ 〈 𝐷 , 𝑓 〉 Cgr 〈 𝐴 , 𝐶 〉 ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
47 |
14 46
|
mpd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) |
48 |
47
|
exp32 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) ) |
49 |
|
3ancoma |
⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
50 |
|
btwncom |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ↔ 𝐵 Btwn 〈 𝐶 , 𝐴 〉 ) ) |
51 |
49 50
|
sylan2b |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ↔ 𝐵 Btwn 〈 𝐶 , 𝐴 〉 ) ) |
52 |
51
|
3adant3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ↔ 𝐵 Btwn 〈 𝐶 , 𝐴 〉 ) ) |
53 |
|
simp3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
54 |
|
simp22 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) |
55 |
|
axsegcon |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) ) |
56 |
4 53 54 9 55
|
syl112anc |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) ) |
57 |
56
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) ) |
58 |
|
cgrextend |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) → 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) |
59 |
18 40 21 22 28 58
|
syl113anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) → 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) ) |
60 |
|
simpll |
⊢ ( ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) → 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) |
61 |
|
simpr |
⊢ ( ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) → 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) |
62 |
|
simplr |
⊢ ( ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) → 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) |
63 |
60 61 62
|
3jca |
⊢ ( ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) |
64 |
63
|
ex |
⊢ ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) → ( 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) |
65 |
64
|
adantl |
⊢ ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) → ( 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) |
66 |
59 65
|
sylcom |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 𝐶 〉 Cgr 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) |
67 |
|
an4 |
⊢ ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ∧ ( 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) ) ↔ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) ) ) |
68 |
|
cgrcom |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ↔ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) |
69 |
18 22 28 20 27 68
|
syl122anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ↔ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) |
70 |
69
|
anbi2d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) ↔ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) |
71 |
70
|
anbi2d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) ) ↔ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) ) |
72 |
67 71
|
syl5bb |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ∧ ( 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) ) ↔ ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ) ∧ ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐵 , 𝐶 〉 Cgr 〈 𝐸 , 𝑓 〉 ) ) ) ) |
73 |
66 72 42
|
3imtr4d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ∧ ( 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) ) → 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
74 |
73
|
expdimp |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ( ( 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) → 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
75 |
74
|
an32s |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) → 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
76 |
75
|
reximdva |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ( ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐸 Btwn 〈 𝐷 , 𝑓 〉 ∧ 〈 𝐸 , 𝑓 〉 Cgr 〈 𝐵 , 𝐶 〉 ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
77 |
57 76
|
mpd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) |
78 |
77
|
exp32 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn 〈 𝐴 , 𝐶 〉 → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) ) |
79 |
52 78
|
sylbird |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn 〈 𝐶 , 𝐴 〉 → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) ) |
80 |
|
cgrxfr |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn 〈 𝐴 , 𝐵 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑓 Btwn 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 〈 𝐶 , 𝐵 〉 〉 Cgr3 〈 𝐷 , 〈 𝑓 , 𝐸 〉 〉 ) ) ) |
81 |
4 8 9 54 53 80
|
syl131anc |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn 〈 𝐴 , 𝐵 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑓 Btwn 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 〈 𝐶 , 𝐵 〉 〉 Cgr3 〈 𝐷 , 〈 𝑓 , 𝐸 〉 〉 ) ) ) |
82 |
|
cgr3permute1 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ↔ 〈 𝐴 , 〈 𝐶 , 𝐵 〉 〉 Cgr3 〈 𝐷 , 〈 𝑓 , 𝐸 〉 〉 ) ) |
83 |
18 40 21 22 28 82
|
syl113anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ↔ 〈 𝐴 , 〈 𝐶 , 𝐵 〉 〉 Cgr3 〈 𝐷 , 〈 𝑓 , 𝐸 〉 〉 ) ) |
84 |
83
|
biimprd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 〈 𝐴 , 〈 𝐶 , 𝐵 〉 〉 Cgr3 〈 𝐷 , 〈 𝑓 , 𝐸 〉 〉 → 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
85 |
84
|
adantld |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑓 Btwn 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 〈 𝐶 , 𝐵 〉 〉 Cgr3 〈 𝐷 , 〈 𝑓 , 𝐸 〉 〉 ) → 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
86 |
85
|
reximdva |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑓 Btwn 〈 𝐷 , 𝐸 〉 ∧ 〈 𝐴 , 〈 𝐶 , 𝐵 〉 〉 Cgr3 〈 𝐷 , 〈 𝑓 , 𝐸 〉 〉 ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
87 |
81 86
|
syld |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn 〈 𝐴 , 𝐵 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
88 |
87
|
expd |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn 〈 𝐴 , 𝐵 〉 → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) ) |
89 |
48 79 88
|
3jaod |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∨ 𝐵 Btwn 〈 𝐶 , 𝐴 〉 ∨ 𝐶 Btwn 〈 𝐴 , 𝐵 〉 ) → ( 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) ) |
90 |
89
|
impd |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 Btwn 〈 𝐵 , 𝐶 〉 ∨ 𝐵 Btwn 〈 𝐶 , 𝐴 〉 ∨ 𝐶 Btwn 〈 𝐴 , 𝐵 〉 ) ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |
91 |
3 90
|
sylbid |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Colinear 〈 𝐵 , 𝐶 〉 ∧ 〈 𝐴 , 𝐵 〉 Cgr 〈 𝐷 , 𝐸 〉 ) → ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑁 ) 〈 𝐴 , 〈 𝐵 , 𝐶 〉 〉 Cgr3 〈 𝐷 , 〈 𝐸 , 𝑓 〉 〉 ) ) |