Metamath Proof Explorer

Theorem 4sqlem11

Description: Lemma for 4sq . Use the pigeonhole principle to show that the sets { m ^ 2 | m e. ( 0 ... N ) } and { -u 1 - n ^ 2 | n e. ( 0 ... N ) } have a common element, mod P . (Contributed by Mario Carneiro, 15-Jul-2014)

Ref Expression
Hypotheses 4sq.1 
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
4sq.2 
|- ( ph -> N e. NN )
4sq.3 
|- ( ph -> P = ( ( 2 x. N ) + 1 ) )
4sq.4 
|- ( ph -> P e. Prime )
4sqlem11.5 
|- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }
4sqlem11.6 
|- F = ( v e. A |-> ( ( P - 1 ) - v ) )
Assertion 4sqlem11 
|- ( ph -> ( A i^i ran F ) =/= (/) )

Proof

Step Hyp Ref Expression
1 4sq.1 
 |-  S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
2 4sq.2 
 |-  ( ph -> N e. NN )
3 4sq.3 
 |-  ( ph -> P = ( ( 2 x. N ) + 1 ) )
4 4sq.4 
 |-  ( ph -> P e. Prime )
5 4sqlem11.5 
 |-  A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }
6 4sqlem11.6 
 |-  F = ( v e. A |-> ( ( P - 1 ) - v ) )
7 fzfid 
 |-  ( ph -> ( 0 ... ( P - 1 ) ) e. Fin )
8 elfzelz 
 |-  ( m e. ( 0 ... N ) -> m e. ZZ )
9 zsqcl 
 |-  ( m e. ZZ -> ( m ^ 2 ) e. ZZ )
10 8 9 syl 
 |-  ( m e. ( 0 ... N ) -> ( m ^ 2 ) e. ZZ )
11 prmnn 
 |-  ( P e. Prime -> P e. NN )
12 4 11 syl 
 |-  ( ph -> P e. NN )
13 zmodfz 
 |-  ( ( ( m ^ 2 ) e. ZZ /\ P e. NN ) -> ( ( m ^ 2 ) mod P ) e. ( 0 ... ( P - 1 ) ) )
14 10 12 13 syl2anr 
 |-  ( ( ph /\ m e. ( 0 ... N ) ) -> ( ( m ^ 2 ) mod P ) e. ( 0 ... ( P - 1 ) ) )
15 eleq1a 
 |-  ( ( ( m ^ 2 ) mod P ) e. ( 0 ... ( P - 1 ) ) -> ( u = ( ( m ^ 2 ) mod P ) -> u e. ( 0 ... ( P - 1 ) ) ) )
16 14 15 syl 
 |-  ( ( ph /\ m e. ( 0 ... N ) ) -> ( u = ( ( m ^ 2 ) mod P ) -> u e. ( 0 ... ( P - 1 ) ) ) )
17 16 rexlimdva 
 |-  ( ph -> ( E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) -> u e. ( 0 ... ( P - 1 ) ) ) )
18 17 abssdv 
 |-  ( ph -> { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) } C_ ( 0 ... ( P - 1 ) ) )
19 5 18 eqsstrid 
 |-  ( ph -> A C_ ( 0 ... ( P - 1 ) ) )
20 prmz 
 |-  ( P e. Prime -> P e. ZZ )
21 4 20 syl 
 |-  ( ph -> P e. ZZ )
22 peano2zm 
 |-  ( P e. ZZ -> ( P - 1 ) e. ZZ )
23 21 22 syl 
 |-  ( ph -> ( P - 1 ) e. ZZ )
24 23 zcnd 
 |-  ( ph -> ( P - 1 ) e. CC )
25 24 addlidd 
 |-  ( ph -> ( 0 + ( P - 1 ) ) = ( P - 1 ) )
26 25 oveq1d 
 |-  ( ph -> ( ( 0 + ( P - 1 ) ) - v ) = ( ( P - 1 ) - v ) )
