Step | Hyp | Ref
| Expression |
1 | | fmul01.6 |
. 2
       |
2 | | fveq2 5888 |
. . . . . 6
           |
3 | 2 | breq2d 4428 |
. . . . 5
 
   
       |
4 | 2 | breq1d 4426 |
. . . . 5
     
       |
5 | 3, 4 | anbi12d 722 |
. . . 4
          
         
    |
6 | 5 | imbi2d 322 |
. . 3
  
          
         
     |
7 | | fveq2 5888 |
. . . . . 6
           |
8 | 7 | breq2d 4428 |
. . . . 5
 
   
       |
9 | 7 | breq1d 4426 |
. . . . 5
     
       |
10 | 8, 9 | anbi12d 722 |
. . . 4
          
         
    |
11 | 10 | imbi2d 322 |
. . 3
  
          
         
     |
12 | | fveq2 5888 |
. . . . . 6
               |
13 | 12 | breq2d 4428 |
. . . . 5
   
   
         |
14 | 12 | breq1d 4426 |
. . . . 5
       
         |
15 | 13, 14 | anbi12d 722 |
. . . 4
            
                  |
16 | 15 | imbi2d 322 |
. . 3
    
          
                   |
17 | | fveq2 5888 |
. . . . . 6
           |
18 | 17 | breq2d 4428 |
. . . . 5
 
   
       |
19 | 17 | breq1d 4426 |
. . . . 5
     
       |
20 | 18, 19 | anbi12d 722 |
. . . 4
          
         
    |
21 | 20 | imbi2d 322 |
. . 3
  
          
         
     |
22 | | fmul01.4 |
. . . . . . . . . 10
   |
23 | 22 | zred 11069 |
. . . . . . . . 9
   |
24 | 23 | leidd 10208 |
. . . . . . . 8

  |
25 | | fmul01.5 |
. . . . . . . . 9
       |
26 | | eluzelz 11197 |
. . . . . . . . . . 11
    
  |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
   |
28 | | eluz 11201 |
. . . . . . . . . 10
 
     
   |
29 | 22, 27, 28 | syl2anc 671 |
. . . . . . . . 9
     
   |
30 | 25, 29 | mpbid 215 |
. . . . . . . 8

  |
31 | | elfz 11819 |
. . . . . . . . 9
 
 
   
     |
32 | 22, 22, 27, 31 | syl3anc 1276 |
. . . . . . . 8
      
    |
33 | 24, 30, 32 | mpbir2and 938 |
. . . . . . 7
       |
34 | 33 | ancli 558 |
. . . . . . 7
         |
35 | | fmul01.2 |
. . . . . . . . . 10
   |
36 | | nfv 1772 |
. . . . . . . . . 10
      |
37 | 35, 36 | nfan 2022 |
. . . . . . . . 9
         |
38 | | nfcv 2603 |
. . . . . . . . . 10
   |
39 | | nfcv 2603 |
. . . . . . . . . 10
  |
40 | | fmul01.1 |
. . . . . . . . . . 11
   |
41 | | nfcv 2603 |
. . . . . . . . . . 11
   |
42 | 40, 41 | nffv 5895 |
. . . . . . . . . 10
       |
43 | 38, 39, 42 | nfbr 4461 |
. . . . . . . . 9
 
     |
44 | 37, 43 | nfim 2014 |
. . . . . . . 8
   
    
      |
45 | | eleq1 2528 |
. . . . . . . . . 10
     
       |
46 | 45 | anbi2d 715 |
. . . . . . . . 9
  
    
         |
47 | | fveq2 5888 |
. . . . . . . . . 10
           |
48 | 47 | breq2d 4428 |
. . . . . . . . 9
 
   
       |
49 | 46, 48 | imbi12d 326 |
. . . . . . . 8
   
    
    
      
        |
50 | | fmul01.8 |
. . . . . . . 8
 
    
      |
51 | 44, 49, 50 | vtoclg1f 3118 |
. . . . . . 7
      
            |
52 | 33, 34, 51 | sylc 62 |
. . . . . 6

      |
53 | | fmul01.3 |
. . . . . . . 8
    |
54 | 53 | fveq1i 5889 |
. . . . . . 7
           |
55 | | seq1 12258 |
. . . . . . . 8
             |
56 | 22, 55 | syl 17 |
. . . . . . 7
             |
57 | 54, 56 | syl5eq 2508 |
. . . . . 6
           |
58 | 52, 57 | breqtrrd 4443 |
. . . . 5

      |
59 | | nfcv 2603 |
. . . . . . . . . 10
   |
60 | 42, 39, 59 | nfbr 4461 |
. . . . . . . . 9
     
 |
