Metamath Proof Explorer


Theorem bgoldbtbndlem2

Description: Lemma 2 for bgoldbtbnd . (Contributed by AV, 1-Aug-2020)

Ref Expression
Hypotheses bgoldbtbnd.m φ M 11
bgoldbtbnd.n φ N 11
bgoldbtbnd.b φ n Even 4 < n n < N n GoldbachEven
bgoldbtbnd.d φ D 3
bgoldbtbnd.f φ F RePart D
bgoldbtbnd.i φ i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i
bgoldbtbnd.0 φ F 0 = 7
bgoldbtbnd.1 φ F 1 = 13
bgoldbtbnd.l φ M < F D
bgoldbtbndlem2.s S = X F I 1
Assertion bgoldbtbndlem2 φ X Odd I 1 ..^ D X F I F I + 1 X F I 4 S Even S < N 4 < S

Proof

Step Hyp Ref Expression
1 bgoldbtbnd.m φ M 11
2 bgoldbtbnd.n φ N 11
3 bgoldbtbnd.b φ n Even 4 < n n < N n GoldbachEven
4 bgoldbtbnd.d φ D 3
5 bgoldbtbnd.f φ F RePart D
6 bgoldbtbnd.i φ i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i
7 bgoldbtbnd.0 φ F 0 = 7
8 bgoldbtbnd.1 φ F 1 = 13
9 bgoldbtbnd.l φ M < F D
10 bgoldbtbndlem2.s S = X F I 1
11 elfzoelz I 1 ..^ D I
12 elfzoel2 I 1 ..^ D D
13 elfzom1b I D I 1 ..^ D I 1 0 ..^ D 1
14 fzossrbm1 D 0 ..^ D 1 0 ..^ D
15 14 adantl I D 0 ..^ D 1 0 ..^ D
16 15 sseld I D I 1 0 ..^ D 1 I 1 0 ..^ D
17 13 16 sylbid I D I 1 ..^ D I 1 0 ..^ D
18 17 com12 I 1 ..^ D I D I 1 0 ..^ D
19 11 12 18 mp2and I 1 ..^ D I 1 0 ..^ D
20 fveq2 i = I 1 F i = F I 1
21 20 eleq1d i = I 1 F i 2 F I 1 2
22 fvoveq1 i = I 1 F i + 1 = F I - 1 + 1
23 22 20 oveq12d i = I 1 F i + 1 F i = F I - 1 + 1 F I 1
24 23 breq1d i = I 1 F i + 1 F i < N 4 F I - 1 + 1 F I 1 < N 4
25 23 breq2d i = I 1 4 < F i + 1 F i 4 < F I - 1 + 1 F I 1
26 21 24 25 3anbi123d i = I 1 F i 2 F i + 1 F i < N 4 4 < F i + 1 F i F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1
27 26 rspcv I 1 0 ..^ D i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1
28 19 27 syl I 1 ..^ D i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1
29 6 28 syl5com φ I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1
30 29 a1d φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1
31 30 3imp φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1
32 simp2 φ X Odd I 1 ..^ D X Odd
33 oddprmALTV F I 1 2 F I 1 Odd
34 33 3ad2ant1 F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 F I 1 Odd
35 32 34 anim12i φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X Odd F I 1 Odd
36 35 adantr φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 X Odd F I 1 Odd
37 omoeALTV X Odd F I 1 Odd X F I 1 Even
38 36 37 syl φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 X F I 1 Even
39 10 38 eqeltrid φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 S Even
40 11 zcnd I 1 ..^ D I
41 40 3ad2ant3 φ X Odd I 1 ..^ D I
42 npcan1 I I - 1 + 1 = I
43 41 42 syl φ X Odd I 1 ..^ D I - 1 + 1 = I
44 43 fveq2d φ X Odd I 1 ..^ D F I - 1 + 1 = F I
45 44 oveq1d φ X Odd I 1 ..^ D F I - 1 + 1 F I 1 = F I F I 1
46 45 breq1d φ X Odd I 1 ..^ D F I - 1 + 1 F I 1 < N 4 F I F I 1 < N 4
47 46 adantr φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 F I F I 1 < N 4
48 eldifi F I 1 2 F I 1
49 prmz F I 1 F I 1
50 zre F I 1 F I 1
51 simp1 F i 2 F i + 1 F i < N 4 4 < F i + 1 F i F i 2
52 51 ralimi i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i i 0 ..^ D F i 2
53 fzo0ss1 1 ..^ D 0 ..^ D
54 53 sseli I 1 ..^ D I 0 ..^ D
55 54 adantl φ I 1 ..^ D I 0 ..^ D
56 fveq2 i = I F i = F I
57 56 eleq1d i = I F i 2 F I 2
58 57 rspcv I 0 ..^ D i 0 ..^ D F i 2 F I 2
59 55 58 syl φ I 1 ..^ D i 0 ..^ D F i 2 F I 2
60 59 ex φ I 1 ..^ D i 0 ..^ D F i 2 F I 2
61 60 com23 φ i 0 ..^ D F i 2 I 1 ..^ D F I 2
62 61 a1i X Odd φ i 0 ..^ D F i 2 I 1 ..^ D F I 2
63 62 com13 i 0 ..^ D F i 2 φ X Odd I 1 ..^ D F I 2
64 52 63 syl i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i φ X Odd I 1 ..^ D F I 2
65 6 64 mpcom φ X Odd I 1 ..^ D F I 2
66 65 3imp φ X Odd I 1 ..^ D F I 2
67 eldifi F I 2 F I
68 prmz F I F I
69 zre F I F I
70 eluzelz N 11 N
71 zre N N
72 oddz X Odd X
73 72 zred X Odd X
74 simplr N X F I F I 1 X
75 simprl N X F I F I 1 F I
76 4re 4
77 76 a1i N X F I F I 1 4
78 74 75 77 lesubaddd N X F I F I 1 X F I 4 X 4 + F I
79 simpllr N X F I F I 1 X 4 + F I F I F I 1 < N 4 X
80 simplrr N X F I F I 1 X 4 + F I F I F I 1 < N 4 F I 1
81 79 80 resubcld N X F I F I 1 X 4 + F I F I F I 1 < N 4 X F I 1
82 76 a1i N X F I F I 1 X 4 + F I F I F I 1 < N 4 4
83 simplrl N X F I F I 1 X 4 + F I F I F I 1 < N 4 F I
84 82 83 readdcld N X F I F I 1 X 4 + F I F I F I 1 < N 4 4 + F I
85 84 80 resubcld N X F I F I 1 X 4 + F I F I F I 1 < N 4 4 + F I - F I 1
86 simplll N X F I F I 1 X 4 + F I F I F I 1 < N 4 N
87 77 75 readdcld N X F I F I 1 4 + F I
88 simprr N X F I F I 1 F I 1
89 74 87 88 lesub1d N X F I F I 1 X 4 + F I X F I 1 4 + F I - F I 1
90 89 biimpa N X F I F I 1 X 4 + F I X F I 1 4 + F I - F I 1
91 90 adantrr N X F I F I 1 X 4 + F I F I F I 1 < N 4 X F I 1 4 + F I - F I 1
92 resubcl F I F I 1 F I F I 1
93 92 adantl N X F I F I 1 F I F I 1
94 simpll N X F I F I 1 N
95 ltaddsub2 4 F I F I 1 N 4 + F I - F I 1 < N F I F I 1 < N 4
96 95 bicomd 4 F I F I 1 N F I F I 1 < N 4 4 + F I - F I 1 < N
97 77 93 94 96 syl3anc N X F I F I 1 F I F I 1 < N 4 4 + F I - F I 1 < N
98 97 biimpd N X F I F I 1 F I F I 1 < N 4 4 + F I - F I 1 < N
99 98 adantld N X F I F I 1 X 4 + F I F I F I 1 < N 4 4 + F I - F I 1 < N
100 99 imp N X F I F I 1 X 4 + F I F I F I 1 < N 4 4 + F I - F I 1 < N
101 4cn 4
102 101 a1i N X F I F I 1 4
103 75 recnd N X F I F I 1 F I
104 recn F I 1 F I 1
105 104 adantl F I F I 1 F I 1
106 105 adantl N X F I F I 1 F I 1
107 102 103 106 addsubassd N X F I F I 1 4 + F I - F I 1 = 4 + F I - F I 1
108 107 breq1d N X F I F I 1 4 + F I - F I 1 < N 4 + F I - F I 1 < N
109 108 adantr N X F I F I 1 X 4 + F I F I F I 1 < N 4 4 + F I - F I 1 < N 4 + F I - F I 1 < N
110 100 109 mpbird N X F I F I 1 X 4 + F I F I F I 1 < N 4 4 + F I - F I 1 < N
111 81 85 86 91 110 lelttrd N X F I F I 1 X 4 + F I F I F I 1 < N 4 X F I 1 < N
112 111 exp32 N X F I F I 1 X 4 + F I F I F I 1 < N 4 X F I 1 < N
113 78 112 sylbid N X F I F I 1 X F I 4 F I F I 1 < N 4 X F I 1 < N
114 113 com23 N X F I F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
115 114 exp32 N X F I F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
116 73 115 sylan2 N X Odd F I F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
117 116 ex N X Odd F I F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
118 71 117 syl N X Odd F I F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
119 2 70 118 3syl φ X Odd F I F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
120 119 imp φ X Odd F I F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
121 120 3adant3 φ X Odd I 1 ..^ D F I F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
122 69 121 syl5com F I φ X Odd I 1 ..^ D F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
123 67 68 122 3syl F I 2 φ X Odd I 1 ..^ D F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
124 66 123 mpcom φ X Odd I 1 ..^ D F I 1 F I F I 1 < N 4 X F I 4 X F I 1 < N
125 50 124 syl5com F I 1 φ X Odd I 1 ..^ D F I F I 1 < N 4 X F I 4 X F I 1 < N
126 48 49 125 3syl F I 1 2 φ X Odd I 1 ..^ D F I F I 1 < N 4 X F I 4 X F I 1 < N
127 126 impcom φ X Odd I 1 ..^ D F I 1 2 F I F I 1 < N 4 X F I 4 X F I 1 < N
128 47 127 sylbid φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 X F I 4 X F I 1 < N
129 128 expcom F I 1 2 φ X Odd I 1 ..^ D F I - 1 + 1 F I 1 < N 4 X F I 4 X F I 1 < N
130 129 com23 F I 1 2 F I - 1 + 1 F I 1 < N 4 φ X Odd I 1 ..^ D X F I 4 X F I 1 < N
131 130 imp F I 1 2 F I - 1 + 1 F I 1 < N 4 φ X Odd I 1 ..^ D X F I 4 X F I 1 < N
132 131 3adant3 F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 φ X Odd I 1 ..^ D X F I 4 X F I 1 < N
133 132 impcom φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I 4 X F I 1 < N
134 133 com12 X F I 4 φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I 1 < N
135 134 adantl X F I F I + 1 X F I 4 φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I 1 < N
136 135 impcom φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 X F I 1 < N
137 10 136 eqbrtrid φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 S < N
138 76 a1i φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 4
139 1eluzge0 1 0
140 fzoss1 1 0 1 ..^ D 0 ..^ D
141 139 140 mp1i φ 1 ..^ D 0 ..^ D
142 141 sselda φ I 1 ..^ D I 0 ..^ D
143 fvoveq1 i = I F i + 1 = F I + 1
144 143 56 oveq12d i = I F i + 1 F i = F I + 1 F I
145 144 breq1d i = I F i + 1 F i < N 4 F I + 1 F I < N 4
146 144 breq2d i = I 4 < F i + 1 F i 4 < F I + 1 F I
147 57 145 146 3anbi123d i = I F i 2 F i + 1 F i < N 4 4 < F i + 1 F i F I 2 F I + 1 F I < N 4 4 < F I + 1 F I
148 147 rspcv I 0 ..^ D i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i F I 2 F I + 1 F I < N 4 4 < F I + 1 F I
149 142 148 syl φ I 1 ..^ D i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i F I 2 F I + 1 F I < N 4 4 < F I + 1 F I
150 68 zred F I F I
151 67 150 syl F I 2 F I
152 151 3ad2ant1 F I 2 F I + 1 F I < N 4 4 < F I + 1 F I F I
153 149 152 syl6 φ I 1 ..^ D i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i F I
154 153 ex φ I 1 ..^ D i 0 ..^ D F i 2 F i + 1 F i < N 4 4 < F i + 1 F i F I
155 6 154 mpid φ I 1 ..^ D F I
156 155 imp φ I 1 ..^ D F I
157 156 3adant2 φ X Odd I 1 ..^ D F I
158 157 ad2antrr φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 F I
159 49 zred F I 1 F I 1
160 48 159 syl F I 1 2 F I 1
161 160 3ad2ant1 F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 F I 1
162 161 ad2antlr φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 F I 1
163 158 162 resubcld φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 F I F I 1
164 73 3ad2ant2 φ X Odd I 1 ..^ D X
165 resubcl X F I 1 X F I 1
166 164 161 165 syl2an φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I 1
167 166 adantr φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 X F I 1
168 40 42 syl I 1 ..^ D I - 1 + 1 = I
169 168 3ad2ant3 φ X Odd I 1 ..^ D I - 1 + 1 = I
170 169 fveq2d φ X Odd I 1 ..^ D F I - 1 + 1 = F I
171 170 oveq1d φ X Odd I 1 ..^ D F I - 1 + 1 F I 1 = F I F I 1
172 171 breq2d φ X Odd I 1 ..^ D 4 < F I - 1 + 1 F I 1 4 < F I F I 1
173 172 biimpcd 4 < F I - 1 + 1 F I 1 φ X Odd I 1 ..^ D 4 < F I F I 1
174 173 3ad2ant3 F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 φ X Odd I 1 ..^ D 4 < F I F I 1
175 174 impcom φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 4 < F I F I 1
176 175 adantr φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 4 < F I F I 1
177 164 ad2antrr φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 X
178 eluzge3nn D 3 D
179 4 178 syl φ D
180 179 adantr φ I 1 ..^ D D
181 5 adantr φ I 1 ..^ D F RePart D
182 139 140 mp1i D 3 1 ..^ D 0 ..^ D
183 fzossfz 0 ..^ D 0 D
184 182 183 sstrdi D 3 1 ..^ D 0 D
185 4 184 syl φ 1 ..^ D 0 D
186 185 sselda φ I 1 ..^ D I 0 D
187 180 181 186 iccpartxr φ I 1 ..^ D F I *
188 fzofzp1 I 0 ..^ D I + 1 0 D
189 142 188 syl φ I 1 ..^ D I + 1 0 D
190 180 181 189 iccpartxr φ I 1 ..^ D F I + 1 *
191 187 190 jca φ I 1 ..^ D F I * F I + 1 *
192 191 3adant2 φ X Odd I 1 ..^ D F I * F I + 1 *
193 elico1 F I * F I + 1 * X F I F I + 1 X * F I X X < F I + 1
194 192 193 syl φ X Odd I 1 ..^ D X F I F I + 1 X * F I X X < F I + 1
195 simp2 X * F I X X < F I + 1 F I X
196 194 195 syl6bi φ X Odd I 1 ..^ D X F I F I + 1 F I X
197 196 adantrd φ X Odd I 1 ..^ D X F I F I + 1 X F I 4 F I X
198 197 adantr φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 F I X
199 198 imp φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 F I X
200 158 177 162 199 lesub1dd φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 F I F I 1 X F I 1
201 138 163 167 176 200 ltletrd φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 4 < X F I 1
202 201 10 breqtrrdi φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 4 < S
203 39 137 202 3jca φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 S Even S < N 4 < S
204 203 ex φ X Odd I 1 ..^ D F I 1 2 F I - 1 + 1 F I 1 < N 4 4 < F I - 1 + 1 F I 1 X F I F I + 1 X F I 4 S Even S < N 4 < S
205 31 204 mpdan φ X Odd I 1 ..^ D X F I F I + 1 X F I 4 S Even S < N 4 < S