27 26 adantr 
 |-  ( ( ph /\ v e. A ) -> ( ( 0 + ( P - 1 ) ) - v ) = ( ( P - 1 ) - v ) )
28 19 sselda 
 |-  ( ( ph /\ v e. A ) -> v e. ( 0 ... ( P - 1 ) ) )
29 fzrev3i 
 |-  ( v e. ( 0 ... ( P - 1 ) ) -> ( ( 0 + ( P - 1 ) ) - v ) e. ( 0 ... ( P - 1 ) ) )
30 28 29 syl 
 |-  ( ( ph /\ v e. A ) -> ( ( 0 + ( P - 1 ) ) - v ) e. ( 0 ... ( P - 1 ) ) )
31 27 30 eqeltrrd 
 |-  ( ( ph /\ v e. A ) -> ( ( P - 1 ) - v ) e. ( 0 ... ( P - 1 ) ) )
32 31 6 fmptd 
 |-  ( ph -> F : A --> ( 0 ... ( P - 1 ) ) )
33 32 frnd 
 |-  ( ph -> ran F C_ ( 0 ... ( P - 1 ) ) )
34 19 33 unssd 
 |-  ( ph -> ( A u. ran F ) C_ ( 0 ... ( P - 1 ) ) )
35 7 34 ssfid 
 |-  ( ph -> ( A u. ran F ) e. Fin )
