Metamath Proof Explorer

Theorem prmreclem3

Description: Lemma for prmrec . The main inequality established here is # M <_ # { x e. M | ( Qx ) = 1 } x. sqrt N , where { x e. M | ( Qx ) = 1 } is the set of squarefree numbers in M . This is demonstrated by the map y |-> <. y / ( Qy ) ^ 2 , ( Qy ) >. where Qy is the largest number whose square divides y . (Contributed by Mario Carneiro, 5-Aug-2014)

Ref Expression
Hypotheses prmrec.1 
|- F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )
prmrec.2 
|- ( ph -> K e. NN )
prmrec.3 
|- ( ph -> N e. NN )
prmrec.4 
|- M = { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n }
prmreclem2.5 
|- Q = ( n e. NN |-> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )
Assertion prmreclem3 
|- ( ph -> ( # ` M ) <_ ( ( 2 ^ K ) x. ( sqrt ` N ) ) )

Proof

Step Hyp Ref Expression
1 prmrec.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( 1 / n ) , 0 ) )
2 prmrec.2 
 |-  ( ph -> K e. NN )
3 prmrec.3 
 |-  ( ph -> N e. NN )
4 prmrec.4 
 |-  M = { n e. ( 1 ... N ) | A. p e. ( Prime \ ( 1 ... K ) ) -. p || n }
5 prmreclem2.5 
 |-  Q = ( n e. NN |-> sup ( { r e. NN | ( r ^ 2 ) || n } , RR , < ) )
6 fzfi 
 |-  ( 1 ... N ) e. Fin
7 4 ssrab3 
 |-  M C_ ( 1 ... N )
8 ssfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ M C_ ( 1 ... N ) ) -> M e. Fin )
9 6 7 8 mp2an 
 |-  M e. Fin
