Step | Hyp | Ref
| Expression |
1 | | elnn1uz2 11269 |
. . 3

        |
2 | | 1t1e1 10791 |
. . . . . . . . 9
   |
3 | 2 | eqcomi 2471 |
. . . . . . . 8
   |
4 | | simpl 463 |
. . . . . . . 8
  #b       |
5 | | oveq2 6328 |
. . . . . . . . . . . 12
   #b 
 ..^    ..^ #b     |
6 | 5 | eqcoms 2470 |
. . . . . . . . . . 11
 #b   
 ..^    ..^ #b     |
7 | | fveq2 5892 |
. . . . . . . . . . . . . 14
 #b  #b    |
8 | | blen1 40764 |
. . . . . . . . . . . . . 14
#b   |
9 | 7, 8 | syl6eq 2512 |
. . . . . . . . . . . . 13
 #b    |
10 | 9 | oveq2d 6336 |
. . . . . . . . . . . 12
  ..^ #b    ..^   |
11 | | fzo01 12032 |
. . . . . . . . . . . 12
 ..^    |
12 | 10, 11 | syl6eq 2512 |
. . . . . . . . . . 11
  ..^ #b       |
13 | 6, 12 | sylan9eqr 2518 |
. . . . . . . . . 10
  #b      ..^       |
14 | 13 | sumeq1d 13822 |
. . . . . . . . 9
  #b       ..^       digit         
     digit           |
15 | | oveq2 6328 |
. . . . . . . . . . . . 13
   digit      digit      |
16 | 15 | oveq1d 6335 |
. . . . . . . . . . . 12
    digit            digit           |
17 | 16 | sumeq2sdv 13825 |
. . . . . . . . . . 11
       digit               digit           |
18 | | c0ex 9668 |
. . . . . . . . . . . 12
 |
19 | | ax-1cn 9628 |
. . . . . . . . . . . . 13
 |
20 | 19, 19 | mulcli 9679 |
. . . . . . . . . . . 12
   |
21 | | oveq1 6327 |
. . . . . . . . . . . . . . 15
   digit      digit      |
22 | | 1ex 9669 |
. . . . . . . . . . . . . . . . 17
 |
23 | 22 | prid2 4094 |
. . . . . . . . . . . . . . . 16
    |
24 | | 0dig2pr01 40790 |
. . . . . . . . . . . . . . . 16
      digit      |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . . . . . . 15
  digit     |
26 | 21, 25 | syl6eq 2512 |
. . . . . . . . . . . . . 14
   digit      |
27 | | oveq2 6328 |
. . . . . . . . . . . . . . 15
           |
28 | | 2cn 10713 |
. . . . . . . . . . . . . . . 16
 |
29 | | exp0 12314 |
. . . . . . . . . . . . . . . 16
       |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     |
31 | 27, 30 | syl6eq 2512 |
. . . . . . . . . . . . . 14
       |
32 | 26, 31 | oveq12d 6338 |
. . . . . . . . . . . . 13
    digit             |
33 | 32 | sumsn 13862 |
. . . . . . . . . . . 12
           digit             |
34 | 18, 20, 33 | mp2an 683 |
. . . . . . . . . . 11
      digit            |
35 | 17, 34 | syl6eq 2512 |
. . . . . . . . . 10
       digit             |
36 | 35 | adantr 471 |
. . . . . . . . 9
  #b           digit             |
37 | 14, 36 | eqtrd 2496 |
. . . . . . . 8
  #b       ..^       digit             |
38 | 3, 4, 37 | 3eqtr4a 2522 |
. . . . . . 7
  #b       ..^       digit           |
39 | 38 | ex 440 |
. . . . . 6
  #b      ..^       digit            |
40 | 39 | a1d 26 |
. . . . 5
  
 #b    ..^     digit           #b    
 ..^       digit             |
