Step | Hyp | Ref
| Expression |
1 | | simpr 463 |
. . . . 5
 
   |
2 | 1 | fveq2d 5869 |
. . . 4
 
           |
3 | | fmul01lt1lem1.3 |
. . . . . 6
    |
4 | 3 | a1i 11 |
. . . . 5
 
      |
5 | 4 | fveq1d 5867 |
. . . 4
 
    
        |
6 | | fmul01lt1lem1.4 |
. . . . . 6
   |
7 | | seq1 12226 |
. . . . . 6
             |
8 | 6, 7 | syl 17 |
. . . . 5
             |
9 | 8 | adantr 467 |
. . . 4
 
             |
10 | 2, 5, 9 | 3eqtrd 2489 |
. . 3
 
           |
11 | | fmul01lt1lem1.10 |
. . . 4
    
  |
12 | 11 | adantr 467 |
. . 3
 
       |
13 | 10, 12 | eqbrtrd 4423 |
. 2
 
       |
14 | | simpr 463 |
. . . . 5
 

  |
15 | 14 | neqned 2631 |
. . . 4
 
   |
16 | 6 | zred 11040 |
. . . . . . 7
   |
17 | | fmul01lt1lem1.5 |
. . . . . . . . 9
       |
18 | | eluzelz 11168 |
. . . . . . . . 9
    
  |
19 | 17, 18 | syl 17 |
. . . . . . . 8
   |
20 | 19 | zred 11040 |
. . . . . . 7
   |
21 | | eluzle 11171 |
. . . . . . . 8
    
  |
22 | 17, 21 | syl 17 |
. . . . . . 7

  |
23 | 16, 20, 22 | 3jca 1188 |
. . . . . 6
     |
24 | 23 | adantr 467 |
. . . . 5
 
 
   |
25 | | leltne 9723 |
. . . . 5
 
 
   |
26 | 24, 25 | syl 17 |
. . . 4
 
 
   |
27 | 15, 26 | mpbird 236 |
. . 3
 
   |
28 | 3 | fveq1i 5866 |
. . . 4
           |
29 | | remulcl 9624 |
. . . . . . 7
 
     |
30 | 29 | adantl 468 |
. . . . . 6
    
 
    |
31 | | recn 9629 |
. . . . . . . . 9
   |
32 | 31 | 3ad2ant1 1029 |
. . . . . . . 8
 
   |
33 | | recn 9629 |
. . . . . . . . 9
   |
34 | 33 | 3ad2ant2 1030 |
. . . . . . . 8
 
   |
35 | | recn 9629 |
. . . . . . . . 9
   |
36 | 35 | 3ad2ant3 1031 |
. . . . . . . 8
 
   |
37 | 32, 34, 36 | mulassd 9666 |
. . . . . . 7
 
           |
38 | 37 | adantl 468 |
. . . . . 6
    
            |
39 | | simpr 463 |
. . . . . . . . . 10
 

  |
40 | 39 | olcd 395 |
. . . . . . . . 9
 

    |
41 | 20, 16 | jca 535 |
. . . . . . . . . . 11
     |
42 | 41 | adantr 467 |
. . . . . . . . . 10
 

    |
43 | | lttri2 9716 |
. . . . . . . . . 10
 
       |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
 

      |
45 | 40, 44 | mpbird 236 |
. . . . . . . 8
 

  |
46 | 45 | neneqd 2629 |
. . . . . . 7
 

  |
47 | | uzp1 11192 |
. . . . . . . . . 10
    

         |
48 | 17, 47 | syl 17 |
. . . . . . . . 9
           |
49 | 48 | adantr 467 |
. . . . . . . 8
 


         |
50 | 49 | ord 379 |
. . . . . . 7
 


   
     |
51 | 46, 50 | mpd 15 |
. . . . . 6
 

        |
52 | 6 | adantr 467 |
. . . . . . 7
 

  |
53 | | uzid 11173 |
. . . . . . 7
       |
54 | 52, 53 | syl 17 |
. . . . . 6
 

      |
55 | | fmul01lt1lem1.2 |
. . . . . . . . . 10
   |
56 | | nfv 1761 |
. . . . . . . . . 10
      |
57 | 55, 56 | nfan 2011 |
. . . . . . . . 9
         |
58 | | fmul01lt1lem1.1 |
. . . . . . . . . . 11
   |