10 hashcl 
 |-  ( M e. Fin -> ( # ` M ) e. NN0 )
11 9 10 ax-mp 
 |-  ( # ` M ) e. NN0
12 11 nn0rei 
 |-  ( # ` M ) e. RR
13 12 a1i 
 |-  ( ph -> ( # ` M ) e. RR )
14 2nn 
 |-  2 e. NN
15 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
16 nnexpcl 
 |-  ( ( 2 e. NN /\ K e. NN0 ) -> ( 2 ^ K ) e. NN )
17 14 15 16 sylancr 
 |-  ( ph -> ( 2 ^ K ) e. NN )
18 17 nnnn0d 
 |-  ( ph -> ( 2 ^ K ) e. NN0 )
19 3 nnrpd 
 |-  ( ph -> N e. RR+ )
20 19 rpsqrtcld 
 |-  ( ph -> ( sqrt ` N ) e. RR+ )
21 20 rprege0d 
 |-  ( ph -> ( ( sqrt ` N ) e. RR /\ 0 <_ ( sqrt ` N ) ) )
22 flge0nn0 
 |-  ( ( ( sqrt ` N ) e. RR /\ 0 <_ ( sqrt ` N ) ) -> ( |_ ` ( sqrt ` N ) ) e. NN0 )
23 21 22 syl 
 |-  ( ph -> ( |_ ` ( sqrt ` N ) ) e. NN0 )
24 18 23 nn0mulcld 
 |-  ( ph -> ( ( 2 ^ K ) x. ( |_ ` ( sqrt ` N ) ) ) e. NN0 )
25 24 nn0red 
 |-  ( ph -> ( ( 2 ^ K ) x. ( |_ ` ( sqrt ` N ) ) ) e. RR )
26 17 nnred 
 |-  ( ph -> ( 2 ^ K ) e. RR )
27 20 rpred 
 |-  ( ph -> ( sqrt ` N ) e. RR )
28 26 27 remulcld 
 |-  ( ph -> ( ( 2 ^ K ) x. ( sqrt ` N ) ) e. RR )
29 ssrab2 
 |-  { x e. M | ( Q ` x ) = 1 } C_ M
30 ssfi 
 |-  ( ( M e. Fin /\ { x e. M | ( Q ` x ) = 1 } C_ M ) -> { x e. M | ( Q ` x ) = 1 } e. Fin )
31 9 29 30 mp2an 
 |-  { x e. M | ( Q ` x ) = 1 } e. Fin
32 hashcl 
 |-  ( { x e. M | ( Q ` x ) = 1 } e. Fin -> ( # ` { x e. M | ( Q ` x ) = 1 } ) e. NN0 )
33 31 32 ax-mp 
 |-  ( # ` { x e. M | ( Q ` x ) = 1 } ) e. NN0
34 33 nn0rei 
 |-  ( # ` { x e. M | ( Q ` x ) = 1 } ) e. RR
35 23 nn0red 
 |-  ( ph -> ( |_ ` ( sqrt ` N ) ) e. RR )
36 remulcl 
 |-  ( ( ( # ` { x e. M | ( Q ` x ) = 1 } ) e. RR /\ ( |_ ` ( sqrt ` N ) ) e. RR ) -> ( ( # ` { x e. M | ( Q ` x ) = 1 } ) x. ( |_ ` ( sqrt ` N ) ) ) e. RR )
37 34 35 36 sylancr 
 |-  ( ph -> ( ( # ` { x e. M | ( Q ` x ) = 1 } ) x. ( |_ ` ( sqrt ` N ) ) ) e. RR )
38 fzfi 
 |-  ( 1 ... ( |_ ` ( sqrt ` N ) ) ) e. Fin
39 xpfi 
 |-  ( ( { x e. M | ( Q ` x ) = 1 } e. Fin /\ ( 1 ... ( |_ ` ( sqrt ` N ) ) ) e. Fin ) -> ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) e. Fin )
40 31 38 39 mp2an 
 |-  ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) e. Fin
41 fveqeq2 
 |-  ( x = ( y / ( ( Q ` y ) ^ 2 ) ) -> ( ( Q ` x ) = 1 <-> ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) = 1 ) )
42 simpr 
 |-  ( ( ph /\ y e. M ) -> y e. M )
43 7 42 sselid 
 |-  ( ( ph /\ y e. M ) -> y e. ( 1 ... N ) )
44 elfznn 
 |-  ( y e. ( 1 ... N ) -> y e. NN )
45 43 44 syl 
 |-  ( ( ph /\ y e. M ) -> y e. NN )
46 5 prmreclem1 
 |-  ( y e. NN -> ( ( Q ` y ) e. NN /\ ( ( Q ` y ) ^ 2 ) || y /\ ( n e. ( ZZ>= ` 2 ) -> -. ( n ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) ) ) )
47 46 simp2d 
 |-  ( y e. NN -> ( ( Q ` y ) ^ 2 ) || y )
48 45 47 syl 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) ^ 2 ) || y )
49 46 simp1d 
 |-  ( y e. NN -> ( Q ` y ) e. NN )
50 45 49 syl 
 |-  ( ( ph /\ y e. M ) -> ( Q ` y ) e. NN )
51 50 nnsqcld 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) ^ 2 ) e. NN )
52 51 nnzd 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) ^ 2 ) e. ZZ )
53 51 nnne0d 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) ^ 2 ) =/= 0 )
54 45 nnzd 
 |-  ( ( ph /\ y e. M ) -> y e. ZZ )
55 dvdsval2 
 |-  ( ( ( ( Q ` y ) ^ 2 ) e. ZZ /\ ( ( Q ` y ) ^ 2 ) =/= 0 /\ y e. ZZ ) -> ( ( ( Q ` y ) ^ 2 ) || y <-> ( y / ( ( Q ` y ) ^ 2 ) ) e. ZZ ) )
56 52 53 54 55 syl3anc 
 |-  ( ( ph /\ y e. M ) -> ( ( ( Q ` y ) ^ 2 ) || y <-> ( y / ( ( Q ` y ) ^ 2 ) ) e. ZZ ) )
57 48 56 mpbid 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) e. ZZ )
58 nnre 
 |-  ( y e. NN -> y e. RR )
59 nngt0 
 |-  ( y e. NN -> 0 < y )
60 58 59 jca 
 |-  ( y e. NN -> ( y e. RR /\ 0 < y ) )
61 nnre 
 |-  ( ( ( Q ` y ) ^ 2 ) e. NN -> ( ( Q ` y ) ^ 2 ) e. RR )
62 nngt0 
 |-  ( ( ( Q ` y ) ^ 2 ) e. NN -> 0 < ( ( Q ` y ) ^ 2 ) )
63 61 62 jca 
 |-  ( ( ( Q ` y ) ^ 2 ) e. NN -> ( ( ( Q ` y ) ^ 2 ) e. RR /\ 0 < ( ( Q ` y ) ^ 2 ) ) )
64 divgt0 
 |-  ( ( ( y e. RR /\ 0 < y ) /\ ( ( ( Q ` y ) ^ 2 ) e. RR /\ 0 < ( ( Q ` y ) ^ 2 ) ) ) -> 0 < ( y / ( ( Q ` y ) ^ 2 ) ) )
65 60 63 64 syl2an 
 |-  ( ( y e. NN /\ ( ( Q ` y ) ^ 2 ) e. NN ) -> 0 < ( y / ( ( Q ` y ) ^ 2 ) ) )
66 45 51 65 syl2anc 
 |-  ( ( ph /\ y e. M ) -> 0 < ( y / ( ( Q ` y ) ^ 2 ) ) )
67 elnnz 
 |-  ( ( y / ( ( Q ` y ) ^ 2 ) ) e. NN <-> ( ( y / ( ( Q ` y ) ^ 2 ) ) e. ZZ /\ 0 < ( y / ( ( Q ` y ) ^ 2 ) ) ) )
68 57 66 67 sylanbrc 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) e. NN )
69 68 nnred 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) e. RR )
70 45 nnred 
 |-  ( ( ph /\ y e. M ) -> y e. RR )
71 3 nnred 
 |-  ( ph -> N e. RR )
72 71 adantr 
 |-  ( ( ph /\ y e. M ) -> N e. RR )
73 dvdsmul1 
 |-  ( ( ( y / ( ( Q ` y ) ^ 2 ) ) e. ZZ /\ ( ( Q ` y ) ^ 2 ) e. ZZ ) -> ( y / ( ( Q ` y ) ^ 2 ) ) || ( ( y / ( ( Q ` y ) ^ 2 ) ) x. ( ( Q ` y ) ^ 2 ) ) )
74 57 52 73 syl2anc 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) || ( ( y / ( ( Q ` y ) ^ 2 ) ) x. ( ( Q ` y ) ^ 2 ) ) )
75 45 nncnd 
 |-  ( ( ph /\ y e. M ) -> y e. CC )
76 51 nncnd 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) ^ 2 ) e. CC )
77 75 76 53 divcan1d 
 |-  ( ( ph /\ y e. M ) -> ( ( y / ( ( Q ` y ) ^ 2 ) ) x. ( ( Q ` y ) ^ 2 ) ) = y )
78 74 77 breqtrd 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) || y )
79 dvdsle 
 |-  ( ( ( y / ( ( Q ` y ) ^ 2 ) ) e. ZZ /\ y e. NN ) -> ( ( y / ( ( Q ` y ) ^ 2 ) ) || y -> ( y / ( ( Q ` y ) ^ 2 ) ) <_ y ) )
80 57 45 79 syl2anc 
 |-  ( ( ph /\ y e. M ) -> ( ( y / ( ( Q ` y ) ^ 2 ) ) || y -> ( y / ( ( Q ` y ) ^ 2 ) ) <_ y ) )
81 78 80 mpd 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) <_ y )
82 elfzle2 
 |-  ( y e. ( 1 ... N ) -> y <_ N )
83 43 82 syl 
 |-  ( ( ph /\ y e. M ) -> y <_ N )
84 69 70 72 81 83 letrd 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) <_ N )
85 nnuz 
 |-  NN = ( ZZ>= ` 1 )
86 68 85 eleqtrdi 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) e. ( ZZ>= ` 1 ) )
87 3 nnzd 
 |-  ( ph -> N e. ZZ )
88 87 adantr 
 |-  ( ( ph /\ y e. M ) -> N e. ZZ )
89 elfz5 
 |-  ( ( ( y / ( ( Q ` y ) ^ 2 ) ) e. ( ZZ>= ` 1 ) /\ N e. ZZ ) -> ( ( y / ( ( Q ` y ) ^ 2 ) ) e. ( 1 ... N ) <-> ( y / ( ( Q ` y ) ^ 2 ) ) <_ N ) )
90 86 88 89 syl2anc 
 |-  ( ( ph /\ y e. M ) -> ( ( y / ( ( Q ` y ) ^ 2 ) ) e. ( 1 ... N ) <-> ( y / ( ( Q ` y ) ^ 2 ) ) <_ N ) )
91 84 90 mpbird 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) e. ( 1 ... N ) )
92 breq2 
 |-  ( n = y -> ( p || n <-> p || y ) )
93 92 notbid 
 |-  ( n = y -> ( -. p || n <-> -. p || y ) )
94 93 ralbidv 
 |-  ( n = y -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
95 94 4 elrab2 
 |-  ( y e. M <-> ( y e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
96 42 95 sylib 
 |-  ( ( ph /\ y e. M ) -> ( y e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || y ) )
97 96 simprd 
 |-  ( ( ph /\ y e. M ) -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || y )
98 78 adantr 
 |-  ( ( ( ph /\ y e. M ) /\ p e. ( Prime \ ( 1 ... K ) ) ) -> ( y / ( ( Q ` y ) ^ 2 ) ) || y )
99 eldifi 
 |-  ( p e. ( Prime \ ( 1 ... K ) ) -> p e. Prime )
100 prmz 
 |-  ( p e. Prime -> p e. ZZ )
101 99 100 syl 
 |-  ( p e. ( Prime \ ( 1 ... K ) ) -> p e. ZZ )
102 101 adantl 
 |-  ( ( ( ph /\ y e. M ) /\ p e. ( Prime \ ( 1 ... K ) ) ) -> p e. ZZ )
103 57 adantr 
 |-  ( ( ( ph /\ y e. M ) /\ p e. ( Prime \ ( 1 ... K ) ) ) -> ( y / ( ( Q ` y ) ^ 2 ) ) e. ZZ )
104 54 adantr 
 |-  ( ( ( ph /\ y e. M ) /\ p e. ( Prime \ ( 1 ... K ) ) ) -> y e. ZZ )
105 dvdstr 
 |-  ( ( p e. ZZ /\ ( y / ( ( Q ` y ) ^ 2 ) ) e. ZZ /\ y e. ZZ ) -> ( ( p || ( y / ( ( Q ` y ) ^ 2 ) ) /\ ( y / ( ( Q ` y ) ^ 2 ) ) || y ) -> p || y ) )
106 102 103 104 105 syl3anc 
 |-  ( ( ( ph /\ y e. M ) /\ p e. ( Prime \ ( 1 ... K ) ) ) -> ( ( p || ( y / ( ( Q ` y ) ^ 2 ) ) /\ ( y / ( ( Q ` y ) ^ 2 ) ) || y ) -> p || y ) )
107 98 106 mpan2d 
 |-  ( ( ( ph /\ y e. M ) /\ p e. ( Prime \ ( 1 ... K ) ) ) -> ( p || ( y / ( ( Q ` y ) ^ 2 ) ) -> p || y ) )
108 107 con3d 
 |-  ( ( ( ph /\ y e. M ) /\ p e. ( Prime \ ( 1 ... K ) ) ) -> ( -. p || y -> -. p || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
109 108 ralimdva 
 |-  ( ( ph /\ y e. M ) -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || y -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
110 97 109 mpd 
 |-  ( ( ph /\ y e. M ) -> A. p e. ( Prime \ ( 1 ... K ) ) -. p || ( y / ( ( Q ` y ) ^ 2 ) ) )
111 breq2 
 |-  ( n = ( y / ( ( Q ` y ) ^ 2 ) ) -> ( p || n <-> p || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
112 111 notbid 
 |-  ( n = ( y / ( ( Q ` y ) ^ 2 ) ) -> ( -. p || n <-> -. p || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
113 112 ralbidv 
 |-  ( n = ( y / ( ( Q ` y ) ^ 2 ) ) -> ( A. p e. ( Prime \ ( 1 ... K ) ) -. p || n <-> A. p e. ( Prime \ ( 1 ... K ) ) -. p || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
114 113 4 elrab2 
 |-  ( ( y / ( ( Q ` y ) ^ 2 ) ) e. M <-> ( ( y / ( ( Q ` y ) ^ 2 ) ) e. ( 1 ... N ) /\ A. p e. ( Prime \ ( 1 ... K ) ) -. p || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
115 91 110 114 sylanbrc 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) e. M )
116 5 prmreclem1 
 |-  ( ( y / ( ( Q ` y ) ^ 2 ) ) e. NN -> ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) e. NN /\ ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) /\ ( A e. ( ZZ>= ` 2 ) -> -. ( A ^ 2 ) || ( ( y / ( ( Q ` y ) ^ 2 ) ) / ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) ^ 2 ) ) ) ) )
117 116 simp2d 
 |-  ( ( y / ( ( Q ` y ) ^ 2 ) ) e. NN -> ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) )
118 68 117 syl 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) )
119 116 simp1d 
 |-  ( ( y / ( ( Q ` y ) ^ 2 ) ) e. NN -> ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) e. NN )
120 68 119 syl 
 |-  ( ( ph /\ y e. M ) -> ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) e. NN )
121 elnn1uz2 
 |-  ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) e. NN <-> ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) = 1 \/ ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) e. ( ZZ>= ` 2 ) ) )
122 120 121 sylib 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) = 1 \/ ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) e. ( ZZ>= ` 2 ) ) )
123 122 ord 
 |-  ( ( ph /\ y e. M ) -> ( -. ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) = 1 -> ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) e. ( ZZ>= ` 2 ) ) )
124 5 prmreclem1 
 |-  ( y e. NN -> ( ( Q ` y ) e. NN /\ ( ( Q ` y ) ^ 2 ) || y /\ ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) e. ( ZZ>= ` 2 ) -> -. ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) ) ) )