41 | 40 | 2a1d 27 |
. . . 4
          #b    ..^     digit           #b    
 ..^       digit               |
42 | | eluzge2nn0 11232 |
. . . . . . . . 9
    
  |
43 | | nn0ob 40699 |
. . . . . . . . . 10

    
       |
44 | 43 | bicomd 206 |
. . . . . . . . 9

    
       |
45 | 42, 44 | syl 17 |
. . . . . . . 8
    
    
       |
46 | | blennngt2o2 40772 |
. . . . . . . . 9
           #b   #b         |
47 | 46 | ex 440 |
. . . . . . . 8
    
    
#b   #b          |
48 | 45, 47 | sylbid 223 |
. . . . . . 7
    
    
#b   #b          |
49 | 48 | imp 435 |
. . . . . 6
           #b   #b         |
50 | | fveq2 5892 |
. . . . . . . . . . . . . 14
     #b  #b        |
51 | 50 | eqeq1d 2464 |
. . . . . . . . . . . . 13
      #b 
#b         |
52 | | id 22 |
. . . . . . . . . . . . . 14
           |
53 | | oveq2 6328 |
. . . . . . . . . . . . . . . 16
       digit      digit          |
54 | 53 | oveq1d 6335 |
. . . . . . . . . . . . . . 15
        digit            digit               |
55 | 54 | sumeq2sdv 13825 |
. . . . . . . . . . . . . 14
       ..^     digit           ..^     digit               |
56 | 52, 55 | eqeq12d 2477 |
. . . . . . . . . . . . 13
        ..^     digit               ..^     digit                |
57 | 51, 56 | imbi12d 326 |
. . . . . . . . . . . 12
       #b 
  ..^     digit           #b          
 ..^     digit                 |
58 | 57 | rspcva 3160 |
. . . . . . . . . . 11
        #b 
  ..^     digit          
 #b          
 ..^     digit                |
59 | | eqeq1 2466 |
. . . . . . . . . . . . . . . 16
 #b   
 #b   #b      
   #b          |
60 | | nncn 10650 |
. . . . . . . . . . . . . . . . . . . . 21
   |
61 | 60 | ad2antll 740 |
. . . . . . . . . . . . . . . . . . . 20
  #b              
 
  |
62 | | blennn0elnn 40757 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
#b        |
63 | 62 | nncnd 10658 |
. . . . . . . . . . . . . . . . . . . . . 22
    
#b        |
64 | 63 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
     
     #b        |
65 | 64 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . 20
  #b              
 
#b        |
66 | | 1cnd 9690 |
. . . . . . . . . . . . . . . . . . . 20
  #b              
 
  |
67 | 61, 65, 66 | addcan2d 9868 |
. . . . . . . . . . . . . . . . . . 19
  #b              
 
    #b       #b         |
68 | | eqcom 2469 |
. . . . . . . . . . . . . . . . . . . 20
 #b      #b        |
69 | | nnz 10993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
70 | 69 | ad2antll 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  #b              
 
  |
71 | | fzval3 12020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      ..^     |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  #b              
 
     ..^     |
73 | 72 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  #b              
 
 ..^         |
74 | 73 | sumeq1d 13822 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  #b              
 
  ..^       digit                  digit           |
75 | | nnnn0 10910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
76 | | elnn0uz 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

      |
77 | 75, 76 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
78 | 77 | ad2antll 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  #b              
 
      |
79 | | 2nn 10801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           
       |
81 | | elfzelz 11835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
82 | 81 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           
       |
83 | | nn0rp0 11774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36

     |
84 | 42, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    
     |
85 | 84 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
          |
86 | 85 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           
          |
87 | | digvalnn0 40779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
      digit      |
88 | 80, 82, 86, 87 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
       digit      |
89 | 88 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
            digit       |
90 | 89 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  #b              
 
    
  digit       |
91 | 90 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   #b         
    
         digit      |
92 | 91 | nn0cnd 10961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   #b         
    
         digit      |
