Metamath Proof Explorer

Theorem gausslemma2dlem1a

Description: Lemma for gausslemma2dlem1 . (Contributed by AV, 1-Jul-2021)

Ref Expression
Hypotheses gausslemma2d.p 
|- ( ph -> P e. ( Prime \ { 2 } ) )
gausslemma2d.h 
|- H = ( ( P - 1 ) / 2 )
gausslemma2d.r 
|- R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )
Assertion gausslemma2dlem1a 
|- ( ph -> ran R = ( 1 ... H ) )

Proof

Step Hyp Ref Expression
1 gausslemma2d.p 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 gausslemma2d.h 
 |-  H = ( ( P - 1 ) / 2 )
3 gausslemma2d.r 
 |-  R = ( x e. ( 1 ... H ) |-> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )
4 3 elrnmpt 
 |-  ( y e. _V -> ( y e. ran R <-> E. x e. ( 1 ... H ) y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) ) )
5 4 elv 
 |-  ( y e. ran R <-> E. x e. ( 1 ... H ) y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )
6 iftrue 
 |-  ( ( x x. 2 ) < ( P / 2 ) -> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) = ( x x. 2 ) )
7 6 eqeq2d 
 |-  ( ( x x. 2 ) < ( P / 2 ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) <-> y = ( x x. 2 ) ) )
8 7 adantr 
 |-  ( ( ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) <-> y = ( x x. 2 ) ) )
9 elfz1b 
 |-  ( x e. ( 1 ... H ) <-> ( x e. NN /\ H e. NN /\ x <_ H ) )
10 id 
 |-  ( x e. NN -> x e. NN )
11 2nn 
 |-  2 e. NN
12 11 a1i 
 |-  ( x e. NN -> 2 e. NN )
13 10 12 nnmulcld 
 |-  ( x e. NN -> ( x x. 2 ) e. NN )
14 13 3ad2ant1 
 |-  ( ( x e. NN /\ H e. NN /\ x <_ H ) -> ( x x. 2 ) e. NN )
15 14 3ad2ant1 
 |-  ( ( ( x e. NN /\ H e. NN /\ x <_ H ) /\ ph /\ ( x x. 2 ) < ( P / 2 ) ) -> ( x x. 2 ) e. NN )
16 2 eleq1i 
 |-  ( H e. NN <-> ( ( P - 1 ) / 2 ) e. NN )
17 16 biimpi 
 |-  ( H e. NN -> ( ( P - 1 ) / 2 ) e. NN )
18 17 3ad2ant2 
 |-  ( ( x e. NN /\ H e. NN /\ x <_ H ) -> ( ( P - 1 ) / 2 ) e. NN )
19 18 3ad2ant1 
 |-  ( ( ( x e. NN /\ H e. NN /\ x <_ H ) /\ ph /\ ( x x. 2 ) < ( P / 2 ) ) -> ( ( P - 1 ) / 2 ) e. NN )
20 nnoddn2prm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. NN /\ -. 2 || P ) )
21 nnz 
 |-  ( P e. NN -> P e. ZZ )
22 21 anim1i 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( P e. ZZ /\ -. 2 || P ) )
23 20 22 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. ZZ /\ -. 2 || P ) )
24 nnz 
 |-  ( x e. NN -> x e. ZZ )
25 2z 
 |-  2 e. ZZ
26 25 a1i 
 |-  ( x e. NN -> 2 e. ZZ )
27 24 26 zmulcld 
 |-  ( x e. NN -> ( x x. 2 ) e. ZZ )
28 27 3ad2ant1 
 |-  ( ( x e. NN /\ H e. NN /\ x <_ H ) -> ( x x. 2 ) e. ZZ )
29 23 28 anim12i 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ ( x e. NN /\ H e. NN /\ x <_ H ) ) -> ( ( P e. ZZ /\ -. 2 || P ) /\ ( x x. 2 ) e. ZZ ) )
30 df-3an 
 |-  ( ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) <-> ( ( P e. ZZ /\ -. 2 || P ) /\ ( x x. 2 ) e. ZZ ) )
31 29 30 sylibr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ ( x e. NN /\ H e. NN /\ x <_ H ) ) -> ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) )
32 31 ex 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( x e. NN /\ H e. NN /\ x <_ H ) -> ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) ) )
33 1 32 syl 
 |-  ( ph -> ( ( x e. NN /\ H e. NN /\ x <_ H ) -> ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) ) )
34 33 impcom 
 |-  ( ( ( x e. NN /\ H e. NN /\ x <_ H ) /\ ph ) -> ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) )
35 ltoddhalfle 
 |-  ( ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) -> ( ( x x. 2 ) < ( P / 2 ) <-> ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) ) )
36 34 35 syl 
 |-  ( ( ( x e. NN /\ H e. NN /\ x <_ H ) /\ ph ) -> ( ( x x. 2 ) < ( P / 2 ) <-> ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) ) )
37 36 biimp3a 
 |-  ( ( ( x e. NN /\ H e. NN /\ x <_ H ) /\ ph /\ ( x x. 2 ) < ( P / 2 ) ) -> ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) )
38 15 19 37 3jca 
 |-  ( ( ( x e. NN /\ H e. NN /\ x <_ H ) /\ ph /\ ( x x. 2 ) < ( P / 2 ) ) -> ( ( x x. 2 ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) ) )
39 38 3exp 
 |-  ( ( x e. NN /\ H e. NN /\ x <_ H ) -> ( ph -> ( ( x x. 2 ) < ( P / 2 ) -> ( ( x x. 2 ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) ) ) ) )
40 9 39 sylbi 
 |-  ( x e. ( 1 ... H ) -> ( ph -> ( ( x x. 2 ) < ( P / 2 ) -> ( ( x x. 2 ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) ) ) ) )
41 40 impcom 
 |-  ( ( ph /\ x e. ( 1 ... H ) ) -> ( ( x x. 2 ) < ( P / 2 ) -> ( ( x x. 2 ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) ) ) )
