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 1 54 63 91 4syl 
 |-  ( ph -> ( x e. ( 1 ... H ) -> 1 <_ ( P - ( x x. 2 ) ) ) )
93 92 imp 
 |-  ( ( ph /\ x e. ( 1 ... H ) ) -> 1 <_ ( P - ( x x. 2 ) ) )
94 93 adantl 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> 1 <_ ( P - ( x x. 2 ) ) )
95 elnnz1 
 |-  ( ( P - ( x x. 2 ) ) e. NN <-> ( ( P - ( x x. 2 ) ) e. ZZ /\ 1 <_ ( P - ( x x. 2 ) ) ) )
96 62 94 95 sylanbrc 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( P - ( x x. 2 ) ) e. NN )
97 9 simp2bi 
 |-  ( x e. ( 1 ... H ) -> H e. NN )
98 97 ad2antll 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> H e. NN )
99 nnre 
 |-  ( P e. NN -> P e. RR )
100 99 rehalfcld 
 |-  ( P e. NN -> ( P / 2 ) e. RR )
101 100 adantr 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( P / 2 ) e. RR )
102 60 zred 
 |-  ( x e. ( 1 ... H ) -> ( x x. 2 ) e. RR )
103 lenlt 
 |-  ( ( ( P / 2 ) e. RR /\ ( x x. 2 ) e. RR ) -> ( ( P / 2 ) <_ ( x x. 2 ) <-> -. ( x x. 2 ) < ( P / 2 ) ) )
104 101 102 103 syl2an 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P / 2 ) <_ ( x x. 2 ) <-> -. ( x x. 2 ) < ( P / 2 ) ) )
105 22 60 anim12i 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P e. ZZ /\ -. 2 || P ) /\ ( x x. 2 ) e. ZZ ) )
106 105 30 sylibr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) )
107 halfleoddlt 
 |-  ( ( P e. ZZ /\ -. 2 || P /\ ( x x. 2 ) e. ZZ ) -> ( ( P / 2 ) <_ ( x x. 2 ) <-> ( P / 2 ) < ( x x. 2 ) ) )
108 106 107 syl 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P / 2 ) <_ ( x x. 2 ) <-> ( P / 2 ) < ( x x. 2 ) ) )
109 108 biimpa 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P / 2 ) < ( x x. 2 ) )
110 nncn 
 |-  ( P e. NN -> P e. CC )
111 subhalfhalf 
 |-  ( P e. CC -> ( P - ( P / 2 ) ) = ( P / 2 ) )
112 110 111 syl 
 |-  ( P e. NN -> ( P - ( P / 2 ) ) = ( P / 2 ) )
113 112 breq1d 
 |-  ( P e. NN -> ( ( P - ( P / 2 ) ) < ( x x. 2 ) <-> ( P / 2 ) < ( x x. 2 ) ) )
114 113 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 ) ) )
115 109 114 mpbird 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P - ( P / 2 ) ) < ( x x. 2 ) )
116 99 ad2antrr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> P e. RR )
117 100 ad2antrr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P / 2 ) e. RR )
118 102 adantl 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( x x. 2 ) e. RR )
119 116 117 118 3jca 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P e. RR /\ ( P / 2 ) e. RR /\ ( x x. 2 ) e. RR ) )
120 119 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 ) )
121 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 ) ) )
122 120 121 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 ) ) )
123 115 122 mpbid 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P - ( x x. 2 ) ) < ( P / 2 ) )
124 21 ad2antrr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> P e. ZZ )
125 simplr 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> -. 2 || P )
126 60 adantl 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( x x. 2 ) e. ZZ )
127 124 126 zsubcld 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P - ( x x. 2 ) ) e. ZZ )
128 124 125 127 3jca 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( P e. ZZ /\ -. 2 || P /\ ( P - ( x x. 2 ) ) e. ZZ ) )
129 128 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 ) )
130 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 ) ) )
131 129 130 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 ) ) )
132 123 131 mpbid 
 |-  ( ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) /\ ( P / 2 ) <_ ( x x. 2 ) ) -> ( P - ( x x. 2 ) ) <_ ( ( P - 1 ) / 2 ) )
133 132 ex 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P / 2 ) <_ ( x x. 2 ) -> ( P - ( x x. 2 ) ) <_ ( ( P - 1 ) / 2 ) ) )
134 2 breq2i 
 |-  ( ( P - ( x x. 2 ) ) <_ H <-> ( P - ( x x. 2 ) ) <_ ( ( P - 1 ) / 2 ) )
