Step | Hyp | Ref
| Expression |
1 | | fmul01lt1lem2.1 |
. . 3
|
2 | | fmul01lt1lem2.2 |
. . . 4
|
3 | | nfv 1843 |
. . . 4
|
4 | 2, 3 | nfan 1828 |
. . 3
|
5 | | fmul01lt1lem2.3 |
. . 3
|
6 | | fmul01lt1lem2.4 |
. . . 4
|
7 | 6 | adantr 481 |
. . 3
|
8 | | fmul01lt1lem2.5 |
. . . 4
|
9 | 8 | adantr 481 |
. . 3
|
10 | | fmul01lt1lem2.6 |
. . . 4
|
11 | 10 | adantlr 751 |
. . 3
|
12 | | fmul01lt1lem2.7 |
. . . 4
|
13 | 12 | adantlr 751 |
. . 3
|
14 | | fmul01lt1lem2.8 |
. . . 4
|
15 | 14 | adantlr 751 |
. . 3
|
16 | | fmul01lt1lem2.9 |
. . . 4
|
17 | 16 | adantr 481 |
. . 3
|
18 | | simpr 477 |
. . . . 5
|
19 | 18 | fveq2d 6195 |
. . . 4
|
20 | | fmul01lt1lem2.11 |
. . . . 5
|
21 | 20 | adantr 481 |
. . . 4
|
22 | 19, 21 | eqbrtrrd 4677 |
. . 3
|
23 | 1, 4, 5, 7, 9, 11,
13, 15, 17, 22 | fmul01lt1lem1 39816 |
. 2
|
24 | 5 | fveq1i 6192 |
. . 3
|
25 | | nfv 1843 |
. . . . . . . . 9
|
26 | 2, 25 | nfan 1828 |
. . . . . . . 8
|
27 | | nfcv 2764 |
. . . . . . . . . 10
|
28 | 1, 27 | nffv 6198 |
. . . . . . . . 9
|
29 | 28 | nfel1 2779 |
. . . . . . . 8
|
30 | 26, 29 | nfim 1825 |
. . . . . . 7
|
31 | | eleq1 2689 |
. . . . . . . . 9
|
32 | 31 | anbi2d 740 |
. . . . . . . 8
|
33 | | fveq2 6191 |
. . . . . . . . 9
|
34 | 33 | eleq1d 2686 |
. . . . . . . 8
|
35 | 32, 34 | imbi12d 334 |
. . . . . . 7
|
36 | 30, 35, 10 | chvar 2262 |
. . . . . 6
|
37 | | remulcl 10021 |
. . . . . . 7
|
38 | 37 | adantl 482 |
. . . . . 6
|
39 | 8, 36, 38 | seqcl 12821 |
. . . . 5
|
40 | 39 | adantr 481 |
. . . 4
|
41 | | fmul01lt1lem2.10 |
. . . . . . 7
|
42 | | elfzuz3 12339 |
. . . . . . 7
|
43 | 41, 42 | syl 17 |
. . . . . 6
|
44 | | nfv 1843 |
. . . . . . . . 9
|
45 | 2, 44 | nfan 1828 |
. . . . . . . 8
|
46 | 45, 29 | nfim 1825 |
. . . . . . 7
|
47 | | eleq1 2689 |
. . . . . . . . 9
|
48 | 47 | anbi2d 740 |
. . . . . . . 8
|
49 | 48, 34 | imbi12d 334 |
. . . . . . 7
|
50 | 6 | adantr 481 |
. . . . . . . . . 10
|
51 | | eluzelz 11697 |
. . . . . . . . . . . 12
|
52 | 8, 51 | syl 17 |
. . . . . . . . . . 11
|
53 | 52 | adantr 481 |
. . . . . . . . . 10
|
54 | | elfzelz 12342 |
. . . . . . . . . . 11
|
55 | 54 | adantl 482 |
. . . . . . . . . 10
|
56 | 50, 53, 55 | 3jca 1242 |
. . . . . . . . 9
|
57 | 6 | zred 11482 |
. . . . . . . . . . . 12
|
58 | 57 | adantr 481 |
. . . . . . . . . . 11
|
59 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
|
60 | 41, 59 | syl 17 |
. . . . . . . . . . . . 13
|
61 | 60 | zred 11482 |
. . . . . . . . . . . 12
|
62 | 61 | adantr 481 |
. . . . . . . . . . 11
|
63 | 54 | zred 11482 |
. . . . . . . . . . . 12
|
64 | 63 | adantl 482 |
. . . . . . . . . . 11
|
65 | | elfzle1 12344 |
. . . . . . . . . . . . 13
|
66 | 41, 65 | syl 17 |
. . . . . . . . . . . 12
|
67 | 66 | adantr 481 |
. . . . . . . . . . 11
|
68 | | elfzle1 12344 |
. . . . . . . . . . . 12
|
69 | 68 | adantl 482 |
. . . . . . . . . . 11
|
70 | 58, 62, 64, 67, 69 | letrd 10194 |
. . . . . . . . . 10
|
71 | | elfzle2 12345 |
. . . . . . . . . . 11
|
72 | 71 | adantl 482 |
. . . . . . . . . 10
|
73 | 70, 72 | jca 554 |
. . . . . . . . 9
|
74 | | elfz2 12333 |
. . . . . . . . 9
|
75 | 56, 73, 74 | sylanbrc 698 |
. . . . . . . 8
|
76 | 75, 10 | syldan 487 |
. . . . . . 7
|
77 | 46, 49, 76 | chvar 2262 |
. . . . . 6
|
78 | 43, 77, 38 | seqcl 12821 |
. . . . 5
|
79 | 78 | adantr 481 |
. . . 4
|
80 | 16 | rpred 11872 |
. . . . 5
|
81 | 80 | adantr 481 |
. . . 4
|
82 | | remulcl 10021 |
. . . . . . . . 9
|
83 | 82 | adantl 482 |
. . . . . . . 8
|
84 | | simp1 1061 |
. . . . . . . . . . 11
|
85 | 84 | recnd 10068 |
. . . . . . . . . 10
|
86 | | simp2 1062 |
. . . . . . . . . . 11
|
87 | 86 | recnd 10068 |
. . . . . . . . . 10
|
88 | | simp3 1063 |
. . . . . . . . . . 11
|
89 | 88 | recnd 10068 |
. . . . . . . . . 10
|
90 | 85, 87, 89 | mulassd 10063 |
. . . . . . . . 9
|
91 | 90 | adantl 482 |
. . . . . . . 8
|
92 | 60 | zcnd 11483 |
. . . . . . . . . . . 12
|
93 | | 1cnd 10056 |
. . . . . . . . . . . 12
|
94 | 92, 93 | npcand 10396 |
. . . . . . . . . . 11
|
95 | 94 | fveq2d 6195 |
. . . . . . . . . 10
|
96 | 43, 95 | eleqtrrd 2704 |
. . . . . . . . 9
|
97 | 96 | adantr 481 |
. . . . . . . 8
|
98 | 6 | adantr 481 |
. . . . . . . . 9
|
99 | 60 | adantr 481 |
. . . . . . . . . 10
|
100 | | 1zzd 11408 |
. . . . . . . . . 10
|
101 | 99, 100 | zsubcld 11487 |
. . . . . . . . 9
|
102 | | simpr 477 |
. . . . . . . . . . . 12
|
103 | | eqcom 2629 |
. . . . . . . . . . . 12
|
104 | 102, 103 | sylnib 318 |
. . . . . . . . . . 11
|
105 | 57, 61 | leloed 10180 |
. . . . . . . . . . . . 13
|
106 | 66, 105 | mpbid 222 |
. . . . . . . . . . . 12
|
107 | 106 | adantr 481 |
. . . . . . . . . . 11
|
108 | | orel2 398 |
. . . . . . . . . . 11
|
109 | 104, 107,
108 | sylc 65 |
. . . . . . . . . 10
|
110 | | zltlem1 11430 |
. . . . . . . . . . . 12
|
111 | 6, 60, 110 | syl2anc 693 |
. . . . . . . . . . 11
|
112 | 111 | adantr 481 |
. . . . . . . . . 10
|
113 | 109, 112 | mpbid 222 |
. . . . . . . . 9
|
114 | | eluz2 11693 |
. . . . . . . . 9
|
115 | 98, 101, 113, 114 | syl3anbrc 1246 |
. . . . . . . 8
|
116 | | nfv 1843 |
. . . . . . . . . . . 12
|
117 | 2, 116 | nfan 1828 |
. . . . . . . . . . 11
|
118 | 117, 25 | nfan 1828 |
. . . . . . . . . 10
|
119 | 118, 29 | nfim 1825 |
. . . . . . . . 9
|
120 | 31 | anbi2d 740 |
. . . . . . . . . 10
|
121 | 120, 34 | imbi12d 334 |
. . . . . . . . 9
|
122 | 10 | adantlr 751 |
. . . . . . . . 9
|
123 | 119, 121,
122 | chvar 2262 |
. . . . . . . 8
|
124 | 83, 91, 97, 115, 123 | seqsplit 12834 |
. . . . . . 7
|
125 | 94 | adantr 481 |
. . . . . . . . . 10
|
126 | 125 | seqeq1d 12807 |
. . . . . . . . 9
|
127 | 126 | fveq1d 6193 |
. . . . . . . 8
|
128 | 127 | oveq2d 6666 |
. . . . . . 7
|
129 | 124, 128 | eqtrd 2656 |
. . . . . 6
|
130 | | nfv 1843 |
. . . . . . . . . . 11
|
131 | 117, 130 | nfan 1828 |
. . . . . . . . . 10
|
132 | 131, 29 | nfim 1825 |
. . . . . . . . 9
|
133 | | eleq1 2689 |
. . . . . . . . . . 11
|
134 | 133 | anbi2d 740 |
. . . . . . . . . 10
|
135 | 134, 34 | imbi12d 334 |
. . . . . . . . 9
|
136 | 6 | adantr 481 |
. . . . . . . . . . . . 13
|
137 | 52 | adantr 481 |
. . . . . . . . . . . . 13
|
138 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
|
139 | 138 | adantl 482 |
. . . . . . . . . . . . 13
|
140 | 136, 137,
139 | 3jca 1242 |
. . . . . . . . . . . 12
|
141 | | elfzle1 12344 |
. . . . . . . . . . . . . 14
|
142 | 141 | adantl 482 |
. . . . . . . . . . . . 13
|
143 | 138 | zred 11482 |
. . . . . . . . . . . . . . 15
|
144 | 143 | adantl 482 |
. . . . . . . . . . . . . 14
|
145 | 61 | adantr 481 |
. . . . . . . . . . . . . 14
|
146 | 52 | zred 11482 |
. . . . . . . . . . . . . . 15
|
147 | 146 | adantr 481 |
. . . . . . . . . . . . . 14
|
148 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
|
149 | 61, 148 | resubcld 10458 |
. . . . . . . . . . . . . . . 16
|
150 | 149 | adantr 481 |
. . . . . . . . . . . . . . 15
|
151 | | elfzle2 12345 |
. . . . . . . . . . . . . . . 16
|
152 | 151 | adantl 482 |
. . . . . . . . . . . . . . 15
|
153 | 61 | lem1d 10957 |
. . . . . . . . . . . . . . . 16
|
154 | 153 | adantr 481 |
. . . . . . . . . . . . . . 15
|
155 | 144, 150,
145, 152, 154 | letrd 10194 |
. . . . . . . . . . . . . 14
|
156 | | elfzle2 12345 |
. . . . . . . . . . . . . . . 16
|
157 | 41, 156 | syl 17 |
. . . . . . . . . . . . . . 15
|
158 | 157 | adantr 481 |
. . . . . . . . . . . . . 14
|
159 | 144, 145,
147, 155, 158 | letrd 10194 |
. . . . . . . . . . . . 13
|
160 | 142, 159 | jca 554 |
. . . . . . . . . . . 12
|
161 | 140, 160,
74 | sylanbrc 698 |
. . . . . . . . . . 11
|
162 | 161, 10 | syldan 487 |
. . . . . . . . . 10
|
163 | 162 | adantlr 751 |
. . . . . . . . 9
|
164 | 132, 135,
163 | chvar 2262 |
. . . . . . . 8
|
165 | 37 | adantl 482 |
. . . . . . . 8
|
166 | 115, 164,
165 | seqcl 12821 |
. . . . . . 7
|
167 | | 1red 10055 |
. . . . . . 7
|
168 | | eqid 2622 |
. . . . . . . . 9
|
169 | 43 | adantr 481 |
. . . . . . . . 9
|
170 | | eluzfz2 12349 |
. . . . . . . . . . 11
|
171 | 43, 170 | syl 17 |
. . . . . . . . . 10
|
172 | 171 | adantr 481 |
. . . . . . . . 9
|
173 | 76 | adantlr 751 |
. . . . . . . . 9
|
174 | 75, 12 | syldan 487 |
. . . . . . . . . 10
|
175 | 174 | adantlr 751 |
. . . . . . . . 9
|
176 | 75, 14 | syldan 487 |
. . . . . . . . . 10
|
177 | 176 | adantlr 751 |
. . . . . . . . 9
|
178 | 1, 117, 168, 99, 169, 172, 173, 175, 177 | fmul01 39812 |
. . . . . . . 8
|
179 | 178 | simpld 475 |
. . . . . . 7
|
180 | | eqid 2622 |
. . . . . . . . 9
|
181 | 8 | adantr 481 |
. . . . . . . . 9
|
182 | | 1zzd 11408 |
. . . . . . . . . . . . 13
|
183 | 60, 182 | zsubcld 11487 |
. . . . . . . . . . . 12
|
184 | 6, 52, 183 | 3jca 1242 |
. . . . . . . . . . 11
|
185 | 184 | adantr 481 |
. . . . . . . . . 10
|
186 | 149, 61, 146 | 3jca 1242 |
. . . . . . . . . . . . 13
|
187 | 186 | adantr 481 |
. . . . . . . . . . . 12
|
188 | 61 | adantr 481 |
. . . . . . . . . . . . . 14
|
189 | 188 | lem1d 10957 |
. . . . . . . . . . . . 13
|
190 | 157 | adantr 481 |
. . . . . . . . . . . . 13
|
191 | 189, 190 | jca 554 |
. . . . . . . . . . . 12
|
192 | | letr 10131 |
. . . . . . . . . . . 12
|
193 | 187, 191,
192 | sylc 65 |
. . . . . . . . . . 11
|
194 | 113, 193 | jca 554 |
. . . . . . . . . 10
|
195 | | elfz2 12333 |
. . . . . . . . . 10
|
196 | 185, 194,
195 | sylanbrc 698 |
. . . . . . . . 9
|
197 | 12 | adantlr 751 |
. . . . . . . . 9
|
198 | 14 | adantlr 751 |
. . . . . . . . 9
|
199 | 1, 117, 180, 98, 181, 196, 122, 197, 198 | fmul01 39812 |
. . . . . . . 8
|
200 | 199 | simprd 479 |
. . . . . . 7
|
201 | 166, 167,
79, 179, 200 | lemul1ad 10963 |
. . . . . 6
|
202 | 129, 201 | eqbrtrd 4675 |
. . . . 5
|
203 | 79 | recnd 10068 |
. . . . . 6
|
204 | 203 | mulid2d 10058 |
. . . . 5
|
205 | 202, 204 | breqtrd 4679 |
. . . 4
|
206 | 1, 2, 168, 60, 43, 76, 174, 176, 16, 20 | fmul01lt1lem1 39816 |
. . . . 5
|
207 | 206 | adantr 481 |
. . . 4
|
208 | 40, 79, 81, 205, 207 | lelttrd 10195 |
. . 3
|
209 | 24, 208 | syl5eqbr 4688 |
. 2
|
210 | 23, 209 | pm2.61dan 832 |
1
|