Metamath Proof Explorer

Theorem aks6d1c2

Description: Claim 2 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 2-May-2025)

Ref Expression
Hypotheses aks6d1c2a.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
aks6d1c2a.2 
|- P = ( chr ` K )
aks6d1c2a.3 
|- ( ph -> K e. Field )
aks6d1c2a.4 
|- ( ph -> P e. Prime )
aks6d1c2a.5 
|- ( ph -> R e. NN )
aks6d1c2a.6 
|- ( ph -> N e. NN )
aks6d1c2a.7 
|- ( ph -> P || N )
aks6d1c2a.8 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c2a.10 
|- G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
aks6d1c2a.11 
|- ( ph -> A e. NN0 )
aks6d1c2a.12 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c2a.13 
|- L = ( ZRHom ` ( Z/nZ ` R ) )
aks6d1c2a.14 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
aks6d1c2a.15 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
aks6d1c2a.16 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks6d1c2a.17 
|- H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
aks6d1c2a.18 
|- B = ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
aks6d1c2a.19 
|- C = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) )
aks6d1c2a.20 
|- ( ph -> ( Q e. Prime /\ Q || N /\ P =/= Q ) )
Assertion aks6d1c2 
|- ( ph -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) )

Proof

Step Hyp Ref Expression
1 aks6d1c2a.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
2 aks6d1c2a.2 
 |-  P = ( chr ` K )
3 aks6d1c2a.3 
 |-  ( ph -> K e. Field )
4 aks6d1c2a.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c2a.5 
 |-  ( ph -> R e. NN )
6 aks6d1c2a.6 
 |-  ( ph -> N e. NN )
7 aks6d1c2a.7 
 |-  ( ph -> P || N )
8 aks6d1c2a.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c2a.10 
 |-  G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
10 aks6d1c2a.11 
 |-  ( ph -> A e. NN0 )
11 aks6d1c2a.12 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
12 aks6d1c2a.13 
 |-  L = ( ZRHom ` ( Z/nZ ` R ) )
13 aks6d1c2a.14 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
14 aks6d1c2a.15 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
15 aks6d1c2a.16 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
16 aks6d1c2a.17 
 |-  H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
17 aks6d1c2a.18 
 |-  B = ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
18 aks6d1c2a.19 
 |-  C = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) )
19 aks6d1c2a.20 
 |-  ( ph -> ( Q e. Prime /\ Q || N /\ P =/= Q ) )
20 simpl 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( b < c /\ E. d e. NN c = ( b + ( d x. R ) ) ) ) -> ( ( ph /\ b e. C ) /\ c e. C ) )
21 simprl 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( b < c /\ E. d e. NN c = ( b + ( d x. R ) ) ) ) -> b < c )
22 20 21 jca 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( b < c /\ E. d e. NN c = ( b + ( d x. R ) ) ) ) -> ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) )
23 simprr 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( b < c /\ E. d e. NN c = ( b + ( d x. R ) ) ) ) -> E. d e. NN c = ( b + ( d x. R ) ) )
24 22 23 jca 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( b < c /\ E. d e. NN c = ( b + ( d x. R ) ) ) ) -> ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ E. d e. NN c = ( b + ( d x. R ) ) ) )
25 3 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> K e. Field )
26 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> P e. Prime )
27 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> R e. NN )
28 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> N e. NN )
29 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> P || N )
30 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> ( N gcd R ) = 1 )
31 0nn0 
 |-  0 e. NN0
32 31 a1i 
 |-  ( ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) /\ j e. ( 0 ... A ) ) -> 0 e. NN0 )
33 eqid 
 |-  ( j e. ( 0 ... A ) |-> 0 ) = ( j e. ( 0 ... A ) |-> 0 )
