Theorem ax5seglem4

Description: Lemma for ax5seg . Given two distinct points, the scaling constant in a betweenness statement is nonzero. (Contributed by Scott Fenton, 11-Jun-2013)

	Ref	Expression
Assertion	ax5seglem4	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ 𝐴 ≠ 𝐵 ) → 𝑇 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑇 = 0 → ( 1 − 𝑇 ) = ( 1 − 0 ) )
2		1m0e1	⊢ ( 1 − 0 ) = 1
3	1 2	eqtrdi	⊢ ( 𝑇 = 0 → ( 1 − 𝑇 ) = 1 )
4	3	oveq1d	⊢ ( 𝑇 = 0 → ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) = ( 1 · ( 𝐴 ‘ 𝑖 ) ) )
5		oveq1	⊢ ( 𝑇 = 0 → ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) = ( 0 · ( 𝐶 ‘ 𝑖 ) ) )
6	4 5	oveq12d	⊢ ( 𝑇 = 0 → ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) = ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) )
7	6	eqeq2d	⊢ ( 𝑇 = 0 → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
8	7	ralbidv	⊢ ( 𝑇 = 0 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
9	8	biimpac	⊢ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ 𝑇 = 0 ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) )
10		eqeefv	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )
11	10	3adant1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )
12	11	3adant3r3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )
13		simplr1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
14		fveecn	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
15	13 14	sylancom	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
16		simplr3	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
17		fveecn	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
18	16 17	sylancom	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
19		mulid2	⊢ ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ → ( 1 · ( 𝐴 ‘ 𝑖 ) ) = ( 𝐴 ‘ 𝑖 ) )
20		mul02	⊢ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ → ( 0 · ( 𝐶 ‘ 𝑖 ) ) = 0 )
21	19 20	oveqan12d	⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) = ( ( 𝐴 ‘ 𝑖 ) + 0 ) )
22		addid1	⊢ ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ → ( ( 𝐴 ‘ 𝑖 ) + 0 ) = ( 𝐴 ‘ 𝑖 ) )
23	22	adantr	⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( ( 𝐴 ‘ 𝑖 ) + 0 ) = ( 𝐴 ‘ 𝑖 ) )
24	21 23	eqtrd	⊢ ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) = ( 𝐴 ‘ 𝑖 ) )
25	15 18 24	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) = ( 𝐴 ‘ 𝑖 ) )
26	25	eqeq1d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) = ( 𝐵 ‘ 𝑖 ) ↔ ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )
27		eqcom	⊢ ( ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) = ( 𝐵 ‘ 𝑖 ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) )
28	26 27	bitr3di	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
29	28	ralbidva	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
30	12 29	bitrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( 1 · ( 𝐴 ‘ 𝑖 ) ) + ( 0 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
31	9 30	syl5ibr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ 𝑇 = 0 ) → 𝐴 = 𝐵 ) )
32	31	expdimp	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( 𝑇 = 0 → 𝐴 = 𝐵 ) )
33	32	necon3d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( 𝐴 ≠ 𝐵 → 𝑇 ≠ 0 ) )
34	33	3impia	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ 𝐴 ≠ 𝐵 ) → 𝑇 ≠ 0 )