42 41 impcom 
 |-  ( ( ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( ( x x. 2 ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) ) )
43 2 oveq2i 
 |-  ( 1 ... H ) = ( 1 ... ( ( P - 1 ) / 2 ) )
44 43 eleq2i 
 |-  ( ( x x. 2 ) e. ( 1 ... H ) <-> ( x x. 2 ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) )
45 elfz1b 
 |-  ( ( x x. 2 ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) <-> ( ( x x. 2 ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) ) )
46 44 45 bitri 
 |-  ( ( x x. 2 ) e. ( 1 ... H ) <-> ( ( x x. 2 ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( x x. 2 ) <_ ( ( P - 1 ) / 2 ) ) )
47 42 46 sylibr 
 |-  ( ( ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( x x. 2 ) e. ( 1 ... H ) )
48 eleq1 
 |-  ( y = ( x x. 2 ) -> ( y e. ( 1 ... H ) <-> ( x x. 2 ) e. ( 1 ... H ) ) )
49 47 48 syl5ibrcom 
 |-  ( ( ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( y = ( x x. 2 ) -> y e. ( 1 ... H ) ) )
50 8 49 sylbid 
 |-  ( ( ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) -> y e. ( 1 ... H ) ) )
51 iffalse 
 |-  ( -. ( x x. 2 ) < ( P / 2 ) -> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) = ( P - ( x x. 2 ) ) )
52 51 eqeq2d 
 |-  ( -. ( x x. 2 ) < ( P / 2 ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) <-> y = ( P - ( x x. 2 ) ) ) )
53 52 adantr 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) <-> y = ( P - ( x x. 2 ) ) ) )
54 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
55 prmz 
 |-  ( P e. Prime -> P e. ZZ )
56 1 54 55 3syl 
 |-  ( ph -> P e. ZZ )
57 56 ad2antrl 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> P e. ZZ )
58 elfzelz 
 |-  ( x e. ( 1 ... H ) -> x e. ZZ )
59 25 a1i 
 |-  ( x e. ( 1 ... H ) -> 2 e. ZZ )
60 58 59 zmulcld 
 |-  ( x e. ( 1 ... H ) -> ( x x. 2 ) e. ZZ )
61 60 ad2antll 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( x x. 2 ) e. ZZ )
62 57 61 zsubcld 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( P - ( x x. 2 ) ) e. ZZ )
63 55 zred 
 |-  ( P e. Prime -> P e. RR )
64 2 breq2i 
 |-  ( x <_ H <-> x <_ ( ( P - 1 ) / 2 ) )
65 nnre 
 |-  ( x e. NN -> x e. RR )
66 65 adantr 
 |-  ( ( x e. NN /\ P e. RR ) -> x e. RR )
67 peano2rem 
 |-  ( P e. RR -> ( P - 1 ) e. RR )
68 67 adantl 
 |-  ( ( x e. NN /\ P e. RR ) -> ( P - 1 ) e. RR )
69 2re 
 |-  2 e. RR
70 2pos 
 |-  0 < 2
71 69 70 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
72 71 a1i 
 |-  ( ( x e. NN /\ P e. RR ) -> ( 2 e. RR /\ 0 < 2 ) )
73 lemuldiv 
 |-  ( ( x e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( x x. 2 ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
74 66 68 72 73 syl3anc 
 |-  ( ( x e. NN /\ P e. RR ) -> ( ( x x. 2 ) <_ ( P - 1 ) <-> x <_ ( ( P - 1 ) / 2 ) ) )
75 64 74 bitr4id 
 |-  ( ( x e. NN /\ P e. RR ) -> ( x <_ H <-> ( x x. 2 ) <_ ( P - 1 ) ) )
76 13 nnred 
 |-  ( x e. NN -> ( x x. 2 ) e. RR )
77 76 adantr 
 |-  ( ( x e. NN /\ P e. RR ) -> ( x x. 2 ) e. RR )
78 simpr 
 |-  ( ( x e. NN /\ P e. RR ) -> P e. RR )
79 77 68 78 lesub2d 
 |-  ( ( x e. NN /\ P e. RR ) -> ( ( x x. 2 ) <_ ( P - 1 ) <-> ( P - ( P - 1 ) ) <_ ( P - ( x x. 2 ) ) ) )
80 recn 
 |-  ( P e. RR -> P e. CC )
81 1cnd 
 |-  ( P e. RR -> 1 e. CC )
82 80 81 nncand 
 |-  ( P e. RR -> ( P - ( P - 1 ) ) = 1 )
83 82 adantl 
 |-  ( ( x e. NN /\ P e. RR ) -> ( P - ( P - 1 ) ) = 1 )
84 83 breq1d 
 |-  ( ( x e. NN /\ P e. RR ) -> ( ( P - ( P - 1 ) ) <_ ( P - ( x x. 2 ) ) <-> 1 <_ ( P - ( x x. 2 ) ) ) )
85 84 biimpd 
 |-  ( ( x e. NN /\ P e. RR ) -> ( ( P - ( P - 1 ) ) <_ ( P - ( x x. 2 ) ) -> 1 <_ ( P - ( x x. 2 ) ) ) )
86 79 85 sylbid 
 |-  ( ( x e. NN /\ P e. RR ) -> ( ( x x. 2 ) <_ ( P - 1 ) -> 1 <_ ( P - ( x x. 2 ) ) ) )
87 75 86 sylbid 
 |-  ( ( x e. NN /\ P e. RR ) -> ( x <_ H -> 1 <_ ( P - ( x x. 2 ) ) ) )
88 87 impancom 
 |-  ( ( x e. NN /\ x <_ H ) -> ( P e. RR -> 1 <_ ( P - ( x x. 2 ) ) ) )
89 88 3adant2 
 |-  ( ( x e. NN /\ H e. NN /\ x <_ H ) -> ( P e. RR -> 1 <_ ( P - ( x x. 2 ) ) ) )
90 9 89 sylbi 
 |-  ( x e. ( 1 ... H ) -> ( P e. RR -> 1 <_ ( P - ( x x. 2 ) ) ) )
91 90 com12 
 |-  ( P e. RR -> ( x e. ( 1 ... H ) -> 1 <_ ( P - ( x x. 2 ) ) ) )
92 63 91 syl 
 |-  ( P e. Prime -> ( x e. ( 1 ... H ) -> 1 <_ ( P - ( x x. 2 ) ) ) )
93 1 54 92 3syl 
 |-  ( ph -> ( x e. ( 1 ... H ) -> 1 <_ ( P - ( x x. 2 ) ) ) )
94 93 imp 
 |-  ( ( ph /\ x e. ( 1 ... H ) ) -> 1 <_ ( P - ( x x. 2 ) ) )
95 94 adantl 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> 1 <_ ( P - ( x x. 2 ) ) )
96 elnnz1 
 |-  ( ( P - ( x x. 2 ) ) e. NN <-> ( ( P - ( x x. 2 ) ) e. ZZ /\ 1 <_ ( P - ( x x. 2 ) ) ) )
97 62 95 96 sylanbrc 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( P - ( x x. 2 ) ) e. NN )
98 9 simp2bi 
 |-  ( x e. ( 1 ... H ) -> H e. NN )
99 98 ad2antll 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> H e. NN )
100 nnre 
 |-  ( P e. NN -> P e. RR )