135 133 134 imbitrrdi 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( ( P / 2 ) <_ ( x x. 2 ) -> ( P - ( x x. 2 ) ) <_ H ) )
136 104 135 sylbird 
 |-  ( ( ( P e. NN /\ -. 2 || P ) /\ x e. ( 1 ... H ) ) -> ( -. ( x x. 2 ) < ( P / 2 ) -> ( P - ( x x. 2 ) ) <_ H ) )
137 136 ex 
 |-  ( ( P e. NN /\ -. 2 || P ) -> ( x e. ( 1 ... H ) -> ( -. ( x x. 2 ) < ( P / 2 ) -> ( P - ( x x. 2 ) ) <_ H ) ) )
138 1 20 137 3syl 
 |-  ( ph -> ( x e. ( 1 ... H ) -> ( -. ( x x. 2 ) < ( P / 2 ) -> ( P - ( x x. 2 ) ) <_ H ) ) )
139 138 imp 
 |-  ( ( ph /\ x e. ( 1 ... H ) ) -> ( -. ( x x. 2 ) < ( P / 2 ) -> ( P - ( x x. 2 ) ) <_ H ) )
140 139 impcom 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( P - ( x x. 2 ) ) <_ H )
141 elfz1b 
 |-  ( ( P - ( x x. 2 ) ) e. ( 1 ... H ) <-> ( ( P - ( x x. 2 ) ) e. NN /\ H e. NN /\ ( P - ( x x. 2 ) ) <_ H ) )
142 96 98 140 141 syl3anbrc 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( P - ( x x. 2 ) ) e. ( 1 ... H ) )
143 eleq1 
 |-  ( y = ( P - ( x x. 2 ) ) -> ( y e. ( 1 ... H ) <-> ( P - ( x x. 2 ) ) e. ( 1 ... H ) ) )
144 142 143 syl5ibrcom 
 |-  ( ( -. ( x x. 2 ) < ( P / 2 ) /\ ( ph /\ x e. ( 1 ... H ) ) ) -> ( y = ( P - ( x x. 2 ) ) -> y e. ( 1 ... H ) ) )
145 53 144 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 ) ) )
146 50 145 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 ) ) )
147 146 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 ) ) )
148 elfz1b 
 |-  ( y e. ( 1 ... H ) <-> ( y e. NN /\ H e. NN /\ y <_ H ) )
149 simp1 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> y e. NN )
150 simpl 
 |-  ( ( 2 || y /\ ph ) -> 2 || y )
151 nnehalf 
 |-  ( ( y e. NN /\ 2 || y ) -> ( y / 2 ) e. NN )
152 149 150 151 syl2anr 
 |-  ( ( ( 2 || y /\ ph ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( y / 2 ) e. NN )
153 simpr2 
 |-  ( ( ( 2 || y /\ ph ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> H e. NN )
154 nnre 
 |-  ( y e. NN -> y e. RR )
155 154 ad2antrr 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( 2 || y /\ ph ) ) -> y e. RR )
156 nnrp 
 |-  ( H e. NN -> H e. RR+ )
157 156 adantl 
 |-  ( ( y e. NN /\ H e. NN ) -> H e. RR+ )
158 157 adantr 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( 2 || y /\ ph ) ) -> H e. RR+ )
159 2rp 
 |-  2 e. RR+
160 1le2 
 |-  1 <_ 2
161 159 160 pm3.2i 
 |-  ( 2 e. RR+ /\ 1 <_ 2 )
162 161 a1i 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( 2 || y /\ ph ) ) -> ( 2 e. RR+ /\ 1 <_ 2 ) )
163 ledivge1le 
 |-  ( ( y e. RR /\ H e. RR+ /\ ( 2 e. RR+ /\ 1 <_ 2 ) ) -> ( y <_ H -> ( y / 2 ) <_ H ) )
164 155 158 162 163 syl3anc 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( 2 || y /\ ph ) ) -> ( y <_ H -> ( y / 2 ) <_ H ) )
165 164 ex 
 |-  ( ( y e. NN /\ H e. NN ) -> ( ( 2 || y /\ ph ) -> ( y <_ H -> ( y / 2 ) <_ H ) ) )
166 165 com23 
 |-  ( ( y e. NN /\ H e. NN ) -> ( y <_ H -> ( ( 2 || y /\ ph ) -> ( y / 2 ) <_ H ) ) )