125 124 simp3d 
 |-  ( y e. NN -> ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) e. ( ZZ>= ` 2 ) -> -. ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
126 45 123 125 sylsyld 
 |-  ( ( ph /\ y e. M ) -> ( -. ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) = 1 -> -. ( ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) ^ 2 ) || ( y / ( ( Q ` y ) ^ 2 ) ) ) )
127 118 126 mt4d 
 |-  ( ( ph /\ y e. M ) -> ( Q ` ( y / ( ( Q ` y ) ^ 2 ) ) ) = 1 )
128 41 115 127 elrabd 
 |-  ( ( ph /\ y e. M ) -> ( y / ( ( Q ` y ) ^ 2 ) ) e. { x e. M | ( Q ` x ) = 1 } )
129 51 nnred 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) ^ 2 ) e. RR )
130 dvdsle 
 |-  ( ( ( ( Q ` y ) ^ 2 ) e. ZZ /\ y e. NN ) -> ( ( ( Q ` y ) ^ 2 ) || y -> ( ( Q ` y ) ^ 2 ) <_ y ) )
131 52 45 130 syl2anc 
 |-  ( ( ph /\ y e. M ) -> ( ( ( Q ` y ) ^ 2 ) || y -> ( ( Q ` y ) ^ 2 ) <_ y ) )
132 48 131 mpd 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) ^ 2 ) <_ y )
133 129 70 72 132 83 letrd 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) ^ 2 ) <_ N )
134 72 recnd 
 |-  ( ( ph /\ y e. M ) -> N e. CC )
135 134 sqsqrtd 
 |-  ( ( ph /\ y e. M ) -> ( ( sqrt ` N ) ^ 2 ) = N )
136 133 135 breqtrrd 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) ^ 2 ) <_ ( ( sqrt ` N ) ^ 2 ) )
137 50 nnrpd 
 |-  ( ( ph /\ y e. M ) -> ( Q ` y ) e. RR+ )