101 100 rehalfcld 
 |-  ( P e. NN -> ( P / 2 ) e. RR )
102 101 adantr 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( P / 2 ) e. RR )
103 60 zred 
 |-  ( x e. ( 1 ... H ) -> ( x x. 2 ) e. RR )
104 lenlt 
 |-  ( ( ( P / 2 ) e. RR /\ ( x x. 2 ) e. RR ) -> ( ( P / 2 ) <_ ( x x. 2 ) <-> -. ( x x. 2 ) < ( P / 2 ) ) )
105 102 103 104 syl2an 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P / 2 ) <_ ( x x. 2 ) <-> -. ( x x. 2 ) < ( P / 2 ) ) )
106 22 60 anim12i 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P e. ZZ /\ -. 2 || P ) /\ ( x x. 2 ) e. ZZ ) )
107 106 30 sylibr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) )
108 halfleoddlt 
 |-  ( ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) -> ( ( P / 2 ) <_ ( x x. 2 ) <-> ( P / 2 ) < ( x x. 2 ) ) )
109 107 108 syl 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P / 2 ) <_ ( x x. 2 ) <-> ( P / 2 ) < ( x x. 2 ) ) )
110 109 biimpa 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P / 2 ) < ( x x. 2 ) )
111 nncn 
 |-  ( P e. NN -> P e. CC )
112 subhalfhalf 
 |-  ( P e. CC -> ( P - ( P / 2 ) ) = ( P / 2 ) )
113 111 112 syl 
 |-  ( P e. NN -> ( P - ( P / 2 ) ) = ( P / 2 ) )
114 113 breq1d 
 |-  ( P e. NN -> ( ( P - ( P / 2 ) ) < ( x x. 2 ) <-> ( P / 2 ) < ( x x. 2 ) ) )
115 114 ad3antrrr 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( ( P - ( P / 2 ) ) < ( x x. 2 ) <-> ( P / 2 ) < ( x x. 2 ) ) )
116 110 115 mpbird 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P - ( P / 2 ) ) < ( x x. 2 ) )
117 100 ad2antrr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> P e. RR )
118 101 ad2antrr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P / 2 ) e. RR )
119 103 adantl 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( x x. 2 ) e. RR )
120 117 118 119 3jca 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P e. RR /\ ( P / 2 ) e. RR /\ ( x x. 2 ) e. RR ) )
121 120 adantr 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P e. RR /\ ( P / 2 ) e. RR /\ ( x x. 2 ) e. RR ) )
122 ltsub23 
 |-  ( ( P e. RR /\ ( P / 2 ) e. RR /\ ( x x. 2 ) e. RR ) -> ( ( P - ( P / 2 ) ) < ( x x. 2 ) <-> ( P - ( x x. 2 ) ) < ( P / 2 ) ) )
123 121 122 syl 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( ( P - ( P / 2 ) ) < ( x x. 2 ) <-> ( P - ( x x. 2 ) ) < ( P / 2 ) ) )
124 116 123 mpbid 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P - ( x x. 2 ) ) < ( P / 2 ) )
125 21 ad2antrr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> P e. ZZ )
126 simplr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> -. 2 || P )
127 60 adantl 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( x x. 2 ) e. ZZ )
128 125 127 zsubcld 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P - ( x x. 2 ) ) e. ZZ )
129 125 126 128 3jca 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P e. ZZ /\ -. 2 || P /\ ( P - ( x x. 2 ) ) e. ZZ ) )
130 129 adantr 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P e. ZZ /\ -. 2 || P /\ ( P - ( x x. 2 ) ) e. ZZ ) )
131 ltoddhalfle 
 |-  ( ( P e. ZZ /\ -. 2 || P /\ ( P - ( x x. 2 ) ) e. ZZ ) -> ( ( P - ( x x. 2 ) ) < ( P / 2 ) <-> ( P - ( x x. 2 ) ) <_ ( ( P - 1 ) / 2 ) ) )
132 130 131 syl 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( ( P - ( x x. 2 ) ) < ( P / 2 ) <-> ( P - ( x x. 2 ) ) <_ ( ( P - 1 ) / 2 ) ) )
133 124 132 mpbid 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P - ( x x. 2 ) ) <_ ( ( P - 1 ) / 2 ) )
134 133 ex 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P / 2 ) <_ ( x x. 2 ) -> ( P - ( x x. 2 ) ) <_ ( ( P - 1 ) / 2 ) ) )
135 2 breq2i 
 |-  ( ( P - ( x x. 2 ) ) <_ H <-> ( P - ( x x. 2 ) ) <_ ( ( P - 1 ) / 2 ) )
136 134 135 syl6ibr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P / 2 ) <_ ( x x. 2 ) -> ( P - ( x x. 2 ) ) <_ H ) )
137 105 136 sylbird 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( -. ( x x. 2 ) < ( P / 2 ) -> ( P - ( x x. 2 ) ) <_ H ) )
138 137 ex 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( x e. ( 1 ... H ) -> ( -. ( x x. 2 ) < ( P / 2 ) -> ( P - ( x x. 2 ) ) <_ H ) ) )
139 1 20 138 3syl 
 |-  ( ph -> ( x e. ( 1 ... H ) -> ( -. ( x x. 2 ) < ( P / 2 ) -> ( P - ( x x. 2 ) ) <_ H ) ) )
140 139 imp 
 |-  ( ( ph /\ x e. ( 1 ... H ) ) -> ( -. ( x x. 2 ) < ( P / 2 ) -> ( P - ( x x. 2 ) ) <_ H ) )
141 140 impcom 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( P - ( x x. 2 ) ) <_ H )
142 elfz1b 
 |-  ( ( P - ( x x. 2 ) ) e. ( 1 ... H ) <-> ( ( P - ( x x. 2 ) ) e. NN /\ H e. NN /\ ( P - ( x x. 2 ) ) <_ H ) )
143 97 99 141 142 syl3anbrc 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( P - ( x x. 2 ) ) e. ( 1 ... H ) )
144 eleq1 
 |-  ( y = ( P - ( x x. 2 ) ) -> ( y e. ( 1 ... H ) <-> ( P - ( x x. 2 ) ) e. ( 1 ... H ) ) )
