Step |
Hyp |
Ref |
Expression |
1 |
|
2lgslem1b.i |
|- I = ( A ... B ) |
2 |
|
2lgslem1b.f |
|- F = ( j e. I |-> ( j x. 2 ) ) |
3 |
|
eqeq1 |
|- ( x = ( j x. 2 ) -> ( x = ( i x. 2 ) <-> ( j x. 2 ) = ( i x. 2 ) ) ) |
4 |
3
|
rexbidv |
|- ( x = ( j x. 2 ) -> ( E. i e. I x = ( i x. 2 ) <-> E. i e. I ( j x. 2 ) = ( i x. 2 ) ) ) |
5 |
|
elfzelz |
|- ( j e. ( A ... B ) -> j e. ZZ ) |
6 |
5 1
|
eleq2s |
|- ( j e. I -> j e. ZZ ) |
7 |
|
2z |
|- 2 e. ZZ |
8 |
7
|
a1i |
|- ( j e. I -> 2 e. ZZ ) |
9 |
6 8
|
zmulcld |
|- ( j e. I -> ( j x. 2 ) e. ZZ ) |
10 |
|
id |
|- ( j e. I -> j e. I ) |
11 |
|
oveq1 |
|- ( i = j -> ( i x. 2 ) = ( j x. 2 ) ) |
12 |
11
|
eqeq2d |
|- ( i = j -> ( ( j x. 2 ) = ( i x. 2 ) <-> ( j x. 2 ) = ( j x. 2 ) ) ) |
13 |
12
|
adantl |
|- ( ( j e. I /\ i = j ) -> ( ( j x. 2 ) = ( i x. 2 ) <-> ( j x. 2 ) = ( j x. 2 ) ) ) |
14 |
|
eqidd |
|- ( j e. I -> ( j x. 2 ) = ( j x. 2 ) ) |
15 |
10 13 14
|
rspcedvd |
|- ( j e. I -> E. i e. I ( j x. 2 ) = ( i x. 2 ) ) |
16 |
4 9 15
|
elrabd |
|- ( j e. I -> ( j x. 2 ) e. { x e. ZZ | E. i e. I x = ( i x. 2 ) } ) |
17 |
2 16
|
fmpti |
|- F : I --> { x e. ZZ | E. i e. I x = ( i x. 2 ) } |
18 |
|
oveq1 |
|- ( j = y -> ( j x. 2 ) = ( y x. 2 ) ) |
19 |
|
simpl |
|- ( ( y e. I /\ z e. I ) -> y e. I ) |
20 |
|
ovexd |
|- ( ( y e. I /\ z e. I ) -> ( y x. 2 ) e. _V ) |
21 |
2 18 19 20
|
fvmptd3 |
|- ( ( y e. I /\ z e. I ) -> ( F ` y ) = ( y x. 2 ) ) |
22 |
|
oveq1 |
|- ( j = z -> ( j x. 2 ) = ( z x. 2 ) ) |
23 |
|
simpr |
|- ( ( y e. I /\ z e. I ) -> z e. I ) |
24 |
|
ovexd |
|- ( ( y e. I /\ z e. I ) -> ( z x. 2 ) e. _V ) |
25 |
2 22 23 24
|
fvmptd3 |
|- ( ( y e. I /\ z e. I ) -> ( F ` z ) = ( z x. 2 ) ) |
26 |
21 25
|
eqeq12d |
|- ( ( y e. I /\ z e. I ) -> ( ( F ` y ) = ( F ` z ) <-> ( y x. 2 ) = ( z x. 2 ) ) ) |
27 |
|
elfzelz |
|- ( y e. ( A ... B ) -> y e. ZZ ) |
28 |
27 1
|
eleq2s |
|- ( y e. I -> y e. ZZ ) |
29 |
28
|
zcnd |
|- ( y e. I -> y e. CC ) |
30 |
29
|
adantr |
|- ( ( y e. I /\ z e. I ) -> y e. CC ) |
31 |
|
elfzelz |
|- ( z e. ( A ... B ) -> z e. ZZ ) |
32 |
31 1
|
eleq2s |
|- ( z e. I -> z e. ZZ ) |
33 |
32
|
zcnd |
|- ( z e. I -> z e. CC ) |
34 |
33
|
adantl |
|- ( ( y e. I /\ z e. I ) -> z e. CC ) |
35 |
|
2cnd |
|- ( ( y e. I /\ z e. I ) -> 2 e. CC ) |
36 |
|
2ne0 |
|- 2 =/= 0 |
37 |
36
|
a1i |
|- ( ( y e. I /\ z e. I ) -> 2 =/= 0 ) |
38 |
30 34 35 37
|
mulcan2d |
|- ( ( y e. I /\ z e. I ) -> ( ( y x. 2 ) = ( z x. 2 ) <-> y = z ) ) |
39 |
38
|
biimpd |
|- ( ( y e. I /\ z e. I ) -> ( ( y x. 2 ) = ( z x. 2 ) -> y = z ) ) |
40 |
26 39
|
sylbid |
|- ( ( y e. I /\ z e. I ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) ) |
41 |
40
|
rgen2 |
|- A. y e. I A. z e. I ( ( F ` y ) = ( F ` z ) -> y = z ) |
42 |
|
dff13 |
|- ( F : I -1-1-> { x e. ZZ | E. i e. I x = ( i x. 2 ) } <-> ( F : I --> { x e. ZZ | E. i e. I x = ( i x. 2 ) } /\ A. y e. I A. z e. I ( ( F ` y ) = ( F ` z ) -> y = z ) ) ) |
43 |
17 41 42
|
mpbir2an |
|- F : I -1-1-> { x e. ZZ | E. i e. I x = ( i x. 2 ) } |
44 |
|
oveq1 |
|- ( j = i -> ( j x. 2 ) = ( i x. 2 ) ) |
45 |
44
|
eqeq2d |
|- ( j = i -> ( x = ( j x. 2 ) <-> x = ( i x. 2 ) ) ) |
46 |
45
|
cbvrexvw |
|- ( E. j e. I x = ( j x. 2 ) <-> E. i e. I x = ( i x. 2 ) ) |
47 |
|
elfzelz |
|- ( i e. ( A ... B ) -> i e. ZZ ) |
48 |
7
|
a1i |
|- ( i e. ( A ... B ) -> 2 e. ZZ ) |
49 |
47 48
|
zmulcld |
|- ( i e. ( A ... B ) -> ( i x. 2 ) e. ZZ ) |
50 |
49 1
|
eleq2s |
|- ( i e. I -> ( i x. 2 ) e. ZZ ) |
51 |
|
eleq1 |
|- ( x = ( i x. 2 ) -> ( x e. ZZ <-> ( i x. 2 ) e. ZZ ) ) |
52 |
50 51
|
syl5ibrcom |
|- ( i e. I -> ( x = ( i x. 2 ) -> x e. ZZ ) ) |
53 |
52
|
rexlimiv |
|- ( E. i e. I x = ( i x. 2 ) -> x e. ZZ ) |
54 |
53
|
pm4.71ri |
|- ( E. i e. I x = ( i x. 2 ) <-> ( x e. ZZ /\ E. i e. I x = ( i x. 2 ) ) ) |
55 |
46 54
|
bitri |
|- ( E. j e. I x = ( j x. 2 ) <-> ( x e. ZZ /\ E. i e. I x = ( i x. 2 ) ) ) |
56 |
55
|
abbii |
|- { x | E. j e. I x = ( j x. 2 ) } = { x | ( x e. ZZ /\ E. i e. I x = ( i x. 2 ) ) } |
57 |
2
|
rnmpt |
|- ran F = { x | E. j e. I x = ( j x. 2 ) } |
58 |
|
df-rab |
|- { x e. ZZ | E. i e. I x = ( i x. 2 ) } = { x | ( x e. ZZ /\ E. i e. I x = ( i x. 2 ) ) } |
59 |
56 57 58
|
3eqtr4i |
|- ran F = { x e. ZZ | E. i e. I x = ( i x. 2 ) } |
60 |
|
dff1o5 |
|- ( F : I -1-1-onto-> { x e. ZZ | E. i e. I x = ( i x. 2 ) } <-> ( F : I -1-1-> { x e. ZZ | E. i e. I x = ( i x. 2 ) } /\ ran F = { x e. ZZ | E. i e. I x = ( i x. 2 ) } ) ) |
61 |
43 59 60
|
mpbir2an |
|- F : I -1-1-onto-> { x e. ZZ | E. i e. I x = ( i x. 2 ) } |