Step | Hyp | Ref
| Expression |
1 | | stoweidlem3.4 |
. . . 4
   |
2 | | elnnuz 11192 |
. . . 4

      |
3 | 1, 2 | sylib 200 |
. . 3
       |
4 | | eluzfz2 11804 |
. . 3
    
      |
5 | 3, 4 | syl 17 |
. 2
       |
6 | | oveq2 6296 |
. . . . 5
           |
7 | | fveq2 5863 |
. . . . 5
           |
8 | 6, 7 | breq12d 4414 |
. . . 4
     
   
           |
9 | 8 | imbi2d 318 |
. . 3
  
        
             |
10 | | oveq2 6296 |
. . . . 5
           |
11 | | fveq2 5863 |
. . . . 5
           |
12 | 10, 11 | breq12d 4414 |
. . . 4
     
   
           |
13 | 12 | imbi2d 318 |
. . 3
  
        
    
        |
14 | | oveq2 6296 |
. . . . 5
               |
15 | | fveq2 5863 |
. . . . 5
          
    |
16 | 14, 15 | breq12d 4414 |
. . . 4
       
   
               |
17 | 16 | imbi2d 318 |
. . 3
    
        
                 |
18 | | oveq2 6296 |
. . . . 5
           |
19 | | fveq2 5863 |
. . . . 5
           |
20 | 18, 19 | breq12d 4414 |
. . . 4
     
   
           |
21 | 20 | imbi2d 318 |
. . 3
  
        
    
        |
22 | | 1zzd 10965 |
. . . . . . . . 9
   |
23 | 1 | nnzd 11036 |
. . . . . . . . 9
   |
24 | 22, 23, 22 | 3jca 1187 |
. . . . . . . 8
 
   |
25 | | 1le1 10237 |
. . . . . . . . 9
 |
26 | 25 | a1i 11 |
. . . . . . . 8

  |
27 | 1 | nnge1d 10649 |
. . . . . . . 8

  |
28 | 24, 26, 27 | jca32 538 |
. . . . . . 7
    
    |
29 | | elfz2 11788 |
. . . . . . 7
    
 
 
    |
30 | 28, 29 | sylibr 216 |
. . . . . 6
       |
31 | 30 | ancli 554 |
. . . . . 6
         |
32 | | stoweidlem3.2 |
. . . . . . . . 9
   |
33 | | nfv 1760 |
. . . . . . . . 9
       |
34 | 32, 33 | nfan 2010 |
. . . . . . . 8
         |
35 | | nfcv 2591 |
. . . . . . . . 9
   |
36 | | nfcv 2591 |
. . . . . . . . 9
  |
37 | | stoweidlem3.1 |
. . . . . . . . . 10
   |
38 | | nfcv 2591 |
. . . . . . . . . 10
   |
39 | 37, 38 | nffv 5870 |
. . . . . . . . 9
       |
40 | 35, 36, 39 | nfbr 4446 |
. . . . . . . 8
      |
41 | 34, 40 | nfim 2002 |
. . . . . . 7
   
           |
42 | | eleq1 2516 |
. . . . . . . . 9
     
       |
43 | 42 | anbi2d 709 |
. . . . . . . 8
  
    
         |
44 | | fveq2 5863 |
. . . . . . . . 9
           |
45 | 44 | breq2d 4413 |
. . . . . . . 8
     
       |
46 | 43, 45 | imbi12d 322 |
. . . . . . 7
   
                         |
47 | | stoweidlem3.6 |
. . . . . . 7
 
           |
48 | 41, 46, 47 | vtoclg1f 3105 |
. . . . . 6
      
            |
49 | 30, 31, 48 | sylc 62 |
. . . . 5
       |
50 | | stoweidlem3.7 |
. . . . . . 7
   |
51 | 50 | rpcnd 11340 |
. . . . . 6
   |
52 | 51 | exp1d 12408 |
. . . . 5
       |
53 | | stoweidlem3.3 |
. . . . . . . 8
    |
54 | 53 | fveq1i 5864 |
. . . . . . 7
           |
55 | | 1z 10964 |
. . . . . . . 8
 |
56 | | seq1 12223 |
. . . . . . . 8
             |
57 | 55, 56 | ax-mp 5 |
. . . . . . 7
           |
58 | 54, 57 | eqtri 2472 |
. . . . . 6
         |
59 | 58 | a1i 11 |
. . . . 5
           |
60 | 49, 52, 59 | 3brtr4d 4432 |
. . . 4
           |
61 | 60 | a1i 11 |
. . 3
    
            |
62 | 50 | 3ad2ant3 1030 |
. . . . . . . 8
   ..^          

  |
