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