167 166 3impia 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( 2 || y /\ ph ) -> ( y / 2 ) <_ H ) )
168 167 impcom 
 |-  ( ( ( 2 || y /\ ph ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( y / 2 ) <_ H )
169 152 153 168 3jca 
 |-  ( ( ( 2 || y /\ ph ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) )
170 169 ex 
 |-  ( ( 2 || y /\ ph ) -> ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) ) )
171 148 170 biimtrid 
 |-  ( ( 2 || y /\ ph ) -> ( y e. ( 1 ... H ) -> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) ) )
172 171 3impia 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) )
173 elfz1b 
 |-  ( ( y / 2 ) e. ( 1 ... H ) <-> ( ( y / 2 ) e. NN /\ H e. NN /\ ( y / 2 ) <_ H ) )
174 172 173 sylibr 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( y / 2 ) e. ( 1 ... H ) )
175 oveq1 
 |-  ( x = ( y / 2 ) -> ( x x. 2 ) = ( ( y / 2 ) x. 2 ) )
176 175 breq1d 
 |-  ( x = ( y / 2 ) -> ( ( x x. 2 ) < ( P / 2 ) <-> ( ( y / 2 ) x. 2 ) < ( P / 2 ) ) )
177 175 oveq2d 
 |-  ( x = ( y / 2 ) -> ( P - ( x x. 2 ) ) = ( P - ( ( y / 2 ) x. 2 ) ) )
178 176 175 177 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 ) ) ) )
179 178 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 ) ) ) ) )
180 179 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 ) ) ) ) )
181 elfzelz 
 |-  ( y e. ( 1 ... H ) -> y e. ZZ )
182 181 zcnd 
 |-  ( y e. ( 1 ... H ) -> y e. CC )
183 182 3ad2ant3 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> y e. CC )
184 2cnd 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> 2 e. CC )
185 2ne0 
 |-  2 =/= 0
186 185 a1i 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> 2 =/= 0 )
187 183 184 186 divcan1d 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( y / 2 ) x. 2 ) = y )
188 2 breq2i 
 |-  ( y <_ H <-> y <_ ( ( P - 1 ) / 2 ) )
189 nnz 
 |-  ( y e. NN -> y e. ZZ )
190 1 20 22 3syl 
 |-  ( ph -> ( P e. ZZ /\ -. 2 || P ) )
191 190 adantl 
 |-  ( ( 2 || y /\ ph ) -> ( P e. ZZ /\ -. 2 || P ) )
192 189 191 anim12ci 
 |-  ( ( y e. NN /\ ( 2 || y /\ ph ) ) -> ( ( P e. ZZ /\ -. 2 || P ) /\ y e. ZZ ) )
193 df-3an 
 |-  ( ( P e. ZZ /\ -. 2 || P /\ y e. ZZ ) <-> ( ( P e. ZZ /\ -. 2 || P ) /\ y e. ZZ ) )
194 192 193 sylibr 
 |-  ( ( y e. NN /\ ( 2 || y /\ ph ) ) -> ( P e. ZZ /\ -. 2 || P /\ y e. ZZ ) )
195 ltoddhalfle 
 |-  ( ( P e. ZZ /\ -. 2 || P /\ y e. ZZ ) -> ( y < ( P / 2 ) <-> y <_ ( ( P - 1 ) / 2 ) ) )
196 194 195 syl 
 |-  ( ( y e. NN /\ ( 2 || y /\ ph ) ) -> ( y < ( P / 2 ) <-> y <_ ( ( P - 1 ) / 2 ) ) )
197 196 exbiri 
 |-  ( y e. NN -> ( ( 2 || y /\ ph ) -> ( y <_ ( ( P - 1 ) / 2 ) -> y < ( P / 2 ) ) ) )
198 197 com23 
 |-  ( y e. NN -> ( y <_ ( ( P - 1 ) / 2 ) -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) ) )
199 188 198 biimtrid 
 |-  ( y e. NN -> ( y <_ H -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) ) )
200 199 a1d 
 |-  ( y e. NN -> ( H e. NN -> ( y <_ H -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) ) ) )
201 200 3imp 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) )
202 148 201 sylbi 
 |-  ( y e. ( 1 ... H ) -> ( ( 2 || y /\ ph ) -> y < ( P / 2 ) ) )
203 202 com12 
 |-  ( ( 2 || y /\ ph ) -> ( y e. ( 1 ... H ) -> y < ( P / 2 ) ) )
