Step |
Hyp |
Ref |
Expression |
1 |
|
axlowdimlem13.1 |
|- P = ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) |
2 |
|
axlowdimlem13.2 |
|- Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) |
3 |
|
2ne0 |
|- 2 =/= 0 |
4 |
3
|
neii |
|- -. 2 = 0 |
5 |
|
eqcom |
|- ( 2 = 0 <-> 0 = 2 ) |
6 |
|
1pneg1e0 |
|- ( 1 + -u 1 ) = 0 |
7 |
6
|
eqcomi |
|- 0 = ( 1 + -u 1 ) |
8 |
|
df-2 |
|- 2 = ( 1 + 1 ) |
9 |
7 8
|
eqeq12i |
|- ( 0 = 2 <-> ( 1 + -u 1 ) = ( 1 + 1 ) ) |
10 |
|
ax-1cn |
|- 1 e. CC |
11 |
|
neg1cn |
|- -u 1 e. CC |
12 |
10 11 10
|
addcani |
|- ( ( 1 + -u 1 ) = ( 1 + 1 ) <-> -u 1 = 1 ) |
13 |
5 9 12
|
3bitri |
|- ( 2 = 0 <-> -u 1 = 1 ) |
14 |
4 13
|
mtbi |
|- -. -u 1 = 1 |
15 |
14
|
intnanr |
|- -. ( -u 1 = 1 /\ 0 = 0 ) |
16 |
|
ax-1ne0 |
|- 1 =/= 0 |
17 |
16
|
neii |
|- -. 1 = 0 |
18 |
|
negeq0 |
|- ( 1 e. CC -> ( 1 = 0 <-> -u 1 = 0 ) ) |
19 |
10 18
|
ax-mp |
|- ( 1 = 0 <-> -u 1 = 0 ) |
20 |
17 19
|
mtbi |
|- -. -u 1 = 0 |
21 |
20
|
intnanr |
|- -. ( -u 1 = 0 /\ 0 = 1 ) |
22 |
15 21
|
pm3.2ni |
|- -. ( ( -u 1 = 1 /\ 0 = 0 ) \/ ( -u 1 = 0 /\ 0 = 1 ) ) |
23 |
|
negex |
|- -u 1 e. _V |
24 |
|
c0ex |
|- 0 e. _V |
25 |
|
1ex |
|- 1 e. _V |
26 |
23 24 25 24
|
preq12b |
|- ( { -u 1 , 0 } = { 1 , 0 } <-> ( ( -u 1 = 1 /\ 0 = 0 ) \/ ( -u 1 = 0 /\ 0 = 1 ) ) ) |
27 |
22 26
|
mtbir |
|- -. { -u 1 , 0 } = { 1 , 0 } |
28 |
|
3ex |
|- 3 e. _V |
29 |
28
|
rnsnop |
|- ran { <. 3 , -u 1 >. } = { -u 1 } |
30 |
29
|
a1i |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran { <. 3 , -u 1 >. } = { -u 1 } ) |
31 |
|
elnnuz |
|- ( N e. NN <-> N e. ( ZZ>= ` 1 ) ) |
32 |
|
eluzfz1 |
|- ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) ) |
33 |
31 32
|
sylbi |
|- ( N e. NN -> 1 e. ( 1 ... N ) ) |
34 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
35 |
|
1e0p1 |
|- 1 = ( 0 + 1 ) |
36 |
34 35
|
eqeq12i |
|- ( 3 = 1 <-> ( 2 + 1 ) = ( 0 + 1 ) ) |
37 |
|
2cn |
|- 2 e. CC |
38 |
|
0cn |
|- 0 e. CC |
39 |
37 38 10
|
addcan2i |
|- ( ( 2 + 1 ) = ( 0 + 1 ) <-> 2 = 0 ) |
40 |
36 39
|
bitri |
|- ( 3 = 1 <-> 2 = 0 ) |
41 |
40
|
necon3bii |
|- ( 3 =/= 1 <-> 2 =/= 0 ) |
42 |
3 41
|
mpbir |
|- 3 =/= 1 |
43 |
42
|
necomi |
|- 1 =/= 3 |
44 |
|
eldifsn |
|- ( 1 e. ( ( 1 ... N ) \ { 3 } ) <-> ( 1 e. ( 1 ... N ) /\ 1 =/= 3 ) ) |
45 |
33 43 44
|
sylanblrc |
|- ( N e. NN -> 1 e. ( ( 1 ... N ) \ { 3 } ) ) |
46 |
45
|
adantr |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> 1 e. ( ( 1 ... N ) \ { 3 } ) ) |
47 |
|
ne0i |
|- ( 1 e. ( ( 1 ... N ) \ { 3 } ) -> ( ( 1 ... N ) \ { 3 } ) =/= (/) ) |
48 |
|
rnxp |
|- ( ( ( 1 ... N ) \ { 3 } ) =/= (/) -> ran ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) = { 0 } ) |
49 |
46 47 48
|
3syl |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) = { 0 } ) |
50 |
30 49
|
uneq12d |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( ran { <. 3 , -u 1 >. } u. ran ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { -u 1 } u. { 0 } ) ) |
51 |
|
rnun |
|- ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( ran { <. 3 , -u 1 >. } u. ran ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) |
52 |
|
df-pr |
|- { -u 1 , 0 } = ( { -u 1 } u. { 0 } ) |
53 |
50 51 52
|
3eqtr4g |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = { -u 1 , 0 } ) |
54 |
|
ovex |
|- ( I + 1 ) e. _V |
55 |
54
|
rnsnop |
|- ran { <. ( I + 1 ) , 1 >. } = { 1 } |
56 |
55
|
a1i |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran { <. ( I + 1 ) , 1 >. } = { 1 } ) |
57 |
|
nnz |
|- ( N e. NN -> N e. ZZ ) |
58 |
|
fzssp1 |
|- ( 1 ... ( N - 1 ) ) C_ ( 1 ... ( ( N - 1 ) + 1 ) ) |
59 |
|
zcn |
|- ( N e. ZZ -> N e. CC ) |
60 |
|
npcan1 |
|- ( N e. CC -> ( ( N - 1 ) + 1 ) = N ) |
61 |
60
|
oveq2d |
|- ( N e. CC -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) ) |
62 |
59 61
|
syl |
|- ( N e. ZZ -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) ) |
63 |
58 62
|
sseqtrid |
|- ( N e. ZZ -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) ) |
64 |
57 63
|
syl |
|- ( N e. NN -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) ) |
65 |
64
|
sselda |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> I e. ( 1 ... N ) ) |
66 |
|
elfzelz |
|- ( I e. ( 1 ... ( N - 1 ) ) -> I e. ZZ ) |
67 |
66
|
zred |
|- ( I e. ( 1 ... ( N - 1 ) ) -> I e. RR ) |
68 |
|
id |
|- ( I e. RR -> I e. RR ) |
69 |
|
ltp1 |
|- ( I e. RR -> I < ( I + 1 ) ) |
70 |
68 69
|
ltned |
|- ( I e. RR -> I =/= ( I + 1 ) ) |
71 |
67 70
|
syl |
|- ( I e. ( 1 ... ( N - 1 ) ) -> I =/= ( I + 1 ) ) |
72 |
71
|
adantl |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> I =/= ( I + 1 ) ) |
73 |
|
eldifsn |
|- ( I e. ( ( 1 ... N ) \ { ( I + 1 ) } ) <-> ( I e. ( 1 ... N ) /\ I =/= ( I + 1 ) ) ) |
74 |
65 72 73
|
sylanbrc |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> I e. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) |
75 |
|
ne0i |
|- ( I e. ( ( 1 ... N ) \ { ( I + 1 ) } ) -> ( ( 1 ... N ) \ { ( I + 1 ) } ) =/= (/) ) |
76 |
|
rnxp |
|- ( ( ( 1 ... N ) \ { ( I + 1 ) } ) =/= (/) -> ran ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) = { 0 } ) |
77 |
74 75 76
|
3syl |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) = { 0 } ) |
78 |
56 77
|
uneq12d |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( ran { <. ( I + 1 ) , 1 >. } u. ran ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) = ( { 1 } u. { 0 } ) ) |
79 |
|
rnun |
|- ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) = ( ran { <. ( I + 1 ) , 1 >. } u. ran ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) |
80 |
|
df-pr |
|- { 1 , 0 } = ( { 1 } u. { 0 } ) |
81 |
78 79 80
|
3eqtr4g |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) = { 1 , 0 } ) |
82 |
53 81
|
eqeq12d |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) <-> { -u 1 , 0 } = { 1 , 0 } ) ) |
83 |
27 82
|
mtbiri |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> -. ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) ) |
84 |
|
rneq |
|- ( ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) -> ran ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ran ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) ) |
85 |
83 84
|
nsyl |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> -. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) ) |
86 |
1 2
|
eqeq12i |
|- ( P = Q <-> ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) ) |
87 |
86
|
necon3abii |
|- ( P =/= Q <-> -. ( { <. 3 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) ) = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) ) |
88 |
85 87
|
sylibr |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> P =/= Q ) |