Step |
Hyp |
Ref |
Expression |
1 |
|
eleesub.1 |
|- C = ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) |
2 |
|
fveere |
|- ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR ) |
3 |
|
fveere |
|- ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR ) |
4 |
|
resubcl |
|- ( ( ( A ` i ) e. RR /\ ( B ` i ) e. RR ) -> ( ( A ` i ) - ( B ` i ) ) e. RR ) |
5 |
2 3 4
|
syl2an |
|- ( ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) /\ ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) ) -> ( ( A ` i ) - ( B ` i ) ) e. RR ) |
6 |
5
|
anandirs |
|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) - ( B ` i ) ) e. RR ) |
7 |
6
|
ralrimiva |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A. i e. ( 1 ... N ) ( ( A ` i ) - ( B ` i ) ) e. RR ) |
8 |
|
eleenn |
|- ( A e. ( EE ` N ) -> N e. NN ) |
9 |
|
mptelee |
|- ( N e. NN -> ( ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) <-> A. i e. ( 1 ... N ) ( ( A ` i ) - ( B ` i ) ) e. RR ) ) |
10 |
8 9
|
syl |
|- ( A e. ( EE ` N ) -> ( ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) <-> A. i e. ( 1 ... N ) ( ( A ` i ) - ( B ` i ) ) e. RR ) ) |
11 |
10
|
adantr |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) <-> A. i e. ( 1 ... N ) ( ( A ` i ) - ( B ` i ) ) e. RR ) ) |
12 |
7 11
|
mpbird |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( i e. ( 1 ... N ) |-> ( ( A ` i ) - ( B ` i ) ) ) e. ( EE ` N ) ) |
13 |
1 12
|
eqeltrid |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> C e. ( EE ` N ) ) |