Metamath Proof Explorer

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 mulid2 ⊢ ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ → ( 1 · ( 𝐴 ‘ 𝑖 ) ) = ( 𝐴 ‘ 𝑖 ) )
18 mul02 ⊢ ( ( 𝑇 ‘ 𝑖 ) ∈ ℂ → ( 0 · ( 𝑇 ‘ 𝑖 ) ) = 0 )
19 17 18 oveqan12d ⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( 𝐴 ‘ 𝑖 ) + 0 ) )
20 addid1 ⊢ ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ → ( ( 𝐴 ‘ 𝑖 ) + 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 ⟨ 𝑥 , 𝑦 ⟩ ) ) )