93 | | 2nn0 10920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
95 | | elfznn0 11922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
96 | 94, 95 | nn0expcld 12476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
97 | 96 | nn0cnd 10961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
98 | 97 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   #b         
    
             |
99 | 92, 98 | mulcld 9694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   #b         
    
          digit           |
100 | | oveq1 6327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   digit      digit      |
101 | 100, 27 | oveq12d 6338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    digit            digit           |
102 | 30 | oveq2i 6331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   digit            digit      |
103 | 101, 102 | syl6eq 2512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    digit            digit       |
104 | 78, 99, 103 | fsum1p 13869 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  #b              
 
         digit             digit                digit            |
105 | 42 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
       |
106 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
    
       |
107 | 106 | biimparc 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
           |
108 | | 0dig2nn0o 40793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         digit      |
109 | 105, 107,
108 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
       digit      |
110 | 109 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  #b              
 
  digit      |
111 | 110 | oveq1d 6335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  #b              
 
   digit         |
112 | 111, 2 | syl6eq 2512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  #b              
 
   digit       |
113 | | 1z 11001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
114 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  #b              
 
  |
115 | | 0p1e1 10754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
116 | 115, 113 | eqeltri 2536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
117 | 116 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  #b              
 
    |
118 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
               |
119 | | elfzelz 11835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
         |
120 | 119 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
               |
121 | 42 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
               |
122 | 121, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                  |
123 | 118, 120,
122, 87 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
               digit      |
124 | 123 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
      
  digit       |
125 | 124 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
              digit       |
126 | 125 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  #b              
 
      
  digit       |
127 | 126 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   #b         
    
           digit      |
128 | 127 | nn0cnd 10961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   #b         
    
           digit      |
129 | | 2cnd 10715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
130 | | elfznn 11863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
131 | 130 | nnnn0d 10959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
132 | 115 | oveq1i 6330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
133 | 131, 132 | eleq2s 2558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
134 | 129, 133 | expcld 12454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             |
135 | 134 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   #b         
    
               |
136 | 128, 135 | mulcld 9694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   #b         
    
            digit           |
137 | | oveq1 6327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     digit        digit      |
138 | | oveq2 6328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
139 | 137, 138 | oveq12d 6338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      digit              digit             |
140 | 114, 117,
70, 136, 139 | fsumshftm 13897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  #b              
 
           digit                          digit             |
141 | 112, 140 | oveq12d 6338 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  #b              
 
    digit                digit                            digit              |
142 | 74, 104, 141 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  #b              
 
  ..^       digit                           digit              |
143 | 142 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        ..^     digit              #b         
    
     ..^       digit                           digit              |
144 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           
 ..^    |
145 | | elfzoelz 11957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
  ..^
  |
146 | 145 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           
 ..^    |
147 | | nn0rp0 11774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
         |
148 | 147 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     
              |
149 | 148 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           
 ..^           |
150 | | digvalnn0 40779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
          digit          |
151 | 144, 146,
149, 150 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           
 ..^    digit          |
152 | 151 | nn0cnd 10961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           
 ..^    digit          |
153 | 152 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
       ..^   digit           |
154 | 153 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  #b              
 
  ..^   digit           |
155 | 154 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   #b         
    
   ..^ 
  digit          |
156 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  ..^
  |
157 | | elfzonn0 11997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  ..^
  |
158 | 156, 157 | nn0expcld 12476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  ..^
      |
159 | 158 | nn0cnd 10961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  ..^
      |
160 | 159 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   #b         
    
   ..^ 
      |
161 | | 2cnd 10715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   #b         
    
   ..^ 
  |
162 | 155, 160,
161 | mulassd 9697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   #b         
    
   ..^ 
    digit                 digit                 |
163 | 162 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   #b         
    
   ..^ 
   digit                   digit                |
164 | 163 | sumeq2dv 13824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  #b              
 
  ..^     digit                 ..^      digit                |
