Metamath Proof Explorer


Theorem bgoldbtbndlem3

Description: Lemma 3 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
bgoldbtbnd.r φ F D
bgoldbtbndlem3.s S = X F I
Assertion bgoldbtbndlem3 φ X Odd I 1 ..^ D X F I F I + 1 4 < S 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 bgoldbtbnd.r φ F D
11 bgoldbtbndlem3.s S = X F I
12 fzo0ss1 1 ..^ D 0 ..^ D
13 12 sseli I 1 ..^ D I 0 ..^ D
14 fveq2 i = I F i = F I
15 14 eleq1d i = I F i 2 F I 2
16 fvoveq1 i = I F i + 1 = F I + 1
17 16 14 oveq12d i = I F i + 1 F i = F I + 1 F I
18 17 breq1d i = I F i + 1 F i < N 4 F I + 1 F I < N 4
19 17 breq2d i = I 4 < F i + 1 F i 4 < F I + 1 F I
20 15 18 19 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
21 20 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
22 13 6 21 syl2imc φ I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I
23 22 a1d φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I
24 23 3imp φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I
25 simp2 φ X Odd I 1 ..^ D X Odd
26 oddprmALTV F I 2 F I Odd
27 26 3ad2ant1 F I 2 F I + 1 F I < N 4 4 < F I + 1 F I F I Odd
28 25 27 anim12i φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X Odd F I Odd
29 28 adantr φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 4 < S X Odd F I Odd
30 omoeALTV X Odd F I Odd X F I Even
31 29 30 syl φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 4 < S X F I Even
32 11 31 eqeltrid φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 4 < S S Even
33 eldifi F I 2 F I
34 prmz F I F I
35 34 zred F I F I
36 fzofzp1 I 1 ..^ D I + 1 1 D
37 elfzo2 I 1 ..^ D I 1 D I < D
38 1zzd I 1 D I < D 1
39 simp2 I 1 D I < D D
40 eluz2 I 1 1 I 1 I
41 zre 1 1
42 zre I I
43 zre D D
44 leltletr 1 I D 1 I I < D 1 D
45 41 42 43 44 syl3an 1 I D 1 I I < D 1 D
46 45 exp5o 1 I D 1 I I < D 1 D
47 46 com34 1 I 1 I D I < D 1 D
48 47 3imp 1 I 1 I D I < D 1 D
49 40 48 sylbi I 1 D I < D 1 D
50 49 3imp I 1 D I < D 1 D
51 eluz2 D 1 1 D 1 D
52 38 39 50 51 syl3anbrc I 1 D I < D D 1
53 37 52 sylbi I 1 ..^ D D 1
54 fzisfzounsn D 1 1 D = 1 ..^ D D
55 53 54 syl I 1 ..^ D 1 D = 1 ..^ D D
56 55 eleq2d I 1 ..^ D I + 1 1 D I + 1 1 ..^ D D
57 elun I + 1 1 ..^ D D I + 1 1 ..^ D I + 1 D
58 56 57 bitrdi I 1 ..^ D I + 1 1 D I + 1 1 ..^ D I + 1 D
59 eluzge3nn D 3 D
60 4 59 syl φ D
61 60 ad2antrl I 1 ..^ D I + 1 1 ..^ D φ X Odd D
62 5 ad2antrl I 1 ..^ D I + 1 1 ..^ D φ X Odd F RePart D
63 simplr I 1 ..^ D I + 1 1 ..^ D φ X Odd I + 1 1 ..^ D
64 61 62 63 iccpartipre I 1 ..^ D I + 1 1 ..^ D φ X Odd F I + 1
65 64 exp31 I 1 ..^ D I + 1 1 ..^ D φ X Odd F I + 1
66 elsni I + 1 D I + 1 = D
67 10 ad2antrl I + 1 = D φ X Odd F D
68 fveq2 I + 1 = D F I + 1 = F D
69 68 eleq1d I + 1 = D F I + 1 F D
70 69 adantr I + 1 = D φ X Odd F I + 1 F D
71 67 70 mpbird I + 1 = D φ X Odd F I + 1
72 71 ex I + 1 = D φ X Odd F I + 1
73 66 72 syl I + 1 D φ X Odd F I + 1
74 73 a1i I 1 ..^ D I + 1 D φ X Odd F I + 1
75 65 74 jaod I 1 ..^ D I + 1 1 ..^ D I + 1 D φ X Odd F I + 1
76 58 75 sylbid I 1 ..^ D I + 1 1 D φ X Odd F I + 1
77 36 76 mpd I 1 ..^ D φ X Odd F I + 1
78 77 com12 φ X Odd I 1 ..^ D F I + 1
79 78 3impia φ X Odd I 1 ..^ D F I + 1
80 eluzelre N 11 N
81 2 80 syl φ N
82 oddz X Odd X
83 82 zred X Odd X
84 rexr F I + 1 F I + 1 *
85 rexr F I F I *
86 84 85 anim12ci F I + 1 F I F I * F I + 1 *
87 86 adantl N X F I + 1 F I F I * F I + 1 *
88 elico1 F I * F I + 1 * X F I F I + 1 X * F I X X < F I + 1
89 87 88 syl N X F I + 1 F I X F I F I + 1 X * F I X X < F I + 1
90 simpllr N X F I + 1 F I X < F I + 1 X
91 simplrl N X F I + 1 F I X < F I + 1 F I + 1
92 simplrr N X F I + 1 F I X < F I + 1 F I
93 simpr N X F I + 1 F I X < F I + 1 X < F I + 1
94 90 91 92 93 ltsub1dd N X F I + 1 F I X < F I + 1 X F I < F I + 1 F I
95 simplr N X F I + 1 F I X
96 simprr N X F I + 1 F I F I
97 95 96 resubcld N X F I + 1 F I X F I
98 97 adantr N X F I + 1 F I X < F I + 1 X F I
99 91 92 resubcld N X F I + 1 F I X < F I + 1 F I + 1 F I
100 simplll N X F I + 1 F I X < F I + 1 N
101 4re 4
102 101 a1i N X F I + 1 F I X < F I + 1 4
103 100 102 resubcld N X F I + 1 F I X < F I + 1 N 4
104 lttr X F I F I + 1 F I N 4 X F I < F I + 1 F I F I + 1 F I < N 4 X F I < N 4
105 98 99 103 104 syl3anc N X F I + 1 F I X < F I + 1 X F I < F I + 1 F I F I + 1 F I < N 4 X F I < N 4
106 94 105 mpand N X F I + 1 F I X < F I + 1 F I + 1 F I < N 4 X F I < N 4
107 106 impr N X F I + 1 F I X < F I + 1 F I + 1 F I < N 4 X F I < N 4
108 4pos 0 < 4
109 101 a1i N X 4
110 simpl N X N
111 109 110 ltsubposd N X 0 < 4 N 4 < N
112 108 111 mpbii N X N 4 < N
113 112 adantr N X F I + 1 F I N 4 < N
114 113 adantr N X F I + 1 F I X < F I + 1 F I + 1 F I < N 4 N 4 < N
115 simpll N X F I + 1 F I N
116 101 a1i N X F I + 1 F I 4
117 115 116 resubcld N X F I + 1 F I N 4
118 lttr X F I N 4 N X F I < N 4 N 4 < N X F I < N
119 97 117 115 118 syl3anc N X F I + 1 F I X F I < N 4 N 4 < N X F I < N
120 119 adantr N X F I + 1 F I X < F I + 1 F I + 1 F I < N 4 X F I < N 4 N 4 < N X F I < N
121 107 114 120 mp2and N X F I + 1 F I X < F I + 1 F I + 1 F I < N 4 X F I < N
122 121 exp32 N X F I + 1 F I X < F I + 1 F I + 1 F I < N 4 X F I < N
123 122 com12 X < F I + 1 N X F I + 1 F I F I + 1 F I < N 4 X F I < N
124 123 3ad2ant3 X * F I X X < F I + 1 N X F I + 1 F I F I + 1 F I < N 4 X F I < N
125 124 com12 N X F I + 1 F I X * F I X X < F I + 1 F I + 1 F I < N 4 X F I < N
126 89 125 sylbid N X F I + 1 F I X F I F I + 1 F I + 1 F I < N 4 X F I < N
127 126 com23 N X F I + 1 F I F I + 1 F I < N 4 X F I F I + 1 X F I < N
128 127 exp32 N X F I + 1 F I F I + 1 F I < N 4 X F I F I + 1 X F I < N
129 128 com34 N X F I + 1 F I + 1 F I < N 4 F I X F I F I + 1 X F I < N
130 81 83 129 syl2an φ X Odd F I + 1 F I + 1 F I < N 4 F I X F I F I + 1 X F I < N
131 130 3adant3 φ X Odd I 1 ..^ D F I + 1 F I + 1 F I < N 4 F I X F I F I + 1 X F I < N
132 79 131 mpd φ X Odd I 1 ..^ D F I + 1 F I < N 4 F I X F I F I + 1 X F I < N
133 132 com13 F I F I + 1 F I < N 4 φ X Odd I 1 ..^ D X F I F I + 1 X F I < N
134 33 35 133 3syl F I 2 F I + 1 F I < N 4 φ X Odd I 1 ..^ D X F I F I + 1 X F I < N
135 134 imp F I 2 F I + 1 F I < N 4 φ X Odd I 1 ..^ D X F I F I + 1 X F I < N
136 135 3adant3 F I 2 F I + 1 F I < N 4 4 < F I + 1 F I φ X Odd I 1 ..^ D X F I F I + 1 X F I < N
137 136 impcom φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 X F I < N
138 137 imp φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 X F I < N
139 138 adantrr φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 4 < S X F I < N
140 11 139 eqbrtrid φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 4 < S S < N
141 simprr φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 4 < S 4 < S
142 32 140 141 3jca φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 4 < S S Even S < N 4 < S
143 142 ex φ X Odd I 1 ..^ D F I 2 F I + 1 F I < N 4 4 < F I + 1 F I X F I F I + 1 4 < S S Even S < N 4 < S
144 24 143 mpdan φ X Odd I 1 ..^ D X F I F I + 1 4 < S S Even S < N 4 < S