Metamath Proof Explorer

Theorem gausslemma2dlem2

Description: Lemma 2 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 gausslemma2dlem2 
|- ( ph -> A. k e. ( 1 ... M ) ( R ` k ) = ( 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. ( 1 ... M ) ) /\ 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 elfz1b 
 |-  ( k e. ( 1 ... M ) <-> ( k e. NN /\ M e. NN /\ k <_ M ) )
11 nnre 
 |-  ( k e. NN -> k e. RR )
12 11 adantr 
 |-  ( ( k e. NN /\ M e. NN ) -> k e. RR )
13 nnre 
 |-  ( M e. NN -> M e. RR )
14 13 adantl 
 |-  ( ( k e. NN /\ M e. NN ) -> M e. RR )
15 2re 
 |-  2 e. RR
16 2pos 
 |-  0 < 2
17 15 16 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
18 17 a1i 
 |-  ( ( k e. NN /\ M e. NN ) -> ( 2 e. RR /\ 0 < 2 ) )
19 lemul1 
 |-  ( ( k e. RR /\ M e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( k <_ M <-> ( k x. 2 ) <_ ( M x. 2 ) ) )
20 12 14 18 19 syl3anc 
 |-  ( ( k e. NN /\ M e. NN ) -> ( k <_ M <-> ( k x. 2 ) <_ ( M x. 2 ) ) )
21 1 4 gausslemma2dlem0e 
 |-  ( ph -> ( M x. 2 ) < ( P / 2 ) )
22 21 adantl 
 |-  ( ( ( k e. NN /\ M e. NN ) /\ ph ) -> ( M x. 2 ) < ( P / 2 ) )
23 15 a1i 
 |-  ( k e. NN -> 2 e. RR )
24 11 23 remulcld 
 |-  ( k e. NN -> ( k x. 2 ) e. RR )
25 24 adantr 
 |-  ( ( k e. NN /\ M e. NN ) -> ( k x. 2 ) e. RR )
26 15 a1i 
 |-  ( M e. NN -> 2 e. RR )
27 13 26 remulcld 
 |-  ( M e. NN -> ( M x. 2 ) e. RR )
28 27 adantl 
 |-  ( ( k e. NN /\ M e. NN ) -> ( M x. 2 ) e. RR )
29 1 gausslemma2dlem0a 
 |-  ( ph -> P e. NN )
30 29 nnred 
 |-  ( ph -> P e. RR )
31 30 rehalfcld 
 |-  ( ph -> ( P / 2 ) e. RR )
32 lelttr 
 |-  ( ( ( k x. 2 ) e. RR /\ ( M x. 2 ) e. RR /\ ( P / 2 ) e. RR ) -> ( ( ( k x. 2 ) <_ ( M x. 2 ) /\ ( M x. 2 ) < ( P / 2 ) ) -> ( k x. 2 ) < ( P / 2 ) ) )
33 25 28 31 32 syl2an3an 
 |-  ( ( ( k e. NN /\ M e. NN ) /\ ph ) -> ( ( ( k x. 2 ) <_ ( M x. 2 ) /\ ( M x. 2 ) < ( P / 2 ) ) -> ( k x. 2 ) < ( P / 2 ) ) )
34 22 33 mpan2d 
 |-  ( ( ( k e. NN /\ M e. NN ) /\ ph ) -> ( ( k x. 2 ) <_ ( M x. 2 ) -> ( k x. 2 ) < ( P / 2 ) ) )
35 34 ex 
 |-  ( ( k e. NN /\ M e. NN ) -> ( ph -> ( ( k x. 2 ) <_ ( M x. 2 ) -> ( k x. 2 ) < ( P / 2 ) ) ) )
36 35 com23 
 |-  ( ( k e. NN /\ M e. NN ) -> ( ( k x. 2 ) <_ ( M x. 2 ) -> ( ph -> ( k x. 2 ) < ( P / 2 ) ) ) )
37 20 36 sylbid 
 |-  ( ( k e. NN /\ M e. NN ) -> ( k <_ M -> ( ph -> ( k x. 2 ) < ( P / 2 ) ) ) )
38 37 3impia 
 |-  ( ( k e. NN /\ M e. NN /\ k <_ M ) -> ( ph -> ( k x. 2 ) < ( P / 2 ) ) )
39 10 38 sylbi 
 |-  ( k e. ( 1 ... M ) -> ( ph -> ( k x. 2 ) < ( P / 2 ) ) )
40 39 impcom 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( k x. 2 ) < ( P / 2 ) )
41 40 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ x = k ) -> ( k x. 2 ) < ( P / 2 ) )
42 41 iftrued 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ x = k ) -> if ( ( k x. 2 ) < ( P / 2 ) , ( k x. 2 ) , ( P - ( k x. 2 ) ) ) = ( k x. 2 ) )
43 9 42 eqtrd 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ x = k ) -> if ( ( x x. 2 ) < ( P / 2 ) , ( x x. 2 ) , ( P - ( x x. 2 ) ) ) = ( k x. 2 ) )
44 1 4 gausslemma2dlem0d 
 |-  ( ph -> M e. NN0 )
45 44 nn0zd 
 |-  ( ph -> M e. ZZ )
46 1 2 gausslemma2dlem0b 
 |-  ( ph -> H e. NN )
47 46 nnzd 
 |-  ( ph -> H e. ZZ )
48 1 4 2 gausslemma2dlem0g 
 |-  ( ph -> M <_ H )
49 eluz2 
 |-  ( H e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ H e. ZZ /\ M <_ H ) )
50 45 47 48 49 syl3anbrc 
 |-  ( ph -> H e. ( ZZ>= ` M ) )
51 fzss2 
 |-  ( H e. ( ZZ>= ` M ) -> ( 1 ... M ) C_ ( 1 ... H ) )
52 50 51 syl 
 |-  ( ph -> ( 1 ... M ) C_ ( 1 ... H ) )
53 52 sselda 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> k e. ( 1 ... H ) )
54 ovexd 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( k x. 2 ) e. _V )
55 3 43 53 54 fvmptd2 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( R ` k ) = ( k x. 2 ) )
56 55 ralrimiva 
 |-  ( ph -> A. k e. ( 1 ... M ) ( R ` k ) = ( k x. 2 ) )