145 143 144 syl5ibrcom 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( y = ( P - ( x x. 2 ) ) -> y e. ( 1 ... H ) ) )
146 53 145 sylbid 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) -> y e. ( 1 ... H ) ) )
147 50 146 pm2.61ian 
 |-  ( ( ph /\ x e. ( 1 ... H ) ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) -> y e. ( 1 ... H ) ) )
148 147 rexlimdva 
 |-  ( ph -> ( E. x e. ( 1 ... H ) y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) -> y e. ( 1 ... H ) ) )
149 elfz1b 
 |-  ( y e. ( 1 ... H ) <-> ( y e. NN /\ H e. NN /\ y <_ H ) )
150 simp1 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> y e. NN )
151 simpl 
 |-  ( ( 2 || y /\ ph ) -> 2 || y )
152 nnehalf 
 |-  ( ( y e. NN /\ 2 || y ) -> ( y / 2 ) e. NN )
153 150 151 152 syl2anr 
 |-  ( ( ( 2 || y /\ ph ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( y / 2 ) e. NN )
154 simpr2 
 |-  ( ( ( 2 || y /\ ph ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> H e. NN )
155 nnre 
 |-  ( y e. NN -> y e. RR )
156 155 ad2antrr 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( 2 || y /\ ph ) ) -> y e. RR )
157 nnrp 
 |-  ( H e. NN -> H e. RR+ )
158 157 adantl 
 |-  ( ( y e. NN /\ H e. NN ) -> H e. RR+ )
159 158 adantr 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( 2 || y /\ ph ) ) -> H e. RR+ )
160 2rp 
 |-  2 e. RR+
161 1le2 
 |-  1 <_ 2
162 160 161 pm3.2i 
 |-  ( 2 e. RR+ /\ 1 <_ 2 )
163 162 a1i 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( 2 || y /\ ph ) ) -> ( 2 e. RR+ /\ 1 <_ 2 ) )
164 ledivge1le 
 |-  ( ( y e. RR /\ H e. RR+ /\ ( 2 e. RR+ /\ 1 <_ 2 ) ) -> ( y <_ H -> ( y / 2 ) <_ H ) )
165 156 159 163 164 syl3anc 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( 2 || y /\ ph ) ) -> ( y <_ H -> ( y / 2 ) <_ H ) )
166 165 ex 
 |-  ( ( y e. NN /\ H e. NN ) -> ( ( 2 || y /\ ph ) -> ( y <_ H -> ( y / 2 ) <_ H ) ) )
167 166 com23 
 |-  ( ( y e. NN /\ H e. NN ) -> ( y <_ H -> ( ( 2 || y /\ ph ) -> ( y / 2 ) <_ H ) ) )
168 167 3impia 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( 2 || y /\ ph ) -> ( y / 2 ) <_ H ) )
169 168 impcom 
 |-  ( ( ( 2 || y /\ ph ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( y / 2 ) <_ H )
170 153 154 169 3jca 
 |-  ( ( ( 2 || y /\ ph ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) )
171 170 ex 
 |-  ( ( 2 || y /\ ph ) -> ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) ) )
172 149 171 syl5bi 
 |-  ( ( 2 || y /\ ph ) -> ( y e. ( 1 ... H ) -> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) ) )
173 172 3impia 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) )
174 elfz1b 
 |-  ( ( y / 2 ) e. ( 1 ... H ) <-> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) )
175 173 174 sylibr 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( y / 2 ) e. ( 1 ... H ) )
176 oveq1 
 |-  ( x = ( y / 2 ) -> ( x x. 2 ) = ( ( y / 2 ) x. 2 ) )
177 176 breq1d 
 |-  ( x = ( y / 2 ) -> ( ( x x. 2 ) < ( P / 2 ) <-> ( ( y / 2 ) x. 2 ) < ( P / 2 ) ) )
178 176 oveq2d 
 |-  ( x = ( y / 2 ) -> ( P - ( x x. 2 ) ) = ( P - ( ( y / 2 ) x. 2 ) ) )
179 177 176 178 ifbieq12d 
 |-  ( x = ( y / 2 ) -> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) = if ( ( ( y / 2 ) x. 2 ) < ( P / 2 ) , ( ( y / 2 ) x. 2 ) , ( P - ( ( y / 2 ) x. 2 ) ) ) )
180 179 eqeq2d 
 |-  ( x = ( y / 2 ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) <-> y = if ( ( ( y / 2 ) x. 2 ) < ( P / 2 ) , ( ( y / 2 ) x. 2 ) , ( P - ( ( y / 2 ) x. 2 ) ) ) ) )
181 180 adantl 
 |-  ( ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) /\ x = ( y / 2 ) ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) <-> y = if ( ( ( y / 2 ) x. 2 ) < ( P / 2 ) , ( ( y / 2 ) x. 2 ) , ( P - ( ( y / 2 ) x. 2 ) ) ) ) )
182 elfzelz 
 |-  ( y e. ( 1 ... H ) -> y e. ZZ )
183 182 zcnd 
 |-  ( y e. ( 1 ... H ) -> y e. CC )
184 183 3ad2ant3 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> y e. CC )
185 2cnd 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> 2 e. CC )
186 2ne0 
 |-  2 =/= 0
187 186 a1i 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> 2 =/= 0 )
188 184 185 187 divcan1d 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( y / 2 ) x. 2 ) = y )
189 2 breq2i 
 |-  ( y <_ H <-> y <_ ( ( P - 1 ) / 2 ) )
190 nnz 
 |-  ( y e. NN -> y e. ZZ )
191 1 20 22 3syl 
 |-  ( ph -> ( P e. ZZ /\ -. 2 || P ) )
192 191 adantl 
 |-  ( ( 2 || y /\ ph ) -> ( P e. ZZ /\ -. 2 || P ) )
193 190 192 anim12ci 
 |-  ( ( y e. NN /\ ( 2 || y /\ ph ) ) -> ( ( P e. ZZ /\ -. 2 || P ) /\ y e. ZZ ) )
194 df-3an 
 |-  ( ( P e. ZZ /\ -. 2 || P /\ y e. ZZ ) <-> ( ( P e. ZZ /\ -. 2 || P ) /\ y e. ZZ ) )
195 193 194 sylibr 
 |-  ( ( y e. NN /\ ( 2 || y /\ ph ) ) -> ( P e. ZZ /\ -. 2 || P /\ y e. ZZ ) )
196 ltoddhalfle 
 |-  ( ( P e. ZZ /\ -. 2 || P /\ y e. ZZ ) -> ( y < ( P / 2 ) <-> y <_ ( ( P - 1 ) / 2 ) ) )