204 203 3impia 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> y < ( P / 2 ) )
205 187 204 eqbrtrd 
 |-  ( ( 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( y / 2 ) x. 2 ) < ( P / 2 ) )
206 205 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 ) )
207 206 187 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 ) ) ) )
208 174 180 207 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 ) ) ) )
209 208 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 ) ) ) ) ) )
210 54 55 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ZZ )
211 210 ad2antrr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> P e. ZZ )
212 189 3ad2ant1 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> y e. ZZ )
213 212 adantl 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> y e. ZZ )
214 211 213 zsubcld 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - y ) e. ZZ )
215 154 ad2antrl 
 |-  ( ( P e. RR /\ ( y e. NN /\ H e. NN ) ) -> y e. RR )
216 67 rehalfcld 
 |-  ( P e. RR -> ( ( P - 1 ) / 2 ) e. RR )
217 216 adantr 
 |-  ( ( P e. RR /\ ( y e. NN /\ H e. NN ) ) -> ( ( P - 1 ) / 2 ) e. RR )
218 simpl 
 |-  ( ( P e. RR /\ ( y e. NN /\ H e. NN ) ) -> P e. RR )
219 215 217 218 3jca 
 |-  ( ( P e. RR /\ ( y e. NN /\ H e. NN ) ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) )
220 219 ex 
 |-  ( P e. RR -> ( ( y e. NN /\ H e. NN ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) ) )
221 54 63 220 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( y e. NN /\ H e. NN ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) ) )
222 221 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( ( y e. NN /\ H e. NN ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) ) )
223 222 impcom 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) )
224 lesub2 
 |-  ( ( y e. RR /\ ( ( P - 1 ) / 2 ) e. RR /\ P e. RR ) -> ( y <_ ( ( P - 1 ) / 2 ) <-> ( P - ( ( P - 1 ) / 2 ) ) <_ ( P - y ) ) )
225 223 224 syl 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( y <_ ( ( P - 1 ) / 2 ) <-> ( P - ( ( P - 1 ) / 2 ) ) <_ ( P - y ) ) )
226 55 zcnd 
 |-  ( P e. Prime -> P e. CC )
227 1cnd 
 |-  ( P e. CC -> 1 e. CC )
228 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
229 228 a1i 
 |-  ( P e. CC -> ( 2 e. CC /\ 2 =/= 0 ) )
230 divsubdir 
 |-  ( ( P e. CC /\ 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( P - 1 ) / 2 ) = ( ( P / 2 ) - ( 1 / 2 ) ) )
231 227 229 230 mpd3an23 
 |-  ( P e. CC -> ( ( P - 1 ) / 2 ) = ( ( P / 2 ) - ( 1 / 2 ) ) )
232 231 oveq2d 
 |-  ( P e. CC -> ( P - ( ( P - 1 ) / 2 ) ) = ( P - ( ( P / 2 ) - ( 1 / 2 ) ) ) )
233 id 
 |-  ( P e. CC -> P e. CC )
234 halfcl 
 |-  ( P e. CC -> ( P / 2 ) e. CC )
235 halfcn 
 |-  ( 1 / 2 ) e. CC
236 235 a1i 
 |-  ( P e. CC -> ( 1 / 2 ) e. CC )
237 233 234 236 subsubd 
 |-  ( P e. CC -> ( P - ( ( P / 2 ) - ( 1 / 2 ) ) ) = ( ( P - ( P / 2 ) ) + ( 1 / 2 ) ) )
238 111 oveq1d 
 |-  ( P e. CC -> ( ( P - ( P / 2 ) ) + ( 1 / 2 ) ) = ( ( P / 2 ) + ( 1 / 2 ) ) )
239 232 237 238 3eqtrd 
 |-  ( P e. CC -> ( P - ( ( P - 1 ) / 2 ) ) = ( ( P / 2 ) + ( 1 / 2 ) ) )
240 54 226 239 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P - ( ( P - 1 ) / 2 ) ) = ( ( P / 2 ) + ( 1 / 2 ) ) )
241 240 ad2antrl 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( P - ( ( P - 1 ) / 2 ) ) = ( ( P / 2 ) + ( 1 / 2 ) ) )
242 241 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 ) ) )
243 prmnn 
 |-  ( P e. Prime -> P e. NN )
244 halfre 
 |-  ( 1 / 2 ) e. RR
245 244 a1i 
 |-  ( P e. NN -> ( 1 / 2 ) e. RR )
