Metamath Proof Explorer

Theorem hashscontpow

Description: If a set contains all N -th powers, then the size of the image under the ZR homomorphism is greater than the R -th order of N . (Contributed by metakunt, 28-Apr-2025)

Ref Expression
Hypotheses hashscontpow.1 
|- ( ph -> E C_ ZZ )
hashscontpow.2 
|- ( ph -> N e. NN )
hashscontpow.3 
|- ( ph -> A. k e. NN0 ( N ^ k ) e. E )
hashscontpow.4 
|- ( ph -> R e. NN )
hashscontpow.5 
|- ( ph -> ( N gcd R ) = 1 )
hashscontpow.6 
|- L = ( ZRHom ` Y )
hashscontpow.7 
|- Y = ( Z/nZ ` R )
Assertion hashscontpow 
|- ( ph -> ( ( odZ ` R ) ` N ) <_ ( # ` ( L " E ) ) )

Proof

Step Hyp Ref Expression
1 hashscontpow.1 
 |-  ( ph -> E C_ ZZ )
2 hashscontpow.2 
 |-  ( ph -> N e. NN )
3 hashscontpow.3 
 |-  ( ph -> A. k e. NN0 ( N ^ k ) e. E )
4 hashscontpow.4 
 |-  ( ph -> R e. NN )
5 hashscontpow.5 
 |-  ( ph -> ( N gcd R ) = 1 )
6 hashscontpow.6 
 |-  L = ( ZRHom ` Y )
7 hashscontpow.7 
 |-  Y = ( Z/nZ ` R )
8 2 nnzd 
 |-  ( ph -> N e. ZZ )
9 odzcl 
 |-  ( ( R e. NN /\ N e. ZZ /\ ( N gcd R ) = 1 ) -> ( ( odZ ` R ) ` N ) e. NN )
10 4 8 5 9 syl3anc 
 |-  ( ph -> ( ( odZ ` R ) ` N ) e. NN )
11 10 nnnn0d 
 |-  ( ph -> ( ( odZ ` R ) ` N ) e. NN0 )
12 hashfz1 
 |-  ( ( ( odZ ` R ) ` N ) e. NN0 -> ( # ` ( 1 ... ( ( odZ ` R ) ` N ) ) ) = ( ( odZ ` R ) ` N ) )
13 11 12 syl 
 |-  ( ph -> ( # ` ( 1 ... ( ( odZ ` R ) ` N ) ) ) = ( ( odZ ` R ) ` N ) )
14 ovexd 
 |-  ( ph -> ( 1 ... ( ( odZ ` R ) ` N ) ) e. _V )
15 14 mptexd 
 |-  ( ph -> ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) e. _V )
16 6 fvexi 
 |-  L e. _V
17 16 a1i 
 |-  ( ph -> L e. _V )
18 imaexg 
 |-  ( L e. _V -> ( L " E ) e. _V )
19 17 18 syl 
 |-  ( ph -> ( L " E ) e. _V )
20 4 nnnn0d 
 |-  ( ph -> R e. NN0 )
21 7 zncrng 
 |-  ( R e. NN0 -> Y e. CRing )
22 20 21 syl 
 |-  ( ph -> Y e. CRing )
23 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
24 6 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
25 zringbas 
 |-  ZZ = ( Base ` ZZring )
26 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
27 25 26 rhmf 
 |-  ( L e. ( ZZring RingHom Y ) -> L : ZZ --> ( Base ` Y ) )
28 22 23 24 27 4syl 
 |-  ( ph -> L : ZZ --> ( Base ` Y ) )
29 28 ffnd 
 |-  ( ph -> L Fn ZZ )
30 29 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> L Fn ZZ )
31 8 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> N e. ZZ )
32 elfznn 
 |-  ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) -> x e. NN )
33 32 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> x e. NN )
34 33 nnnn0d 
 |-  ( ( ph /\ x e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> x e. NN0 )
35 31 34 zexpcld 
 |-  ( ( ph /\ x e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( N ^ x ) e. ZZ )
36 oveq2 
 |-  ( k = x -> ( N ^ k ) = ( N ^ x ) )
37 36 eleq1d 
 |-  ( k = x -> ( ( N ^ k ) e. E <-> ( N ^ x ) e. E ) )
38 3 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> A. k e. NN0 ( N ^ k ) e. E )
39 37 38 34 rspcdva 
 |-  ( ( ph /\ x e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( N ^ x ) e. E )
40 30 35 39 fnfvimad 
 |-  ( ( ph /\ x e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( L ` ( N ^ x ) ) e. ( L " E ) )
41 40 fmpttd 
 |-  ( ph -> ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) : ( 1 ... ( ( odZ ` R ) ` N ) ) --> ( L " E ) )
42 2 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ a < b ) -> N e. NN )
43 simpllr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ a < b ) -> a e. ( 1 ... ( ( odZ ` R ) ` N ) ) )
44 simplr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ a < b ) -> b e. ( 1 ... ( ( odZ ` R ) ` N ) ) )
45 4 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ a < b ) -> R e. NN )
46 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ a < b ) -> ( N gcd R ) = 1 )
47 simpr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ a < b ) -> a < b )
48 42 43 44 45 46 6 7 47 hashscontpow1 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ a < b ) -> ( L ` ( N ^ a ) ) =/= ( L ` ( N ^ b ) ) )
49 2 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b < a ) -> N e. NN )
50 simplr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b < a ) -> b e. ( 1 ... ( ( odZ ` R ) ` N ) ) )
51 simpllr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b < a ) -> a e. ( 1 ... ( ( odZ ` R ) ` N ) ) )
52 4 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b < a ) -> R e. NN )
53 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b < a ) -> ( N gcd R ) = 1 )
54 simpr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b < a ) -> b < a )
55 49 50 51 52 53 6 7 54 hashscontpow1 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b < a ) -> ( L ` ( N ^ b ) ) =/= ( L ` ( N ^ a ) ) )
56 55 necomd 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b < a ) -> ( L ` ( N ^ a ) ) =/= ( L ` ( N ^ b ) ) )
57 48 56 jaodan 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ ( a < b \/ b < a ) ) -> ( L ` ( N ^ a ) ) =/= ( L ` ( N ^ b ) ) )
58 57 ex 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( ( a < b \/ b < a ) -> ( L ` ( N ^ a ) ) =/= ( L ` ( N ^ b ) ) ) )
59 biidd 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( a = b <-> a = b ) )
60 59 necon3bbid 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( -. a = b <-> a =/= b ) )
61 elfzelz 
 |-  ( a e. ( 1 ... ( ( odZ ` R ) ` N ) ) -> a e. ZZ )
62 61 adantl 
 |-  ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> a e. ZZ )
