Metamath Proof Explorer

Theorem 2lgslem1b

Description: Lemma 2 for 2lgslem1 . (Contributed by AV, 18-Jun-2021)

Ref Expression
Hypotheses 2lgslem1b.i 
|- I = ( A ... B )
2lgslem1b.f 
|- F = ( j e. I |-> ( j x. 2 ) )
Assertion 2lgslem1b 
|- F : I -1-1-onto-> { x e. ZZ | E. i e. I x = ( i x. 2 ) }

Proof

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 ) }