Theorem axeuclid

Description: Euclid's axiom. Take an angle B A C and a point D between B and C . Now, if you extend the segment A D to a point T , then T lies between two points x and y that lie on the angle. Axiom A10 of Schwabhauser p. 13. (Contributed by Scott Fenton, 9-Sep-2013)

	Ref	Expression
Assertion	axeuclid	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑇 ⟩ ∧ 𝐷 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐴 ≠ 𝐷 ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑦 ⟩ ∧ 𝑇 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl21	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
2		simpl22	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
3	1 2	jca	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
4		simpl23	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5		simpl3r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) )
6	4 5	jca	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) )
7		simprll	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → 𝑝 ∈ ( 0 [,] 1 ) )
8		simprlr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → 𝑞 ∈ ( 0 [,] 1 ) )
9		simp21	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
10	9	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
11		fveecn	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
12	10 11	sylan	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
13		simp3r	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) )
14	13	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) → 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) )
15		fveecn	⊢ ( ( 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑖 ) ∈ ℂ )
16	14 15	sylan	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑖 ) ∈ ℂ )
17		mullid	⊢ ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ → ( 1 · ( 𝐴 ‘ 𝑖 ) ) = ( 𝐴 ‘ 𝑖 ) )
18		mul02	⊢ ( ( 𝑇 ‘ 𝑖 ) ∈ ℂ → ( 0 · ( 𝑇 ‘ 𝑖 ) ) = 0 )
19	17 18	oveqan12d	⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( 𝐴 ‘ 𝑖 ) + 0 ) )
20		addrid	⊢ ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ → ( ( 𝐴 ‘ 𝑖 ) + 0 ) = ( 𝐴 ‘ 𝑖 ) )
21	20	adantr	⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) → ( ( 𝐴 ‘ 𝑖 ) + 0 ) = ( 𝐴 ‘ 𝑖 ) )
22	19 21	eqtrd	⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝑇 ‘ 𝑖 ) ) ) = ( 𝐴 ‘ 𝑖 ) )
23	12 16 22	syl2anc	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝑇 ‘ 𝑖 ) ) ) = ( 𝐴 ‘ 𝑖 ) )
24		oveq2	⊢ ( 𝑝 = 0 → ( 1 − 𝑝 ) = ( 1 − 0 ) )
25		1m0e1	⊢ ( 1 − 0 ) = 1
26	24 25	eqtrdi	⊢ ( 𝑝 = 0 → ( 1 − 𝑝 ) = 1 )
27	26	oveq1d	⊢ ( 𝑝 = 0 → ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) = ( 1 · ( 𝐴 ‘ 𝑖 ) ) )
28		oveq1	⊢ ( 𝑝 = 0 → ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) = ( 0 · ( 𝑇 ‘ 𝑖 ) ) )
29	27 28	oveq12d	⊢ ( 𝑝 = 0 → ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝑇 ‘ 𝑖 ) ) ) )
30	29	eqeq1d	⊢ ( 𝑝 = 0 → ( ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) = ( 𝐴 ‘ 𝑖 ) ↔ ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝑇 ‘ 𝑖 ) ) ) = ( 𝐴 ‘ 𝑖 ) ) )
31	30	ad2antlr	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) = ( 𝐴 ‘ 𝑖 ) ↔ ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝑇 ‘ 𝑖 ) ) ) = ( 𝐴 ‘ 𝑖 ) ) )
32	23 31	mpbird	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) = ( 𝐴 ‘ 𝑖 ) )
33	32	eqeq2d	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ↔ ( 𝐷 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) ) )
34		eqcom	⊢ ( ( 𝐷 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) ↔ ( 𝐴 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) )
35	33 34	bitrdi	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ↔ ( 𝐴 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) ) )
36	35	biimpd	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) → ( 𝐴 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) ) )
37	36	adantrd	⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( 𝐴 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) ) )
38	37	ralimdva	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑝 = 0 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) ) )
39	38	impancom	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 𝑝 = 0 → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) ) )
40	9	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
41		simp3l	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
42	41	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
43		eqeefv	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 = 𝐷 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) ) )
44	40 42 43	syl2anc	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 𝐴 = 𝐷 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) ) )
45	39 44	sylibrd	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 𝑝 = 0 → 𝐴 = 𝐷 ) )
46	45	necon3d	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ( 𝐴 ≠ 𝐷 → 𝑝 ≠ 0 ) )
47	46	impr	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) → 𝑝 ≠ 0 )
48	47	anasss	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → 𝑝 ≠ 0 )
49		eqtr2	⊢ ( ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) )
50	49	ralimi	⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) )
51	50	adantr	⊢ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) )
52	51	ad2antll	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) )
53		axeuclidlem	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ∧ 𝑝 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
54	3 6 7 8 48 52 53	syl231anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
55	54	exp32	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑝 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) ) )
56	55	rexlimdvv	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
57		brbtwn	⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝑇 ⟩ ↔ ∃ 𝑝 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ) )
58	41 9 13 57	syl3anc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝑇 ⟩ ↔ ∃ 𝑝 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ) )
59		simp22	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
60		simp23	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
61		brbtwn	⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐷 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
62	41 59 60 61	syl3anc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐷 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
63	58 62	3anbi12d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑇 ⟩ ∧ 𝐷 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐴 ≠ 𝐷 ) ↔ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) )
64		r19.26	⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
65	64	2rexbii	⊢ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
66		reeanv	⊢ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
67	65 66	bitri	⊢ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
68	67	anbi1i	⊢ ( ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ↔ ( ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) )
69		r19.41vv	⊢ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ↔ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) )
70		df-3an	⊢ ( ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ 𝐴 ≠ 𝐷 ) ↔ ( ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) )
71	68 69 70	3bitr4i	⊢ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ↔ ( ∃ 𝑝 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ 𝐴 ≠ 𝐷 ) )
72	63 71	bitr4di	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑇 ⟩ ∧ 𝐷 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐴 ≠ 𝐷 ) ↔ ∃ 𝑝 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑝 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑝 · ( 𝑇 ‘ 𝑖 ) ) ) ∧ ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∧ 𝐴 ≠ 𝐷 ) ) )
73		simpl22	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
74		simpl21	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
75		simprl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
76		brbtwn	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
77	73 74 75 76	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
78		simpl23	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
79		simprr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
80		brbtwn	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝑦 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
81	78 74 79 80	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝑦 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
82		simpl3r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) )
83		brbtwn	⊢ ( ( 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑇 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
84	82 75 79 83	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑇 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
85	77 81 84	3anbi123d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑦 ⟩ ∧ 𝑇 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
86		r19.26-3	⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
87	86	rexbii	⊢ ( ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑢 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
88	87	2rexbii	⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
89		3reeanv	⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
90	88 89	bitri	⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
91	85 90	bitr4di	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑦 ⟩ ∧ 𝑇 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
92	91	2rexbidva	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑦 ⟩ ∧ 𝑇 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
93	56 72 92	3imtr4d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝑇 ⟩ ∧ 𝐷 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐴 ≠ 𝐷 ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑦 ⟩ ∧ 𝑇 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) )