246 nngt0 
 |-  ( P e. NN -> 0 < P )
247 71 a1i 
 |-  ( P e. NN -> ( 2 e. RR /\ 0 < 2 ) )
248 divgt0 
 |-  ( ( ( P e. RR /\ 0 < P ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 < ( P / 2 ) )
249 99 246 247 248 syl21anc 
 |-  ( P e. NN -> 0 < ( P / 2 ) )
250 halfgt0 
 |-  0 < ( 1 / 2 )
251 250 a1i 
 |-  ( P e. NN -> 0 < ( 1 / 2 ) )
252 100 245 249 251 addgt0d 
 |-  ( P e. NN -> 0 < ( ( P / 2 ) + ( 1 / 2 ) ) )
253 54 243 252 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> 0 < ( ( P / 2 ) + ( 1 / 2 ) ) )
254 253 ad2antrl 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> 0 < ( ( P / 2 ) + ( 1 / 2 ) ) )
255 0red 
 |-  ( ( y e. RR /\ P e. RR ) -> 0 e. RR )
256 simpr 
 |-  ( ( y e. RR /\ P e. RR ) -> P e. RR )
257 256 rehalfcld 
 |-  ( ( y e. RR /\ P e. RR ) -> ( P / 2 ) e. RR )
258 244 a1i 
 |-  ( ( y e. RR /\ P e. RR ) -> ( 1 / 2 ) e. RR )
259 257 258 readdcld 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) + ( 1 / 2 ) ) e. RR )
260 resubcl 
 |-  ( ( P e. RR /\ y e. RR ) -> ( P - y ) e. RR )
261 260 ancoms 
 |-  ( ( y e. RR /\ P e. RR ) -> ( P - y ) e. RR )
262 255 259 261 3jca 
 |-  ( ( y e. RR /\ P e. RR ) -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) )
263 262 ex 
 |-  ( y e. RR -> ( P e. RR -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
264 154 263 syl 
 |-  ( y e. NN -> ( P e. RR -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
265 264 adantr 
 |-  ( ( y e. NN /\ H e. NN ) -> ( P e. RR -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
266 265 com12 
 |-  ( P e. RR -> ( ( y e. NN /\ H e. NN ) -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
267 54 63 266 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( y e. NN /\ H e. NN ) -> ( 0 e. RR /\ ( ( P / 2 ) + ( 1 / 2 ) ) e. RR /\ ( P - y ) e. RR ) ) )
268 267 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 ) ) )
269 268 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 ) )
270 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 ) ) )
271 269 270 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 ) ) )
272 254 271 mpand 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( ( ( P / 2 ) + ( 1 / 2 ) ) <_ ( P - y ) -> 0 < ( P - y ) ) )
273 242 272 sylbid 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( ( P - ( ( P - 1 ) / 2 ) ) <_ ( P - y ) -> 0 < ( P - y ) ) )
274 225 273 sylbid 
 |-  ( ( ( y e. NN /\ H e. NN ) /\ ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) ) -> ( y <_ ( ( P - 1 ) / 2 ) -> 0 < ( P - y ) ) )
275 274 ex 
 |-  ( ( y e. NN /\ H e. NN ) -> ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( y <_ ( ( P - 1 ) / 2 ) -> 0 < ( P - y ) ) ) )
276 275 com23 
 |-  ( ( y e. NN /\ H e. NN ) -> ( y <_ ( ( P - 1 ) / 2 ) -> ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> 0 < ( P - y ) ) ) )
277 188 276 biimtrid 
 |-  ( ( y e. NN /\ H e. NN ) -> ( y <_ H -> ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> 0 < ( P - y ) ) ) )
278 277 3impia 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> 0 < ( P - y ) ) )
279 278 impcom 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> 0 < ( P - y ) )
280 elnnz 
 |-  ( ( P - y ) e. NN <-> ( ( P - y ) e. ZZ /\ 0 < ( P - y ) ) )
281 214 279 280 sylanbrc 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - y ) e. NN )
282 23 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( P e. ZZ /\ -. 2 || P ) )
283 simpr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> -. 2 || y )
284 283 212 anim12ci 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( y e. ZZ /\ -. 2 || y ) )
285 omoe 
 |-  ( ( ( P e. ZZ /\ -. 2 || P ) /\ ( y e. ZZ /\ -. 2 || y ) ) -> 2 || ( P - y ) )