138 20 adantr 
 |-  ( ( ph /\ y e. M ) -> ( sqrt ` N ) e. RR+ )
139 rprege0 
 |-  ( ( Q ` y ) e. RR+ -> ( ( Q ` y ) e. RR /\ 0 <_ ( Q ` y ) ) )
140 rprege0 
 |-  ( ( sqrt ` N ) e. RR+ -> ( ( sqrt ` N ) e. RR /\ 0 <_ ( sqrt ` N ) ) )
141 le2sq 
 |-  ( ( ( ( Q ` y ) e. RR /\ 0 <_ ( Q ` y ) ) /\ ( ( sqrt ` N ) e. RR /\ 0 <_ ( sqrt ` N ) ) ) -> ( ( Q ` y ) <_ ( sqrt ` N ) <-> ( ( Q ` y ) ^ 2 ) <_ ( ( sqrt ` N ) ^ 2 ) ) )
142 139 140 141 syl2an 
 |-  ( ( ( Q ` y ) e. RR+ /\ ( sqrt ` N ) e. RR+ ) -> ( ( Q ` y ) <_ ( sqrt ` N ) <-> ( ( Q ` y ) ^ 2 ) <_ ( ( sqrt ` N ) ^ 2 ) ) )
143 137 138 142 syl2anc 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) <_ ( sqrt ` N ) <-> ( ( Q ` y ) ^ 2 ) <_ ( ( sqrt ` N ) ^ 2 ) ) )
144 136 143 mpbird 
 |-  ( ( ph /\ y e. M ) -> ( Q ` y ) <_ ( sqrt ` N ) )