59 | | nfcv 2592 |
. . . . . . . . . . 11
   |
60 | 58, 59 | nffv 5872 |
. . . . . . . . . 10
       |
61 | 60 | nfel1 2606 |
. . . . . . . . 9
       |
62 | 57, 61 | nfim 2003 |
. . . . . . . 8
   
           |
63 | | eleq1 2517 |
. . . . . . . . . 10
     
       |
64 | 63 | anbi2d 710 |
. . . . . . . . 9
  
    
         |
65 | | fveq2 5865 |
. . . . . . . . . 10
           |
66 | 65 | eleq1d 2513 |
. . . . . . . . 9
     
       |
67 | 64, 66 | imbi12d 322 |
. . . . . . . 8
   
           
             |
68 | | fmul01lt1lem1.6 |
. . . . . . . 8
 
    
      |
69 | 62, 67, 68 | chvar 2106 |
. . . . . . 7
 
    
      |
70 | 69 | adantlr 721 |
. . . . . 6
               |
71 | 30, 38, 51, 54, 70 | seqsplit 12246 |
. . . . 5
 

                        |
72 | | eluzfz1 11806 |
. . . . . . . . . . 11
    
      |
73 | 17, 72 | syl 17 |
. . . . . . . . . 10
       |
74 | 73 | ancli 554 |
. . . . . . . . . 10
         |
75 | | nfv 1761 |
. . . . . . . . . . . . 13
      |
76 | 55, 75 | nfan 2011 |
. . . . . . . . . . . 12
         |
77 | | nfcv 2592 |
. . . . . . . . . . . . . 14
   |
78 | 58, 77 | nffv 5872 |
. . . . . . . . . . . . 13
       |
79 | 78 | nfel1 2606 |
. . . . . . . . . . . 12
       |
80 | 76, 79 | nfim 2003 |
. . . . . . . . . . 11
   
           |
81 | | eleq1 2517 |
. . . . . . . . . . . . 13
     
       |
82 | 81 | anbi2d 710 |
. . . . . . . . . . . 12
  
    
         |
83 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
84 | 83 | eleq1d 2513 |
. . . . . . . . . . . 12
     
       |
85 | 82, 84 | imbi12d 322 |
. . . . . . . . . . 11
   
           
             |
86 | 80, 85, 68 | vtoclg1f 3106 |
. . . . . . . . . 10
      
            |
87 | 73, 74, 86 | sylc 62 |
. . . . . . . . 9
       |
88 | 8, 87 | eqeltrd 2529 |
. . . . . . . 8
         |
89 | 88 | adantr 467 |
. . . . . . 7
 

        |
90 | 6 | adantr 467 |
. . . . . . . . . . . 12
 
         |
91 | 19 | adantr 467 |
. . . . . . . . . . . 12
 
         |
92 | | elfzelz 11800 |
. . . . . . . . . . . . 13
         |
93 | 92 | adantl 468 |
. . . . . . . . . . . 12
 
         |
94 | 90, 91, 93 | 3jca 1188 |
. . . . . . . . . . 11
 
       
   |
95 | 16 | adantr 467 |
. . . . . . . . . . . . 13
 
         |
96 | | peano2re 9806 |
. . . . . . . . . . . . . . 15
 
   |
97 | 16, 96 | syl 17 |
. . . . . . . . . . . . . 14
     |
98 | 97 | adantr 467 |
. . . . . . . . . . . . 13
 
       
   |
99 | 92 | zred 11040 |
. . . . . . . . . . . . . 14
         |
100 | 99 | adantl 468 |
. . . . . . . . . . . . 13
 
         |
101 | 16 | lep1d 10538 |
. . . . . . . . . . . . . 14

    |
102 | 101 | adantr 467 |
. . . . . . . . . . . . 13
 
           |
103 | | elfzle1 11802 |
. . . . . . . . . . . . . 14
       
   |
104 | 103 | adantl 468 |
. . . . . . . . . . . . 13
 
       
   |
105 | 95, 98, 100, 102, 104 | letrd 9792 |
. . . . . . . . . . . 12
 
         |
106 | | elfzle2 11803 |
. . . . . . . . . . . . 13
         |
107 | 106 | adantl 468 |
. . . . . . . . . . . 12
 
         |
108 | 105, 107 | jca 535 |
. . . . . . . . . . 11
 
           |
