Proof of Theorem pntlemr
Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . . . . . . . 13
ψ |
2 | | pntlem1.a |
. . . . . . . . . . . . 13
|
3 | | pntlem1.b |
. . . . . . . . . . . . 13
|
4 | | pntlem1.l |
. . . . . . . . . . . . 13
|
5 | | pntlem1.d |
. . . . . . . . . . . . 13
|
6 | | pntlem1.f |
. . . . . . . . . . . . 13
; |
7 | 1, 2, 3, 4, 5, 6 | pntlemd 25283 |
. . . . . . . . . . . 12
|
8 | 7 | simp1d 1073 |
. . . . . . . . . . 11
|
9 | | pntlem1.u |
. . . . . . . . . . . . 13
|
10 | | pntlem1.u2 |
. . . . . . . . . . . . 13
|
11 | | pntlem1.e |
. . . . . . . . . . . . 13
|
12 | | pntlem1.k |
. . . . . . . . . . . . 13
|
13 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12 | pntlemc 25284 |
. . . . . . . . . . . 12
|
14 | 13 | simp1d 1073 |
. . . . . . . . . . 11
|
15 | 8, 14 | rpmulcld 11888 |
. . . . . . . . . 10
|
16 | | 4re 11097 |
. . . . . . . . . . 11
|
17 | | 4pos 11116 |
. . . . . . . . . . 11
|
18 | 16, 17 | elrpii 11835 |
. . . . . . . . . 10
|
19 | | rpdivcl 11856 |
. . . . . . . . . 10
|
20 | 15, 18, 19 | sylancl 694 |
. . . . . . . . 9
|
21 | 20 | rpred 11872 |
. . . . . . . 8
|
22 | | pntlem1.y |
. . . . . . . . . . . 12
|
23 | | pntlem1.x |
. . . . . . . . . . . 12
|
24 | | pntlem1.c |
. . . . . . . . . . . 12
|
25 | | pntlem1.w |
. . . . . . . . . . . 12
; |
26 | | pntlem1.z |
. . . . . . . . . . . 12
|
27 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26 | pntlemb 25286 |
. . . . . . . . . . 11
; |
28 | 27 | simp1d 1073 |
. . . . . . . . . 10
|
29 | | pntlem1.v |
. . . . . . . . . 10
|
30 | 28, 29 | rpdivcld 11889 |
. . . . . . . . 9
|
31 | 30 | rpred 11872 |
. . . . . . . 8
|
32 | 21, 31 | remulcld 10070 |
. . . . . . 7
|
33 | | pntlem1.i |
. . . . . . . . . 10
|
34 | | fzfid 12772 |
. . . . . . . . . 10
|
35 | 33, 34 | syl5eqel 2705 |
. . . . . . . . 9
|
36 | | hashcl 13147 |
. . . . . . . . 9
|
37 | 35, 36 | syl 17 |
. . . . . . . 8
|
38 | 37 | nn0red 11352 |
. . . . . . 7
|
39 | 32 | recnd 10068 |
. . . . . . . . . . . 12
|
40 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . 18
|
41 | | rpaddcl 11854 |
. . . . . . . . . . . . . . . . . 18
|
42 | 40, 15, 41 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
43 | 42, 29 | rpmulcld 11888 |
. . . . . . . . . . . . . . . 16
|
44 | 28, 43 | rpdivcld 11889 |
. . . . . . . . . . . . . . 15
|
45 | 44 | rpred 11872 |
. . . . . . . . . . . . . 14
|
46 | | reflcl 12597 |
. . . . . . . . . . . . . 14
|
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . 13
|
48 | 47 | recnd 10068 |
. . . . . . . . . . . 12
|
49 | | 1cnd 10056 |
. . . . . . . . . . . 12
|
50 | 39, 48, 49 | add32d 10263 |
. . . . . . . . . . 11
|
51 | | peano2re 10209 |
. . . . . . . . . . . . . 14
|
52 | 32, 51 | syl 17 |
. . . . . . . . . . . . 13
|
53 | 52, 47 | readdcld 10069 |
. . . . . . . . . . . 12
|
54 | | reflcl 12597 |
. . . . . . . . . . . . . 14
|
55 | 31, 54 | syl 17 |
. . . . . . . . . . . . 13
|
56 | | peano2re 10209 |
. . . . . . . . . . . . 13
|
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
|
58 | 15 | rphalfcld 11884 |
. . . . . . . . . . . . . . . 16
|
59 | 58, 30 | rpmulcld 11888 |
. . . . . . . . . . . . . . 15
|
60 | 59 | rpred 11872 |
. . . . . . . . . . . . . 14
|
61 | 60, 45 | readdcld 10069 |
. . . . . . . . . . . . 13
|
62 | | rpdivcl 11856 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 18, 15, 62 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 63 | rpred 11872 |
. . . . . . . . . . . . . . . . . 18
|
65 | 28 | rpsqrtcld 14150 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | 65 | rpred 11872 |
. . . . . . . . . . . . . . . . . . 19
|
67 | 27 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . 20
; |
68 | 67 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . 19
|
69 | 43 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
70 | 13 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
71 | | pntlem1.j |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ |
72 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^
|
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
74 | 73 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
75 | 70, 74 | rpexpcld 13032 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
76 | 75 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
77 | | pntlem1.V |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
78 | 77 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
79 | 78 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
80 | 70 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
81 | 70, 73 | rpexpcld 13032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
82 | 81 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
83 | 80, 82 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
84 | | pntlem1.m |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
85 | | pntlem1.n |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
86 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 84, 85 | pntlemg 25287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
87 | 86 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
88 | | elfzouz 12474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^
|
89 | 71, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
90 | | eluznn 11758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
91 | 87, 89, 90 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
92 | 91 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
93 | 80, 92 | expp1d 13009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
94 | 83, 93 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
95 | 79, 94 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
96 | 69, 76, 95 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
97 | | fzofzp1 12565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^
|
98 | 71, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
99 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 84, 85 | pntlemh 25288 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
100 | 98, 99 | mpdan 702 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
101 | 100 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
102 | 69, 76, 66, 96, 101 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
103 | 69, 66, 65 | lemul2d 11916 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
104 | 102, 103 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
|
105 | 28 | rprege0d 11879 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
106 | | remsqsqrt 13997 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
108 | 104, 107 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
|
109 | 28 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . 22
|
110 | 66, 109, 43 | lemuldivd 11921 |
. . . . . . . . . . . . . . . . . . . . 21
|
111 | 108, 110 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | 29 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
113 | 112 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
114 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
115 | 42 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
116 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
117 | | ltaddrp 11867 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
118 | 116, 15, 117 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
119 | 114, 115,
29, 118 | ltmul1dd 11927 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
120 | 113, 119 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . . 22
|
121 | 29, 43, 28 | ltdiv2d 11895 |
. . . . . . . . . . . . . . . . . . . . . 22
|
122 | 120, 121 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
|
123 | 45, 31, 122 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . 20
|
124 | 66, 45, 31, 111, 123 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
|
125 | 64, 66, 31, 68, 124 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
|
126 | 64, 31, 31, 125 | leadd2dd 10642 |
. . . . . . . . . . . . . . . . 17
|
127 | 30 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . 18
|
128 | 127 | 2timesd 11275 |
. . . . . . . . . . . . . . . . 17
|
129 | 126, 128 | breqtrrd 4681 |
. . . . . . . . . . . . . . . 16
|
130 | 31, 64 | readdcld 10069 |
. . . . . . . . . . . . . . . . 17
|
131 | | 2re 11090 |
. . . . . . . . . . . . . . . . . 18
|
132 | | remulcl 10021 |
. . . . . . . . . . . . . . . . . 18
|
133 | 131, 31, 132 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
134 | 130, 133,
20 | lemul2d 11916 |
. . . . . . . . . . . . . . . 16
|
135 | 129, 134 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
136 | 20 | rpcnd 11874 |
. . . . . . . . . . . . . . . . 17
|
137 | 63 | rpcnd 11874 |
. . . . . . . . . . . . . . . . 17
|
138 | 136, 127,
137 | adddid 10064 |
. . . . . . . . . . . . . . . 16
|
139 | 15 | rpcnne0d 11881 |
. . . . . . . . . . . . . . . . . 18
|
140 | | rpcnne0 11850 |
. . . . . . . . . . . . . . . . . . 19
|
141 | 18, 140 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
|
142 | | divcan6 10732 |
. . . . . . . . . . . . . . . . . 18
|
143 | 139, 141,
142 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
144 | 143 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
145 | 138, 144 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
146 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . 17
|
147 | 136, 146,
127 | mulassd 10063 |
. . . . . . . . . . . . . . . 16
|
148 | 15 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . 21
|
149 | | 2rp 11837 |
. . . . . . . . . . . . . . . . . . . . . 22
|
150 | | rpcnne0 11850 |
. . . . . . . . . . . . . . . . . . . . . 22
|
151 | 149, 150 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
|
152 | | divdiv1 10736 |
. . . . . . . . . . . . . . . . . . . . 21
|
153 | 148, 151,
151, 152 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
|
154 | | 2t2e4 11177 |
. . . . . . . . . . . . . . . . . . . . 21
|
155 | 154 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . 20
|
156 | 153, 155 | syl6req 2673 |
. . . . . . . . . . . . . . . . . . 19
|
157 | 156 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
158 | 148 | halfcld 11277 |
. . . . . . . . . . . . . . . . . . 19
|
159 | 151 | simprd 479 |
. . . . . . . . . . . . . . . . . . 19
|
160 | 158, 146,
159 | divcan1d 10802 |
. . . . . . . . . . . . . . . . . 18
|
161 | 157, 160 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
162 | 161 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
163 | 147, 162 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
|
164 | 135, 145,
163 | 3brtr3d 4684 |
. . . . . . . . . . . . . 14
|
165 | | flle 12600 |
. . . . . . . . . . . . . . 15
|
166 | 45, 165 | syl 17 |
. . . . . . . . . . . . . 14
|
167 | 52, 47, 60, 45, 164, 166 | le2addd 10646 |
. . . . . . . . . . . . 13
|
168 | 58 | rpred 11872 |
. . . . . . . . . . . . . . . 16
|
169 | 42 | rprecred 11883 |
. . . . . . . . . . . . . . . 16
|
170 | 168, 169 | readdcld 10069 |
. . . . . . . . . . . . . . 15
|
171 | 15 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . 20
|
172 | 14 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . 21
|
173 | 8 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
174 | | eliooord 12233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
175 | 4, 174 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
176 | 175 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
177 | 173, 114,
14, 176 | ltmul1dd 11927 |
. . . . . . . . . . . . . . . . . . . . . 22
|
178 | 14 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
179 | 178 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . . . 22
|
180 | 177, 179 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
|
181 | 13 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
182 | 181 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
183 | | eliooord 12233 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
185 | 184 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . 21
|
186 | 171, 172,
114, 180, 185 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . . 20
|
187 | 171, 114,
114, 186 | ltadd2dd 10196 |
. . . . . . . . . . . . . . . . . . 19
|
188 | | df-2 11079 |
. . . . . . . . . . . . . . . . . . 19
|
189 | 187, 188 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . 18
|
190 | 42 | rpregt0d 11878 |
. . . . . . . . . . . . . . . . . . 19
|
191 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
192 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . . . 20
|
193 | 192 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
194 | 15 | rpregt0d 11878 |
. . . . . . . . . . . . . . . . . . 19
|
195 | | ltdiv2 10909 |
. . . . . . . . . . . . . . . . . . 19
|
196 | 190, 191,
193, 194, 195 | syl121anc 1331 |
. . . . . . . . . . . . . . . . . 18
|
197 | 189, 196 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
198 | 42 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . 19
|
199 | 42 | rpcnne0d 11881 |
. . . . . . . . . . . . . . . . . . 19
|
200 | | divsubdir 10721 |
. . . . . . . . . . . . . . . . . . 19
|
201 | 198, 49, 199, 200 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
202 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . 20
|
203 | | pncan2 10288 |
. . . . . . . . . . . . . . . . . . . 20
|
204 | 202, 148,
203 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
|
205 | 204 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
206 | | divid 10714 |
. . . . . . . . . . . . . . . . . . . 20
|
207 | 199, 206 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 207 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
209 | 201, 205,
208 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . 17
|
210 | 197, 209 | breqtrd 4679 |
. . . . . . . . . . . . . . . 16
|
211 | 168, 169,
114 | ltaddsubd 10627 |
. . . . . . . . . . . . . . . 16
|
212 | 210, 211 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
213 | 170, 114,
30, 212 | ltmul1dd 11927 |
. . . . . . . . . . . . . 14
|
214 | | reccl 10692 |
. . . . . . . . . . . . . . . . 17
|
215 | 199, 214 | syl 17 |
. . . . . . . . . . . . . . . 16
|
216 | 158, 215,
127 | adddird 10065 |
. . . . . . . . . . . . . . 15
|
217 | 198, 112 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . 18
|
218 | 217 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
219 | 28 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . 18
|
220 | 29 | rpcnne0d 11881 |
. . . . . . . . . . . . . . . . . 18
|
221 | | divdiv1 10736 |
. . . . . . . . . . . . . . . . . 18
|
222 | 219, 220,
199, 221 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
223 | 42 | rpne0d 11877 |
. . . . . . . . . . . . . . . . . 18
|
224 | 127, 198,
223 | divrec2d 10805 |
. . . . . . . . . . . . . . . . 17
|
225 | 218, 222,
224 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . . 16
|
226 | 225 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
227 | 216, 226 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
228 | 127 | mulid2d 10058 |
. . . . . . . . . . . . . 14
|
229 | 213, 227,
228 | 3brtr3d 4684 |
. . . . . . . . . . . . 13
|
230 | 53, 61, 31, 167, 229 | lelttrd 10195 |
. . . . . . . . . . . 12
|
231 | | fllep1 12602 |
. . . . . . . . . . . . 13
|
232 | 31, 231 | syl 17 |
. . . . . . . . . . . 12
|
233 | 53, 31, 57, 230, 232 | ltletrd 10197 |
. . . . . . . . . . 11
|
234 | 50, 233 | eqbrtrd 4675 |
. . . . . . . . . 10
|
235 | 32, 47 | readdcld 10069 |
. . . . . . . . . . 11
|
236 | 235, 55, 114 | ltadd1d 10620 |
. . . . . . . . . 10
|
237 | 234, 236 | mpbird 247 |
. . . . . . . . 9
|
238 | 32, 47, 55 | ltaddsubd 10627 |
. . . . . . . . 9
|
239 | 237, 238 | mpbid 222 |
. . . . . . . 8
|
240 | 31 | flcld 12599 |
. . . . . . . . . . . 12
|
241 | | fzval3 12536 |
. . . . . . . . . . . 12
..^ |
242 | 240, 241 | syl 17 |
. . . . . . . . . . 11
..^ |
243 | 33, 242 | syl5eq 2668 |
. . . . . . . . . 10
..^ |
244 | 243 | fveq2d 6195 |
. . . . . . . . 9
..^ |
245 | | flword2 12614 |
. . . . . . . . . . . 12
|
246 | 45, 31, 123, 245 | syl3anc 1326 |
. . . . . . . . . . 11
|
247 | | eluzp1p1 11713 |
. . . . . . . . . . 11
|
248 | 246, 247 | syl 17 |
. . . . . . . . . 10
|
249 | | hashfzo 13216 |
. . . . . . . . . 10
..^
|
250 | 248, 249 | syl 17 |
. . . . . . . . 9
..^
|
251 | 55 | recnd 10068 |
. . . . . . . . . 10
|
252 | 251, 48, 49 | pnpcan2d 10430 |
. . . . . . . . 9
|
253 | 244, 250,
252 | 3eqtrd 2660 |
. . . . . . . 8
|
254 | 239, 253 | breqtrrd 4681 |
. . . . . . 7
|
255 | 32, 38, 254 | ltled 10185 |
. . . . . 6
|
256 | 21, 38, 30 | lemuldivd 11921 |
. . . . . 6
|
257 | 255, 256 | mpbid 222 |
. . . . 5
|
258 | 29 | rpred 11872 |
. . . . . . . . . . . . . . 15
|
259 | 69, 76, 66, 95, 101 | ltletrd 10197 |
. . . . . . . . . . . . . . . 16
|
260 | 258, 69, 66, 120, 259 | lttrd 10198 |
. . . . . . . . . . . . . . 15
|
261 | 258, 66, 260 | ltled 10185 |
. . . . . . . . . . . . . 14
|
262 | 29 | rprege0d 11879 |
. . . . . . . . . . . . . . 15
|
263 | 65 | rprege0d 11879 |
. . . . . . . . . . . . . . 15
|
264 | | le2sq 12938 |
. . . . . . . . . . . . . . 15
|
265 | 262, 263,
264 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
266 | 261, 265 | mpbid 222 |
. . . . . . . . . . . . 13
|
267 | | resqrtth 13996 |
. . . . . . . . . . . . . 14
|
268 | 105, 267 | syl 17 |
. . . . . . . . . . . . 13
|
269 | 266, 268 | breqtrd 4679 |
. . . . . . . . . . . 12
|
270 | | 2z 11409 |
. . . . . . . . . . . . . . 15
|
271 | | rpexpcl 12879 |
. . . . . . . . . . . . . . 15
|
272 | 29, 270, 271 | sylancl 694 |
. . . . . . . . . . . . . 14
|
273 | 272 | rpred 11872 |
. . . . . . . . . . . . 13
|
274 | 273, 109,
28 | lemul2d 11916 |
. . . . . . . . . . . 12
|
275 | 269, 274 | mpbid 222 |
. . . . . . . . . . 11
|
276 | 219 | sqvald 13005 |
. . . . . . . . . . 11
|
277 | 275, 276 | breqtrrd 4681 |
. . . . . . . . . 10
|
278 | 109 | resqcld 13035 |
. . . . . . . . . . 11
|
279 | 109, 278,
272 | lemuldivd 11921 |
. . . . . . . . . 10
|
280 | 277, 279 | mpbid 222 |
. . . . . . . . 9
|
281 | 29 | rpne0d 11877 |
. . . . . . . . . 10
|
282 | 219, 112,
281 | sqdivd 13021 |
. . . . . . . . 9
|
283 | 280, 282 | breqtrrd 4681 |
. . . . . . . 8
|
284 | | rpexpcl 12879 |
. . . . . . . . . 10
|
285 | 30, 270, 284 | sylancl 694 |
. . . . . . . . 9
|
286 | 28, 285 | logled 24373 |
. . . . . . . 8
|
287 | 283, 286 | mpbid 222 |
. . . . . . 7
|
288 | | relogexp 24342 |
. . . . . . . 8
|
289 | 30, 270, 288 | sylancl 694 |
. . . . . . 7
|
290 | 287, 289 | breqtrd 4679 |
. . . . . 6
|
291 | 28 | relogcld 24369 |
. . . . . . 7
|
292 | 30 | relogcld 24369 |
. . . . . . 7
|
293 | | ledivmul 10899 |
. . . . . . 7
|
294 | 291, 292,
191, 193, 293 | syl112anc 1330 |
. . . . . 6
|
295 | 290, 294 | mpbird 247 |
. . . . 5
|
296 | 20 | rprege0d 11879 |
. . . . . 6
|
297 | 38, 30 | rerpdivcld 11903 |
. . . . . 6
|
298 | 27 | simp2d 1074 |
. . . . . . . . . 10
|
299 | 298 | simp1d 1073 |
. . . . . . . . 9
|
300 | 109, 299 | rplogcld 24375 |
. . . . . . . 8
|
301 | 300 | rphalfcld 11884 |
. . . . . . 7
|
302 | 301 | rprege0d 11879 |
. . . . . 6
|
303 | | lemul12a 10881 |
. . . . . 6
|
304 | 296, 297,
302, 292, 303 | syl22anc 1327 |
. . . . 5
|
305 | 257, 295,
304 | mp2and 715 |
. . . 4
|
306 | 300 | rpcnd 11874 |
. . . . . 6
|
307 | | 8nn 11191 |
. . . . . . . 8
|
308 | | nnrp 11842 |
. . . . . . . 8
|
309 | 307, 308 | ax-mp 5 |
. . . . . . 7
|
310 | | rpcnne0 11850 |
. . . . . . 7
|
311 | 309, 310 | mp1i 13 |
. . . . . 6
|
312 | | div23 10704 |
. . . . . 6
|
313 | 148, 306,
311, 312 | syl3anc 1326 |
. . . . 5
|
314 | | divmuldiv 10725 |
. . . . . . 7
|
315 | 148, 306,
141, 151, 314 | syl22anc 1327 |
. . . . . 6
|
316 | | 4t2e8 11181 |
. . . . . . 7
|
317 | 316 | oveq2i 6661 |
. . . . . 6
|
318 | 315, 317 | syl6req 2673 |
. . . . 5
|
319 | 313, 318 | eqtr3d 2658 |
. . . 4
|
320 | 38 | recnd 10068 |
. . . . 5
|
321 | 292 | recnd 10068 |
. . . . 5
|
322 | 30 | rpcnne0d 11881 |
. . . . 5
|
323 | | divass 10703 |
. . . . . 6
|
324 | | div23 10704 |
. . . . . 6
|
325 | 323, 324 | eqtr3d 2658 |
. . . . 5
|
326 | 320, 321,
322, 325 | syl3anc 1326 |
. . . 4
|
327 | 305, 319,
326 | 3brtr4d 4685 |
. . 3
|
328 | | rpdivcl 11856 |
. . . . . . 7
|
329 | 15, 309, 328 | sylancl 694 |
. . . . . 6
|
330 | 329, 300 | rpmulcld 11888 |
. . . . 5
|
331 | 330 | rpred 11872 |
. . . 4
|
332 | 292, 30 | rerpdivcld 11903 |
. . . . 5
|
333 | 38, 332 | remulcld 10070 |
. . . 4
|
334 | 181 | simp3d 1075 |
. . . 4
|
335 | 331, 333,
334 | lemul2d 11916 |
. . 3
|
336 | 327, 335 | mpbid 222 |
. 2
|
337 | 334 | rpcnd 11874 |
. . 3
|
338 | 332 | recnd 10068 |
. . 3
|
339 | 337, 320,
338 | mul12d 10245 |
. 2
|
340 | 336, 339 | breqtrd 4679 |
1
|