63 | 62 | rpred 11338 |
. . . . . . 7
   ..^          

  |
64 | | elfzouz 11921 |
. . . . . . . . 9
  ..^
      |
65 | | elnnuz 11192 |
. . . . . . . . . 10

      |
66 | | nnnn0 10873 |
. . . . . . . . . 10
   |
67 | 65, 66 | sylbir 217 |
. . . . . . . . 9
    
  |
68 | 64, 67 | syl 17 |
. . . . . . . 8
  ..^
  |
69 | 68 | 3ad2ant1 1028 |
. . . . . . 7
   ..^          

  |
70 | 63, 69 | reexpcld 12430 |
. . . . . 6
   ..^          
       |
71 | 53 | fveq1i 5864 |
. . . . . . . 8
           |
72 | 64 | adantr 467 |
. . . . . . . . 9
   ..^        |
73 | | nfv 1760 |
. . . . . . . . . . . . 13
  ..^  |
74 | 73, 32 | nfan 2010 |
. . . . . . . . . . . 12
    ..^   |
75 | | nfv 1760 |
. . . . . . . . . . . 12
      |
76 | 74, 75 | nfan 2010 |
. . . . . . . . . . 11
     ..^ 
      |
77 | | nfcv 2591 |
. . . . . . . . . . . . 13
   |
78 | 37, 77 | nffv 5870 |
. . . . . . . . . . . 12
       |
79 | 78 | nfel1 2605 |
. . . . . . . . . . 11
       |
80 | 76, 79 | nfim 2002 |
. . . . . . . . . 10
      ..^ 
           |
81 | | eleq1 2516 |
. . . . . . . . . . . 12
     
       |
82 | 81 | anbi2d 709 |
. . . . . . . . . . 11
     ..^ 
        ..^ 
        |
83 | | fveq2 5863 |
. . . . . . . . . . . 12
           |
84 | 83 | eleq1d 2512 |
. . . . . . . . . . 11
     
       |
85 | 82, 84 | imbi12d 322 |
. . . . . . . . . 10
      ..^ 
              ..^ 
             |
86 | | stoweidlem3.5 |
. . . . . . . . . . . 12
           |
87 | 86 | ad2antlr 732 |
. . . . . . . . . . 11
    ..^                 |
88 | | 1zzd 10965 |
. . . . . . . . . . . . . 14
    ..^         |
89 | 23 | ad2antlr 732 |
. . . . . . . . . . . . . 14
    ..^         |
90 | | elfzelz 11797 |
. . . . . . . . . . . . . . 15
       |
91 | 90 | adantl 468 |
. . . . . . . . . . . . . 14
    ..^         |
92 | 88, 89, 91 | 3jca 1187 |
. . . . . . . . . . . . 13
    ..^       
   |
93 | | elfzle1 11799 |
. . . . . . . . . . . . . 14
       |
94 | 93 | adantl 468 |
. . . . . . . . . . . . 13
    ..^         |
95 | 90 | zred 11037 |
. . . . . . . . . . . . . . 15
       |
96 | 95 | adantl 468 |
. . . . . . . . . . . . . 14
    ..^         |
97 | | elfzoelz 11917 |
. . . . . . . . . . . . . . . 16
  ..^
  |
98 | 97 | zred 11037 |
. . . . . . . . . . . . . . 15
  ..^
  |
99 | 98 | ad2antrr 731 |
. . . . . . . . . . . . . 14
    ..^         |
100 | 1 | nnred 10621 |
. . . . . . . . . . . . . . 15
   |
101 | 100 | ad2antlr 732 |
. . . . . . . . . . . . . 14
    ..^         |
102 | | elfzle2 11800 |
. . . . . . . . . . . . . . 15
       |
103 | 102 | adantl 468 |
. . . . . . . . . . . . . 14
    ..^         |
104 | | elfzoel2 11916 |
. . . . . . . . . . . . . . . . 17
  ..^
  |
105 | 104 | zred 11037 |
. . . . . . . . . . . . . . . 16
  ..^
  |
106 | | elfzolt2 11926 |
. . . . . . . . . . . . . . . 16
  ..^
  |
107 | 98, 105, 106 | ltled 9780 |
. . . . . . . . . . . . . . 15
  ..^
  |
108 | 107 | ad2antrr 731 |
. . . . . . . . . . . . . 14
    ..^         |
109 | 96, 99, 101, 103, 108 | letrd 9789 |
. . . . . . . . . . . . 13
    ..^         |
110 | 92, 94, 109 | jca32 538 |
. . . . . . . . . . . 12
    ..^        
 
    |
111 | | elfz2 11788 |
. . . . . . . . . . . 12
    
 
 
    |
