Step |
Hyp |
Ref |
Expression |
1 |
|
1re |
|- 1 e. RR |
2 |
1
|
fconst6 |
|- ( ( 1 ... N ) X. { 1 } ) : ( 1 ... N ) --> RR |
3 |
|
elee |
|- ( N e. NN -> ( ( ( 1 ... N ) X. { 1 } ) e. ( EE ` N ) <-> ( ( 1 ... N ) X. { 1 } ) : ( 1 ... N ) --> RR ) ) |
4 |
2 3
|
mpbiri |
|- ( N e. NN -> ( ( 1 ... N ) X. { 1 } ) e. ( EE ` N ) ) |
5 |
|
0re |
|- 0 e. RR |
6 |
5
|
fconst6 |
|- ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> RR |
7 |
|
elee |
|- ( N e. NN -> ( ( ( 1 ... N ) X. { 0 } ) e. ( EE ` N ) <-> ( ( 1 ... N ) X. { 0 } ) : ( 1 ... N ) --> RR ) ) |
8 |
6 7
|
mpbiri |
|- ( N e. NN -> ( ( 1 ... N ) X. { 0 } ) e. ( EE ` N ) ) |
9 |
|
ax-1ne0 |
|- 1 =/= 0 |
10 |
9
|
neii |
|- -. 1 = 0 |
11 |
|
1ex |
|- 1 e. _V |
12 |
11
|
sneqr |
|- ( { 1 } = { 0 } -> 1 = 0 ) |
13 |
10 12
|
mto |
|- -. { 1 } = { 0 } |
14 |
|
elnnuz |
|- ( N e. NN <-> N e. ( ZZ>= ` 1 ) ) |
15 |
|
eluzfz1 |
|- ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) ) |
16 |
14 15
|
sylbi |
|- ( N e. NN -> 1 e. ( 1 ... N ) ) |
17 |
16
|
ne0d |
|- ( N e. NN -> ( 1 ... N ) =/= (/) ) |
18 |
|
rnxp |
|- ( ( 1 ... N ) =/= (/) -> ran ( ( 1 ... N ) X. { 1 } ) = { 1 } ) |
19 |
17 18
|
syl |
|- ( N e. NN -> ran ( ( 1 ... N ) X. { 1 } ) = { 1 } ) |
20 |
|
rnxp |
|- ( ( 1 ... N ) =/= (/) -> ran ( ( 1 ... N ) X. { 0 } ) = { 0 } ) |
21 |
17 20
|
syl |
|- ( N e. NN -> ran ( ( 1 ... N ) X. { 0 } ) = { 0 } ) |
22 |
19 21
|
eqeq12d |
|- ( N e. NN -> ( ran ( ( 1 ... N ) X. { 1 } ) = ran ( ( 1 ... N ) X. { 0 } ) <-> { 1 } = { 0 } ) ) |
23 |
13 22
|
mtbiri |
|- ( N e. NN -> -. ran ( ( 1 ... N ) X. { 1 } ) = ran ( ( 1 ... N ) X. { 0 } ) ) |
24 |
|
rneq |
|- ( ( ( 1 ... N ) X. { 1 } ) = ( ( 1 ... N ) X. { 0 } ) -> ran ( ( 1 ... N ) X. { 1 } ) = ran ( ( 1 ... N ) X. { 0 } ) ) |
25 |
23 24
|
nsyl |
|- ( N e. NN -> -. ( ( 1 ... N ) X. { 1 } ) = ( ( 1 ... N ) X. { 0 } ) ) |
26 |
25
|
neqned |
|- ( N e. NN -> ( ( 1 ... N ) X. { 1 } ) =/= ( ( 1 ... N ) X. { 0 } ) ) |
27 |
|
neeq1 |
|- ( x = ( ( 1 ... N ) X. { 1 } ) -> ( x =/= y <-> ( ( 1 ... N ) X. { 1 } ) =/= y ) ) |
28 |
|
neeq2 |
|- ( y = ( ( 1 ... N ) X. { 0 } ) -> ( ( ( 1 ... N ) X. { 1 } ) =/= y <-> ( ( 1 ... N ) X. { 1 } ) =/= ( ( 1 ... N ) X. { 0 } ) ) ) |
29 |
27 28
|
rspc2ev |
|- ( ( ( ( 1 ... N ) X. { 1 } ) e. ( EE ` N ) /\ ( ( 1 ... N ) X. { 0 } ) e. ( EE ` N ) /\ ( ( 1 ... N ) X. { 1 } ) =/= ( ( 1 ... N ) X. { 0 } ) ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) x =/= y ) |
30 |
4 8 26 29
|
syl3anc |
|- ( N e. NN -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) x =/= y ) |