286 282 284 285 syl2an2r 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> 2 || ( P - y ) )
287 nnehalf 
 |-  ( ( ( P - y ) e. NN /\ 2 || ( P - y ) ) -> ( ( P - y ) / 2 ) e. NN )
288 281 286 287 syl2anc 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( P - y ) / 2 ) e. NN )
289 simpr2 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> H e. NN )
290 1red 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> 1 e. RR )
291 154 3ad2ant1 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> y e. RR )
292 291 adantl 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> y e. RR )
293 54 63 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. RR )
294 293 ad2antrr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> P e. RR )
295 nnge1 
 |-  ( y e. NN -> 1 <_ y )
296 295 3ad2ant1 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> 1 <_ y )
297 296 adantl 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> 1 <_ y )
298 290 292 294 297 lesub2dd 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - y ) <_ ( P - 1 ) )
299 294 292 resubcld 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - y ) e. RR )
300 54 63 67 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P - 1 ) e. RR )
301 300 ad2antrr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( P - 1 ) e. RR )
302 71 a1i 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( 2 e. RR /\ 0 < 2 ) )
303 lediv1 
 |-  ( ( ( P - y ) e. RR /\ ( P - 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( P - y ) <_ ( P - 1 ) <-> ( ( P - y ) / 2 ) <_ ( ( P - 1 ) / 2 ) ) )
304 299 301 302 303 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 ) ) )
305 298 304 mpbid 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( P - y ) / 2 ) <_ ( ( P - 1 ) / 2 ) )
306 2 breq2i 
 |-  ( ( ( P - y ) / 2 ) <_ H <-> ( ( P - y ) / 2 ) <_ ( ( P - 1 ) / 2 ) )
307 305 306 sylibr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) /\ ( y e. NN /\ H e. NN /\ y <_ H ) ) -> ( ( P - y ) / 2 ) <_ H )
308 288 289 307 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 ) )
309 308 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 ) ) )
310 elfz1b 
 |-  ( ( ( P - y ) / 2 ) e. ( 1 ... H ) <-> ( ( ( P - y ) / 2 ) e. NN /\ H e. NN /\ ( ( P - y ) / 2 ) <_ H ) )
311 309 148 310 3imtr4g 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ -. 2 || y ) -> ( y e. ( 1 ... H ) -> ( ( P - y ) / 2 ) e. ( 1 ... H ) ) )
312 311 ex 
 |-  ( P e. ( Prime \ { 2 } ) -> ( -. 2 || y -> ( y e. ( 1 ... H ) -> ( ( P - y ) / 2 ) e. ( 1 ... H ) ) ) )
313 1 312 syl 
 |-  ( ph -> ( -. 2 || y -> ( y e. ( 1 ... H ) -> ( ( P - y ) / 2 ) e. ( 1 ... H ) ) ) )
314 313 3imp21 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( P - y ) / 2 ) e. ( 1 ... H ) )
315 oveq1 
 |-  ( x = ( ( P - y ) / 2 ) -> ( x x. 2 ) = ( ( ( P - y ) / 2 ) x. 2 ) )
316 315 breq1d 
 |-  ( x = ( ( P - y ) / 2 ) -> ( ( x x. 2 ) < ( P / 2 ) <-> ( ( ( P - y ) / 2 ) x. 2 ) < ( P / 2 ) ) )
317 315 oveq2d 
 |-  ( x = ( ( P - y ) / 2 ) -> ( P - ( x x. 2 ) ) = ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) )
318 316 315 317 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 ) ) ) )
319 318 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 ) ) ) ) )
320 319 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 ) ) ) ) )
321 1 54 226 3syl 
 |-  ( ph -> P e. CC )
322 321 3ad2ant2 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> P e. CC )
323 182 3ad2ant3 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> y e. CC )
324 322 323 subcld 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( P - y ) e. CC )
325 2cnd 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> 2 e. CC )
326 185 a1i 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> 2 =/= 0 )
327 324 325 326 divcan1d 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( ( ( P - y ) / 2 ) x. 2 ) = ( P - y ) )
328 zre 
 |-  ( P e. ZZ -> P e. RR )
329 halfge0 
 |-  0 <_ ( 1 / 2 )
330 rehalfcl 
 |-  ( P e. RR -> ( P / 2 ) e. RR )
331 330 adantl 
 |-  ( ( y e. RR /\ P e. RR ) -> ( P / 2 ) e. RR )