112 | 110, 111 | sylibr 216 |
. . . . . . . . . . 11
    ..^             |
113 | 87, 112 | ffvelrnd 6021 |
. . . . . . . . . 10
    ..^             |
114 | 80, 85, 113 | chvar 2105 |
. . . . . . . . 9
    ..^             |
115 | | remulcl 9621 |
. . . . . . . . . 10
 
     |
116 | 115 | adantl 468 |
. . . . . . . . 9
    ..^         |
117 | 72, 114, 116 | seqcl 12230 |
. . . . . . . 8
   ..^          |
118 | 71, 117 | syl5eqel 2532 |
. . . . . . 7
   ..^        |
119 | 118 | 3adant2 1026 |
. . . . . 6
   ..^          
       |
120 | 86 | 3ad2ant3 1030 |
. . . . . . 7
   ..^          
           |
121 | | fzofzp1 12005 |
. . . . . . . 8
  ..^
        |
122 | 121 | 3ad2ant1 1028 |
. . . . . . 7
   ..^          
         |
123 | 120, 122 | ffvelrnd 6021 |
. . . . . 6
   ..^          
         |
124 | 50 | rpge0d 11342 |
. . . . . . . 8

  |
125 | 124 | 3ad2ant3 1030 |
. . . . . . 7
   ..^          

  |
126 | 63, 69, 125 | expge0d 12431 |
. . . . . 6
   ..^          

      |
127 | | simp3 1009 |
. . . . . . 7
   ..^          
   |
128 | | simp2 1008 |
. . . . . . 7
   ..^          
 
           |
129 | 127, 128 | mpd 15 |
. . . . . 6
   ..^          
    
      |
130 | 121 | adantr 467 |
. . . . . . . 8
   ..^          |
131 | | simpr 463 |
. . . . . . . . 9
   ..^    |
132 | 131, 130 | jca 535 |
. . . . . . . 8
   ..^   
        |
133 | | nfv 1760 |
. . . . . . . . . . 11
         |
134 | 32, 133 | nfan 2010 |
. . . . . . . . . 10
           |
135 | | nfcv 2591 |
. . . . . . . . . . . 12
     |
136 | 37, 135 | nffv 5870 |
. . . . . . . . . . 11
         |
137 | 35, 36, 136 | nfbr 4446 |
. . . . . . . . . 10
        |
138 | 134, 137 | nfim 2002 |
. . . . . . . . 9
    
              |
139 | | eleq1 2516 |
. . . . . . . . . . 11
       
         |
140 | 139 | anbi2d 709 |
. . . . . . . . . 10
    
    
           |
141 | | fveq2 5863 |
. . . . . . . . . . 11
          
    |
142 | 141 | breq2d 4413 |
. . . . . . . . . 10
       
         |
143 | 140, 142 | imbi12d 322 |
. . . . . . . . 9
     
                             |
144 | 138, 143,
47 | vtoclg1f 3105 |
. . . . . . . 8
        
          
     |
145 | 130, 132,
144 | sylc 62 |
. . . . . . 7
   ..^          |
146 | 145 | 3adant2 1026 |
. . . . . 6
   ..^          
    
    |
147 | 70, 119, 63, 123, 126, 129, 125, 146 | ltmul12ad 10545 |
. . . . 5
   ..^          
      
              |
148 | 51 | 3ad2ant3 1030 |
. . . . . 6
   ..^          

  |
149 | 148, 69 | expp1d 12414 |
. . . . 5
   ..^          
               |
150 | 53 | fveq1i 5864 |
. . . . . . 7
               |
151 | 150 | a1i 11 |
. . . . . 6
   ..^          
                 |
152 | 64 | 3ad2ant1 1028 |
. . . . . . 7
   ..^          

      |
153 | | seqp1 12225 |
. . . . . . 7
    
                        |
154 | 152, 153 | syl 17 |
. . . . . 6
   ..^          
      
                  |
155 | 71 | a1i 11 |
. . . . . . . 8
   ..^          
             |
156 | 155 | eqcomd 2456 |
. . . . . . 7
   ..^          
             |
157 | 156 | oveq1d 6303 |
. . . . . 6
   ..^          
                             |
158 | 151, 154,
157 | 3eqtrd 2488 |
. . . . 5
   ..^          
               
     |
159 | 147, 149,
158 | 3brtr4d 4432 |
. . . 4
   ..^          
               |
160 | 159 | 3exp 1206 |
. . 3
  ..^
          
                 |
161 | 9, 13, 17, 21, 61, 160 | fzind2 12020 |
. 2
                 |
162 | 5, 161 | mpcom 37 |
1
    
      |