197 195 196 syl 
 |-  ( ( y e. NN /\ ( 2 || y /\ ph ) ) -> ( y < ( P / 2 ) <-> y <_ ( ( P - 1 ) / 2 ) ) )
198 197 exbiri 
 |-  ( y e. NN -> ( ( 2 || y /\ ph ) -> ( y <_ ( ( P - 1 ) / 2 ) -> y < ( P / 2 ) ) ) )
199 198 com23 
 |-  ( y e. NN -> ( y <_ ( ( P - 1 ) / 2 ) -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) ) )
200 189 199 syl5bi 
 |-  ( y e. NN -> ( y <_ H -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) ) )
201 200 a1d 
 |-  ( y e. NN -> ( H e. NN -> ( y <_ H -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) ) ) )
202 201 3imp 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) )
203 149 202 sylbi 
 |-  ( y e. ( 1 ... H ) -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) )
204 203 com12 
 |-  ( ( 2 || y /\ ph ) -> ( y e. ( 1 ... H ) -> y < ( P / 2 ) ) )
205 204 3impia 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> y < ( P / 2 ) )
206 188 205 eqbrtrd 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( y / 2 ) x. 2 ) < ( P / 2 ) )
207 206 iftrued 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> if ( ( ( y / 2 ) x. 2 ) < ( P / 2 ) , ( ( y / 2 ) x. 2 ) , ( P - ( ( y / 2 ) x. 2 ) ) ) = ( ( y / 2 ) x. 2 ) )
208 207 188 eqtr2d 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> y = if ( ( ( y / 2 ) x. 2 ) < ( P / 2 ) , ( ( y / 2 ) x. 2 ) , ( P - ( ( y / 2 ) x. 2 ) ) ) )
209 175 181 208 rspcedvd 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> E. x e. ( 1 ... H ) y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )
210 209 3exp 
 |-  ( 2 || y -> ( ph -> ( y e. ( 1 ... H ) -> E. x e. ( 1 ... H ) y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) ) ) )
211 54 55 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ZZ )
212 211 ad2antrr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> P e. ZZ )
213 190 3ad2ant1 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> y e. ZZ )
214 213 adantl 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> y e. ZZ )
215 212 214 zsubcld 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - y ) e. ZZ )
216 155 ad2antrl 
 |-  ( ( P e. RR /\ ( y e. NN /\ H e. NN ) ) -> y e. RR )
217 67 rehalfcld 
 |-  ( P e. RR -> ( ( P - 1 ) / 2 ) e. RR )
218 217 adantr 
 |-  ( ( P e. RR /\ ( y e. NN /\ H e. NN ) ) -> ( ( P - 1 ) / 2 ) e. RR )
219 simpl 
 |-  ( ( P e. RR /\ ( y e. NN /\ H e. NN ) ) -> P e. RR )
220 216 218 219 3jca 
 |-  ( ( P e. RR /\ ( y e. NN /\ H e. NN ) ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) )
221 220 ex 
 |-  ( P e. RR -> ( ( y e. NN /\ H e. NN ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) ) )
222 54 63 221 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( y e. NN /\ H e. NN ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) ) )
223 222 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( ( y e. NN /\ H e. NN ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) ) )
224 223 impcom 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) )
225 lesub2 
 |-  ( ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) -> ( y <_ ( ( P - 1 ) / 2 ) <-> ( P - ( ( P - 1 ) / 2 ) ) <_ ( P - y ) ) )
226 224 225 syl 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( y <_ ( ( P - 1 ) / 2 ) <-> ( P - ( ( P - 1 ) / 2 ) ) <_ ( P - y ) ) )
227 55 zcnd 
 |-  ( P e. Prime -> P e. CC )
228 1cnd 
 |-  ( P e. CC -> 1 e. CC )
229 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
230 229 a1i 
 |-  ( P e. CC -> ( 2 e. CC /\ 2 =/= 0 ) )
231 divsubdir 
 |-  ( ( P e. CC /\ 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( P - 1 ) / 2 ) = ( ( P / 2 ) - ( 1 / 2 ) ) )
232 228 230 231 mpd3an23 
 |-  ( P e. CC -> ( ( P - 1 ) / 2 ) = ( ( P / 2 ) - ( 1 / 2 ) ) )
233 232 oveq2d 
 |-  ( P e. CC -> ( P - ( ( P - 1 ) / 2 ) ) = ( P - ( ( P / 2 ) - ( 1 / 2 ) ) ) )
234 id 
 |-  ( P e. CC -> P e. CC )
235 halfcl 
 |-  ( P e. CC -> ( P / 2 ) e. CC )
236 halfcn 
 |-  ( 1 / 2 ) e. CC
237 236 a1i 
 |-  ( P e. CC -> ( 1 / 2 ) e. CC )
238 234 235 237 subsubd 
 |-  ( P e. CC -> ( P - ( ( P / 2 ) - ( 1 / 2 ) ) ) = ( ( P - ( P / 2 ) ) + ( 1 / 2 ) ) )
239 112 oveq1d 
 |-  ( P e. CC -> ( ( P - ( P / 2 ) ) + ( 1 / 2 ) ) = ( ( P / 2 ) + ( 1 / 2 ) ) )
240 233 238 239 3eqtrd 
 |-  ( P e. CC -> ( P - ( ( P - 1 ) / 2 ) ) = ( ( P / 2 ) + ( 1 / 2 ) ) )
241 54 227 240 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P - ( ( P - 1 ) / 2 ) ) = ( ( P / 2 ) + ( 1 / 2 ) ) )
242 241 ad2antrl 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( P - ( ( P - 1 ) / 2 ) ) = ( ( P / 2 ) + ( 1 / 2 ) ) )
243 242 breq1d 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( ( P - ( ( P - 1 ) / 2 ) ) <_ ( P - y ) <-> ( ( P / 2 ) + ( 1 / 2 ) ) <_ ( P - y ) ) )
244 prmnn 
 |-  ( P e. Prime -> P e. NN )
245 halfre 
 |-  ( 1 / 2 ) e. RR
246 245 a1i 
 |-  ( P e. NN -> ( 1 / 2 ) e. RR )
247 nngt0 
 |-  ( P e. NN -> 0 < P )
248 71 a1i 
 |-  ( P e. NN -> ( 2 e. RR /\ 0 < 2 ) )
