Theorem ax5seglem5

Description: Lemma for ax5seg . If B is between A and C , and A is distinct from B , then A is distinct from C . (Contributed by Scott Fenton, 11-Jun-2013)

	Ref	Expression
Assertion	ax5seglem5	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) =/= 0 )

Proof

Step	Hyp	Ref	Expression
1		fveq1	|- ( A = C -> ( A ` i ) = ( C ` i ) )
2	1	oveq2d	|- ( A = C -> ( T x. ( A ` i ) ) = ( T x. ( C ` i ) ) )
3	2	oveq2d	|- ( A = C -> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) )
4	3	eqeq2d	|- ( A = C -> ( ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) <-> ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) )
5	4	ralbidv	|- ( A = C -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) )
6	5	biimparc	|- ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A = C ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) )
7		simplr1	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> A e. ( EE ` N ) )
8		simplr2	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> B e. ( EE ` N ) )
9		eqeefv	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
10	7 8 9	syl2anc	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
11		fveecn	|- ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
12	7 11	sylan	|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
13		elicc01	|- ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
14	13	simp1bi	|- ( T e. ( 0 [,] 1 ) -> T e. RR )
15	14	recnd	|- ( T e. ( 0 [,] 1 ) -> T e. CC )
16	15	ad2antlr	|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> T e. CC )
17		ax-1cn	|- 1 e. CC
18		npcan	|- ( ( 1 e. CC /\ T e. CC ) -> ( ( 1 - T ) + T ) = 1 )
19	17 18	mpan	|- ( T e. CC -> ( ( 1 - T ) + T ) = 1 )
20	19	oveq1d	|- ( T e. CC -> ( ( ( 1 - T ) + T ) x. ( A ` i ) ) = ( 1 x. ( A ` i ) ) )
21		mullid	|- ( ( A ` i ) e. CC -> ( 1 x. ( A ` i ) ) = ( A ` i ) )
22	20 21	sylan9eqr	|- ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) + T ) x. ( A ` i ) ) = ( A ` i ) )
23		subcl	|- ( ( 1 e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
24	17 23	mpan	|- ( T e. CC -> ( 1 - T ) e. CC )
25	24	adantl	|- ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
26		simpr	|- ( ( ( A ` i ) e. CC /\ T e. CC ) -> T e. CC )
27		simpl	|- ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( A ` i ) e. CC )
28	25 26 27	adddird	|- ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) + T ) x. ( A ` i ) ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) )
29	22 28	eqtr3d	|- ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( A ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) )
30	29	eqeq1d	|- ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( ( A ` i ) = ( B ` i ) <-> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) = ( B ` i ) ) )
31	12 16 30	syl2anc	|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) = ( B ` i ) <-> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) = ( B ` i ) ) )
32		eqcom	|- ( ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) = ( B ` i ) <-> ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) )
33	31 32	bitrdi	|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) = ( B ` i ) <-> ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) ) )
34	33	ralbidva	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) ) )
35	10 34	bitrd	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) ) )
36	6 35	imbitrrid	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A = C ) -> A = B ) )
37	36	expd	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) -> ( A = C -> A = B ) ) )
38	37	impr	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( A = C -> A = B ) )
39	38	necon3d	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( A =/= B -> A =/= C ) )
40	39	ex	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> ( A =/= B -> A =/= C ) ) )
41	40	com23	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A =/= B -> ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> A =/= C ) ) )
42	41	exp4a	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A =/= B -> ( T e. ( 0 [,] 1 ) -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) -> A =/= C ) ) ) )
43	42	3imp2	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> A =/= C )
44		simplr1	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> A e. ( EE ` N ) )
45		simplr3	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> C e. ( EE ` N ) )
46		eqeelen	|- ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A = C <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = 0 ) )
47	44 45 46	syl2anc	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( A = C <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = 0 ) )
48	47	necon3bid	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( A =/= C <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) =/= 0 ) )
49	43 48	mpbid	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) =/= 0 )