145 27 adantr 
 |-  ( ( ph /\ y e. M ) -> ( sqrt ` N ) e. RR )
146 50 nnzd 
 |-  ( ( ph /\ y e. M ) -> ( Q ` y ) e. ZZ )
147 flge 
 |-  ( ( ( sqrt ` N ) e. RR /\ ( Q ` y ) e. ZZ ) -> ( ( Q ` y ) <_ ( sqrt ` N ) <-> ( Q ` y ) <_ ( |_ ` ( sqrt ` N ) ) ) )
148 145 146 147 syl2anc 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) <_ ( sqrt ` N ) <-> ( Q ` y ) <_ ( |_ ` ( sqrt ` N ) ) ) )
149 144 148 mpbid 
 |-  ( ( ph /\ y e. M ) -> ( Q ` y ) <_ ( |_ ` ( sqrt ` N ) ) )
150 50 85 eleqtrdi 
 |-  ( ( ph /\ y e. M ) -> ( Q ` y ) e. ( ZZ>= ` 1 ) )
151 23 nn0zd 
 |-  ( ph -> ( |_ ` ( sqrt ` N ) ) e. ZZ )
152 151 adantr 
 |-  ( ( ph /\ y e. M ) -> ( |_ ` ( sqrt ` N ) ) e. ZZ )
