Step | Hyp | Ref
| Expression |
1 | | nnre 11027 |
. . . . . . . . . . . . 13
|
2 | 1 | adantl 482 |
. . . . . . . . . . . 12
|
3 | | stoweidlem60.17 |
. . . . . . . . . . . . . 14
|
4 | 3 | rpred 11872 |
. . . . . . . . . . . . 13
|
5 | 4 | adantr 481 |
. . . . . . . . . . . 12
|
6 | 3 | rpne0d 11877 |
. . . . . . . . . . . . 13
|
7 | 6 | adantr 481 |
. . . . . . . . . . . 12
|
8 | 2, 5, 7 | redivcld 10853 |
. . . . . . . . . . 11
|
9 | | 1red 10055 |
. . . . . . . . . . 11
|
10 | 8, 9 | readdcld 10069 |
. . . . . . . . . 10
|
11 | 10 | adantr 481 |
. . . . . . . . 9
|
12 | | arch 11289 |
. . . . . . . . 9
|
13 | 11, 12 | syl 17 |
. . . . . . . 8
|
14 | | stoweidlem60.2 |
. . . . . . . . . . . . . . 15
|
15 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
16 | 14, 15 | nfan 1828 |
. . . . . . . . . . . . . 14
|
17 | | nfra1 2941 |
. . . . . . . . . . . . . 14
|
18 | 16, 17 | nfan 1828 |
. . . . . . . . . . . . 13
|
19 | | nfv 1843 |
. . . . . . . . . . . . 13
|
20 | 18, 19 | nfan 1828 |
. . . . . . . . . . . 12
|
21 | | nfv 1843 |
. . . . . . . . . . . 12
|
22 | 20, 21 | nfan 1828 |
. . . . . . . . . . 11
|
23 | | simp-5l 808 |
. . . . . . . . . . . . . 14
|
24 | | stoweidlem60.3 |
. . . . . . . . . . . . . . . 16
|
25 | | stoweidlem60.4 |
. . . . . . . . . . . . . . . 16
|
26 | | stoweidlem60.5 |
. . . . . . . . . . . . . . . 16
|
27 | | stoweidlem60.15 |
. . . . . . . . . . . . . . . 16
|
28 | 24, 25, 26, 27 | fcnre 39184 |
. . . . . . . . . . . . . . 15
|
29 | 28 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
|
30 | 23, 29 | sylancom 701 |
. . . . . . . . . . . . 13
|
31 | | simp-5r 809 |
. . . . . . . . . . . . . 14
|
32 | 31 | nnred 11035 |
. . . . . . . . . . . . 13
|
33 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
|
34 | 33 | nnred 11035 |
. . . . . . . . . . . . . . 15
|
35 | | 1red 10055 |
. . . . . . . . . . . . . . 15
|
36 | 34, 35 | resubcld 10458 |
. . . . . . . . . . . . . 14
|
37 | 23, 4 | syl 17 |
. . . . . . . . . . . . . 14
|
38 | 36, 37 | remulcld 10070 |
. . . . . . . . . . . . 13
|
39 | | simpllr 799 |
. . . . . . . . . . . . . 14
|
40 | 39 | r19.21bi 2932 |
. . . . . . . . . . . . 13
|
41 | | simplr 792 |
. . . . . . . . . . . . . 14
|
42 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
43 | | simpl1 1064 |
. . . . . . . . . . . . . . . . . 18
|
44 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . 18
|
45 | 43, 44, 8 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
46 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
|
47 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . 18
|
48 | 47 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
|
49 | 45, 46, 48 | ltaddsubd 10627 |
. . . . . . . . . . . . . . . 16
|
50 | 42, 49 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
51 | 1 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
53 | 48, 46 | resubcld 10458 |
. . . . . . . . . . . . . . . 16
|
54 | 4 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
|
55 | 54 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
56 | 3 | rpgt0d 11875 |
. . . . . . . . . . . . . . . . 17
|
57 | 43, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
|
58 | | ltdivmul2 10900 |
. . . . . . . . . . . . . . . 16
|
59 | 52, 53, 55, 57, 58 | syl112anc 1330 |
. . . . . . . . . . . . . . 15
|
60 | 50, 59 | mpbid 222 |
. . . . . . . . . . . . . 14
|
61 | 23, 31, 33, 41, 60 | syl31anc 1329 |
. . . . . . . . . . . . 13
|
62 | 30, 32, 38, 40, 61 | lttrd 10198 |
. . . . . . . . . . . 12
|
63 | 62 | ex 450 |
. . . . . . . . . . 11
|
64 | 22, 63 | ralrimi 2957 |
. . . . . . . . . 10
|
65 | 64 | ex 450 |
. . . . . . . . 9
|
66 | 65 | reximdva 3017 |
. . . . . . . 8
|
67 | 13, 66 | mpd 15 |
. . . . . . 7
|
68 | | stoweidlem60.1 |
. . . . . . . 8
|
69 | | stoweidlem60.8 |
. . . . . . . 8
|
70 | | stoweidlem60.9 |
. . . . . . . 8
|
71 | 68, 14, 24, 69, 25, 70, 26, 27 | rfcnnnub 39195 |
. . . . . . 7
|
72 | 67, 71 | r19.29a 3078 |
. . . . . 6
|
73 | | df-rex 2918 |
. . . . . 6
|
74 | 72, 73 | sylib 208 |
. . . . 5
|
75 | | simpr 477 |
. . . . . . . . 9
|
76 | 14, 19 | nfan 1828 |
. . . . . . . . . . 11
|
77 | | stoweidlem60.6 |
. . . . . . . . . . 11
|
78 | | stoweidlem60.7 |
. . . . . . . . . . 11
|
79 | | eqid 2622 |
. . . . . . . . . . 11
|
80 | | eqid 2622 |
. . . . . . . . . . 11
|
81 | 69 | adantr 481 |
. . . . . . . . . . 11
|
82 | | stoweidlem60.10 |
. . . . . . . . . . . 12
|
83 | 82 | adantr 481 |
. . . . . . . . . . 11
|
84 | | stoweidlem60.11 |
. . . . . . . . . . . 12
|
85 | 84 | 3adant1r 1319 |
. . . . . . . . . . 11
|
86 | | stoweidlem60.12 |
. . . . . . . . . . . 12
|
87 | 86 | 3adant1r 1319 |
. . . . . . . . . . 11
|
88 | | stoweidlem60.13 |
. . . . . . . . . . . 12
|
89 | 88 | adantlr 751 |
. . . . . . . . . . 11
|
90 | | stoweidlem60.14 |
. . . . . . . . . . . 12
|
91 | 90 | adantlr 751 |
. . . . . . . . . . 11
|
92 | 27 | adantr 481 |
. . . . . . . . . . 11
|
93 | 3 | adantr 481 |
. . . . . . . . . . 11
|
94 | | stoweidlem60.18 |
. . . . . . . . . . . 12
|
95 | 94 | adantr 481 |
. . . . . . . . . . 11
|
96 | | simpr 477 |
. . . . . . . . . . 11
|
97 | 68, 76, 24, 25, 26, 77, 78, 79, 80, 81, 83, 85, 87, 89, 91, 92, 93, 95, 96 | stoweidlem59 40276 |
. . . . . . . . . 10
|
98 | 97 | adantrr 753 |
. . . . . . . . 9
|
99 | | 19.42v 1918 |
. . . . . . . . 9
|
100 | 75, 98, 99 | sylanbrc 698 |
. . . . . . . 8
|
101 | | 3anass 1042 |
. . . . . . . . 9
|
102 | 101 | exbii 1774 |
. . . . . . . 8
|
103 | 100, 102 | sylibr 224 |
. . . . . . 7
|
104 | 103 | ex 450 |
. . . . . 6
|
105 | 104 | eximdv 1846 |
. . . . 5
|
106 | 74, 105 | mpd 15 |
. . . 4
|
107 | | simpl 473 |
. . . . . . . 8
|
108 | | simpr1l 1118 |
. . . . . . . 8
|
109 | | simpr2 1068 |
. . . . . . . 8
|
110 | | nfv 1843 |
. . . . . . . . . 10
|
111 | 14, 19, 110 | nf3an 1831 |
. . . . . . . . 9
|
112 | | simp2 1062 |
. . . . . . . . 9
|
113 | | simp3 1063 |
. . . . . . . . 9
|
114 | | simp1 1061 |
. . . . . . . . . 10
|
115 | 114, 84 | syl3an1 1359 |
. . . . . . . . 9
|
116 | 114, 86 | syl3an1 1359 |
. . . . . . . . 9
|
117 | 88 | 3ad2antl1 1223 |
. . . . . . . . 9
|
118 | 3 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
119 | 118 | rpred 11872 |
. . . . . . . . 9
|
120 | 82 | sselda 3603 |
. . . . . . . . . . 11
|
121 | 24, 25, 26, 120 | fcnre 39184 |
. . . . . . . . . 10
|
122 | 121 | 3ad2antl1 1223 |
. . . . . . . . 9
|
123 | 111, 112,
113, 115, 116, 117, 119, 122 | stoweidlem17 40234 |
. . . . . . . 8
|
124 | 107, 108,
109, 123 | syl3anc 1326 |
. . . . . . 7
|
125 | | nfv 1843 |
. . . . . . . . 9
|
126 | | nfv 1843 |
. . . . . . . . . 10
|
127 | | nfv 1843 |
. . . . . . . . . 10
|
128 | | nfra1 2941 |
. . . . . . . . . 10
|
129 | 126, 127,
128 | nf3an 1831 |
. . . . . . . . 9
|
130 | 125, 129 | nfan 1828 |
. . . . . . . 8
|
131 | | nfra1 2941 |
. . . . . . . . . . 11
|
132 | 19, 131 | nfan 1828 |
. . . . . . . . . 10
|
133 | | nfcv 2764 |
. . . . . . . . . . 11
|
134 | | nfra1 2941 |
. . . . . . . . . . . 12
|
135 | | nfra1 2941 |
. . . . . . . . . . . 12
|
136 | | nfra1 2941 |
. . . . . . . . . . . 12
|
137 | 134, 135,
136 | nf3an 1831 |
. . . . . . . . . . 11
|
138 | 133, 137 | nfral 2945 |
. . . . . . . . . 10
|
139 | 132, 110,
138 | nf3an 1831 |
. . . . . . . . 9
|
140 | 14, 139 | nfan 1828 |
. . . . . . . 8
|
141 | | eqid 2622 |
. . . . . . . 8
|
142 | | uniexg 6955 |
. . . . . . . . . . 11
|
143 | 69, 142 | syl 17 |
. . . . . . . . . 10
|
144 | 25, 143 | syl5eqel 2705 |
. . . . . . . . 9
|
145 | 144 | adantr 481 |
. . . . . . . 8
|
146 | 28 | adantr 481 |
. . . . . . . 8
|
147 | | stoweidlem60.16 |
. . . . . . . . . 10
|
148 | 147 | r19.21bi 2932 |
. . . . . . . . 9
|
149 | 148 | adantlr 751 |
. . . . . . . 8
|
150 | | simpr1r 1119 |
. . . . . . . . 9
|
151 | 150 | r19.21bi 2932 |
. . . . . . . 8
|
152 | 3 | adantr 481 |
. . . . . . . 8
|
153 | 94 | adantr 481 |
. . . . . . . 8
|
154 | | simpll 790 |
. . . . . . . . 9
|
155 | | simplr2 1104 |
. . . . . . . . 9
|
156 | | simpr 477 |
. . . . . . . . 9
|
157 | | simp1 1061 |
. . . . . . . . . 10
|
158 | | ffvelrn 6357 |
. . . . . . . . . . 11
|
159 | 158 | 3adant1 1079 |
. . . . . . . . . 10
|
160 | 82 | sselda 3603 |
. . . . . . . . . . 11
|
161 | 24, 25, 26, 160 | fcnre 39184 |
. . . . . . . . . 10
|
162 | 157, 159,
161 | syl2anc 693 |
. . . . . . . . 9
|
163 | 154, 155,
156, 162 | syl3anc 1326 |
. . . . . . . 8
|
164 | | simp1r3 1159 |
. . . . . . . . . 10
|
165 | | r19.26-3 3066 |
. . . . . . . . . . 11
|
166 | 165 | simp1bi 1076 |
. . . . . . . . . 10
|
167 | | simpl 473 |
. . . . . . . . . . 11
|
168 | 167 | 2ralimi 2953 |
. . . . . . . . . 10
|
169 | 164, 166,
168 | 3syl 18 |
. . . . . . . . 9
|
170 | | simp2 1062 |
. . . . . . . . 9
|
171 | | simp3 1063 |
. . . . . . . . 9
|
172 | | rspa 2930 |
. . . . . . . . . 10
|
173 | 172 | r19.21bi 2932 |
. . . . . . . . 9
|
174 | 169, 170,
171, 173 | syl21anc 1325 |
. . . . . . . 8
|
175 | | simpr 477 |
. . . . . . . . . . 11
|
176 | 175 | 2ralimi 2953 |
. . . . . . . . . 10
|
177 | 164, 166,
176 | 3syl 18 |
. . . . . . . . 9
|
178 | | rspa 2930 |
. . . . . . . . . 10
|
179 | 178 | r19.21bi 2932 |
. . . . . . . . 9
|
180 | 177, 170,
171, 179 | syl21anc 1325 |
. . . . . . . 8
|
181 | | simp1r3 1159 |
. . . . . . . . . 10
|
182 | 165 | simp2bi 1077 |
. . . . . . . . . 10
|
183 | 181, 182 | syl 17 |
. . . . . . . . 9
|
184 | | simp2 1062 |
. . . . . . . . 9
|
185 | | simp3 1063 |
. . . . . . . . 9
|
186 | | rspa 2930 |
. . . . . . . . . 10
|
187 | 186 | r19.21bi 2932 |
. . . . . . . . 9
|
188 | 183, 184,
185, 187 | syl21anc 1325 |
. . . . . . . 8
|
189 | | simp1r3 1159 |
. . . . . . . . . 10
|
190 | 165 | simp3bi 1078 |
. . . . . . . . . 10
|
191 | 189, 190 | syl 17 |
. . . . . . . . 9
|
192 | | simp2 1062 |
. . . . . . . . 9
|
193 | | simp3 1063 |
. . . . . . . . 9
|
194 | | rspa 2930 |
. . . . . . . . . 10
|
195 | 194 | r19.21bi 2932 |
. . . . . . . . 9
|
196 | 191, 192,
193, 195 | syl21anc 1325 |
. . . . . . . 8
|
197 | 68, 130, 140, 77, 78, 141, 108, 145, 146, 149, 151, 152, 153, 163, 174, 180, 188, 196 | stoweidlem34 40251 |
. . . . . . 7
|
198 | | nfmpt1 4747 |
. . . . . . . . . 10
|
199 | 198 | nfeq2 2780 |
. . . . . . . . 9
|
200 | | fveq1 6190 |
. . . . . . . . . . . . 13
|
201 | 200 | breq1d 4663 |
. . . . . . . . . . . 12
|
202 | 200 | breq2d 4665 |
. . . . . . . . . . . 12
|
203 | 201, 202 | anbi12d 747 |
. . . . . . . . . . 11
|
204 | 203 | anbi2d 740 |
. . . . . . . . . 10
|
205 | 204 | rexbidv 3052 |
. . . . . . . . 9
|
206 | 199, 205 | ralbid 2983 |
. . . . . . . 8
|
207 | 206 | rspcev 3309 |
. . . . . . 7
|
208 | 124, 197,
207 | syl2anc 693 |
. . . . . 6
|
209 | 208 | ex 450 |
. . . . 5
|
210 | 209 | 2eximdv 1848 |
. . . 4
|
211 | 106, 210 | mpd 15 |
. . 3
|
212 | | idd 24 |
. . . 4
|
213 | 212 | exlimdv 1861 |
. . 3
|
214 | 211, 213 | mpd 15 |
. 2
|
215 | | idd 24 |
. . 3
|
216 | 215 | exlimdv 1861 |
. 2
|
217 | 214, 216 | mpd 15 |
1
|