36 hashcl 
 |-  ( ( A u. ran F ) e. Fin -> ( # ` ( A u. ran F ) ) e. NN0 )
37 35 36 syl 
 |-  ( ph -> ( # ` ( A u. ran F ) ) e. NN0 )
38 37 nn0red 
 |-  ( ph -> ( # ` ( A u. ran F ) ) e. RR )
39 21 zred 
 |-  ( ph -> P e. RR )
40 ssdomg 
 |-  ( ( 0 ... ( P - 1 ) ) e. Fin -> ( ( A u. ran F ) C_ ( 0 ... ( P - 1 ) ) -> ( A u. ran F ) ~<_ ( 0 ... ( P - 1 ) ) ) )
41 7 34 40 sylc 
 |-  ( ph -> ( A u. ran F ) ~<_ ( 0 ... ( P - 1 ) ) )
42 hashdom 
 |-  ( ( ( A u. ran F ) e. Fin /\ ( 0 ... ( P - 1 ) ) e. Fin ) -> ( ( # ` ( A u. ran F ) ) <_ ( # ` ( 0 ... ( P - 1 ) ) ) <-> ( A u. ran F ) ~<_ ( 0 ... ( P - 1 ) ) ) )
43 35 7 42 syl2anc 
 |-  ( ph -> ( ( # ` ( A u. ran F ) ) <_ ( # ` ( 0 ... ( P - 1 ) ) ) <-> ( A u. ran F ) ~<_ ( 0 ... ( P - 1 ) ) ) )
44 41 43 mpbird 
 |-  ( ph -> ( # ` ( A u. ran F ) ) <_ ( # ` ( 0 ... ( P - 1 ) ) ) )
45 fz01en 
 |-  ( P e. ZZ -> ( 0 ... ( P - 1 ) ) ~~ ( 1 ... P ) )
46 21 45 syl 
 |-  ( ph -> ( 0 ... ( P - 1 ) ) ~~ ( 1 ... P ) )
47 fzfid 
 |-  ( ph -> ( 1 ... P ) e. Fin )
48 hashen 
 |-  ( ( ( 0 ... ( P - 1 ) ) e. Fin /\ ( 1 ... P ) e. Fin ) -> ( ( # ` ( 0 ... ( P - 1 ) ) ) = ( # ` ( 1 ... P ) ) <-> ( 0 ... ( P - 1 ) ) ~~ ( 1 ... P ) ) )
49 7 47 48 syl2anc 
 |-  ( ph -> ( ( # ` ( 0 ... ( P - 1 ) ) ) = ( # ` ( 1 ... P ) ) <-> ( 0 ... ( P - 1 ) ) ~~ ( 1 ... P ) ) )
50 46 49 mpbird 
 |-  ( ph -> ( # ` ( 0 ... ( P - 1 ) ) ) = ( # ` ( 1 ... P ) ) )
51 12 nnnn0d 
 |-  ( ph -> P e. NN0 )
52 hashfz1 
 |-  ( P e. NN0 -> ( # ` ( 1 ... P ) ) = P )
53 51 52 syl 
 |-  ( ph -> ( # ` ( 1 ... P ) ) = P )
54 50 53 eqtrd 
 |-  ( ph -> ( # ` ( 0 ... ( P - 1 ) ) ) = P )
55 44 54 breqtrd 
 |-  ( ph -> ( # ` ( A u. ran F ) ) <_ P )
56 38 39 55 lensymd 
 |-  ( ph -> -. P < ( # ` ( A u. ran F ) ) )
57 39 adantr 
 |-  ( ( ph /\ ( A i^i ran F ) = (/) ) -> P e. RR )
58 57 ltp1d 
 |-  ( ( ph /\ ( A i^i ran F ) = (/) ) -> P < ( P + 1 ) )
59 2 nncnd 
 |-  ( ph -> N e. CC )
60 1cnd 
 |-  ( ph -> 1 e. CC )
61 59 59 60 60 add4d 
 |-  ( ph -> ( ( N + N ) + ( 1 + 1 ) ) = ( ( N + 1 ) + ( N + 1 ) ) )
62 3 oveq1d 
 |-  ( ph -> ( P + 1 ) = ( ( ( 2 x. N ) + 1 ) + 1 ) )
63 2cn 
 |-  2 e. CC
64 mulcl 
 |-  ( ( 2 e. CC /\ N e. CC ) -> ( 2 x. N ) e. CC )
65 63 59 64 sylancr 
 |-  ( ph -> ( 2 x. N ) e. CC )
66 65 60 60 addassd 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) + 1 ) = ( ( 2 x. N ) + ( 1 + 1 ) ) )
67 59 2timesd 
 |-  ( ph -> ( 2 x. N ) = ( N + N ) )
68 67 oveq1d 
 |-  ( ph -> ( ( 2 x. N ) + ( 1 + 1 ) ) = ( ( N + N ) + ( 1 + 1 ) ) )
69 62 66 68 3eqtrd 
 |-  ( ph -> ( P + 1 ) = ( ( N + N ) + ( 1 + 1 ) ) )
70 14 ex 
 |-  ( ph -> ( m e. ( 0 ... N ) -> ( ( m ^ 2 ) mod P ) e. ( 0 ... ( P - 1 ) ) ) )
71 12 adantr 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> P e. NN )
72 8 ad2antrl 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> m e. ZZ )
73 72 9 syl 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m ^ 2 ) e. ZZ )
74 elfzelz 
 |-  ( u e. ( 0 ... N ) -> u e. ZZ )
75 74 ad2antll 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> u e. ZZ )
76 zsqcl 
 |-  ( u e. ZZ -> ( u ^ 2 ) e. ZZ )
77 75 76 syl 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( u ^ 2 ) e. ZZ )
78 moddvds 
 |-  ( ( P e. NN /\ ( m ^ 2 ) e. ZZ /\ ( u ^ 2 ) e. ZZ ) -> ( ( ( m ^ 2 ) mod P ) = ( ( u ^ 2 ) mod P ) <-> P || ( ( m ^ 2 ) - ( u ^ 2 ) ) ) )
79 71 73 77 78 syl3anc 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( ( m ^ 2 ) mod P ) = ( ( u ^ 2 ) mod P ) <-> P || ( ( m ^ 2 ) - ( u ^ 2 ) ) ) )
80 72 zcnd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> m e. CC )
81 75 zcnd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> u e. CC )
82 subsq 
 |-  ( ( m e. CC /\ u e. CC ) -> ( ( m ^ 2 ) - ( u ^ 2 ) ) = ( ( m + u ) x. ( m - u ) ) )
83 80 81 82 syl2anc 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( m ^ 2 ) - ( u ^ 2 ) ) = ( ( m + u ) x. ( m - u ) ) )
84 83 breq2d 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( P || ( ( m ^ 2 ) - ( u ^ 2 ) ) <-> P || ( ( m + u ) x. ( m - u ) ) ) )
85 4 adantr 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> P e. Prime )
86 72 75 zaddcld 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m + u ) e. ZZ )
87 72 75 zsubcld 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m - u ) e. ZZ )
88 euclemma 
 |-  ( ( P e. Prime /\ ( m + u ) e. ZZ /\ ( m - u ) e. ZZ ) -> ( P || ( ( m + u ) x. ( m - u ) ) <-> ( P || ( m + u ) \/ P || ( m - u ) ) ) )
89 85 86 87 88 syl3anc 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( P || ( ( m + u ) x. ( m - u ) ) <-> ( P || ( m + u ) \/ P || ( m - u ) ) ) )
90 79 84 89 3bitrd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( ( m ^ 2 ) mod P ) = ( ( u ^ 2 ) mod P ) <-> ( P || ( m + u ) \/ P || ( m - u ) ) ) )
91 86 zred 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m + u ) e. RR )
92 2re 
 |-  2 e. RR
93 2 nnred 
 |-  ( ph -> N e. RR )
94 remulcl 
 |-  ( ( 2 e. RR /\ N e. RR ) -> ( 2 x. N ) e. RR )
95 92 93 94 sylancr 
 |-  ( ph -> ( 2 x. N ) e. RR )
96 95 adantr 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( 2 x. N ) e. RR )
97 85 20 syl 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> P e. ZZ )
98 97 zred 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> P e. RR )
99 72 zred 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> m e. RR )
100 75 zred 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> u e. RR )
101 93 adantr 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> N e. RR )
102 elfzle2 
 |-  ( m e. ( 0 ... N ) -> m <_ N )
