Metamath Proof Explorer


Theorem gausslemma2dlem4

Description: Lemma 4 for gausslemma2d . (Contributed by AV, 16-Jun-2021)

Ref Expression
Hypotheses gausslemma2d.p φ P 2
gausslemma2d.h H = P 1 2
gausslemma2d.r R = x 1 H if x 2 < P 2 x 2 P x 2
gausslemma2d.m M = P 4
Assertion gausslemma2dlem4 φ H ! = k = 1 M R k k = M + 1 H R k

Proof

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