Metamath Proof Explorer

Theorem gausslemma2dlem4

Description: Lemma 4 for gausslemma2d . (Contributed by AV, 16-Jun-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 gausslemma2dlem4 
|- ( ph -> ( ! ` H ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )

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 1 2 3 gausslemma2dlem1 
 |-  ( ph -> ( ! ` H ) = prod_ k e. ( 1 ... H ) ( R ` k ) )
6 eldif 
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ -. P e. { 2 } ) )
7 prm23ge5 
 |-  ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) )
8 eleq1 
 |-  ( P = 2 -> ( P e. { 2 } <-> 2 e. { 2 } ) )
9 8 notbid 
 |-  ( P = 2 -> ( -. P e. { 2 } <-> -. 2 e. { 2 } ) )
10 2ex 
 |-  2 e. _V
11 10 snid 
 |-  2 e. { 2 }
12 11 2a1i 
 |-  ( P = 2 -> ( prod_ k e. ( 1 ... H ) ( R ` k ) =/= ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) -> 2 e. { 2 } ) )
13 12 necon1bd 
 |-  ( P = 2 -> ( -. 2 e. { 2 } -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
14 13 a1dd 
 |-  ( P = 2 -> ( -. 2 e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
15 9 14 sylbid 
 |-  ( P = 2 -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
16 3lt4 
 |-  3 < 4
17 breq1 
 |-  ( P = 3 -> ( P < 4 <-> 3 < 4 ) )
18 16 17 mpbiri 
 |-  ( P = 3 -> P < 4 )
19 3nn0 
 |-  3 e. NN0
20 eleq1 
 |-  ( P = 3 -> ( P e. NN0 <-> 3 e. NN0 ) )
21 19 20 mpbiri 
 |-  ( P = 3 -> P e. NN0 )
22 4nn 
 |-  4 e. NN
23 divfl0 
 |-  ( ( P e. NN0 /\ 4 e. NN ) -> ( P < 4 <-> ( |_ ` ( P / 4 ) ) = 0 ) )
24 21 22 23 sylancl 
 |-  ( P = 3 -> ( P < 4 <-> ( |_ ` ( P / 4 ) ) = 0 ) )
25 18 24 mpbid 
 |-  ( P = 3 -> ( |_ ` ( P / 4 ) ) = 0 )
26 4 25 eqtrid 
 |-  ( P = 3 -> M = 0 )
27 oveq2 
 |-  ( M = 0 -> ( 1 ... M ) = ( 1 ... 0 ) )
28 27 adantr 
 |-  ( ( M = 0 /\ ph ) -> ( 1 ... M ) = ( 1 ... 0 ) )
29 fz10 
 |-  ( 1 ... 0 ) = (/)
30 28 29 eqtrdi 
 |-  ( ( M = 0 /\ ph ) -> ( 1 ... M ) = (/) )
31 30 prodeq1d 
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( 1 ... M ) ( R ` k ) = prod_ k e. (/) ( R ` k ) )
32 prod0 
 |-  prod_ k e. (/) ( R ` k ) = 1
33 31 32 eqtrdi 
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( 1 ... M ) ( R ` k ) = 1 )
34 oveq1 
 |-  ( M = 0 -> ( M + 1 ) = ( 0 + 1 ) )
35 34 adantr 
 |-  ( ( M = 0 /\ ph ) -> ( M + 1 ) = ( 0 + 1 ) )
36 0p1e1 
 |-  ( 0 + 1 ) = 1
37 35 36 eqtrdi 
 |-  ( ( M = 0 /\ ph ) -> ( M + 1 ) = 1 )
38 37 oveq1d 
 |-  ( ( M = 0 /\ ph ) -> ( ( M + 1 ) ... H ) = ( 1 ... H ) )
39 38 prodeq1d 
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) = prod_ k e. ( 1 ... H ) ( R ` k ) )
40 33 39 oveq12d 
 |-  ( ( M = 0 /\ ph ) -> ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) = ( 1 x. prod_ k e. ( 1 ... H ) ( R ` k ) ) )
41 fzfid 
 |-  ( ( M = 0 /\ ph ) -> ( 1 ... H ) e. Fin )
42 oveq1 
 |-  ( x = k -> ( x x. 2 ) = ( k x. 2 ) )
43 42 breq1d 
 |-  ( x = k -> ( ( x x. 2 ) < ( P / 2 ) <-> ( k x. 2 ) < ( P / 2 ) ) )
44 42 oveq2d 
 |-  ( x = k -> ( P - ( x x. 2 ) ) = ( P - ( k x. 2 ) ) )
45 43 42 44 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 ) ) ) )
46 simpr 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> k e. ( 1 ... H ) )
47 elfzelz 
 |-  ( k e. ( 1 ... H ) -> k e. ZZ )
48 47 zcnd 
 |-  ( k e. ( 1 ... H ) -> k e. CC )
49 2cnd 
 |-  ( k e. ( 1 ... H ) -> 2 e. CC )
50 48 49 mulcld 
 |-  ( k e. ( 1 ... H ) -> ( k x. 2 ) e. CC )
51 50 adantl 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( k x. 2 ) e. CC )
52 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
53 prmz 
 |-  ( P e. Prime -> P e. ZZ )
54 53 zcnd 
 |-  ( P e. Prime -> P e. CC )
55 1 52 54 3syl 
 |-  ( ph -> P e. CC )
56 55 adantr 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> P e. CC )
57 56 51 subcld 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( P - ( k x. 2 ) ) e. CC )
58 51 57 ifcld 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> if ( ( k x. 2 ) < ( P / 2 ) , ( k x. 2 ) , ( P - ( k x. 2 ) ) ) e. CC )
59 3 45 46 58 fvmptd3 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( R ` k ) = if ( ( k x. 2 ) < ( P / 2 ) , ( k x. 2 ) , ( P - ( k x. 2 ) ) ) )
60 59 58 eqeltrd 
 |-  ( ( ph /\ k e. ( 1 ... H ) ) -> ( R ` k ) e. CC )
61 60 adantll 
 |-  ( ( ( M = 0 /\ ph ) /\ k e. ( 1 ... H ) ) -> ( R ` k ) e. CC )
62 41 61 fprodcl 
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( 1 ... H ) ( R ` k ) e. CC )
63 62 mulid2d 
 |-  ( ( M = 0 /\ ph ) -> ( 1 x. prod_ k e. ( 1 ... H ) ( R ` k ) ) = prod_ k e. ( 1 ... H ) ( R ` k ) )
64 40 63 eqtr2d 
 |-  ( ( M = 0 /\ ph ) -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )
65 64 ex 
 |-  ( M = 0 -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
66 26 65 syl 
 |-  ( P = 3 -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
67 66 a1d 
 |-  ( P = 3 -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
68 1 4 gausslemma2dlem0d 
 |-  ( ph -> M e. NN0 )
69 68 nn0red 
 |-  ( ph -> M e. RR )
70 69 ltp1d 
 |-  ( ph -> M < ( M + 1 ) )
71 fzdisj 
 |-  ( M < ( M + 1 ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... H ) ) = (/) )
72 70 71 syl 
 |-  ( ph -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... H ) ) = (/) )
73 72 adantl 
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... H ) ) = (/) )
74 eluzelre 
 |-  ( P e. ( ZZ>= ` 5 ) -> P e. RR )
75 4re 
 |-  4 e. RR
76 75 a1i 
 |-  ( P e. ( ZZ>= ` 5 ) -> 4 e. RR )
77 4ne0 
 |-  4 =/= 0
78 77 a1i 
 |-  ( P e. ( ZZ>= ` 5 ) -> 4 =/= 0 )
79 74 76 78 redivcld 
 |-  ( P e. ( ZZ>= ` 5 ) -> ( P / 4 ) e. RR )
80 79 flcld 
 |-  ( P e. ( ZZ>= ` 5 ) -> ( |_ ` ( P / 4 ) ) e. ZZ )
81 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
82 22 81 ax-mp 
 |-  4 e. RR+
83 eluz2 
 |-  ( P e. ( ZZ>= ` 5 ) <-> ( 5 e. ZZ /\ P e. ZZ /\ 5 <_ P ) )
84 4lt5 
 |-  4 < 5
85 5re 
 |-  5 e. RR
86 85 a1i 
 |-  ( ( 5 e. ZZ /\ P e. ZZ ) -> 5 e. RR )
87 zre 
 |-  ( P e. ZZ -> P e. RR )
88 87 adantl 
 |-  ( ( 5 e. ZZ /\ P e. ZZ ) -> P e. RR )
89 ltleletr 
 |-  ( ( 4 e. RR /\ 5 e. RR /\ P e. RR ) -> ( ( 4 < 5 /\ 5 <_ P ) -> 4 <_ P ) )
90 75 86 88 89 mp3an2i 
 |-  ( ( 5 e. ZZ /\ P e. ZZ ) -> ( ( 4 < 5 /\ 5 <_ P ) -> 4 <_ P ) )
91 84 90 mpani 
 |-  ( ( 5 e. ZZ /\ P e. ZZ ) -> ( 5 <_ P -> 4 <_ P ) )
92 91 3impia 
 |-  ( ( 5 e. ZZ /\ P e. ZZ /\ 5 <_ P ) -> 4 <_ P )
93 83 92 sylbi 
 |-  ( P e. ( ZZ>= ` 5 ) -> 4 <_ P )
94 divge1 
 |-  ( ( 4 e. RR+ /\ P e. RR /\ 4 <_ P ) -> 1 <_ ( P / 4 ) )
95 82 74 93 94 mp3an2i 
 |-  ( P e. ( ZZ>= ` 5 ) -> 1 <_ ( P / 4 ) )
96 1zzd 
 |-  ( P e. ( ZZ>= ` 5 ) -> 1 e. ZZ )
97 flge 
 |-  ( ( ( P / 4 ) e. RR /\ 1 e. ZZ ) -> ( 1 <_ ( P / 4 ) <-> 1 <_ ( |_ ` ( P / 4 ) ) ) )
98 79 96 97 syl2anc 
 |-  ( P e. ( ZZ>= ` 5 ) -> ( 1 <_ ( P / 4 ) <-> 1 <_ ( |_ ` ( P / 4 ) ) ) )
99 95 98 mpbid 
 |-  ( P e. ( ZZ>= ` 5 ) -> 1 <_ ( |_ ` ( P / 4 ) ) )
100 elnnz1 
 |-  ( ( |_ ` ( P / 4 ) ) e. NN <-> ( ( |_ ` ( P / 4 ) ) e. ZZ /\ 1 <_ ( |_ ` ( P / 4 ) ) ) )
101 80 99 100 sylanbrc 
 |-  ( P e. ( ZZ>= ` 5 ) -> ( |_ ` ( P / 4 ) ) e. NN )
102 101 adantl 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> ( |_ ` ( P / 4 ) ) e. NN )
103 oddprm 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
104 103 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> ( ( P - 1 ) / 2 ) e. NN )
105 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
106 52 105 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 2 ) )
107 106 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> P e. ( ZZ>= ` 2 ) )
108 fldiv4lem1div2uz2 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )
109 107 108 syl 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )
110 102 104 109 3jca 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ P e. ( ZZ>= ` 5 ) ) -> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
111 110 ex 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. ( ZZ>= ` 5 ) -> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) ) )
112 1 111 syl 
 |-  ( ph -> ( P e. ( ZZ>= ` 5 ) -> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) ) )