103 102 ad2antrl 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> m <_ N )
104 elfzle2 
 |-  ( u e. ( 0 ... N ) -> u <_ N )
105 104 ad2antll 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> u <_ N )
106 99 100 101 101 103 105 le2addd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m + u ) <_ ( N + N ) )
107 59 adantr 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> N e. CC )
108 107 2timesd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( 2 x. N ) = ( N + N ) )
109 106 108 breqtrrd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m + u ) <_ ( 2 x. N ) )
110 95 ltp1d 
 |-  ( ph -> ( 2 x. N ) < ( ( 2 x. N ) + 1 ) )
111 110 3 breqtrrd 
 |-  ( ph -> ( 2 x. N ) < P )
112 111 adantr 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( 2 x. N ) < P )
113 91 96 98 109 112 lelttrd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m + u ) < P )
114 91 98 ltnled 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( m + u ) < P <-> -. P <_ ( m + u ) ) )
115 113 114 mpbid 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> -. P <_ ( m + u ) )
116 115 adantr 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> -. P <_ ( m + u ) )
117 21 ad2antrr 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> P e. ZZ )
118 86 adantr 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( m + u ) e. ZZ )
119 1red 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> 1 e. RR )
120 nn0abscl 
 |-  ( ( m - u ) e. ZZ -> ( abs ` ( m - u ) ) e. NN0 )
121 87 120 syl 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` ( m - u ) ) e. NN0 )
122 121 nn0red 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` ( m - u ) ) e. RR )
123 122 adantr 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( abs ` ( m - u ) ) e. RR )
124 118 zred 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( m + u ) e. RR )
125 121 adantr 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( abs ` ( m - u ) ) e. NN0 )
126 125 nn0zd 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( abs ` ( m - u ) ) e. ZZ )
127 87 zcnd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m - u ) e. CC )
128 127 adantr 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( m - u ) e. CC )
129 80 81 subeq0ad 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( m - u ) = 0 <-> m = u ) )
130 129 necon3bid 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( m - u ) =/= 0 <-> m =/= u ) )
131 130 biimpar 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( m - u ) =/= 0 )
132 128 131 absrpcld 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( abs ` ( m - u ) ) e. RR+ )
133 132 rpgt0d 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> 0 < ( abs ` ( m - u ) ) )
134 elnnz 
 |-  ( ( abs ` ( m - u ) ) e. NN <-> ( ( abs ` ( m - u ) ) e. ZZ /\ 0 < ( abs ` ( m - u ) ) ) )
135 126 133 134 sylanbrc 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( abs ` ( m - u ) ) e. NN )
136 135 nnge1d 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> 1 <_ ( abs ` ( m - u ) ) )
137 0cnd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> 0 e. CC )
138 80 81 137 abs3difd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` ( m - u ) ) <_ ( ( abs ` ( m - 0 ) ) + ( abs ` ( 0 - u ) ) ) )
139 80 subid1d 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m - 0 ) = m )
140 139 fveq2d 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` ( m - 0 ) ) = ( abs ` m ) )
141 elfzle1 
 |-  ( m e. ( 0 ... N ) -> 0 <_ m )
