Metamath Proof Explorer


Theorem idinside

Description: Law for finding a point inside a segment. Theorem 4.19 of Schwabhauser p. 38. (Contributed by Scott Fenton, 7-Oct-2013)

Ref Expression
Assertion idinside ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simp3l ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp3r ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
4 cgrid2 ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) )
5 1 2 2 3 4 syl13anc ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) )
6 simp2l ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
7 axbtwnid ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ → 𝐶 = 𝐴 ) )
8 1 2 6 7 syl3anc ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ → 𝐶 = 𝐴 ) )
9 opeq1 ( 𝐶 = 𝐴 → ⟨ 𝐶 , 𝐶 ⟩ = ⟨ 𝐴 , 𝐶 ⟩ )
10 opeq1 ( 𝐶 = 𝐴 → ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ )
11 9 10 breq12d ( 𝐶 = 𝐴 → ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ) )
12 11 imbi1d ( 𝐶 = 𝐴 → ( ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ↔ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ) )
13 12 biimpcd ( ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) → ( 𝐶 = 𝐴 → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ) )
14 ax-1 ( 𝐶 = 𝐷 → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ → 𝐶 = 𝐷 ) )
15 13 14 syl8 ( ( ⟨ 𝐶 , 𝐶 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ → 𝐶 = 𝐷 ) → ( 𝐶 = 𝐴 → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ) ) )
16 5 8 15 sylsyld ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ → 𝐶 = 𝐷 ) ) ) )
17 16 3impd ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )
18 opeq2 ( 𝐴 = 𝐵 → ⟨ 𝐴 , 𝐴 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
19 18 breq2d ( 𝐴 = 𝐵 → ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ ↔ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
20 19 3anbi1d ( 𝐴 = 𝐵 → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ↔ ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) )
21 20 imbi1d ( 𝐴 = 𝐵 → ( ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ↔ ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ) )
22 17 21 syl5ib ( 𝐴 = 𝐵 → ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ) )
23 simpr1 ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑁 ∈ ℕ )
24 simpr2l ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
25 simpr2r ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
26 simpr3l ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
27 btwncolinear1 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ → 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) )
28 23 24 25 26 27 syl13anc ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ → 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) )
29 idd ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ → ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ) )
30 idd ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) )
31 28 29 30 3anim123d ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) )
32 simp1 ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ )
33 32 anim2i ( ( 𝐴𝐵 ∧ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( 𝐴𝐵𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) )
34 3simpc ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) )
35 34 adantl ( ( 𝐴𝐵 ∧ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) )
36 33 35 jca ( ( 𝐴𝐵 ∧ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( ( 𝐴𝐵𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) )
37 lineid ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴𝐵𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ) ∧ ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → 𝐶 = 𝐷 ) )
38 36 37 syl5 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴𝐵 ∧ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) ) → 𝐶 = 𝐷 ) )
39 38 expd ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴𝐵 → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ) )
40 39 impcom ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )
41 31 40 syld ( ( 𝐴𝐵 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )
42 41 ex ( 𝐴𝐵 → ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) ) )
43 22 42 pm2.61ine ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 = 𝐷 ) )