332 331 258 subge02d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( 0 <_ ( 1 / 2 ) <-> ( ( P / 2 ) - ( 1 / 2 ) ) <_ ( P / 2 ) ) )
333 329 332 mpbii 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) - ( 1 / 2 ) ) <_ ( P / 2 ) )
334 simpl 
 |-  ( ( y e. RR /\ P e. RR ) -> y e. RR )
335 244 a1i 
 |-  ( P e. RR -> ( 1 / 2 ) e. RR )
336 330 335 resubcld 
 |-  ( P e. RR -> ( ( P / 2 ) - ( 1 / 2 ) ) e. RR )
337 336 adantl 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) - ( 1 / 2 ) ) e. RR )
338 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 ) ) )
339 334 337 331 338 syl3anc 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( y <_ ( ( P / 2 ) - ( 1 / 2 ) ) /\ ( ( P / 2 ) - ( 1 / 2 ) ) <_ ( P / 2 ) ) -> y <_ ( P / 2 ) ) )
340 333 339 mpan2d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( y <_ ( ( P / 2 ) - ( 1 / 2 ) ) -> y <_ ( P / 2 ) ) )
341 80 adantl 
 |-  ( ( y e. RR /\ P e. RR ) -> P e. CC )
342 1cnd 
 |-  ( ( y e. RR /\ P e. RR ) -> 1 e. CC )
343 228 a1i 
 |-  ( ( y e. RR /\ P e. RR ) -> ( 2 e. CC /\ 2 =/= 0 ) )
344 341 342 343 230 syl3anc 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P - 1 ) / 2 ) = ( ( P / 2 ) - ( 1 / 2 ) ) )
345 344 breq2d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( y <_ ( ( P - 1 ) / 2 ) <-> y <_ ( ( P / 2 ) - ( 1 / 2 ) ) ) )
346 lesub 
 |-  ( ( ( P / 2 ) e. RR /\ P e. RR /\ y e. RR ) -> ( ( P / 2 ) <_ ( P - y ) <-> y <_ ( P - ( P / 2 ) ) ) )
347 331 256 334 346 syl3anc 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) <_ ( P - y ) <-> y <_ ( P - ( P / 2 ) ) ) )
348 257 261 lenltd 
 |-  ( ( y e. RR /\ P e. RR ) -> ( ( P / 2 ) <_ ( P - y ) <-> -. ( P - y ) < ( P / 2 ) ) )
349 2cnd 
 |-  ( P e. RR -> 2 e. CC )
350 185 a1i 
 |-  ( P e. RR -> 2 =/= 0 )
351 80 349 350 divcan1d 
 |-  ( P e. RR -> ( ( P / 2 ) x. 2 ) = P )
352 351 eqcomd 
 |-  ( P e. RR -> P = ( ( P / 2 ) x. 2 ) )
353 352 oveq1d 
 |-  ( P e. RR -> ( P - ( P / 2 ) ) = ( ( ( P / 2 ) x. 2 ) - ( P / 2 ) ) )
354 330 recnd 
 |-  ( P e. RR -> ( P / 2 ) e. CC )
355 354 349 mulcomd 
 |-  ( P e. RR -> ( ( P / 2 ) x. 2 ) = ( 2 x. ( P / 2 ) ) )
356 355 oveq1d 
 |-  ( P e. RR -> ( ( ( P / 2 ) x. 2 ) - ( P / 2 ) ) = ( ( 2 x. ( P / 2 ) ) - ( P / 2 ) ) )
357 349 354 mulsubfacd 
 |-  ( P e. RR -> ( ( 2 x. ( P / 2 ) ) - ( P / 2 ) ) = ( ( 2 - 1 ) x. ( P / 2 ) ) )
358 2m1e1 
 |-  ( 2 - 1 ) = 1
359 358 a1i 
 |-  ( P e. RR -> ( 2 - 1 ) = 1 )
360 359 oveq1d 
 |-  ( P e. RR -> ( ( 2 - 1 ) x. ( P / 2 ) ) = ( 1 x. ( P / 2 ) ) )
361 354 mullidd 
 |-  ( P e. RR -> ( 1 x. ( P / 2 ) ) = ( P / 2 ) )
362 357 360 361 3eqtrd 
 |-  ( P e. RR -> ( ( 2 x. ( P / 2 ) ) - ( P / 2 ) ) = ( P / 2 ) )
363 353 356 362 3eqtrd 
 |-  ( P e. RR -> ( P - ( P / 2 ) ) = ( P / 2 ) )