109 | | elfz2 11791 |
. . . . . . . . . . 11
    
 
      |
110 | 94, 108, 109 | sylanbrc 670 |
. . . . . . . . . 10
 
             |
111 | 110, 69 | syldan 473 |
. . . . . . . . 9
 
             |
112 | 111 | adantlr 721 |
. . . . . . . 8
                 |
113 | 51, 112, 30 | seqcl 12233 |
. . . . . . 7
 

 
        |
114 | 89, 113 | remulcld 9671 |
. . . . . 6
 

                  |
115 | | fmul01lt1lem1.9 |
. . . . . . . 8
   |
116 | 115 | rpred 11341 |
. . . . . . 7
   |
117 | 116 | adantr 467 |
. . . . . 6
 

  |
118 | | 1red 9658 |
. . . . . . . 8
 

  |
119 | | nfcv 2592 |
. . . . . . . . . . . . . 14
   |
120 | | nfcv 2592 |
. . . . . . . . . . . . . 14
  |
121 | 119, 120,
78 | nfbr 4447 |
. . . . . . . . . . . . 13
 
     |
122 | 76, 121 | nfim 2003 |
. . . . . . . . . . . 12
   
    
      |
123 | 83 | breq2d 4414 |
. . . . . . . . . . . . 13
 
   
       |
124 | 82, 123 | imbi12d 322 |
. . . . . . . . . . . 12
   
    
    
      
        |
125 | | fmul01lt1lem1.7 |
. . . . . . . . . . . 12
 
    
      |
126 | 122, 124,
125 | vtoclg1f 3106 |
. . . . . . . . . . 11
      
            |
127 | 73, 74, 126 | sylc 62 |
. . . . . . . . . 10

      |
128 | 127, 8 | breqtrrd 4429 |
. . . . . . . . 9

        |
129 | 128 | adantr 467 |
. . . . . . . 8
 

        |
130 | | nfv 1761 |
. . . . . . . . . . 11
  |
131 | 55, 130 | nfan 2011 |
. . . . . . . . . 10
     |
132 | | eqid 2451 |
. . . . . . . . . 10
 
    
    |
133 | 6 | peano2zd 11043 |
. . . . . . . . . . 11
     |
134 | 133 | adantr 467 |
. . . . . . . . . 10
 

    |
135 | 16 | adantr 467 |
. . . . . . . . . . . . 13
 

  |
136 | 135, 39 | gtned 9770 |
. . . . . . . . . . . 12
 

  |
137 | 136 | neneqd 2629 |
. . . . . . . . . . 11
 

  |
138 | 17 | adantr 467 |
. . . . . . . . . . . 12
 

      |
139 | 138, 47 | syl 17 |
. . . . . . . . . . 11
 


         |
140 | | orel1 384 |
. . . . . . . . . . 11
         
         |
141 | 137, 139,
140 | sylc 62 |
. . . . . . . . . 10
 

        |
142 | 19 | adantr 467 |
. . . . . . . . . . . 12
 

  |
143 | 134, 142,
142 | 3jca 1188 |
. . . . . . . . . . 11
 

 
    |
144 | | zltp1le 10986 |
. . . . . . . . . . . . . 14
 
       |
145 | 52, 142, 144 | syl2anc 667 |
. . . . . . . . . . . . 13
 

      |
146 | 39, 145 | mpbid 214 |
. . . . . . . . . . . 12
 

    |
147 | 20 | adantr 467 |
. . . . . . . . . . . . 13
 

  |
148 | 147 | leidd 10180 |
. . . . . . . . . . . 12
 

  |
149 | 146, 148 | jca 535 |
. . . . . . . . . . 11
 

 
    |
150 | | elfz2 11791 |
. . . . . . . . . . 11
      
   
   
    |
151 | 143, 149,
150 | sylanbrc 670 |
. . . . . . . . . 10
 

        |
152 | 6 | adantr 467 |
. . . . . . . . . . . . . 14
 
         |
153 | 19 | adantr 467 |
. . . . . . . . . . . . . 14
 
         |
154 | | elfzelz 11800 |
. . . . . . . . . . . . . . 15
         |
155 | 154 | adantl 468 |
. . . . . . . . . . . . . 14
 
         |
156 | 152, 153,
155 | 3jca 1188 |
. . . . . . . . . . . . 13
 
       
   |