61 | 37, 60 | nfim 2014 |
. . . . . . . 8
   
        
  |
62 | 47 | breq1d 4426 |
. . . . . . . . 9
     
       |
63 | 46, 62 | imbi12d 326 |
. . . . . . . 8
   
        
  
        
    |
64 | | fmul01.9 |
. . . . . . . 8
 
    
      |
65 | 61, 63, 64 | vtoclg1f 3118 |
. . . . . . 7
      
            |
66 | 33, 34, 65 | sylc 62 |
. . . . . 6
    
  |
67 | 57, 66 | eqbrtrd 4437 |
. . . . 5
    
  |
68 | 58, 67 | jca 539 |
. . . 4
         
   |
69 | 68 | a1i 11 |
. . 3
    
         
    |
70 | | elfzouz 11955 |
. . . . . . . . . 10
  ..^
      |
71 | 70 | 3ad2ant1 1035 |
. . . . . . . . 9
   ..^      
             |
72 | | simpl3 1019 |
. . . . . . . . . 10
    ..^ 
                   |
73 | | elfzouz2 11965 |
. . . . . . . . . . . . 13
  ..^
      |
74 | | fzss2 11867 |
. . . . . . . . . . . . 13
    
          |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
  ..^
          |
76 | 75 | 3ad2ant1 1035 |
. . . . . . . . . . 11
   ..^      
                 |
77 | 76 | sselda 3444 |
. . . . . . . . . 10
    ..^ 
                       |
78 | | nfv 1772 |
. . . . . . . . . . . . 13
      |
79 | 35, 78 | nfan 2022 |
. . . . . . . . . . . 12
         |
80 | | nfcv 2603 |
. . . . . . . . . . . . . 14
   |
81 | 40, 80 | nffv 5895 |
. . . . . . . . . . . . 13
       |
82 | 81 | nfel1 2617 |
. . . . . . . . . . . 12
       |
83 | 79, 82 | nfim 2014 |
. . . . . . . . . . 11
   
           |
84 | | eleq1 2528 |
. . . . . . . . . . . . 13
     
       |
85 | 84 | anbi2d 715 |
. . . . . . . . . . . 12
  
    
         |
86 | | fveq2 5888 |
. . . . . . . . . . . . 13
           |
87 | 86 | eleq1d 2524 |
. . . . . . . . . . . 12
     
       |
88 | 85, 87 | imbi12d 326 |
. . . . . . . . . . 11
   
           
             |
89 | | fmul01.7 |
. . . . . . . . . . 11
 
    
      |
90 | 83, 88, 89 | chvar 2117 |
. . . . . . . . . 10
 
    
      |
91 | 72, 77, 90 | syl2anc 671 |
. . . . . . . . 9
    ..^ 
                       |
92 | | remulcl 9650 |
. . . . . . . . . 10
 
     |
93 | 92 | adantl 472 |
. . . . . . . . 9
    ..^ 
                   |
94 | 71, 91, 93 | seqcl 12265 |
. . . . . . . 8
   ..^      
               |
95 | | simp3 1016 |
. . . . . . . . 9
   ..^      
         |
96 | | fzofzp1 12039 |
. . . . . . . . . 10
  ..^
        |
97 | 96 | 3ad2ant1 1035 |
. . . . . . . . 9
   ..^      
               |
98 | | nfv 1772 |
. . . . . . . . . . . . 13
         |
99 | 35, 98 | nfan 2022 |
. . . . . . . . . . . 12
           |
100 | | nfcv 2603 |
. . . . . . . . . . . . . 14
     |
101 | 40, 100 | nffv 5895 |
. . . . . . . . . . . . 13
         |
102 | 101 | nfel1 2617 |
. . . . . . . . . . . 12
         |
103 | 99, 102 | nfim 2014 |
. . . . . . . . . . 11
                   |
104 | | eleq1 2528 |
. . . . . . . . . . . . 13
       
         |
105 | 104 | anbi2d 715 |
. . . . . . . . . . . 12
    
    
           |
106 | | fveq2 5888 |
. . . . . . . . . . . . 13
               |
107 | 106 | eleq1d 2524 |
. . . . . . . . . . . 12
       
         |
108 | 105, 107 | imbi12d 326 |
. . . . . . . . . . 11
     
                             |
109 | 103, 108,
89 | vtoclg1f 3118 |
. . . . . . . . . 10
        
                |
110 | 109 | anabsi7 833 |
. . . . . . . . 9
 
               |
111 | 95, 97, 110 | syl2anc 671 |
. . . . . . . 8
   ..^      
               |
