Metamath Proof Explorer

Theorem gausslemma2dlem3

Description: Lemma 3 for gausslemma2d . (Contributed by AV, 4-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 ) ) ) )
gausslemma2d.m 
|- M = ( |_ ` ( P / 4 ) )
Assertion gausslemma2dlem3 
|- ( ph -> A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) )

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 gausslemma2d.m 
 |-  M = ( |_ ` ( P / 4 ) )
5 oveq1 
 |-  ( x = k -> ( x x. 2 ) = ( k x. 2 ) )
6 5 breq1d 
 |-  ( x = k -> ( ( x x. 2 ) < ( P / 2 ) <-> ( k x. 2 ) < ( P / 2 ) ) )
7 5 oveq2d 
 |-  ( x = k -> ( P - ( x x. 2 ) ) = ( P - ( k x. 2 ) ) )
8 6 5 7 ifbieq12d 
 |-  ( x = k -> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) = if ( ( k x. 2 ) < ( P / 2 ) , ( k x. 2 ) , ( P - ( k x. 2 ) ) ) )
9 8 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) /\ x = k ) -> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) = if ( ( k x. 2 ) < ( P / 2 ) , ( k x. 2 ) , ( P - ( k x. 2 ) ) ) )
10 1 gausslemma2dlem0a 
 |-  ( ph -> P e. NN )
11 elfz2 
 |-  ( k e. ( ( M + 1 ) ... H ) <-> ( ( ( M + 1 ) e. ZZ /\ H e. ZZ /\ k e. ZZ ) /\ ( ( M + 1 ) <_ k /\ k <_ H ) ) )