142 141 ad2antrl 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> 0 <_ m )
143 99 142 absidd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` m ) = m )
144 140 143 eqtrd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` ( m - 0 ) ) = m )
145 0cn 
 |-  0 e. CC
146 abssub 
 |-  ( ( 0 e. CC /\ u e. CC ) -> ( abs ` ( 0 - u ) ) = ( abs ` ( u - 0 ) ) )
147 145 81 146 sylancr 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` ( 0 - u ) ) = ( abs ` ( u - 0 ) ) )
148 81 subid1d 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( u - 0 ) = u )
149 148 fveq2d 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` ( u - 0 ) ) = ( abs ` u ) )
150 elfzle1 
 |-  ( u e. ( 0 ... N ) -> 0 <_ u )
151 150 ad2antll 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> 0 <_ u )
152 100 151 absidd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` u ) = u )
153 147 149 152 3eqtrd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` ( 0 - u ) ) = u )
154 144 153 oveq12d 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( abs ` ( m - 0 ) ) + ( abs ` ( 0 - u ) ) ) = ( m + u ) )
155 138 154 breqtrd 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( abs ` ( m - u ) ) <_ ( m + u ) )
156 155 adantr 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( abs ` ( m - u ) ) <_ ( m + u ) )
157 119 123 124 136 156 letrd 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> 1 <_ ( m + u ) )
158 elnnz1 
 |-  ( ( m + u ) e. NN <-> ( ( m + u ) e. ZZ /\ 1 <_ ( m + u ) ) )
159 118 157 158 sylanbrc 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( m + u ) e. NN )
160 dvdsle 
 |-  ( ( P e. ZZ /\ ( m + u ) e. NN ) -> ( P || ( m + u ) -> P <_ ( m + u ) ) )