112 | | pm3.35 595 |
. . . . . . . . . . . 12
 
         
   
           |
113 | 112 | ancoms 459 |
. . . . . . . . . . 11
   
          
            |
114 | | simpl 463 |
. . . . . . . . . . 11
 
               |
115 | 113, 114 | syl 17 |
. . . . . . . . . 10
   
          
      |
116 | 115 | 3adant1 1032 |
. . . . . . . . 9
   ..^      
             |
117 | 53 | fveq1i 5889 |
. . . . . . . . 9
           |
118 | 116, 117 | syl6breq 4456 |
. . . . . . . 8
   ..^      
               |
119 | | simp1 1014 |
. . . . . . . . 9
   ..^      
        ..^   |
120 | 96 | adantl 472 |
. . . . . . . . . 10
 
 ..^          |
121 | | simpl 463 |
. . . . . . . . . . 11
 
 ..^    |
122 | 121, 120 | jca 539 |
. . . . . . . . . 10
 
 ..^            |
123 | 38, 39, 101 | nfbr 4461 |
. . . . . . . . . . . 12
 
       |
124 | 99, 123 | nfim 2014 |
. . . . . . . . . . 11
                   |
125 | 106 | breq2d 4428 |
. . . . . . . . . . . 12
   
   
         |
126 | 105, 125 | imbi12d 326 |
. . . . . . . . . . 11
     
    
    
        
          |
127 | 124, 126,
50 | vtoclg1f 3118 |
. . . . . . . . . 10
        
      
         |
128 | 120, 122,
127 | sylc 62 |
. . . . . . . . 9
 
 ..^          |
129 | 95, 119, 128 | syl2anc 671 |
. . . . . . . 8
   ..^      
               |
130 | 94, 111, 118, 129 | mulge0d 10218 |
. . . . . . 7
   ..^      
                       |
131 | | seqp1 12260 |
. . . . . . . 8
    
                        |
132 | 71, 131 | syl 17 |
. . . . . . 7
   ..^      
                               |
133 | 130, 132 | breqtrrd 4443 |
. . . . . 6
   ..^      
                 |
134 | 53 | fveq1i 5889 |
. . . . . 6
               |
135 | 133, 134 | syl6breqr 4457 |
. . . . 5
   ..^      
               |
136 | 94, 111 | remulcld 9697 |
. . . . . . . 8
   ..^      
                       |
137 | | 1red 9684 |
. . . . . . . 8
   ..^      
         |
138 | 95, 97 | jca 539 |
. . . . . . . . . . 11
   ..^      
                 |
139 | 101, 39, 59 | nfbr 4461 |
. . . . . . . . . . . . 13
       
 |
140 | 99, 139 | nfim 2014 |
. . . . . . . . . . . 12
                   |
141 | 106 | breq1d 4426 |
. . . . . . . . . . . . 13
       
         |
142 | 105, 141 | imbi12d 326 |
. . . . . . . . . . . 12
     
        
                    |
143 | 140, 142,
64 | vtoclg1f 3118 |
. . . . . . . . . . 11
        
            
   |
144 | 97, 138, 143 | sylc 62 |
. . . . . . . . . 10
   ..^      
               |
145 | 111, 137,
94, 118, 144 | lemul2ad 10575 |
. . . . . . . . 9
   ..^      
                               |
146 | 94 | recnd 9695 |
. . . . . . . . . 10
   ..^      
               |
147 | 146 | mulid1d 9686 |
. . . . . . . . 9
   ..^      
                       |
148 | 145, 147 | breqtrd 4441 |
. . . . . . . 8
   ..^      
                             |
149 | | simp2 1015 |
. . . . . . . . . 10
   ..^      
        
            |
150 | 112 | simprd 469 |
. . . . . . . . . 10
 
         
         |
151 | 95, 149, 150 | syl2anc 671 |
. . . . . . . . 9
   ..^      
             |
152 | 117, 151 | syl5eqbrr 4451 |
. . . . . . . 8
   ..^      
               |
153 | 136, 94, 137, 148, 152 | letrd 9818 |
. . . . . . 7
   ..^      
                       |
154 | 132, 153 | eqbrtrd 4437 |
. . . . . 6
   ..^      
                 |
155 | 134, 154 | syl5eqbr 4450 |
. . . . 5
   ..^      
               |
156 | 135, 155 | jca 539 |
. . . 4
   ..^      
                       |
157 | 156 | 3exp 1214 |
. . 3
  ..^
      
                         |
158 | 6, 11, 16, 21, 69, 157 | fzind2 12054 |
. 2
          
        |
159 | 1, 158 | mpcom 37 |
1
         
   |