12 4 oveq1i 
 |-  ( M + 1 ) = ( ( |_ ` ( P / 4 ) ) + 1 )
13 12 breq1i 
 |-  ( ( M + 1 ) <_ k <-> ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k )
14 nnre 
 |-  ( P e. NN -> P e. RR )
15 4re 
 |-  4 e. RR
16 15 a1i 
 |-  ( P e. NN -> 4 e. RR )
17 4ne0 
 |-  4 =/= 0
18 17 a1i 
 |-  ( P e. NN -> 4 =/= 0 )
19 14 16 18 redivcld 
 |-  ( P e. NN -> ( P / 4 ) e. RR )
20 19 adantl 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( P / 4 ) e. RR )
21 fllelt 
 |-  ( ( P / 4 ) e. RR -> ( ( |_ ` ( P / 4 ) ) <_ ( P / 4 ) /\ ( P / 4 ) < ( ( |_ ` ( P / 4 ) ) + 1 ) ) )
22 20 21 syl 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( ( |_ ` ( P / 4 ) ) <_ ( P / 4 ) /\ ( P / 4 ) < ( ( |_ ` ( P / 4 ) ) + 1 ) ) )
23 19 flcld 
 |-  ( P e. NN -> ( |_ ` ( P / 4 ) ) e. ZZ )
24 23 zred 
 |-  ( P e. NN -> ( |_ ` ( P / 4 ) ) e. RR )
25 peano2re 
 |-  ( ( |_ ` ( P / 4 ) ) e. RR -> ( ( |_ ` ( P / 4 ) ) + 1 ) e. RR )
26 24 25 syl 
 |-  ( P e. NN -> ( ( |_ ` ( P / 4 ) ) + 1 ) e. RR )
27 26 adantl 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( ( |_ ` ( P / 4 ) ) + 1 ) e. RR )
28 zre 
 |-  ( k e. ZZ -> k e. RR )
29 28 adantr 
 |-  ( ( k e. ZZ /\ P e. NN ) -> k e. RR )
30 ltleletr 
 |-  ( ( ( P / 4 ) e. RR /\ ( ( |_ ` ( P / 4 ) ) + 1 ) e. RR /\ k e. RR ) -> ( ( ( P / 4 ) < ( ( |_ ` ( P / 4 ) ) + 1 ) /\ ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k ) -> ( P / 4 ) <_ k ) )
31 20 27 29 30 syl3anc 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( ( ( P / 4 ) < ( ( |_ ` ( P / 4 ) ) + 1 ) /\ ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k ) -> ( P / 4 ) <_ k ) )
32 31 expd 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( ( P / 4 ) < ( ( |_ ` ( P / 4 ) ) + 1 ) -> ( ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k -> ( P / 4 ) <_ k ) ) )
33 32 adantld 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( ( ( |_ ` ( P / 4 ) ) <_ ( P / 4 ) /\ ( P / 4 ) < ( ( |_ ` ( P / 4 ) ) + 1 ) ) -> ( ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k -> ( P / 4 ) <_ k ) ) )
34 22 33 mpd 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k -> ( P / 4 ) <_ k ) )
35 34 imp 
 |-  ( ( ( k e. ZZ /\ P e. NN ) /\ ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k ) -> ( P / 4 ) <_ k )
36 14 rehalfcld 
 |-  ( P e. NN -> ( P / 2 ) e. RR )
37 36 adantl 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( P / 2 ) e. RR )
38 2re 
 |-  2 e. RR
39 38 a1i 
 |-  ( k e. ZZ -> 2 e. RR )
40 28 39 remulcld 
 |-  ( k e. ZZ -> ( k x. 2 ) e. RR )
41 40 adantr 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( k x. 2 ) e. RR )
42 2pos 
 |-  0 < 2
43 38 42 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
44 43 a1i 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( 2 e. RR /\ 0 < 2 ) )
45 lediv1 
 |-  ( ( ( P / 2 ) e. RR /\ ( k x. 2 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( P / 2 ) <_ ( k x. 2 ) <-> ( ( P / 2 ) / 2 ) <_ ( ( k x. 2 ) / 2 ) ) )
46 37 41 44 45 syl3anc 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( ( P / 2 ) <_ ( k x. 2 ) <-> ( ( P / 2 ) / 2 ) <_ ( ( k x. 2 ) / 2 ) ) )
47 nncn 
 |-  ( P e. NN -> P e. CC )
48 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
49 48 a1i 
 |-  ( P e. NN -> ( 2 e. CC /\ 2 =/= 0 ) )
50 divdiv1 
 |-  ( ( P e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( P / 2 ) / 2 ) = ( P / ( 2 x. 2 ) ) )
51 47 49 49 50 syl3anc 
 |-  ( P e. NN -> ( ( P / 2 ) / 2 ) = ( P / ( 2 x. 2 ) ) )
52 2t2e4 
 |-  ( 2 x. 2 ) = 4
53 52 oveq2i 
 |-  ( P / ( 2 x. 2 ) ) = ( P / 4 )
54 51 53 eqtrdi 
 |-  ( P e. NN -> ( ( P / 2 ) / 2 ) = ( P / 4 ) )
55 zcn 
 |-  ( k e. ZZ -> k e. CC )
56 2cnd 
 |-  ( k e. ZZ -> 2 e. CC )
57 2ne0 
 |-  2 =/= 0
58 57 a1i 
 |-  ( k e. ZZ -> 2 =/= 0 )
59 55 56 58 divcan4d 
 |-  ( k e. ZZ -> ( ( k x. 2 ) / 2 ) = k )
60 54 59 breqan12rd 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( ( ( P / 2 ) / 2 ) <_ ( ( k x. 2 ) / 2 ) <-> ( P / 4 ) <_ k ) )
61 46 60 bitrd 
 |-  ( ( k e. ZZ /\ P e. NN ) -> ( ( P / 2 ) <_ ( k x. 2 ) <-> ( P / 4 ) <_ k ) )
62 61 adantr 
 |-  ( ( ( k e. ZZ /\ P e. NN ) /\ ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k ) -> ( ( P / 2 ) <_ ( k x. 2 ) <-> ( P / 4 ) <_ k ) )
63 35 62 mpbird 
 |-  ( ( ( k e. ZZ /\ P e. NN ) /\ ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k ) -> ( P / 2 ) <_ ( k x. 2 ) )
64 63 exp31 
 |-  ( k e. ZZ -> ( P e. NN -> ( ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k -> ( P / 2 ) <_ ( k x. 2 ) ) ) )
65 64 com23 
 |-  ( k e. ZZ -> ( ( ( |_ ` ( P / 4 ) ) + 1 ) <_ k -> ( P e. NN -> ( P / 2 ) <_ ( k x. 2 ) ) ) )
66 13 65 biimtrid 
 |-  ( k e. ZZ -> ( ( M + 1 ) <_ k -> ( P e. NN -> ( P / 2 ) <_ ( k x. 2 ) ) ) )