161 117 159 160 syl2anc 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( P || ( m + u ) -> P <_ ( m + u ) ) )
162 116 161 mtod 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> -. P || ( m + u ) )
163 162 ex 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m =/= u -> -. P || ( m + u ) ) )
164 163 necon4ad 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( P || ( m + u ) -> m = u ) )
165 dvdsabsb 
 |-  ( ( P e. ZZ /\ ( m - u ) e. ZZ ) -> ( P || ( m - u ) <-> P || ( abs ` ( m - u ) ) ) )
166 97 87 165 syl2anc 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( P || ( m - u ) <-> P || ( abs ` ( m - u ) ) ) )
167 letr 
 |-  ( ( P e. RR /\ ( abs ` ( m - u ) ) e. RR /\ ( m + u ) e. RR ) -> ( ( P <_ ( abs ` ( m - u ) ) /\ ( abs ` ( m - u ) ) <_ ( m + u ) ) -> P <_ ( m + u ) ) )
168 98 122 91 167 syl3anc 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( P <_ ( abs ` ( m - u ) ) /\ ( abs ` ( m - u ) ) <_ ( m + u ) ) -> P <_ ( m + u ) ) )
169 155 168 mpan2d 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( P <_ ( abs ` ( m - u ) ) -> P <_ ( m + u ) ) )
170 115 169 mtod 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> -. P <_ ( abs ` ( m - u ) ) )
171 170 adantr 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> -. P <_ ( abs ` ( m - u ) ) )
172 97 adantr 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> P e. ZZ )
173 dvdsle 
 |-  ( ( P e. ZZ /\ ( abs ` ( m - u ) ) e. NN ) -> ( P || ( abs ` ( m - u ) ) -> P <_ ( abs ` ( m - u ) ) ) )
174 172 135 173 syl2anc 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> ( P || ( abs ` ( m - u ) ) -> P <_ ( abs ` ( m - u ) ) ) )
175 171 174 mtod 
 |-  ( ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) /\ m =/= u ) -> -. P || ( abs ` ( m - u ) ) )
176 175 ex 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( m =/= u -> -. P || ( abs ` ( m - u ) ) ) )
177 176 necon4ad 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( P || ( abs ` ( m - u ) ) -> m = u ) )
178 166 177 sylbid 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( P || ( m - u ) -> m = u ) )
179 164 178 jaod 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( P || ( m + u ) \/ P || ( m - u ) ) -> m = u ) )
180 90 179 sylbid 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( ( m ^ 2 ) mod P ) = ( ( u ^ 2 ) mod P ) -> m = u ) )
181 oveq1 
 |-  ( m = u -> ( m ^ 2 ) = ( u ^ 2 ) )
182 181 oveq1d 
 |-  ( m = u -> ( ( m ^ 2 ) mod P ) = ( ( u ^ 2 ) mod P ) )
183 180 182 impbid1 
 |-  ( ( ph /\ ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) ) -> ( ( ( m ^ 2 ) mod P ) = ( ( u ^ 2 ) mod P ) <-> m = u ) )
184 183 ex 
 |-  ( ph -> ( ( m e. ( 0 ... N ) /\ u e. ( 0 ... N ) ) -> ( ( ( m ^ 2 ) mod P ) = ( ( u ^ 2 ) mod P ) <-> m = u ) ) )
185 70 184 dom2lem 
 |-  ( ph -> ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-> ( 0 ... ( P - 1 ) ) )
186 f1f1orn 
 |-  ( ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-> ( 0 ... ( P - 1 ) ) -> ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-onto-> ran ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) )
187 185 186 syl 
 |-  ( ph -> ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-onto-> ran ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) )
188 eqid 
 |-  ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) = ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) )
189 188 rnmpt 
 |-  ran ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }
190 5 189 eqtr4i 
 |-  A = ran ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) )
191 f1oeq3 
 |-  ( A = ran ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) -> ( ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-onto-> A <-> ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-onto-> ran ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) ) )
192 190 191 ax-mp 
 |-  ( ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-onto-> A <-> ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-onto-> ran ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) )
193 187 192 sylibr 
 |-  ( ph -> ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-onto-> A )
194 ovex 
 |-  ( 0 ... N ) e. _V
195 194 f1oen 
 |-  ( ( m e. ( 0 ... N ) |-> ( ( m ^ 2 ) mod P ) ) : ( 0 ... N ) -1-1-onto-> A -> ( 0 ... N ) ~~ A )