249 divgt0 
 |-  ( ( ( P e. RR /\ 0 < P ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 < ( P / 2 ) )
250 100 247 248 249 syl21anc 
 |-  ( P e. NN -> 0 < ( P / 2 ) )
251 halfgt0 
 |-  0 < ( 1 / 2 )
252 251 a1i 
 |-  ( P e. NN -> 0 < ( 1 / 2 ) )
253 101 246 250 252 addgt0d 
 |-  ( P e. NN -> 0 < ( ( P / 2 ) + ( 1 / 2 ) ) )
254 54 244 253 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> 0 < ( ( P / 2 ) + ( 1 / 2 ) ) )
255 254 ad2antrl 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> 0 < ( ( P / 2 ) + ( 1 / 2 ) ) )
256 0red 
 |-  ( ( y e. RR /\ P e. RR ) -> 0 e. RR )
257 simpr 
 |-  ( ( y e. RR /\ P e. RR ) -> P e. RR )
258 257 rehalfcld 
 |-  ( ( y e. RR /\ P e. RR ) -> ( P / 2 ) e. RR )
259 245 a1i 
 |-  ( ( y e. RR /\ P e. RR ) -> ( 1 / 2 ) e. RR )
260 258 259 readdcld 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) + ( 1 / 2 ) ) e. RR )
261 resubcl 
 |-  ( ( P e. RR /\ y e. RR ) -> ( P - y ) e. RR )
262 261 ancoms 
 |-  ( ( y e. RR /\ P e. RR ) -> ( P - y ) e. RR )
263 256 260 262 3jca 
 |-  ( ( y e. RR /\ P e. RR ) -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) )
264 263 ex 
 |-  ( y e. RR -> ( P e. RR -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
265 155 264 syl 
 |-  ( y e. NN -> ( P e. RR -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
266 265 adantr 
 |-  ( ( y e. NN /\ H e. NN ) -> ( P e. RR -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
267 266 com12 
 |-  ( P e. RR -> ( ( y e. NN /\ H e. NN ) -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
268 54 63 267 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( y e. NN /\ H e. NN ) -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
269 268 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( ( y e. NN /\ H e. NN ) -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
270 269 impcom 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) )
271 ltletr 
 |-  ( ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) -> ( ( 0 < ( ( P / 2 ) + ( 1 / 2 ) ) /\ ( ( P / 2 ) + ( 1 / 2 ) ) <_ ( P - y ) ) -> 0 < ( P - y ) ) )
272 270 271 syl 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( ( 0 < ( ( P / 2 ) + ( 1 / 2 ) ) /\ ( ( P / 2 ) + ( 1 / 2 ) ) <_ ( P - y ) ) -> 0 < ( P - y ) ) )
273 255 272 mpand 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( ( ( P / 2 ) + ( 1 / 2 ) ) <_ ( P - y ) -> 0 < ( P - y ) ) )
274 243 273 sylbid 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( ( P - ( ( P - 1 ) / 2 ) ) <_ ( P - y ) -> 0 < ( P - y ) ) )
275 226 274 sylbid 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( y <_ ( ( P - 1 ) / 2 ) -> 0 < ( P - y ) ) )
276 275 ex 
 |-  ( ( y e. NN /\ H e. NN ) -> ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( y <_ ( ( P - 1 ) / 2 ) -> 0 < ( P - y ) ) ) )
277 276 com23 
 |-  ( ( y e. NN /\ H e. NN ) -> ( y <_ ( ( P - 1 ) / 2 ) -> ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> 0 < ( P - y ) ) ) )
278 189 277 syl5bi 
 |-  ( ( y e. NN /\ H e. NN ) -> ( y <_ H -> ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> 0 < ( P - y ) ) ) )
279 278 3impia 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> 0 < ( P - y ) ) )
280 279 impcom 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> 0 < ( P - y ) )
281 elnnz 
 |-  ( ( P - y ) e. NN <-> ( ( P - y ) e. ZZ /\ 0 < ( P - y ) ) )
282 215 280 281 sylanbrc 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - y ) e. NN )
283 23 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( P e. ZZ /\ -. 2 || P ) )
284 simpr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> -. 2 || y )
285 284 213 anim12ci 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( y e. ZZ /\ -. 2 || y ) )
286 omoe 
 |-  ( ( ( P e. ZZ /\ -. 2 || P ) /\ ( y e. ZZ /\ -. 2 || y ) ) -> 2 || ( P - y ) )
287 283 285 286 syl2an2r 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> 2 || ( P - y ) )
288 nnehalf 
 |-  ( ( ( P - y ) e. NN /\ 2 || ( P - y ) ) -> ( ( P - y ) / 2 ) e. NN )
289 282 287 288 syl2anc 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( P - y ) / 2 ) e. NN )
290 simpr2 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> H e. NN )
291 1red 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> 1 e. RR )
292 155 3ad2ant1 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> y e. RR )
293 292 adantl 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> y e. RR )
294 54 63 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. RR )
295 294 ad2antrr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> P e. RR )
296 nnge1 
 |-  ( y e. NN -> 1 <_ y )
297 296 3ad2ant1 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> 1 <_ y )
298 297 adantl 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> 1 <_ y )
299 291 293 295 298 lesub2dd 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - y ) <_ ( P - 1 ) )
300 295 293 resubcld 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - y ) e. RR )
301 54 63 67 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P - 1 ) e. RR )
302 301 ad2antrr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - 1 ) e. RR )
303 71 a1i 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( 2 e. RR /\ 0 < 2 ) )
304 lediv1 
 |-  ( ( ( P - y ) e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( P - y ) <_ ( P - 1 ) <-> ( ( P - y ) / 2 ) <_ ( ( P - 1 ) / 2 ) ) )
305 300 302 303 304 syl3anc 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( P - y ) <_ ( P - 1 ) <-> ( ( P - y ) / 2 ) <_ ( ( P - 1 ) / 2 ) ) )
306 299 305 mpbid 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( P - y ) / 2 ) <_ ( ( P - 1 ) / 2 ) )
307 2 breq2i 
 |-  ( ( ( P - y ) / 2 ) <_ H <-> ( ( P - y ) / 2 ) <_ ( ( P - 1 ) / 2 ) )
308 306 307 sylibr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( P - y ) / 2 ) <_ H )
309 289 290 308 3jca 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( ( P - y ) / 2 ) e. NN /\ H e. NN /\ ( ( P - y ) / 2 ) <_ H ) )
310 309 ex 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( ( P - y ) / 2 ) e. NN /\ H e. NN /\ ( ( P - y ) / 2 ) <_ H ) ) )
311 elfz1b 
 |-  ( ( ( P - y ) / 2 ) e. ( 1 ... H ) <-> ( ( ( P - y ) / 2 ) e. NN /\ H e. NN /\ ( ( P - y ) / 2 ) <_ H ) )