63 62 adantr 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> a e. ZZ )
64 63 zred 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> a e. RR )
65 elfzelz 
 |-  ( b e. ( 1 ... ( ( odZ ` R ) ` N ) ) -> b e. ZZ )
66 65 zred 
 |-  ( b e. ( 1 ... ( ( odZ ` R ) ` N ) ) -> b e. RR )
67 66 adantl 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> b e. RR )
68 lttri2 
 |-  ( ( a e. RR /\ b e. RR ) -> ( a =/= b <-> ( a < b \/ b < a ) ) )
69 64 67 68 syl2anc 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( a =/= b <-> ( a < b \/ b < a ) ) )
70 60 69 bitrd 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( -. a = b <-> ( a < b \/ b < a ) ) )
71 70 imbi1d 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( ( -. a = b -> ( L ` ( N ^ a ) ) =/= ( L ` ( N ^ b ) ) ) <-> ( ( a < b \/ b < a ) -> ( L ` ( N ^ a ) ) =/= ( L ` ( N ^ b ) ) ) ) )
72 58 71 mpbird 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( -. a = b -> ( L ` ( N ^ a ) ) =/= ( L ` ( N ^ b ) ) ) )
73 72 imp 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> ( L ` ( N ^ a ) ) =/= ( L ` ( N ^ b ) ) )
74 eqidd 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) = ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) )
75 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) /\ x = a ) -> x = a )
76 75 oveq2d 
 |-  ( ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) /\ x = a ) -> ( N ^ x ) = ( N ^ a ) )
