Metamath Proof Explorer

Theorem ax5seglem3a

Description: Lemma for ax5seg . (Contributed by Scott Fenton, 7-May-2015)

Ref Expression
Assertion ax5seglem3a 
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) e. RR /\ ( ( D ` j ) - ( F ` j ) ) e. RR ) )

Proof

Step Hyp Ref Expression
1 simpl21 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> A e. ( EE ` N ) )
2 fveere 
 |-  ( ( A e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. RR )
3 1 2 sylancom 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. RR )
4 simpl23 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> C e. ( EE ` N ) )
5 fveere 
 |-  ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. RR )
6 4 5 sylancom 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. RR )
7 3 6 resubcld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( A ` j ) - ( C ` j ) ) e. RR )
8 simpl31 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> D e. ( EE ` N ) )
9 fveere 
 |-  ( ( D e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( D ` j ) e. RR )
10 8 9 sylancom 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( D ` j ) e. RR )
11 simpl33 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> F e. ( EE ` N ) )
12 fveere 
 |-  ( ( F e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( F ` j ) e. RR )
13 11 12 sylancom 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( F ` j ) e. RR )
14 10 13 resubcld 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( D ` j ) - ( F ` j ) ) e. RR )
15 7 14 jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) e. RR /\ ( ( D ` j ) - ( F ` j ) ) e. RR ) )