67 66 3ad2ant3 
 |-  ( ( ( M + 1 ) e. ZZ /\ H e. ZZ /\ k e. ZZ ) -> ( ( M + 1 ) <_ k -> ( P e. NN -> ( P / 2 ) <_ ( k x. 2 ) ) ) )
68 67 com12 
 |-  ( ( M + 1 ) <_ k -> ( ( ( M + 1 ) e. ZZ /\ H e. ZZ /\ k e. ZZ ) -> ( P e. NN -> ( P / 2 ) <_ ( k x. 2 ) ) ) )
69 68 adantr 
 |-  ( ( ( M + 1 ) <_ k /\ k <_ H ) -> ( ( ( M + 1 ) e. ZZ /\ H e. ZZ /\ k e. ZZ ) -> ( P e. NN -> ( P / 2 ) <_ ( k x. 2 ) ) ) )
70 69 impcom 
 |-  ( ( ( ( M + 1 ) e. ZZ /\ H e. ZZ /\ k e. ZZ ) /\ ( ( M + 1 ) <_ k /\ k <_ H ) ) -> ( P e. NN -> ( P / 2 ) <_ ( k x. 2 ) ) )
71 11 70 sylbi 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( P e. NN -> ( P / 2 ) <_ ( k x. 2 ) ) )
72 71 impcom 
 |-  ( ( P e. NN /\ k e. ( ( M + 1 ) ... H ) ) -> ( P / 2 ) <_ ( k x. 2 ) )
73 elfzelz 
 |-  ( k e. ( ( M + 1 ) ... H ) -> k e. ZZ )
74 73 zred 
 |-  ( k e. ( ( M + 1 ) ... H ) -> k e. RR )
75 38 a1i 
 |-  ( k e. ( ( M + 1 ) ... H ) -> 2 e. RR )
76 74 75 remulcld 
 |-  ( k e. ( ( M + 1 ) ... H ) -> ( k x. 2 ) e. RR )
77 lenlt 
 |-  ( ( ( P / 2 ) e. RR /\ ( k x. 2 ) e. RR ) -> ( ( P / 2 ) <_ ( k x. 2 ) <-> -. ( k x. 2 ) < ( P / 2 ) ) )
78 36 76 77 syl2an 
 |-  ( ( P e. NN /\ k e. ( ( M + 1 ) ... H ) ) -> ( ( P / 2 ) <_ ( k x. 2 ) <-> -. ( k x. 2 ) < ( P / 2 ) ) )
79 72 78 mpbid 
 |-  ( ( P e. NN /\ k e. ( ( M + 1 ) ... H ) ) -> -. ( k x. 2 ) < ( P / 2 ) )
80 10 79 sylan 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> -. ( k x. 2 ) < ( P / 2 ) )
81 80 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) /\ x = k ) -> -. ( k x. 2 ) < ( P / 2 ) )
82 81 iffalsed 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) /\ x = k ) -> if ( ( k x. 2 ) < ( P / 2 ) , ( k x. 2 ) , ( P - ( k x. 2 ) ) ) = ( P - ( k x. 2 ) ) )
83 9 82 eqtrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) /\ x = k ) -> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) = ( P - ( k x. 2 ) ) )
84 1 4 gausslemma2dlem0d 
 |-  ( ph -> M e. NN0 )
85 nn0p1nn 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN )
86 nnuz 
 |-  NN = ( ZZ>= ` 1 )
87 85 86 eleqtrdi 
 |-  ( M e. NN0 -> ( M + 1 ) e. ( ZZ>= ` 1 ) )
88 84 87 syl 
 |-  ( ph -> ( M + 1 ) e. ( ZZ>= ` 1 ) )
89 fzss1 
 |-  ( ( M + 1 ) e. ( ZZ>= ` 1 ) -> ( ( M + 1 ) ... H ) C_ ( 1 ... H ) )
90 88 89 syl 
 |-  ( ph -> ( ( M + 1 ) ... H ) C_ ( 1 ... H ) )
91 90 sselda 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> k e. ( 1 ... H ) )
92 ovexd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> ( P - ( k x. 2 ) ) e. _V )
93 3 83 91 92 fvmptd2 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... H ) ) -> ( R ` k ) = ( P - ( k x. 2 ) ) )
94 93 ralrimiva 
 |-  ( ph -> A. k e. ( ( M + 1 ) ... H ) ( R ` k ) = ( P - ( k x. 2 ) ) )