312 310 149 311 3imtr4g 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( y e. ( 1 ... H ) -> ( ( P - y ) / 2 ) e. ( 1 ... H ) ) )
313 312 ex 
 |-  ( P e. ( Prime \ { 2 } ) -> ( -. 2 || y -> ( y e. ( 1 ... H ) -> ( ( P - y ) / 2 ) e. ( 1 ... H ) ) ) )
314 1 313 syl 
 |-  ( ph -> ( -. 2 || y -> ( y e. ( 1 ... H ) -> ( ( P - y ) / 2 ) e. ( 1 ... H ) ) ) )
315 314 3imp21 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( P - y ) / 2 ) e. ( 1 ... H ) )
316 oveq1 
 |-  ( x = ( ( P - y ) / 2 ) -> ( x x. 2 ) = ( ( ( P - y ) / 2 ) x. 2 ) )
317 316 breq1d 
 |-  ( x = ( ( P - y ) / 2 ) -> ( ( x x. 2 ) < ( P / 2 ) <-> ( ( ( P - y ) / 2 ) x. 2 ) < ( P / 2 ) ) )
318 316 oveq2d 
 |-  ( x = ( ( P - y ) / 2 ) -> ( P - ( x x. 2 ) ) = ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) )
319 317 316 318 ifbieq12d 
 |-  ( x = ( ( P - y ) / 2 ) -> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) = if ( ( ( ( P - y ) / 2 ) x. 2 ) < ( P / 2 ) , ( ( ( P - y ) / 2 ) x. 2 ) , ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) ) )
320 319 eqeq2d 
 |-  ( x = ( ( P - y ) / 2 ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) <-> y = if ( ( ( ( P - y ) / 2 ) x. 2 ) < ( P / 2 ) , ( ( ( P - y ) / 2 ) x. 2 ) , ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) ) ) )
321 320 adantl 
 |-  ( ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) /\ x = ( ( P - y ) / 2 ) ) -> ( y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) <-> y = if ( ( ( ( P - y ) / 2 ) x. 2 ) < ( P / 2 ) , ( ( ( P - y ) / 2 ) x. 2 ) , ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) ) ) )
322 1 54 227 3syl 
 |-  ( ph -> P e. CC )
323 322 3ad2ant2 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> P e. CC )
324 183 3ad2ant3 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> y e. CC )
325 323 324 subcld 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( P - y ) e. CC )
326 2cnd 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> 2 e. CC )
327 186 a1i 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> 2 =/= 0 )
328 325 326 327 divcan1d 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( ( P - y ) / 2 ) x. 2 ) = ( P - y ) )
329 zre 
 |-  ( P e. ZZ -> P e. RR )
330 halfge0 
 |-  0 <_ ( 1 / 2 )
331 rehalfcl 
 |-  ( P e. RR -> ( P / 2 ) e. RR )
332 331 adantl 
 |-  ( ( y e. RR /\ P e. RR ) -> ( P / 2 ) e. RR )
333 332 259 subge02d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( 0 <_ ( 1 / 2 ) <-> ( ( P / 2 ) - ( 1 / 2 ) ) <_ ( P / 2 ) ) )
334 330 333 mpbii 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) - ( 1 / 2 ) ) <_ ( P / 2 ) )
335 simpl 
 |-  ( ( y e. RR /\ P e. RR ) -> y e. RR )
336 245 a1i 
 |-  ( P e. RR -> ( 1 / 2 ) e. RR )
337 331 336 resubcld 
 |-  ( P e. RR -> ( ( P / 2 ) - ( 1 / 2 ) ) e. RR )
338 337 adantl 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) - ( 1 / 2 ) ) e. RR )
339 letr 
 |-  ( ( y e. RR /\ ( ( P / 2 ) - ( 1 / 2 ) ) e. RR /\ ( P / 2 ) e. RR ) -> ( ( y <_ ( ( P / 2 ) - ( 1 / 2 ) ) /\ ( ( P / 2 ) - ( 1 / 2 ) ) <_ ( P / 2 ) ) -> y <_ ( P / 2 ) ) )
340 335 338 332 339 syl3anc 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( y <_ ( ( P / 2 ) - ( 1 / 2 ) ) /\ ( ( P / 2 ) - ( 1 / 2 ) ) <_ ( P / 2 ) ) -> y <_ ( P / 2 ) ) )
341 334 340 mpan2d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( y <_ ( ( P / 2 ) - ( 1 / 2 ) ) -> y <_ ( P / 2 ) ) )
342 80 adantl 
 |-  ( ( y e. RR /\ P e. RR ) -> P e. CC )
343 1cnd 
 |-  ( ( y e. RR /\ P e. RR ) -> 1 e. CC )
344 229 a1i 
 |-  ( ( y e. RR /\ P e. RR ) -> ( 2 e. CC /\ 2 =/= 0 ) )
345 342 343 344 231 syl3anc 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P - 1 ) / 2 ) = ( ( P / 2 ) - ( 1 / 2 ) ) )
346 345 breq2d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( y <_ ( ( P - 1 ) / 2 ) <-> y <_ ( ( P / 2 ) - ( 1 / 2 ) ) ) )
347 lesub 
 |-  ( ( ( P / 2 ) e. RR /\ P e. RR /\ y e. RR ) -> ( ( P / 2 ) <_ ( P - y ) <-> y <_ ( P - ( P / 2 ) ) ) )
348 332 257 335 347 syl3anc 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) <_ ( P - y ) <-> y <_ ( P - ( P / 2 ) ) ) )
349 258 262 lenltd 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) <_ ( P - y ) <-> -. ( P - y ) < ( P / 2 ) ) )
350 2cnd 
 |-  ( P e. RR -> 2 e. CC )
351 186 a1i 
 |-  ( P e. RR -> 2 =/= 0 )
352 80 350 351 divcan1d 
 |-  ( P e. RR -> ( ( P / 2 ) x. 2 ) = P )
353 352 eqcomd 
 |-  ( P e. RR -> P = ( ( P / 2 ) x. 2 ) )
354 353 oveq1d 
 |-  ( P e. RR -> ( P - ( P / 2 ) ) = ( ( ( P / 2 ) x. 2 ) - ( P / 2 ) ) )
355 331 recnd 
 |-  ( P e. RR -> ( P / 2 ) e. CC )