196 193 195 syl 
 |-  ( ph -> ( 0 ... N ) ~~ A )
197 196 ensymd 
 |-  ( ph -> A ~~ ( 0 ... N ) )
198 ax-1cn 
 |-  1 e. CC
199 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
200 59 198 199 sylancl 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
201 200 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) )
202 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
203 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
204 202 203 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
205 204 nn0zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
206 fz01en 
 |-  ( ( N + 1 ) e. ZZ -> ( 0 ... ( ( N + 1 ) - 1 ) ) ~~ ( 1 ... ( N + 1 ) ) )
207 205 206 syl 
 |-  ( ph -> ( 0 ... ( ( N + 1 ) - 1 ) ) ~~ ( 1 ... ( N + 1 ) ) )
208 201 207 eqbrtrrd 
 |-  ( ph -> ( 0 ... N ) ~~ ( 1 ... ( N + 1 ) ) )
209 entr 
 |-  ( ( A ~~ ( 0 ... N ) /\ ( 0 ... N ) ~~ ( 1 ... ( N + 1 ) ) ) -> A ~~ ( 1 ... ( N + 1 ) ) )
210 197 208 209 syl2anc 
 |-  ( ph -> A ~~ ( 1 ... ( N + 1 ) ) )
211 7 19 ssfid 
 |-  ( ph -> A e. Fin )
212 fzfid 
 |-  ( ph -> ( 1 ... ( N + 1 ) ) e. Fin )
