Metamath Proof Explorer

Theorem axsegconlem8

Description: Lemma for axsegcon . Show that a particular mapping generates a point. (Contributed by Scott Fenton, 18-Sep-2013)

Ref Expression
Hypotheses axsegconlem2.1 
|- S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
axsegconlem7.2 
|- T = sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 )
axsegconlem8.3 
|- F = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) )
Assertion axsegconlem8 
|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 
 |-  S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
2 axsegconlem7.2 
 |-  T = sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 )
3 axsegconlem8.3 
 |-  F = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) )
4 1 axsegconlem4 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sqrt ` S ) e. RR )
5 4 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) e. RR )
6 5 ad2antrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( sqrt ` S ) e. RR )
7 2 axsegconlem4 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( sqrt ` T ) e. RR )
8 7 ad2antlr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( sqrt ` T ) e. RR )
9 6 8 readdcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. RR )
10 simpl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
11 fveere 
 |-  ( ( B e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. RR )
12 10 11 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. RR )
13 9 12 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) e. RR )
14 simpl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
15 fveere 
 |-  ( ( A e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. RR )
16 14 15 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. RR )
17 8 16 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. ( A ` k ) ) e. RR )
18 13 17 resubcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) e. RR )
19 1 axsegconlem6 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 < ( sqrt ` S ) )
20 19 gt0ne0d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) =/= 0 )
21 20 ad2antrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( sqrt ` S ) =/= 0 )
22 18 6 21 redivcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) e. RR )
23 22 ralrimiva 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A. k e. ( 1 ... N ) ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) e. RR )
24 eleenn 
 |-  ( D e. ( EE ` N ) -> N e. NN )
25 24 ad2antll 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> N e. NN )
26 mptelee 
 |-  ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) e. RR ) )
27 25 26 syl 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) e. RR ) )
28 23 27 mpbird 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) ) e. ( EE ` N ) )
29 3 28 eqeltrid 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )