Proof of Theorem bposlem7
Step | Hyp | Ref
| Expression |
1 | | bposlem7.4 |
. . . . . . . . . . . . 13
|
2 | 1 | nnrpd 11870 |
. . . . . . . . . . . 12
|
3 | 2 | rpsqrtcld 14150 |
. . . . . . . . . . 11
|
4 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
5 | | id 22 |
. . . . . . . . . . . . 13
|
6 | 4, 5 | oveq12d 6668 |
. . . . . . . . . . . 12
|
7 | | bposlem7.2 |
. . . . . . . . . . . 12
|
8 | | ovex 6678 |
. . . . . . . . . . . 12
|
9 | 6, 7, 8 | fvmpt 6282 |
. . . . . . . . . . 11
|
10 | 3, 9 | syl 17 |
. . . . . . . . . 10
|
11 | | bposlem7.3 |
. . . . . . . . . . . . 13
|
12 | 11 | nnrpd 11870 |
. . . . . . . . . . . 12
|
13 | 12 | rpsqrtcld 14150 |
. . . . . . . . . . 11
|
14 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
15 | | id 22 |
. . . . . . . . . . . . 13
|
16 | 14, 15 | oveq12d 6668 |
. . . . . . . . . . . 12
|
17 | | ovex 6678 |
. . . . . . . . . . . 12
|
18 | 16, 7, 17 | fvmpt 6282 |
. . . . . . . . . . 11
|
19 | 13, 18 | syl 17 |
. . . . . . . . . 10
|
20 | 10, 19 | breq12d 4666 |
. . . . . . . . 9
|
21 | 13 | rpred 11872 |
. . . . . . . . . 10
|
22 | | bposlem7.5 |
. . . . . . . . . . . 12
|
23 | 12 | rprege0d 11879 |
. . . . . . . . . . . . 13
|
24 | | resqrtth 13996 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
|
26 | 22, 25 | breqtrrd 4681 |
. . . . . . . . . . 11
|
27 | 13 | rpge0d 11876 |
. . . . . . . . . . . 12
|
28 | | ere 14819 |
. . . . . . . . . . . . 13
|
29 | | 0re 10040 |
. . . . . . . . . . . . . 14
|
30 | | epos 14935 |
. . . . . . . . . . . . . 14
|
31 | 29, 28, 30 | ltleii 10160 |
. . . . . . . . . . . . 13
|
32 | | le2sq 12938 |
. . . . . . . . . . . . 13
|
33 | 28, 31, 32 | mpanl12 718 |
. . . . . . . . . . . 12
|
34 | 21, 27, 33 | syl2anc 693 |
. . . . . . . . . . 11
|
35 | 26, 34 | mpbird 247 |
. . . . . . . . . 10
|
36 | 3 | rpred 11872 |
. . . . . . . . . 10
|
37 | | bposlem7.6 |
. . . . . . . . . . . 12
|
38 | 2 | rprege0d 11879 |
. . . . . . . . . . . . 13
|
39 | | resqrtth 13996 |
. . . . . . . . . . . . 13
|
40 | 38, 39 | syl 17 |
. . . . . . . . . . . 12
|
41 | 37, 40 | breqtrrd 4681 |
. . . . . . . . . . 11
|
42 | 3 | rpge0d 11876 |
. . . . . . . . . . . 12
|
43 | | le2sq 12938 |
. . . . . . . . . . . . 13
|
44 | 28, 31, 43 | mpanl12 718 |
. . . . . . . . . . . 12
|
45 | 36, 42, 44 | syl2anc 693 |
. . . . . . . . . . 11
|
46 | 41, 45 | mpbird 247 |
. . . . . . . . . 10
|
47 | | logdivlt 24367 |
. . . . . . . . . 10
|
48 | 21, 35, 36, 46, 47 | syl22anc 1327 |
. . . . . . . . 9
|
49 | 21, 36, 27, 42 | lt2sqd 13043 |
. . . . . . . . 9
|
50 | 20, 48, 49 | 3bitr2rd 297 |
. . . . . . . 8
|
51 | 25, 40 | breq12d 4666 |
. . . . . . . 8
|
52 | | relogcl 24322 |
. . . . . . . . . . . . 13
|
53 | | rerpdivcl 11861 |
. . . . . . . . . . . . 13
|
54 | 52, 53 | mpancom 703 |
. . . . . . . . . . . 12
|
55 | 7, 54 | fmpti 6383 |
. . . . . . . . . . 11
|
56 | 55 | ffvelrni 6358 |
. . . . . . . . . 10
|
57 | 3, 56 | syl 17 |
. . . . . . . . 9
|
58 | 55 | ffvelrni 6358 |
. . . . . . . . . 10
|
59 | 13, 58 | syl 17 |
. . . . . . . . 9
|
60 | | 2rp 11837 |
. . . . . . . . . 10
|
61 | | rpsqrtcl 14005 |
. . . . . . . . . 10
|
62 | 60, 61 | mp1i 13 |
. . . . . . . . 9
|
63 | 57, 59, 62 | ltmul2d 11914 |
. . . . . . . 8
|
64 | 50, 51, 63 | 3bitr3d 298 |
. . . . . . 7
|
65 | 64 | biimpd 219 |
. . . . . 6
|
66 | 11 | nnred 11035 |
. . . . . . . . . 10
|
67 | 1 | nnred 11035 |
. . . . . . . . . 10
|
68 | | 2re 11090 |
. . . . . . . . . . . 12
|
69 | | 2pos 11112 |
. . . . . . . . . . . 12
|
70 | 68, 69 | pm3.2i 471 |
. . . . . . . . . . 11
|
71 | 70 | a1i 11 |
. . . . . . . . . 10
|
72 | | ltdiv1 10887 |
. . . . . . . . . 10
|
73 | 66, 67, 71, 72 | syl3anc 1326 |
. . . . . . . . 9
|
74 | 12 | rphalfcld 11884 |
. . . . . . . . . . 11
|
75 | 74 | rpred 11872 |
. . . . . . . . . 10
|
76 | 28, 68 | remulcli 10054 |
. . . . . . . . . . . . 13
|
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
|
78 | 28 | resqcli 12949 |
. . . . . . . . . . . . 13
|
79 | 78 | a1i 11 |
. . . . . . . . . . . 12
|
80 | | egt2lt3 14934 |
. . . . . . . . . . . . . . . . 17
|
81 | 80 | simpli 474 |
. . . . . . . . . . . . . . . 16
|
82 | 68, 28, 81 | ltleii 10160 |
. . . . . . . . . . . . . . 15
|
83 | 68, 28, 28 | lemul2i 10947 |
. . . . . . . . . . . . . . . 16
|
84 | 30, 83 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
85 | 82, 84 | mpbi 220 |
. . . . . . . . . . . . . 14
|
86 | 28 | recni 10052 |
. . . . . . . . . . . . . . 15
|
87 | 86 | sqvali 12943 |
. . . . . . . . . . . . . 14
|
88 | 85, 87 | breqtrri 4680 |
. . . . . . . . . . . . 13
|
89 | 88 | a1i 11 |
. . . . . . . . . . . 12
|
90 | 77, 79, 66, 89, 22 | letrd 10194 |
. . . . . . . . . . 11
|
91 | | lemuldiv 10903 |
. . . . . . . . . . . . 13
|
92 | 28, 70, 91 | mp3an13 1415 |
. . . . . . . . . . . 12
|
93 | 66, 92 | syl 17 |
. . . . . . . . . . 11
|
94 | 90, 93 | mpbid 222 |
. . . . . . . . . 10
|
95 | 2 | rphalfcld 11884 |
. . . . . . . . . . 11
|
96 | 95 | rpred 11872 |
. . . . . . . . . 10
|
97 | 77, 79, 67, 89, 37 | letrd 10194 |
. . . . . . . . . . 11
|
98 | | lemuldiv 10903 |
. . . . . . . . . . . . 13
|
99 | 28, 70, 98 | mp3an13 1415 |
. . . . . . . . . . . 12
|
100 | 67, 99 | syl 17 |
. . . . . . . . . . 11
|
101 | 97, 100 | mpbid 222 |
. . . . . . . . . 10
|
102 | | logdivlt 24367 |
. . . . . . . . . 10
|
103 | 75, 94, 96, 101, 102 | syl22anc 1327 |
. . . . . . . . 9
|
104 | 73, 103 | bitrd 268 |
. . . . . . . 8
|
105 | | fveq2 6191 |
. . . . . . . . . . . 12
|
106 | | id 22 |
. . . . . . . . . . . 12
|
107 | 105, 106 | oveq12d 6668 |
. . . . . . . . . . 11
|
108 | | ovex 6678 |
. . . . . . . . . . 11
|
109 | 107, 7, 108 | fvmpt 6282 |
. . . . . . . . . 10
|
110 | 95, 109 | syl 17 |
. . . . . . . . 9
|
111 | | fveq2 6191 |
. . . . . . . . . . . 12
|
112 | | id 22 |
. . . . . . . . . . . 12
|
113 | 111, 112 | oveq12d 6668 |
. . . . . . . . . . 11
|
114 | | ovex 6678 |
. . . . . . . . . . 11
|
115 | 113, 7, 114 | fvmpt 6282 |
. . . . . . . . . 10
|
116 | 74, 115 | syl 17 |
. . . . . . . . 9
|
117 | 110, 116 | breq12d 4666 |
. . . . . . . 8
|
118 | 55 | ffvelrni 6358 |
. . . . . . . . . 10
|
119 | 95, 118 | syl 17 |
. . . . . . . . 9
|
120 | 55 | ffvelrni 6358 |
. . . . . . . . . 10
|
121 | 74, 120 | syl 17 |
. . . . . . . . 9
|
122 | | 9nn 11192 |
. . . . . . . . . . 11
|
123 | | 4nn 11187 |
. . . . . . . . . . 11
|
124 | | nnrp 11842 |
. . . . . . . . . . . 12
|
125 | | nnrp 11842 |
. . . . . . . . . . . 12
|
126 | | rpdivcl 11856 |
. . . . . . . . . . . 12
|
127 | 124, 125,
126 | syl2an 494 |
. . . . . . . . . . 11
|
128 | 122, 123,
127 | mp2an 708 |
. . . . . . . . . 10
|
129 | 128 | a1i 11 |
. . . . . . . . 9
|
130 | 119, 121,
129 | ltmul2d 11914 |
. . . . . . . 8
|
131 | 104, 117,
130 | 3bitr2d 296 |
. . . . . . 7
|
132 | 131 | biimpd 219 |
. . . . . 6
|
133 | 65, 132 | jcad 555 |
. . . . 5
|
134 | | sqrt2re 14980 |
. . . . . . 7
|
135 | | remulcl 10021 |
. . . . . . 7
|
136 | 134, 57, 135 | sylancr 695 |
. . . . . 6
|
137 | | 9re 11107 |
. . . . . . . 8
|
138 | | 4re 11097 |
. . . . . . . 8
|
139 | | 4ne0 11117 |
. . . . . . . 8
|
140 | 137, 138,
139 | redivcli 10792 |
. . . . . . 7
|
141 | | remulcl 10021 |
. . . . . . 7
|
142 | 140, 119,
141 | sylancr 695 |
. . . . . 6
|
143 | | remulcl 10021 |
. . . . . . 7
|
144 | 134, 59, 143 | sylancr 695 |
. . . . . 6
|
145 | | remulcl 10021 |
. . . . . . 7
|
146 | 140, 121,
145 | sylancr 695 |
. . . . . 6
|
147 | | lt2add 10513 |
. . . . . 6
|
148 | 136, 142,
144, 146, 147 | syl22anc 1327 |
. . . . 5
|
149 | 133, 148 | syld 47 |
. . . 4
|
150 | | ltmul2 10874 |
. . . . . . 7
|
151 | 66, 67, 71, 150 | syl3anc 1326 |
. . . . . 6
|
152 | | rpmulcl 11855 |
. . . . . . . . . 10
|
153 | 60, 12, 152 | sylancr 695 |
. . . . . . . . 9
|
154 | 153 | rpsqrtcld 14150 |
. . . . . . . 8
|
155 | | rpmulcl 11855 |
. . . . . . . . . 10
|
156 | 60, 2, 155 | sylancr 695 |
. . . . . . . . 9
|
157 | 156 | rpsqrtcld 14150 |
. . . . . . . 8
|
158 | | rprege0 11847 |
. . . . . . . . 9
|
159 | | rprege0 11847 |
. . . . . . . . 9
|
160 | | lt2sq 12937 |
. . . . . . . . 9
|
161 | 158, 159,
160 | syl2an 494 |
. . . . . . . 8
|
162 | 154, 157,
161 | syl2anc 693 |
. . . . . . 7
|
163 | 153 | rprege0d 11879 |
. . . . . . . . 9
|
164 | | resqrtth 13996 |
. . . . . . . . 9
|
165 | 163, 164 | syl 17 |
. . . . . . . 8
|
166 | 156 | rprege0d 11879 |
. . . . . . . . 9
|
167 | | resqrtth 13996 |
. . . . . . . . 9
|
168 | 166, 167 | syl 17 |
. . . . . . . 8
|
169 | 165, 168 | breq12d 4666 |
. . . . . . 7
|
170 | 162, 169 | bitr2d 269 |
. . . . . 6
|
171 | | 1lt2 11194 |
. . . . . . . . 9
|
172 | | rplogcl 24350 |
. . . . . . . . 9
|
173 | 68, 171, 172 | mp2an 708 |
. . . . . . . 8
|
174 | 173 | a1i 11 |
. . . . . . 7
|
175 | 154, 157,
174 | ltdiv2d 11895 |
. . . . . 6
|
176 | 151, 170,
175 | 3bitrd 294 |
. . . . 5
|
177 | 176 | biimpd 219 |
. . . 4
|
178 | 149, 177 | jcad 555 |
. . 3
|
179 | 136, 142 | readdcld 10069 |
. . . 4
|
180 | | rpre 11839 |
. . . . . 6
|
181 | 173, 180 | ax-mp 5 |
. . . . 5
|
182 | | rerpdivcl 11861 |
. . . . 5
|
183 | 181, 157,
182 | sylancr 695 |
. . . 4
|
184 | 144, 146 | readdcld 10069 |
. . . 4
|
185 | | rerpdivcl 11861 |
. . . . 5
|
186 | 181, 154,
185 | sylancr 695 |
. . . 4
|
187 | | lt2add 10513 |
. . . 4
|
188 | 179, 183,
184, 186, 187 | syl22anc 1327 |
. . 3
|
189 | 178, 188 | syld 47 |
. 2
|
190 | | fveq2 6191 |
. . . . . . . . 9
|
191 | 190 | fveq2d 6195 |
. . . . . . . 8
|
192 | 191 | oveq2d 6666 |
. . . . . . 7
|
193 | | oveq1 6657 |
. . . . . . . . 9
|
194 | 193 | fveq2d 6195 |
. . . . . . . 8
|
195 | 194 | oveq2d 6666 |
. . . . . . 7
|
196 | 192, 195 | oveq12d 6668 |
. . . . . 6
|
197 | | oveq2 6658 |
. . . . . . . 8
|
198 | 197 | fveq2d 6195 |
. . . . . . 7
|
199 | 198 | oveq2d 6666 |
. . . . . 6
|
200 | 196, 199 | oveq12d 6668 |
. . . . 5
|
201 | | bposlem7.1 |
. . . . 5
|
202 | | ovex 6678 |
. . . . 5
|
203 | 200, 201,
202 | fvmpt 6282 |
. . . 4
|
204 | 1, 203 | syl 17 |
. . 3
|
205 | | fveq2 6191 |
. . . . . . . . 9
|
206 | 205 | fveq2d 6195 |
. . . . . . . 8
|
207 | 206 | oveq2d 6666 |
. . . . . . 7
|
208 | | oveq1 6657 |
. . . . . . . . 9
|
209 | 208 | fveq2d 6195 |
. . . . . . . 8
|
210 | 209 | oveq2d 6666 |
. . . . . . 7
|
211 | 207, 210 | oveq12d 6668 |
. . . . . 6
|
212 | | oveq2 6658 |
. . . . . . . 8
|
213 | 212 | fveq2d 6195 |
. . . . . . 7
|
214 | 213 | oveq2d 6666 |
. . . . . 6
|
215 | 211, 214 | oveq12d 6668 |
. . . . 5
|
216 | | ovex 6678 |
. . . . 5
|
217 | 215, 201,
216 | fvmpt 6282 |
. . . 4
|
218 | 11, 217 | syl 17 |
. . 3
|
219 | 204, 218 | breq12d 4666 |
. 2
|
220 | 189, 219 | sylibrd 249 |
1
|