113 112 impcom 
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
114 2 oveq2i 
 |-  ( 1 ... H ) = ( 1 ... ( ( P - 1 ) / 2 ) )
115 4 114 eleq12i 
 |-  ( M e. ( 1 ... H ) <-> ( |_ ` ( P / 4 ) ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) )
116 elfz1b 
 |-  ( ( |_ ` ( P / 4 ) ) e. ( 1 ... ( ( P - 1 ) / 2 ) ) <-> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
117 115 116 bitri 
 |-  ( M e. ( 1 ... H ) <-> ( ( |_ ` ( P / 4 ) ) e. NN /\ ( ( P - 1 ) / 2 ) e. NN /\ ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
118 113 117 sylibr 
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> M e. ( 1 ... H ) )
119 fzsplit 
 |-  ( M e. ( 1 ... H ) -> ( 1 ... H ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... H ) ) )
120 118 119 syl 
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> ( 1 ... H ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... H ) ) )
121 fzfid 
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> ( 1 ... H ) e. Fin )
122 60 adantll 
 |-  ( ( ( P e. ( ZZ>= ` 5 ) /\ ph ) /\ k e. ( 1 ... H ) ) -> ( R ` k ) e. CC )
123 73 120 121 122 fprodsplit 
 |-  ( ( P e. ( ZZ>= ` 5 ) /\ ph ) -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )
124 123 ex 
 |-  ( P e. ( ZZ>= ` 5 ) -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
125 124 a1d 
 |-  ( P e. ( ZZ>= ` 5 ) -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
126 15 67 125 3jaoi 
 |-  ( ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
127 7 126 syl 
 |-  ( P e. Prime -> ( -. P e. { 2 } -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) ) )
128 127 imp 
 |-  ( ( P e. Prime /\ -. P e. { 2 } ) -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
129 6 128 sylbi 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) ) )
130 1 129 mpcom 
 |-  ( ph -> prod_ k e. ( 1 ... H ) ( R ` k ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )
131 5 130 eqtrd 
 |-  ( ph -> ( ! ` H ) = ( prod_ k e. ( 1 ... M ) ( R ` k ) x. prod_ k e. ( ( M + 1 ) ... H ) ( R ` k ) ) )