77 76 fveq2d 
 |-  ( ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) /\ x = a ) -> ( L ` ( N ^ x ) ) = ( L ` ( N ^ a ) ) )
78 simpllr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> a e. ( 1 ... ( ( odZ ` R ) ` N ) ) )
79 fvexd 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> ( L ` ( N ^ a ) ) e. _V )
80 74 77 78 79 fvmptd 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) = ( L ` ( N ^ a ) ) )
81 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) /\ x = b ) -> x = b )
82 81 oveq2d 
 |-  ( ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) /\ x = b ) -> ( N ^ x ) = ( N ^ b ) )
83 82 fveq2d 
 |-  ( ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) /\ x = b ) -> ( L ` ( N ^ x ) ) = ( L ` ( N ^ b ) ) )
84 simplr 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> b e. ( 1 ... ( ( odZ ` R ) ` N ) ) )
85 fvexd 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> ( L ` ( N ^ b ) ) e. _V )
86 74 83 84 85 fvmptd 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) = ( L ` ( N ^ b ) ) )
87 80 86 neeq12d 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> ( ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) =/= ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) <-> ( L ` ( N ^ a ) ) =/= ( L ` ( N ^ b ) ) ) )
88 73 87 mpbird 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) =/= ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) )
89 88 neneqd 
 |-  ( ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ -. a = b ) -> -. ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) = ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) )
90 89 ex 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( -. a = b -> -. ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) = ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) ) )
91 90 con4d 
 |-  ( ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) /\ b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> ( ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) = ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) -> a = b ) )
92 91 ralrimiva 
 |-  ( ( ph /\ a e. ( 1 ... ( ( odZ ` R ) ` N ) ) ) -> A. b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ( ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) = ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) -> a = b ) )
93 92 ralrimiva 
 |-  ( ph -> A. a e. ( 1 ... ( ( odZ ` R ) ` N ) ) A. b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ( ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) = ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) -> a = b ) )
94 41 93 jca 
 |-  ( ph -> ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) : ( 1 ... ( ( odZ ` R ) ` N ) ) --> ( L " E ) /\ A. a e. ( 1 ... ( ( odZ ` R ) ` N ) ) A. b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ( ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) = ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) -> a = b ) ) )
95 dff13 
 |-  ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) : ( 1 ... ( ( odZ ` R ) ` N ) ) -1-1-> ( L " E ) <-> ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) : ( 1 ... ( ( odZ ` R ) ` N ) ) --> ( L " E ) /\ A. a e. ( 1 ... ( ( odZ ` R ) ` N ) ) A. b e. ( 1 ... ( ( odZ ` R ) ` N ) ) ( ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` a ) = ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) ` b ) -> a = b ) ) )
96 94 95 sylibr 
 |-  ( ph -> ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) : ( 1 ... ( ( odZ ` R ) ` N ) ) -1-1-> ( L " E ) )
97 hashf1dmcdm 
 |-  ( ( ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) e. _V /\ ( L " E ) e. _V /\ ( x e. ( 1 ... ( ( odZ ` R ) ` N ) ) |-> ( L ` ( N ^ x ) ) ) : ( 1 ... ( ( odZ ` R ) ` N ) ) -1-1-> ( L " E ) ) -> ( # ` ( 1 ... ( ( odZ ` R ) ` N ) ) ) <_ ( # ` ( L " E ) ) )
98 15 19 96 97 syl3anc 
 |-  ( ph -> ( # ` ( 1 ... ( ( odZ ` R ) ` N ) ) ) <_ ( # ` ( L " E ) ) )
99 13 98 eqbrtrrd 
 |-  ( ph -> ( ( odZ ` R ) ` N ) <_ ( # ` ( L " E ) ) )