34 32 33 fmptd 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> ( j e. ( 0 ... A ) |-> 0 ) : ( 0 ... A ) --> NN0 )
35 10 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> A e. NN0 )
36 13 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
37 14 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
38 15 ad5antr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
39 simp-5r 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> b e. C )
40 simp-4r 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> c e. C )
41 simpllr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> b < c )
42 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
43 eqid 
 |-  ( var1 ` K ) = ( var1 ` K )
44 eqid 
 |-  ( ( c ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ( -g ` ( Poly1 ` K ) ) ( b ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = ( ( c ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ( -g ` ( Poly1 ` K ) ) ( b ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) )
45 simplr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> d e. NN )
46 simpr 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> c = ( b + ( d x. R ) ) )
47 1 2 25 26 27 28 29 30 34 9 35 11 12 36 37 38 16 17 18 39 40 41 42 43 44 45 46 aks6d1c2lem4 
 |-  ( ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) /\ c = ( b + ( d x. R ) ) ) -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) )
48 47 ex 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ d e. NN ) -> ( c = ( b + ( d x. R ) ) -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) ) )
49 48 rexlimdva 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) -> ( E. d e. NN c = ( b + ( d x. R ) ) -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) ) )
50 49 imp 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ b < c ) /\ E. d e. NN c = ( b + ( d x. R ) ) ) -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) )
51 24 50 syl 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( b < c /\ E. d e. NN c = ( b + ( d x. R ) ) ) ) -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) )
52 simprr 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> b < c )
53 nfcv 
 |-  F/_ s ( L ` t )
54 nfcv 
 |-  F/_ t ( L ` s )
55 fveq2 
 |-  ( t = s -> ( L ` t ) = ( L ` s ) )
56 53 54 55 cbvmpt 
 |-  ( t e. C |-> ( L ` t ) ) = ( s e. C |-> ( L ` s ) )
57 56 a1i 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( t e. C |-> ( L ` t ) ) = ( s e. C |-> ( L ` s ) ) )
58 simpr 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ s = b ) -> s = b )
59 58 fveq2d 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ s = b ) -> ( L ` s ) = ( L ` b ) )
60 simpllr 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> b e. C )
61 fvexd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( L ` b ) e. _V )
62 57 59 60 61 fvmptd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( ( t e. C |-> ( L ` t ) ) ` b ) = ( L ` b ) )
63 62 eqcomd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( L ` b ) = ( ( t e. C |-> ( L ` t ) ) ` b ) )
64 simprl 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) )
65 simpr 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ s = c ) -> s = c )
66 65 fveq2d 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ s = c ) -> ( L ` s ) = ( L ` c ) )
67 simplr 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> c e. C )
68 fvexd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( L ` c ) e. _V )
69 57 66 67 68 fvmptd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( ( t e. C |-> ( L ` t ) ) ` c ) = ( L ` c ) )
70 64 69 eqtrd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( ( t e. C |-> ( L ` t ) ) ` b ) = ( L ` c ) )
71 63 70 eqtrd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( L ` b ) = ( L ` c ) )
72 71 eqcomd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( L ` c ) = ( L ` b ) )
73 5 nnnn0d 
 |-  ( ph -> R e. NN0 )
74 73 adantr 
 |-  ( ( ph /\ b e. C ) -> R e. NN0 )
75 74 adantr 
 |-  ( ( ( ph /\ b e. C ) /\ c e. C ) -> R e. NN0 )
76 75 adantr 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> R e. NN0 )
77 fz0ssnn0 
 |-  ( 0 ... B ) C_ NN0
78 77 a1i 
 |-  ( ph -> ( 0 ... B ) C_ NN0 )
79 78 78 jca 
 |-  ( ph -> ( ( 0 ... B ) C_ NN0 /\ ( 0 ... B ) C_ NN0 ) )
80 eqid 
 |-  ( Z/nZ ` R ) = ( Z/nZ ` R )
81 6 4 7 5 8 11 12 80 hashscontpowcl 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
82 81 nn0red 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR )
83 81 nn0ge0d 
 |-  ( ph -> 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
84 82 83 resqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR )
85 84 flcld 
 |-  ( ph -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ )
86 82 83 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
87 0zd 
 |-  ( ph -> 0 e. ZZ )
88 flge 
 |-  ( ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <-> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
89 84 87 88 syl2anc 
 |-  ( ph -> ( 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <-> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
90 86 89 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
91 85 90 jca 
 |-  ( ph -> ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
92 elnn0z 
 |-  ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. NN0 <-> ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
93 91 92 sylibr 
 |-  ( ph -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. NN0 )
94 17 a1i 
 |-  ( ph -> B = ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
95 94 eleq1d 
 |-  ( ph -> ( B e. NN0 <-> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. NN0 ) )
96 93 95 mpbird 
 |-  ( ph -> B e. NN0 )
97 96 nn0ge0d 
 |-  ( ph -> 0 <_ B )
98 96 nn0zd 
 |-  ( ph -> B e. ZZ )
99 eluz 
 |-  ( ( 0 e. ZZ /\ B e. ZZ ) -> ( B e. ( ZZ>= ` 0 ) <-> 0 <_ B ) )
100 87 98 99 syl2anc 
 |-  ( ph -> ( B e. ( ZZ>= ` 0 ) <-> 0 <_ B ) )
101 97 100 mpbird 
 |-  ( ph -> B e. ( ZZ>= ` 0 ) )
102 fzn0 
 |-  ( ( 0 ... B ) =/= (/) <-> B e. ( ZZ>= ` 0 ) )
103 101 102 sylibr 
 |-  ( ph -> ( 0 ... B ) =/= (/) )
104 103 103 jca 
 |-  ( ph -> ( ( 0 ... B ) =/= (/) /\ ( 0 ... B ) =/= (/) ) )
105 xpnz 
 |-  ( ( ( 0 ... B ) =/= (/) /\ ( 0 ... B ) =/= (/) ) <-> ( ( 0 ... B ) X. ( 0 ... B ) ) =/= (/) )
106 105 biimpi 
 |-  ( ( ( 0 ... B ) =/= (/) /\ ( 0 ... B ) =/= (/) ) -> ( ( 0 ... B ) X. ( 0 ... B ) ) =/= (/) )
107 104 106 syl 
 |-  ( ph -> ( ( 0 ... B ) X. ( 0 ... B ) ) =/= (/) )
108 ssxpb 
 |-  ( ( ( 0 ... B ) X. ( 0 ... B ) ) =/= (/) -> ( ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) <-> ( ( 0 ... B ) C_ NN0 /\ ( 0 ... B ) C_ NN0 ) ) )
109 107 108 syl 
 |-  ( ph -> ( ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) <-> ( ( 0 ... B ) C_ NN0 /\ ( 0 ... B ) C_ NN0 ) ) )
110 79 109 mpbird 
 |-  ( ph -> ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) )
111 imass2 
 |-  ( ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) -> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) C_ ( E " ( NN0 X. NN0 ) ) )
112 110 111 syl 
 |-  ( ph -> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) C_ ( E " ( NN0 X. NN0 ) ) )
113 nfv 
 |-  F/ o ph
114 19 simp1d 
 |-  ( ph -> Q e. Prime )
115 19 simp2d 
 |-  ( ph -> Q || N )
116 19 simp3d 
 |-  ( ph -> P =/= Q )
117 6 4 7 11 114 115 116 aks6d1c2p2 
 |-  ( ph -> E : ( NN0 X. NN0 ) -1-1-> NN )
118 f1f 
 |-  ( E : ( NN0 X. NN0 ) -1-1-> NN -> E : ( NN0 X. NN0 ) --> NN )
119 117 118 syl 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> NN )
120 119 ffnd 
 |-  ( ph -> E Fn ( NN0 X. NN0 ) )
121 120 fnfund 
 |-  ( ph -> Fun E )
122 119 ffvelcdmda 
 |-  ( ( ph /\ o e. ( NN0 X. NN0 ) ) -> ( E ` o ) e. NN )
123 113 121 122 funimassd 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) C_ NN )
124 112 123 sstrd 
 |-  ( ph -> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) C_ NN )
125 18 a1i 
 |-  ( ph -> C = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
126 125 sseq1d 
 |-  ( ph -> ( C C_ NN <-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) C_ NN ) )
127 124 126 mpbird 
 |-  ( ph -> C C_ NN )
128 127 ad2antrr 
 |-  ( ( ( ph /\ b e. C ) /\ c e. C ) -> C C_ NN )
129 simpr 
 |-  ( ( ( ph /\ b e. C ) /\ c e. C ) -> c e. C )
130 128 129 sseldd 
 |-  ( ( ( ph /\ b e. C ) /\ c e. C ) -> c e. NN )
131 130 nnzd 
 |-  ( ( ( ph /\ b e. C ) /\ c e. C ) -> c e. ZZ )
132 131 adantr 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> c e. ZZ )
133 simplr 
 |-  ( ( ( ph /\ b e. C ) /\ c e. C ) -> b e. C )
134 128 133 sseldd 
 |-  ( ( ( ph /\ b e. C ) /\ c e. C ) -> b e. NN )
135 134 nnzd 
 |-  ( ( ( ph /\ b e. C ) /\ c e. C ) -> b e. ZZ )
136 135 adantr 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> b e. ZZ )
137 80 12 zndvds 
 |-  ( ( R e. NN0 /\ c e. ZZ /\ b e. ZZ ) -> ( ( L ` c ) = ( L ` b ) <-> R || ( c - b ) ) )
138 76 132 136 137 syl3anc 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( ( L ` c ) = ( L ` b ) <-> R || ( c - b ) ) )
139 72 138 mpbid 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> R || ( c - b ) )
140 76 nn0zd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> R e. ZZ )
141 132 136 zsubcld 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( c - b ) e. ZZ )
142 divides 
 |-  ( ( R e. ZZ /\ ( c - b ) e. ZZ ) -> ( R || ( c - b ) <-> E. d e. ZZ ( d x. R ) = ( c - b ) ) )
143 140 141 142 syl2anc 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( R || ( c - b ) <-> E. d e. ZZ ( d x. R ) = ( c - b ) ) )
144 143 biimpd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( R || ( c - b ) -> E. d e. ZZ ( d x. R ) = ( c - b ) ) )
145 139 144 mpd 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> E. d e. ZZ ( d x. R ) = ( c - b ) )
146 simprl 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> d e. ZZ )
147 130 ad2antrr 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> c e. NN )
148 147 nnred 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> c e. RR )
149 134 ad2antrr 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> b e. NN )
150 149 nnred 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> b e. RR )
151 148 150 resubcld 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( c - b ) e. RR )
152 5 nnrpd 
 |-  ( ph -> R e. RR+ )
153 152 adantr 
 |-  ( ( ph /\ b e. C ) -> R e. RR+ )
154 153 adantr 
 |-  ( ( ( ph /\ b e. C ) /\ c e. C ) -> R e. RR+ )
155 154 adantr 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> R e. RR+ )
156 155 adantr 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> R e. RR+ )
157 156 rpred 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> R e. RR )
158 52 adantr 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> b < c )
159 150 148 posdifd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( b < c <-> 0 < ( c - b ) ) )
160 158 159 mpbid 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> 0 < ( c - b ) )
161 156 rpgt0d 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> 0 < R )
162 151 157 160 161 divgt0d 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> 0 < ( ( c - b ) / R ) )
163 157 recnd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> R e. CC )
164 146 zred 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> d e. RR )
165 164 recnd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> d e. CC )
166 163 165 mulcomd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( R x. d ) = ( d x. R ) )
167 simprr 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( d x. R ) = ( c - b ) )
168 166 167 eqtrd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( R x. d ) = ( c - b ) )
169 151 recnd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( c - b ) e. CC )
170 161 gt0ne0d 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> R =/= 0 )
171 169 163 165 170 divmuld 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( ( ( c - b ) / R ) = d <-> ( R x. d ) = ( c - b ) ) )
172 168 171 mpbird 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( ( c - b ) / R ) = d )
173 162 172 breqtrd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> 0 < d )
174 146 173 jca 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( d e. ZZ /\ 0 < d ) )
175 elnnz 
 |-  ( d e. NN <-> ( d e. ZZ /\ 0 < d ) )
176 174 175 sylibr 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> d e. NN )
177 167 eqcomd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( c - b ) = ( d x. R ) )
178 148 recnd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> c e. CC )
179 150 recnd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> b e. CC )
180 167 169 eqeltrd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( d x. R ) e. CC )
181 178 179 180 subaddd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( ( c - b ) = ( d x. R ) <-> ( b + ( d x. R ) ) = c ) )
182 177 181 mpbid 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> ( b + ( d x. R ) ) = c )
183 182 eqcomd 
 |-  ( ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) /\ ( d e. ZZ /\ ( d x. R ) = ( c - b ) ) ) -> c = ( b + ( d x. R ) ) )
184 145 176 183 reximssdv 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> E. d e. NN c = ( b + ( d x. R ) ) )
185 52 184 jca 
 |-  ( ( ( ( ph /\ b e. C ) /\ c e. C ) /\ ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) ) -> ( b < c /\ E. d e. NN c = ( b + ( d x. R ) ) ) )
186 fzfid 
 |-  ( ph -> ( 0 ... B ) e. Fin )
187 xpfi 
 |-  ( ( ( 0 ... B ) e. Fin /\ ( 0 ... B ) e. Fin ) -> ( ( 0 ... B ) X. ( 0 ... B ) ) e. Fin )
188 186 186 187 syl2anc 
 |-  ( ph -> ( ( 0 ... B ) X. ( 0 ... B ) ) e. Fin )
189 imafi 
 |-  ( ( Fun E /\ ( ( 0 ... B ) X. ( 0 ... B ) ) e. Fin ) -> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) e. Fin )
190 121 188 189 syl2anc 
 |-  ( ph -> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) e. Fin )
191 125 eleq1d 
 |-  ( ph -> ( C e. Fin <-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) e. Fin ) )
192 190 191 mpbird 
 |-  ( ph -> C e. Fin )
193 80 zncrng 
 |-  ( R e. NN0 -> ( Z/nZ ` R ) e. CRing )
194 73 193 syl 
 |-  ( ph -> ( Z/nZ ` R ) e. CRing )
195 crngring 
 |-  ( ( Z/nZ ` R ) e. CRing -> ( Z/nZ ` R ) e. Ring )
196 194 195 syl 
 |-  ( ph -> ( Z/nZ ` R ) e. Ring )
197 12 zrhrhm 
 |-  ( ( Z/nZ ` R ) e. Ring -> L e. ( ZZring RingHom ( Z/nZ ` R ) ) )
198 196 197 syl 
 |-  ( ph -> L e. ( ZZring RingHom ( Z/nZ ` R ) ) )
199 198 imaexd 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) e. _V )
200 hashclb 
 |-  ( ( L " ( E " ( NN0 X. NN0 ) ) ) e. _V -> ( ( L " ( E " ( NN0 X. NN0 ) ) ) e. Fin <-> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 ) )
201 199 200 syl 
 |-  ( ph -> ( ( L " ( E " ( NN0 X. NN0 ) ) ) e. Fin <-> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 ) )
202 81 201 mpbird 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) e. Fin )
203 hashcl 
 |-  ( ( L " ( E " ( NN0 X. NN0 ) ) ) e. Fin -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
204 202 203 syl 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
205 204 nn0red 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR )
206 204 nn0ge0d 
 |-  ( ph -> 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
207 sqrtmsq 
 |-  ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR /\ 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) -> ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
208 205 206 207 syl2anc 
 |-  ( ph -> ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
209 208 eqcomd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) = ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
210 205 206 jca 
 |-  ( ph -> ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR /\ 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
211 sqrtmul 
 |-  ( ( ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR /\ 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) /\ ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR /\ 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) -> ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
212 210 210 211 syl2anc 
 |-  ( ph -> ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
213 205 206 resqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR )
214 213 flcld 
 |-  ( ph -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ )
215 205 206 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
216 213 87 88 syl2anc 
 |-  ( ph -> ( 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <-> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
217 215 216 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
218 214 217 jca 
 |-  ( ph -> ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
219 218 92 sylibr 
 |-  ( ph -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. NN0 )
220 219 95 mpbird 
 |-  ( ph -> B e. NN0 )
221 220 nn0red 
 |-  ( ph -> B e. RR )
222 1red 
 |-  ( ph -> 1 e. RR )
223 221 222 readdcld 
 |-  ( ph -> ( B + 1 ) e. RR )
224 flltp1 
 |-  ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) < ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) + 1 ) )
225 213 224 syl 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) < ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) + 1 ) )
226 94 oveq1d 
 |-  ( ph -> ( B + 1 ) = ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) + 1 ) )
227 225 226 breqtrrd 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) < ( B + 1 ) )
228 213 223 213 223 215 227 215 227 ltmul12ad 
 |-  ( ph -> ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) x. ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) < ( ( B + 1 ) x. ( B + 1 ) ) )
229 212 228 eqbrtrd 
 |-  ( ph -> ( sqrt ` ( ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) x. ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) < ( ( B + 1 ) x. ( B + 1 ) ) )
230 209 229 eqbrtrd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) < ( ( B + 1 ) x. ( B + 1 ) ) )
231 hashfz0 
 |-  ( B e. NN0 -> ( # ` ( 0 ... B ) ) = ( B + 1 ) )
232 220 231 syl 
 |-  ( ph -> ( # ` ( 0 ... B ) ) = ( B + 1 ) )
233 232 232 oveq12d 
 |-  ( ph -> ( ( # ` ( 0 ... B ) ) x. ( # ` ( 0 ... B ) ) ) = ( ( B + 1 ) x. ( B + 1 ) ) )
234 230 233 breqtrrd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) < ( ( # ` ( 0 ... B ) ) x. ( # ` ( 0 ... B ) ) ) )
235 186 186 jca 
 |-  ( ph -> ( ( 0 ... B ) e. Fin /\ ( 0 ... B ) e. Fin ) )
236 hashxp 
 |-  ( ( ( 0 ... B ) e. Fin /\ ( 0 ... B ) e. Fin ) -> ( # ` ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ( ( # ` ( 0 ... B ) ) x. ( # ` ( 0 ... B ) ) ) )
237 235 236 syl 
 |-  ( ph -> ( # ` ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ( ( # ` ( 0 ... B ) ) x. ( # ` ( 0 ... B ) ) ) )
238 234 237 breqtrrd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) < ( # ` ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
239 ovexd 
 |-  ( ph -> ( 0 ... B ) e. _V )
240 239 239 jca 
 |-  ( ph -> ( ( 0 ... B ) e. _V /\ ( 0 ... B ) e. _V ) )
241 xpexg 
 |-  ( ( ( 0 ... B ) e. _V /\ ( 0 ... B ) e. _V ) -> ( ( 0 ... B ) X. ( 0 ... B ) ) e. _V )
242 240 241 syl 
 |-  ( ph -> ( ( 0 ... B ) X. ( 0 ... B ) ) e. _V )
243 242 mptexd 
 |-  ( ph -> ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) e. _V )
244 120 adantr 
 |-  ( ( ph /\ w e. ( ( 0 ... B ) X. ( 0 ... B ) ) ) -> E Fn ( NN0 X. NN0 ) )
245 110 sselda 
 |-  ( ( ph /\ w e. ( ( 0 ... B ) X. ( 0 ... B ) ) ) -> w e. ( NN0 X. NN0 ) )
246 simpr 
 |-  ( ( ph /\ w e. ( ( 0 ... B ) X. ( 0 ... B ) ) ) -> w e. ( ( 0 ... B ) X. ( 0 ... B ) ) )
247 244 245 246 fnfvimad 
 |-  ( ( ph /\ w e. ( ( 0 ... B ) X. ( 0 ... B ) ) ) -> ( E ` w ) e. ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
248 eqid 
 |-  ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) = ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) )
249 247 248 fmptd 
 |-  ( ph -> ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) --> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
250 119 110 feqresmpt 
 |-  ( ph -> ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) )
251 250 feq1d 
 |-  ( ph -> ( ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) --> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) <-> ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) --> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) )
252 249 251 mpbird 
 |-  ( ph -> ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) --> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
253 f1resf1 
 |-  ( ( E : ( NN0 X. NN0 ) -1-1-> NN /\ ( ( 0 ... B ) X. ( 0 ... B ) ) C_ ( NN0 X. NN0 ) /\ ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) --> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) -> ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
254 117 110 252 253 syl3anc 
 |-  ( ph -> ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
255 eqidd 
 |-  ( ph -> ( ( 0 ... B ) X. ( 0 ... B ) ) = ( ( 0 ... B ) X. ( 0 ... B ) ) )
256 eqidd 
 |-  ( ph -> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
257 250 255 256 f1eq123d 
 |-  ( ph -> ( ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) <-> ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) )
258 254 257 mpbid 
 |-  ( ph -> ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
259 df-ima 
 |-  ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ran ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) )
260 259 a1i 
 |-  ( ph -> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ran ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
261 250 rneqd 
 |-  ( ph -> ran ( E |` ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ran ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) )
262 260 261 eqtr2d 
 |-  ( ph -> ran ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
263 258 262 jca 
 |-  ( ph -> ( ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) /\ ran ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) )
264 dff1o5 
 |-  ( ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-onto-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) <-> ( ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) /\ ran ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) )
265 263 264 sylibr 
 |-  ( ph -> ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-onto-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
266 f1oeq1 
 |-  ( u = ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) -> ( u : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-onto-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) <-> ( w e. ( ( 0 ... B ) X. ( 0 ... B ) ) |-> ( E ` w ) ) : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-onto-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) )
267 243 265 266 spcedv 
 |-  ( ph -> E. u u : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-onto-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) )
268 hasheqf1oi 
 |-  ( ( ( 0 ... B ) X. ( 0 ... B ) ) e. _V -> ( E. u u : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-onto-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) -> ( # ` ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ( # ` ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) ) )
269 242 268 syl 
 |-  ( ph -> ( E. u u : ( ( 0 ... B ) X. ( 0 ... B ) ) -1-1-onto-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) -> ( # ` ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ( # ` ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) ) )
270 267 269 mpd 
 |-  ( ph -> ( # ` ( ( 0 ... B ) X. ( 0 ... B ) ) ) = ( # ` ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) )
271 238 270 breqtrd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) < ( # ` ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) )
272 125 fveq2d 
 |-  ( ph -> ( # ` C ) = ( # ` ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) ) )
273 271 272 breqtrrd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) < ( # ` C ) )
274 zringbas 
 |-  ZZ = ( Base ` ZZring )
275 eqid 
 |-  ( Base ` ( Z/nZ ` R ) ) = ( Base ` ( Z/nZ ` R ) )
276 274 275 rhmf 
 |-  ( L e. ( ZZring RingHom ( Z/nZ ` R ) ) -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
277 198 276 syl 
 |-  ( ph -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
278 277 ffnd 
 |-  ( ph -> L Fn ZZ )
279 278 adantr 
 |-  ( ( ph /\ t e. C ) -> L Fn ZZ )
280 resss 
 |-  ( E |` ( NN0 X. NN0 ) ) C_ E
281 280 a1i 
 |-  ( ph -> ( E |` ( NN0 X. NN0 ) ) C_ E )
282 rnss 
 |-  ( ( E |` ( NN0 X. NN0 ) ) C_ E -> ran ( E |` ( NN0 X. NN0 ) ) C_ ran E )
283 281 282 syl 
 |-  ( ph -> ran ( E |` ( NN0 X. NN0 ) ) C_ ran E )
284 df-ima 
 |-  ( E " ( NN0 X. NN0 ) ) = ran ( E |` ( NN0 X. NN0 ) )
285 284 a1i 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) = ran ( E |` ( NN0 X. NN0 ) ) )
286 285 sseq1d 
 |-  ( ph -> ( ( E " ( NN0 X. NN0 ) ) C_ ran E <-> ran ( E |` ( NN0 X. NN0 ) ) C_ ran E ) )
287 283 286 mpbird 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) C_ ran E )
288 frn 
 |-  ( E : ( NN0 X. NN0 ) --> NN -> ran E C_ NN )
289 119 288 syl 
 |-  ( ph -> ran E C_ NN )
290 287 289 sstrd 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) C_ NN )
291 nnssz 
 |-  NN C_ ZZ
292 291 a1i 
 |-  ( ph -> NN C_ ZZ )
293 290 292 sstrd 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) C_ ZZ )
294 293 adantr 
 |-  ( ( ph /\ t e. C ) -> ( E " ( NN0 X. NN0 ) ) C_ ZZ )
295 125 sseq1d 
 |-  ( ph -> ( C C_ ( E " ( NN0 X. NN0 ) ) <-> ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) ) C_ ( E " ( NN0 X. NN0 ) ) ) )
296 112 295 mpbird 
 |-  ( ph -> C C_ ( E " ( NN0 X. NN0 ) ) )
297 296 sseld 
 |-  ( ph -> ( t e. C -> t e. ( E " ( NN0 X. NN0 ) ) ) )
298 297 imp 
 |-  ( ( ph /\ t e. C ) -> t e. ( E " ( NN0 X. NN0 ) ) )
299 fnfvima 
 |-  ( ( L Fn ZZ /\ ( E " ( NN0 X. NN0 ) ) C_ ZZ /\ t e. ( E " ( NN0 X. NN0 ) ) ) -> ( L ` t ) e. ( L " ( E " ( NN0 X. NN0 ) ) ) )
300 279 294 298 299 syl3anc 
 |-  ( ( ph /\ t e. C ) -> ( L ` t ) e. ( L " ( E " ( NN0 X. NN0 ) ) ) )
301 eqid 
 |-  ( t e. C |-> ( L ` t ) ) = ( t e. C |-> ( L ` t ) )
302 300 301 fmptd 
 |-  ( ph -> ( t e. C |-> ( L ` t ) ) : C --> ( L " ( E " ( NN0 X. NN0 ) ) ) )
303 nnssre 
 |-  NN C_ RR
304 303 a1i 
 |-  ( ph -> NN C_ RR )
305 127 304 sstrd 
 |-  ( ph -> C C_ RR )
306 192 202 273 302 305 hashnexinjle 
 |-  ( ph -> E. b e. C E. c e. C ( ( ( t e. C |-> ( L ` t ) ) ` b ) = ( ( t e. C |-> ( L ` t ) ) ` c ) /\ b < c ) )
307 185 306 reximddv2 
 |-  ( ph -> E. b e. C E. c e. C ( b < c /\ E. d e. NN c = ( b + ( d x. R ) ) ) )
308 51 307 r19.29vva 
 |-  ( ph -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) )