364 363 adantl 
 |-  ( ( y e. RR /\ P e. RR ) -> ( P - ( P / 2 ) ) = ( P / 2 ) )
365 364 breq2d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( y <_ ( P - ( P / 2 ) ) <-> y <_ ( P / 2 ) ) )
366 347 348 365 3bitr3d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( -. ( P - y ) < ( P / 2 ) <-> y <_ ( P / 2 ) ) )
367 340 345 366 3imtr4d 
 |-  ( ( y e. RR /\ P e. RR ) -> ( y <_ ( ( P - 1 ) / 2 ) -> -. ( P - y ) < ( P / 2 ) ) )
368 367 ex 
 |-  ( y e. RR -> ( P e. RR -> ( y <_ ( ( P - 1 ) / 2 ) -> -. ( P - y ) < ( P / 2 ) ) ) )
369 154 368 syl 
 |-  ( y e. NN -> ( P e. RR -> ( y <_ ( ( P - 1 ) / 2 ) -> -. ( P - y ) < ( P / 2 ) ) ) )
370 369 com3l 
 |-  ( P e. RR -> ( y <_ ( ( P - 1 ) / 2 ) -> ( y e. NN -> -. ( P - y ) < ( P / 2 ) ) ) )
371 328 370 syl 
 |-  ( P e. ZZ -> ( y <_ ( ( P - 1 ) / 2 ) -> ( y e. NN -> -. ( P - y ) < ( P / 2 ) ) ) )
372 1 54 55 371 4syl 
 |-  ( ph -> ( y <_ ( ( P - 1 ) / 2 ) -> ( y e. NN -> -. ( P - y ) < ( P / 2 ) ) ) )
373 372 adantl 
 |-  ( ( -. 2 || y /\ ph ) -> ( y <_ ( ( P - 1 ) / 2 ) -> ( y e. NN -> -. ( P - y ) < ( P / 2 ) ) ) )
374 373 com13 
 |-  ( y e. NN -> ( y <_ ( ( P - 1 ) / 2 ) -> ( ( -. 2 || y /\ ph ) -> -. ( P - y ) < ( P / 2 ) ) ) )
375 188 374 biimtrid 
 |-  ( y e. NN -> ( y <_ H -> ( ( -. 2 || y /\ ph ) -> -. ( P - y ) < ( P / 2 ) ) ) )
376 375 a1d 
 |-  ( y e. NN -> ( H e. NN -> ( y <_ H -> ( ( -. 2 || y /\ ph ) -> -. ( P - y ) < ( P / 2 ) ) ) ) )
377 376 3imp 
 |-  ( ( y e. NN /\ H e. NN /\ y <_ H ) -> ( ( -. 2 || y /\ ph ) -> -. ( P - y ) < ( P / 2 ) ) )
378 377 com12 
 |-  ( ( -. 2 || y /\ ph ) -> ( ( y e. NN /\ H e. NN /\ y <_ H ) -> -. ( P - y ) < ( P / 2 ) ) )
379 148 378 biimtrid 
 |-  ( ( -. 2 || y /\ ph ) -> ( y e. ( 1 ... H ) -> -. ( P - y ) < ( P / 2 ) ) )
380 379 3impia 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> -. ( P - y ) < ( P / 2 ) )
381 327 380 eqnbrtrd 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> -. ( ( ( P - y ) / 2 ) x. 2 ) < ( P / 2 ) )
382 381 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 ) ) )
383 327 oveq2d 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( P - ( ( ( P - y ) / 2 ) x. 2 ) ) = ( P - ( P - y ) ) )
384 321 182 anim12i 
 |-  ( ( ph /\ y e. ( 1 ... H ) ) -> ( P e. CC /\ y e. CC ) )
385 384 3adant1 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( P e. CC /\ y e. CC ) )
386 nncan 
 |-  ( ( P e. CC /\ y e. CC ) -> ( P - ( P - y ) ) = y )
387 385 386 syl 
 |-  ( ( -. 2 || y /\ ph /\ y e. ( 1 ... H ) ) -> ( P - ( P - y ) ) = y )
388 382 383 387 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 ) ) ) )
389 314 320 388 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 ) ) ) )
390 389 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 ) ) ) ) ) )
391 209 390 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 ) ) ) ) )
392 147 391 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 ) ) )
393 5 392 bitrid 
 |-  ( ph -> ( y e. ran R <-> y e. ( 1 ... H ) ) )
394 393 eqrdv 
 |-  ( ph -> ran R = ( 1 ... H ) )