157 | 16 | adantr 467 |
. . . . . . . . . . . . . . 15
 
         |
158 | 157, 96 | syl 17 |
. . . . . . . . . . . . . . 15
 
       
   |
159 | 154 | zred 11040 |
. . . . . . . . . . . . . . . 16
         |
160 | 159 | adantl 468 |
. . . . . . . . . . . . . . 15
 
         |
161 | 101 | adantr 467 |
. . . . . . . . . . . . . . 15
 
           |
162 | | elfzle1 11802 |
. . . . . . . . . . . . . . . 16
       
   |
163 | 162 | adantl 468 |
. . . . . . . . . . . . . . 15
 
       
   |
164 | 157, 158,
160, 161, 163 | letrd 9792 |
. . . . . . . . . . . . . 14
 
         |
165 | | elfzle2 11803 |
. . . . . . . . . . . . . . 15
         |
166 | 165 | adantl 468 |
. . . . . . . . . . . . . 14
 
         |
167 | 164, 166 | jca 535 |
. . . . . . . . . . . . 13
 
           |
168 | | elfz2 11791 |
. . . . . . . . . . . . 13
    
 
      |
169 | 156, 167,
168 | sylanbrc 670 |
. . . . . . . . . . . 12
 
             |
170 | 169, 68 | syldan 473 |
. . . . . . . . . . 11
 
             |
171 | 170 | adantlr 721 |
. . . . . . . . . 10
                 |
172 | | simpll 760 |
. . . . . . . . . . 11
             |
173 | 6 | ad2antrr 732 |
. . . . . . . . . . . . 13
             |
174 | 19 | ad2antrr 732 |
. . . . . . . . . . . . 13
             |
175 | 154 | adantl 468 |
. . . . . . . . . . . . 13
             |
176 | 173, 174,
175 | 3jca 1188 |
. . . . . . . . . . . 12
           
   |
177 | 16 | ad2antrr 732 |
. . . . . . . . . . . . . 14
             |
178 | 97 | ad2antrr 732 |
. . . . . . . . . . . . . 14
           
   |
179 | 159 | adantl 468 |
. . . . . . . . . . . . . 14
             |
180 | 101 | ad2antrr 732 |
. . . . . . . . . . . . . 14
               |
181 | 162 | adantl 468 |
. . . . . . . . . . . . . 14
           
   |
182 | 177, 178,
179, 180, 181 | letrd 9792 |
. . . . . . . . . . . . 13
             |
183 | 165 | adantl 468 |
. . . . . . . . . . . . 13
             |
184 | 182, 183 | jca 535 |
. . . . . . . . . . . 12
               |
185 | 176, 184,
168 | sylanbrc 670 |
. . . . . . . . . . 11
                 |
186 | 172, 185,
125 | syl2anc 667 |
. . . . . . . . . 10
                 |
187 | | fmul01lt1lem1.8 |
. . . . . . . . . . 11
 
    
      |
188 | 172, 185,
187 | syl2anc 667 |
. . . . . . . . . 10
                 |
189 | 58, 131, 132, 134, 141, 151, 171, 186, 188 | fmul01 37658 |
. . . . . . . . 9
 

  
     
 
         |
190 | 189 | simprd 465 |
. . . . . . . 8
 

 
     
  |
191 | 113, 118,
89, 129, 190 | lemul2ad 10547 |
. . . . . . 7
 

                          |
192 | 88 | recnd 9669 |
. . . . . . . . 9
         |
193 | 192 | mulid1d 9660 |
. . . . . . . 8
                 |
194 | 193 | adantr 467 |
. . . . . . 7
 

                |
195 | 191, 194 | breqtrd 4427 |
. . . . . 6
 

                        |
196 | 8, 11 | eqbrtrd 4423 |
. . . . . . 7
         |
197 | 196 | adantr 467 |
. . . . . 6
 

     
  |
198 | 114, 89, 117, 195, 197 | lelttrd 9793 |
. . . . 5
 

                  |
199 | 71, 198 | eqbrtrd 4423 |
. . . 4
 

     
  |
200 | 28, 199 | syl5eqbr 4436 |
. . 3
 

      |
201 | 27, 200 | syldan 473 |
. 2
 
       |
202 | 13, 201 | pm2.61dan 800 |
1
    
  |