153 elfz5 
 |-  ( ( ( Q ` y ) e. ( ZZ>= ` 1 ) /\ ( |_ ` ( sqrt ` N ) ) e. ZZ ) -> ( ( Q ` y ) e. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) <-> ( Q ` y ) <_ ( |_ ` ( sqrt ` N ) ) ) )
154 150 152 153 syl2anc 
 |-  ( ( ph /\ y e. M ) -> ( ( Q ` y ) e. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) <-> ( Q ` y ) <_ ( |_ ` ( sqrt ` N ) ) ) )
155 149 154 mpbird 
 |-  ( ( ph /\ y e. M ) -> ( Q ` y ) e. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) )
156 128 155 opelxpd 
 |-  ( ( ph /\ y e. M ) -> <. ( y / ( ( Q ` y ) ^ 2 ) ) , ( Q ` y ) >. e. ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) )
157 156 ex 
 |-  ( ph -> ( y e. M -> <. ( y / ( ( Q ` y ) ^ 2 ) ) , ( Q ` y ) >. e. ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) )
158 ovex 
 |-  ( y / ( ( Q ` y ) ^ 2 ) ) e. _V
159 fvex 
 |-  ( Q ` y ) e. _V
160 158 159 opth 
 |-  ( <. ( y / ( ( Q ` y ) ^ 2 ) ) , ( Q ` y ) >. = <. ( z / ( ( Q ` z ) ^ 2 ) ) , ( Q ` z ) >. <-> ( ( y / ( ( Q ` y ) ^ 2 ) ) = ( z / ( ( Q ` z ) ^ 2 ) ) /\ ( Q ` y ) = ( Q ` z ) ) )
161 oveq1 
 |-  ( ( Q ` y ) = ( Q ` z ) -> ( ( Q ` y ) ^ 2 ) = ( ( Q ` z ) ^ 2 ) )
162 oveq12 
 |-  ( ( ( y / ( ( Q ` y ) ^ 2 ) ) = ( z / ( ( Q ` z ) ^ 2 ) ) /\ ( ( Q ` y ) ^ 2 ) = ( ( Q ` z ) ^ 2 ) ) -> ( ( y / ( ( Q ` y ) ^ 2 ) ) x. ( ( Q ` y ) ^ 2 ) ) = ( ( z / ( ( Q ` z ) ^ 2 ) ) x. ( ( Q ` z ) ^ 2 ) ) )
163 161 162 sylan2 
 |-  ( ( ( y / ( ( Q ` y ) ^ 2 ) ) = ( z / ( ( Q ` z ) ^ 2 ) ) /\ ( Q ` y ) = ( Q ` z ) ) -> ( ( y / ( ( Q ` y ) ^ 2 ) ) x. ( ( Q ` y ) ^ 2 ) ) = ( ( z / ( ( Q ` z ) ^ 2 ) ) x. ( ( Q ` z ) ^ 2 ) ) )
164 160 163 sylbi 
 |-  ( <. ( y / ( ( Q ` y ) ^ 2 ) ) , ( Q ` y ) >. = <. ( z / ( ( Q ` z ) ^ 2 ) ) , ( Q ` z ) >. -> ( ( y / ( ( Q ` y ) ^ 2 ) ) x. ( ( Q ` y ) ^ 2 ) ) = ( ( z / ( ( Q ` z ) ^ 2 ) ) x. ( ( Q ` z ) ^ 2 ) ) )
165 77 adantrr 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> ( ( y / ( ( Q ` y ) ^ 2 ) ) x. ( ( Q ` y ) ^ 2 ) ) = y )
166 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
167 7 166 sstri 
 |-  M C_ NN
168 simprr 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> z e. M )
169 167 168 sselid 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> z e. NN )
170 169 nncnd 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> z e. CC )
171 5 prmreclem1 
 |-  ( z e. NN -> ( ( Q ` z ) e. NN /\ ( ( Q ` z ) ^ 2 ) || z /\ ( 2 e. ( ZZ>= ` 2 ) -> -. ( 2 ^ 2 ) || ( z / ( ( Q ` z ) ^ 2 ) ) ) ) )
172 171 simp1d 
 |-  ( z e. NN -> ( Q ` z ) e. NN )
173 169 172 syl 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> ( Q ` z ) e. NN )
174 173 nnsqcld 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> ( ( Q ` z ) ^ 2 ) e. NN )
175 174 nncnd 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> ( ( Q ` z ) ^ 2 ) e. CC )
176 174 nnne0d 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> ( ( Q ` z ) ^ 2 ) =/= 0 )
177 170 175 176 divcan1d 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> ( ( z / ( ( Q ` z ) ^ 2 ) ) x. ( ( Q ` z ) ^ 2 ) ) = z )
178 165 177 eqeq12d 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> ( ( ( y / ( ( Q ` y ) ^ 2 ) ) x. ( ( Q ` y ) ^ 2 ) ) = ( ( z / ( ( Q ` z ) ^ 2 ) ) x. ( ( Q ` z ) ^ 2 ) ) <-> y = z ) )
179 164 178 imbitrid 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> ( <. ( y / ( ( Q ` y ) ^ 2 ) ) , ( Q ` y ) >. = <. ( z / ( ( Q ` z ) ^ 2 ) ) , ( Q ` z ) >. -> y = z ) )
180 id 
 |-  ( y = z -> y = z )
181 fveq2 
 |-  ( y = z -> ( Q ` y ) = ( Q ` z ) )
182 181 oveq1d 
 |-  ( y = z -> ( ( Q ` y ) ^ 2 ) = ( ( Q ` z ) ^ 2 ) )
183 180 182 oveq12d 
 |-  ( y = z -> ( y / ( ( Q ` y ) ^ 2 ) ) = ( z / ( ( Q ` z ) ^ 2 ) ) )
184 183 181 opeq12d 
 |-  ( y = z -> <. ( y / ( ( Q ` y ) ^ 2 ) ) , ( Q ` y ) >. = <. ( z / ( ( Q ` z ) ^ 2 ) ) , ( Q ` z ) >. )
185 179 184 impbid1 
 |-  ( ( ph /\ ( y e. M /\ z e. M ) ) -> ( <. ( y / ( ( Q ` y ) ^ 2 ) ) , ( Q ` y ) >. = <. ( z / ( ( Q ` z ) ^ 2 ) ) , ( Q ` z ) >. <-> y = z ) )
186 185 ex 
 |-  ( ph -> ( ( y e. M /\ z e. M ) -> ( <. ( y / ( ( Q ` y ) ^ 2 ) ) , ( Q ` y ) >. = <. ( z / ( ( Q ` z ) ^ 2 ) ) , ( Q ` z ) >. <-> y = z ) ) )
187 157 186 dom2d 
 |-  ( ph -> ( ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) e. Fin -> M ~<_ ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) )
188 40 187 mpi 
 |-  ( ph -> M ~<_ ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) )
189 hashdom 
 |-  ( ( M e. Fin /\ ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) e. Fin ) -> ( ( # ` M ) <_ ( # ` ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) <-> M ~<_ ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) )
190 9 40 189 mp2an 
 |-  ( ( # ` M ) <_ ( # ` ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) <-> M ~<_ ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) )
191 188 190 sylibr 
 |-  ( ph -> ( # ` M ) <_ ( # ` ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) )
192 hashxp 
 |-  ( ( { x e. M | ( Q ` x ) = 1 } e. Fin /\ ( 1 ... ( |_ ` ( sqrt ` N ) ) ) e. Fin ) -> ( # ` ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) = ( ( # ` { x e. M | ( Q ` x ) = 1 } ) x. ( # ` ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) )
193 31 38 192 mp2an 
 |-  ( # ` ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) = ( ( # ` { x e. M | ( Q ` x ) = 1 } ) x. ( # ` ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) )
194 hashfz1 
 |-  ( ( |_ ` ( sqrt ` N ) ) e. NN0 -> ( # ` ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) = ( |_ ` ( sqrt ` N ) ) )
195 23 194 syl 
 |-  ( ph -> ( # ` ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) = ( |_ ` ( sqrt ` N ) ) )
196 195 oveq2d 
 |-  ( ph -> ( ( # ` { x e. M | ( Q ` x ) = 1 } ) x. ( # ` ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) = ( ( # ` { x e. M | ( Q ` x ) = 1 } ) x. ( |_ ` ( sqrt ` N ) ) ) )
197 193 196 eqtrid 
 |-  ( ph -> ( # ` ( { x e. M | ( Q ` x ) = 1 } X. ( 1 ... ( |_ ` ( sqrt ` N ) ) ) ) ) = ( ( # ` { x e. M | ( Q ` x ) = 1 } ) x. ( |_ ` ( sqrt ` N ) ) ) )
198 191 197 breqtrd 
 |-  ( ph -> ( # ` M ) <_ ( ( # ` { x e. M | ( Q ` x ) = 1 } ) x. ( |_ ` ( sqrt ` N ) ) ) )
199 34 a1i 
 |-  ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) e. RR )
200 23 nn0ge0d 
 |-  ( ph -> 0 <_ ( |_ ` ( sqrt ` N ) ) )
201 1 2 3 4 5 prmreclem2 
 |-  ( ph -> ( # ` { x e. M | ( Q ` x ) = 1 } ) <_ ( 2 ^ K ) )
202 199 26 35 200 201 lemul1ad 
 |-  ( ph -> ( ( # ` { x e. M | ( Q ` x ) = 1 } ) x. ( |_ ` ( sqrt ` N ) ) ) <_ ( ( 2 ^ K ) x. ( |_ ` ( sqrt ` N ) ) ) )
203 13 37 25 198 202 letrd 
 |-  ( ph -> ( # ` M ) <_ ( ( 2 ^ K ) x. ( |_ ` ( sqrt ` N ) ) ) )
204 17 nnrpd 
 |-  ( ph -> ( 2 ^ K ) e. RR+ )
205 204 rprege0d 
 |-  ( ph -> ( ( 2 ^ K ) e. RR /\ 0 <_ ( 2 ^ K ) ) )
206 fllelt 
 |-  ( ( sqrt ` N ) e. RR -> ( ( |_ ` ( sqrt ` N ) ) <_ ( sqrt ` N ) /\ ( sqrt ` N ) < ( ( |_ ` ( sqrt ` N ) ) + 1 ) ) )
207 27 206 syl 
 |-  ( ph -> ( ( |_ ` ( sqrt ` N ) ) <_ ( sqrt ` N ) /\ ( sqrt ` N ) < ( ( |_ ` ( sqrt ` N ) ) + 1 ) ) )
208 207 simpld 
 |-  ( ph -> ( |_ ` ( sqrt ` N ) ) <_ ( sqrt ` N ) )
209 lemul2a 
 |-  ( ( ( ( |_ ` ( sqrt ` N ) ) e. RR /\ ( sqrt ` N ) e. RR /\ ( ( 2 ^ K ) e. RR /\ 0 <_ ( 2 ^ K ) ) ) /\ ( |_ ` ( sqrt ` N ) ) <_ ( sqrt ` N ) ) -> ( ( 2 ^ K ) x. ( |_ ` ( sqrt ` N ) ) ) <_ ( ( 2 ^ K ) x. ( sqrt ` N ) ) )
210 35 27 205 208 209 syl31anc 
 |-  ( ph -> ( ( 2 ^ K ) x. ( |_ ` ( sqrt ` N ) ) ) <_ ( ( 2 ^ K ) x. ( sqrt ` N ) ) )
211 13 25 28 203 210 letrd 
 |-  ( ph -> ( # ` M ) <_ ( ( 2 ^ K ) x. ( sqrt ` N ) ) )