356 355 350 mulcomd 
 |-  ( P e. RR -> ( ( P / 2 ) x. 2 ) = ( 2 x. ( P / 2 ) ) )
357 356 oveq1d 
 |-  ( P e. RR -> ( ( ( P / 2 ) x. 2 ) - ( P / 2 ) ) = ( ( 2 x. ( P / 2 ) ) - ( P / 2 ) ) )
358 350 355 mulsubfacd 
 |-  ( P e. RR -> ( ( 2 x. ( P / 2 ) ) - ( P / 2 ) ) = ( ( 2 - 1 ) x. ( P / 2 ) ) )
359 2m1e1 
 |-  ( 2 - 1 ) = 1
360 359 a1i 
 |-  ( P e. RR -> ( 2 - 1 ) = 1 )
361 360 oveq1d 
 |-  ( P e. RR -> ( ( 2 - 1 ) x. ( P / 2 ) ) = ( 1 x. ( P / 2 ) ) )
362 355 mulid2d 
 |-  ( P e. RR -> ( 1 x. ( P / 2 ) ) = ( P / 2 ) )
363 358 361 362 3eqtrd 
 |-  ( P e. RR -> ( ( 2 x. ( P / 2 ) ) - ( P / 2 ) ) = ( P / 2 ) )
364 354 357 363 3eqtrd 
 |-  ( P e. RR -> ( P - ( P / 2 ) ) = ( P / 2 ) )
365 364 adantl 
 |-  ( ( y e. RR /\ P e. RR ) -> ( P - ( P / 2 ) ) = ( P / 2 ) )
366 365 breq2d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( y <_ ( P - ( P / 2 ) ) <-> y <_ ( P / 2 ) ) )
367 348 349 366 3bitr3d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( -. ( P - y ) < ( P / 2 ) <-> y <_ ( P / 2 ) ) )
368 341 346 367 3imtr4d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( y <_ ( ( P - 1 ) / 2 ) -> -. ( P - y ) < ( P / 2 ) ) )
369 368 ex 
 |-  ( y e. RR -> ( P e. RR -> ( y <_ ( ( P - 1 ) / 2 ) -> -. ( P - y ) < ( P / 2 ) ) ) )
370 155 369 syl 
 |-  ( y e. NN -> ( P e. RR -> ( y <_ ( ( P - 1 ) / 2 ) -> -. ( P - y ) < ( P / 2 ) ) ) )
371 370 com3l 
 |-  ( P e. RR -> ( y <_ ( ( P - 1 ) / 2 ) -> ( y e. NN -> -. ( P - y ) < ( P / 2 ) ) ) )
372 329 371 syl 
 |-  ( P e. ZZ -> ( y <_ ( ( P - 1 ) / 2 ) -> ( y e. NN -> -. ( P - y ) < ( P / 2 ) ) ) )
373 54 55 372 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( y <_ ( ( P - 1 ) / 2 ) -> ( y e. NN -> -. ( P - y ) < ( P / 2 ) ) ) )
374 1 373 syl 
 |-  ( ph -> ( y <_ ( ( P - 1 ) / 2 ) -> ( y e. NN -> -. ( P - y ) < ( P / 2 ) ) ) )
375 374 adantl 
 |-  ( ( -. 2 || y /\ ph ) -> ( y <_ ( ( P - 1 ) / 2 ) -> ( y e. NN -> -. ( P - y ) < ( P / 2 ) ) ) )
376 375 com13 
 |-  ( y e. NN -> ( y <_ ( ( P - 1 ) / 2 ) -> ( ( -. 2 || y /\ ph ) -> -. ( P - y ) < ( P / 2 ) ) ) )
377 189 376 syl5bi 
 |-  ( y e. NN -> ( y <_ H -> ( ( -. 2 || y /\ ph ) -> -. ( P - y ) < ( P / 2 ) ) ) )
378 377 a1d 
 |-  ( y e. NN -> ( H e. NN -> ( y <_ H -> ( ( -. 2 || y /\ ph ) -> -. ( P - y ) < ( P / 2 ) ) ) ) )
379 378 3imp 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( -. 2 || y /\ ph ) -> -. ( P - y ) < ( P / 2 ) ) )
380 379 com12 
 |-  ( ( -. 2 || y /\ ph ) -> ( ( y e. NN /\ H e. NN /\ y <_ H ) -> -. ( P - y ) < ( P / 2 ) ) )
381 149 380 syl5bi 
 |-  ( ( -. 2 || y /\ ph ) -> ( y e. ( 1 ... H ) -> -. ( P - y ) < ( P / 2 ) ) )
382 381 3impia 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> -. ( P - y ) < ( P / 2 ) )
383 328 382 eqnbrtrd 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> -. ( ( ( P - y ) / 2 ) x. 2 ) < ( P / 2 ) )
384 383 iffalsed 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> if ( ( ( ( P - y ) / 2 ) x. 2 ) < ( P / 2 ) , ( ( ( P - y ) / 2 ) x. 2 ) , ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) ) = ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) )
385 328 oveq2d 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) = ( P - ( P - y ) ) )
386 322 183 anim12i 
 |-  ( ( ph /\ y e. ( 1 ... H ) ) -> ( P e. CC /\ y e. CC ) )
387 386 3adant1 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( P e. CC /\ y e. CC ) )
388 nncan 
 |-  ( ( P e. CC /\ y e. CC ) -> ( P - ( P - y ) ) = y )
389 387 388 syl 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( P - ( P - y ) ) = y )
390 384 385 389 3eqtrrd 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> y = if ( ( ( ( P - y ) / 2 ) x. 2 ) < ( P / 2 ) , ( ( ( P - y ) / 2 ) x. 2 ) , ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) ) )
391 315 321 390 rspcedvd 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> E. x e. ( 1 ... H ) y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) )
392 391 3exp 
 |-  ( -. 2 || y -> ( ph -> ( y e. ( 1 ... H ) -> E. x e. ( 1 ... H ) y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) ) ) )
393 210 392 pm2.61i 
 |-  ( ph -> ( y e. ( 1 ... H ) -> E. x e. ( 1 ... H ) y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) ) )
394 148 393 impbid 
 |-  ( ph -> ( E. x e. ( 1 ... H ) y = if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) <-> y e. ( 1 ... H ) ) )
395 5 394 syl5bb 
 |-  ( ph -> ( y e. ran R <-> y e. ( 1 ... H ) ) )
396 395 eqrdv 
 |-  ( ph -> ran R = ( 1 ... H ) )