165 | 164 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        ..^     digit              #b         
    
     ..^     digit               
 ..^      digit                |
166 | | 0cn 9666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 |
167 | | pncan1 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
168 | 166, 167 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
170 | 169 | oveq1d 6335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   |
171 | | fzoval 11958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  ..^         |
172 | 69, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  ..^         |
173 | 170, 172 | eqtr4d 2499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            ..^   |
174 | 173 | ad2antll 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  #b              
 
           ..^   |
175 | | simprlr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  #b              
 
      |
176 | | elfznn0 11922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
177 | 168 | oveq1i 6330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                 |
178 | 176, 177 | eleq2s 2558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
179 | | dignn0flhalf 40798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           digit      digit            |
180 | 175, 178,
179 | syl2an 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   #b         
    
                 digit      digit            |
181 | | eluzelz 11202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
  |
182 | 181 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             |
183 | | nn0z 10994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
      |
184 | | zob 38898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     
       |
185 | 181, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
    
       |
186 | 183, 185 | syl5ibr 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
    
       |
187 | 186 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                 |
188 | 182, 187 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                   |
189 | 188 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
             |
190 | 189 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  #b              
 
        |
191 | 190 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   #b         
    
                     |
192 | | zofldiv2 40707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                   |
193 | 191, 192 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   #b         
    
                         |
194 | 193 | oveq2d 6336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   #b         
    
               digit            digit          |
195 | 180, 194 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   #b         
    
                 digit      digit          |
196 | | 2cnd 10715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
197 | 196, 178 | expp1d 12455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                         |
198 | 197 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   #b         
    
                           |
199 | 195, 198 | oveq12d 6338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   #b         
    
                  digit              digit                 |
200 | 174, 199 | sumeq12dv 13827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  #b              
 
                 digit             ..^     digit                 |
201 | 200 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        ..^     digit              #b         
    
                    digit             ..^     digit                 |
202 | | oveq1 6327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   digit          digit          |
203 | | oveq2 6328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           |
204 | 202, 203 | oveq12d 6338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    digit                digit               |
205 | 204 | cbvsumv 13817 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  ..^     digit               ..^     digit              |
206 | 205 | eqeq2i 2474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       ..^     digit            
      ..^     digit               |
207 | 206 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       ..^     digit                   ..^     digit               |
208 | 207 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        ..^     digit              #b         
    
         ..^     digit               |
209 | 208 | oveq1d 6335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        ..^     digit              #b         
    
          
 ..^     digit                |
210 | | fzofi 12225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 ..^  |
211 | 210 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        ..^     digit              #b         
    
    ..^   |
212 | | 2cnd 10715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        ..^     digit              #b         
    
     |
213 | 159 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           
 ..^        |
214 | 152, 213 | mulcld 9694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
 ..^     digit               |
215 | 214 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
       ..^    digit                |
216 | 215 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           
   ..^    digit                |
217 | 216 | ad2antll 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        ..^     digit              #b         
    
     ..^    digit                |
218 | 217 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
 ..^     digit              #b              
    ..^ 
   digit               |
219 | 211, 212,
218 | fsummulc1 13901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        ..^     digit              #b         
    
      ..^     digit              
 ..^      digit                |
220 | 209, 219 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        ..^     digit              #b         
    
           ..^      digit                |
221 | 165, 201,
220 | 3eqtr4d 2506 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        ..^     digit              #b         
    
                    digit                   |
222 | 221 | oveq2d 6336 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        ..^     digit              #b         
    
    
                digit                      |
223 | | eluzelcn 11204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
  |
224 | | peano2cnm 9971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
225 | 223, 224 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
    |
226 | | 2cnd 10715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
  |
227 | | 2ne0 10735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
228 | 227 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
  |
229 | 225, 226,
228 | 3jca 1194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
      |
230 | 229 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
           |