213 hashen 
 |-  ( ( A e. Fin /\ ( 1 ... ( N + 1 ) ) e. Fin ) -> ( ( # ` A ) = ( # ` ( 1 ... ( N + 1 ) ) ) <-> A ~~ ( 1 ... ( N + 1 ) ) ) )
214 211 212 213 syl2anc 
 |-  ( ph -> ( ( # ` A ) = ( # ` ( 1 ... ( N + 1 ) ) ) <-> A ~~ ( 1 ... ( N + 1 ) ) ) )
215 210 214 mpbird 
 |-  ( ph -> ( # ` A ) = ( # ` ( 1 ... ( N + 1 ) ) ) )
216 hashfz1 
 |-  ( ( N + 1 ) e. NN0 -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( N + 1 ) )
217 204 216 syl 
 |-  ( ph -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( N + 1 ) )
218 215 217 eqtrd 
 |-  ( ph -> ( # ` A ) = ( N + 1 ) )
219 31 ex 
 |-  ( ph -> ( v e. A -> ( ( P - 1 ) - v ) e. ( 0 ... ( P - 1 ) ) ) )
220 24 adantr 
 |-  ( ( ph /\ ( v e. A /\ k e. A ) ) -> ( P - 1 ) e. CC )
221 fzssuz 
 |-  ( 0 ... ( P - 1 ) ) C_ ( ZZ>= ` 0 )
222 uzssz 
 |-  ( ZZ>= ` 0 ) C_ ZZ
223 zsscn 
 |-  ZZ C_ CC
224 222 223 sstri 
 |-  ( ZZ>= ` 0 ) C_ CC
225 221 224 sstri 
 |-  ( 0 ... ( P - 1 ) ) C_ CC
226 19 225 sstrdi 
 |-  ( ph -> A C_ CC )
227 226 sselda 
 |-  ( ( ph /\ v e. A ) -> v e. CC )
228 227 adantrr 
 |-  ( ( ph /\ ( v e. A /\ k e. A ) ) -> v e. CC )
229 226 sselda 
 |-  ( ( ph /\ k e. A ) -> k e. CC )
230 229 adantrl 
 |-  ( ( ph /\ ( v e. A /\ k e. A ) ) -> k e. CC )
231 220 228 230 subcanad 
 |-  ( ( ph /\ ( v e. A /\ k e. A ) ) -> ( ( ( P - 1 ) - v ) = ( ( P - 1 ) - k ) <-> v = k ) )
232 231 ex 
 |-  ( ph -> ( ( v e. A /\ k e. A ) -> ( ( ( P - 1 ) - v ) = ( ( P - 1 ) - k ) <-> v = k ) ) )
233 219 232 dom2lem 
 |-  ( ph -> ( v e. A |-> ( ( P - 1 ) - v ) ) : A -1-1-> ( 0 ... ( P - 1 ) ) )
234 f1eq1 
 |-  ( F = ( v e. A |-> ( ( P - 1 ) - v ) ) -> ( F : A -1-1-> ( 0 ... ( P - 1 ) ) <-> ( v e. A |-> ( ( P - 1 ) - v ) ) : A -1-1-> ( 0 ... ( P - 1 ) ) ) )
235 6 234 ax-mp 
 |-  ( F : A -1-1-> ( 0 ... ( P - 1 ) ) <-> ( v e. A |-> ( ( P - 1 ) - v ) ) : A -1-1-> ( 0 ... ( P - 1 ) ) )
236 233 235 sylibr 
 |-  ( ph -> F : A -1-1-> ( 0 ... ( P - 1 ) ) )
237 f1f1orn 
 |-  ( F : A -1-1-> ( 0 ... ( P - 1 ) ) -> F : A -1-1-onto-> ran F )
238 236 237 syl 
 |-  ( ph -> F : A -1-1-onto-> ran F )
239 211 238 hasheqf1od 
 |-  ( ph -> ( # ` A ) = ( # ` ran F ) )
240 239 218 eqtr3d 
 |-  ( ph -> ( # ` ran F ) = ( N + 1 ) )
241 218 240 oveq12d 
 |-  ( ph -> ( ( # ` A ) + ( # ` ran F ) ) = ( ( N + 1 ) + ( N + 1 ) ) )
242 61 69 241 3eqtr4d 
 |-  ( ph -> ( P + 1 ) = ( ( # ` A ) + ( # ` ran F ) ) )
243 242 adantr 
 |-  ( ( ph /\ ( A i^i ran F ) = (/) ) -> ( P + 1 ) = ( ( # ` A ) + ( # ` ran F ) ) )
244 211 adantr 
 |-  ( ( ph /\ ( A i^i ran F ) = (/) ) -> A e. Fin )
245 7 33 ssfid 
 |-  ( ph -> ran F e. Fin )
246 245 adantr 
 |-  ( ( ph /\ ( A i^i ran F ) = (/) ) -> ran F e. Fin )
247 simpr 
 |-  ( ( ph /\ ( A i^i ran F ) = (/) ) -> ( A i^i ran F ) = (/) )
248 hashun 
 |-  ( ( A e. Fin /\ ran F e. Fin /\ ( A i^i ran F ) = (/) ) -> ( # ` ( A u. ran F ) ) = ( ( # ` A ) + ( # ` ran F ) ) )
249 244 246 247 248 syl3anc 
 |-  ( ( ph /\ ( A i^i ran F ) = (/) ) -> ( # ` ( A u. ran F ) ) = ( ( # ` A ) + ( # ` ran F ) ) )
250 243 249 eqtr4d 
 |-  ( ( ph /\ ( A i^i ran F ) = (/) ) -> ( P + 1 ) = ( # ` ( A u. ran F ) ) )
251 58 250 breqtrd 
 |-  ( ( ph /\ ( A i^i ran F ) = (/) ) -> P < ( # ` ( A u. ran F ) ) )
252 251 ex 
 |-  ( ph -> ( ( A i^i ran F ) = (/) -> P < ( # ` ( A u. ran F ) ) ) )
253 252 necon3bd 
 |-  ( ph -> ( -. P < ( # ` ( A u. ran F ) ) -> ( A i^i ran F ) =/= (/) ) )
254 56 253 mpd 
 |-  ( ph -> ( A i^i ran F ) =/= (/) )