231 | | divcan1 10312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
           |
232 | 230, 231 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
               |
233 | 232 | oveq2d 6336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                   |
234 | | 1cnd 9690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
  |
235 | 234, 223 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
    |
236 | 235 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
         |
237 | | pncan3 9914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
       |
238 | 236, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
           |
239 | 233, 238 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
               |
240 | 239 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
           |
241 | 240 | ad2antll 740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        ..^     digit              #b         
    
             |
242 | 143, 222,
241 | 3eqtrrd 2501 |
. . . . . . . . . . . . . . . . . . . . . . 23
        ..^     digit              #b         
    
     ..^       digit           |
243 | 242 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . 22
       ..^     digit               #b         
    
    ..^       digit            |
244 | 243 | imim2i 16 |
. . . . . . . . . . . . . . . . . . . . 21
  #b            ..^     digit               #b        #b         
    
 
  ..^       digit             |
245 | 244 | com13 83 |
. . . . . . . . . . . . . . . . . . . 20
  #b              
 
 #b        #b     
      ..^     digit              
 ..^       digit             |
246 | 68, 245 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . 19
  #b              
 
 #b        #b     
      ..^     digit              
 ..^       digit             |
247 | 67, 246 | sylbid 223 |
. . . . . . . . . . . . . . . . . 18
  #b              
 
    #b      
  #b            ..^     digit              
 ..^       digit             |
248 | 247 | ex 440 |
. . . . . . . . . . . . . . . . 17
 #b   
           
     #b         #b          
 ..^     digit                ..^       digit              |
249 | 248 | com23 81 |
. . . . . . . . . . . . . . . 16
 #b   
    #b      
           
   #b          
 ..^     digit                ..^       digit              |
250 | 59, 249 | sylbid 223 |
. . . . . . . . . . . . . . 15
 #b   
 #b   #b             
    

  #b            ..^     digit              
 ..^       digit              |
251 | 250 | com23 81 |
. . . . . . . . . . . . . 14
 #b   
           
  #b   #b         #b            ..^     digit             
  ..^       digit              |
252 | 251 | com14 91 |
. . . . . . . . . . . . 13
  #b            ..^     digit                    
    
  #b   #b        #b      ..^       digit              |
253 | 252 | exp4c 617 |
. . . . . . . . . . . 12
  #b            ..^     digit                          #b   #b        #b      ..^       digit                |
254 | 253 | com35 93 |
. . . . . . . . . . 11
  #b            ..^     digit                    #b   #b              #b      ..^       digit                |
255 | 58, 254 | syl 17 |
. . . . . . . . . 10
        #b 
  ..^     digit          
    
 #b   #b       
      #b      ..^       digit                |
256 | 255 | ex 440 |
. . . . . . . . 9
    
 
 #b 
  ..^     digit                #b   #b              #b      ..^       digit                 |
257 | 256 | pm2.43a 51 |
. . . . . . . 8
    
 
 #b 
  ..^     digit           #b   #b              #b      ..^       digit                |
258 | 257 | com25 94 |
. . . . . . 7
    
    
 #b   #b           #b  
 ..^     digit           #b      ..^       digit                |
259 | 258 | impcom 436 |
. . . . . 6
            #b   #b           #b    ..^     digit           #b    
 ..^       digit               |
260 | 49, 259 | mpd 15 |
. . . . 5
               #b  
 ..^     digit           #b      ..^       digit              |
261 | 260 | ex 440 |
. . . 4
    
    
  
 #b    ..^     digit           #b    
 ..^       digit               |
262 | 41, 261 | jaoi 385 |
. . 3
                #b  
 ..^     digit           #b      ..^       digit               |
263 | 1, 262 | sylbi 200 |
. 2
          #b    ..^     digit           #b    
 ..^       digit               |
264 | 263 | imp31 438 |
1
       
    #b  
 ..^     digit           #b      ..^       digit             |