Step | Hyp | Ref
| Expression |
1 | | hashnzfzclim.m |
. . . . . 6
   |
2 | 1 | adantr 467 |
. . . . 5
 
      
  |
3 | | hashnzfzclim.j |
. . . . . 6
   |
4 | 3 | adantr 467 |
. . . . 5
 
      
  |
5 | | simpr 463 |
. . . . 5
 
      
        |
6 | 2, 4, 5 | hashnzfz 36663 |
. . . 4
 
      
   
                            |
7 | 6 | oveq1d 6303 |
. . 3
 
      
                                    |
8 | 7 | mpteq2dva 4488 |
. 2
            
                
                       |
9 | | nnuz 11191 |
. . . . 5
     |
10 | | 1z 10964 |
. . . . . 6
 |
11 | 10 | a1i 11 |
. . . . 5
   |
12 | 1 | nncnd 10622 |
. . . . . . . . . 10
   |
13 | 1 | nnne0d 10651 |
. . . . . . . . . 10
   |
14 | 12, 13 | reccld 10373 |
. . . . . . . . 9
     |
15 | 9 | eqimss2i 3486 |
. . . . . . . . . 10
     |
16 | | nnex 10612 |
. . . . . . . . . 10
 |
17 | 15, 16 | climconst2 13605 |
. . . . . . . . 9
   
           |
18 | 14, 10, 17 | sylancl 667 |
. . . . . . . 8
           |
19 | 16 | mptex 6134 |
. . . . . . . . 9
         |
20 | 19 | a1i 11 |
. . . . . . . 8
           |
21 | | ax-1cn 9594 |
. . . . . . . . 9
 |
22 | | divcnv 13904 |
. . . . . . . . 9
       |
23 | 21, 22 | mp1i 13 |
. . . . . . . 8
       |
24 | | ovex 6316 |
. . . . . . . . . . 11
   |
25 | 24 | fvconst2 6118 |
. . . . . . . . . 10
               |
26 | 25 | adantl 468 |
. . . . . . . . 9
 

              |
27 | 14 | adantr 467 |
. . . . . . . . 9
 

    |
28 | 26, 27 | eqeltrd 2528 |
. . . . . . . 8
 

            |
29 | | eqidd 2451 |
. . . . . . . . . . 11
 

          |
30 | | oveq2 6296 |
. . . . . . . . . . . 12
       |
31 | 30 | adantl 468 |
. . . . . . . . . . 11
           |
32 | | simpr 463 |
. . . . . . . . . . 11
 

  |
33 | | ovex 6316 |
. . . . . . . . . . . 12
   |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
 

    |
35 | 29, 31, 32, 34 | fvmptd 5952 |
. . . . . . . . . 10
 

            |
36 | 32 | nnrecred 10652 |
. . . . . . . . . 10
 

    |
37 | 35, 36 | eqeltrd 2528 |
. . . . . . . . 9
 

          |
38 | 37 | recnd 9666 |
. . . . . . . 8
 

          |
39 | | eqidd 2451 |
. . . . . . . . . 10
 

                  |
40 | 30 | oveq2d 6304 |
. . . . . . . . . . 11
               |
41 | 40 | adantl 468 |
. . . . . . . . . 10
                   |
42 | | ovex 6316 |
. . . . . . . . . . 11
       |
43 | 42 | a1i 11 |
. . . . . . . . . 10
 

        |
44 | 39, 41, 32, 43 | fvmptd 5952 |
. . . . . . . . 9
 

                    |
45 | 26, 35 | oveq12d 6306 |
. . . . . . . . 9
 

                            |
46 | 44, 45 | eqtr4d 2487 |
. . . . . . . 8
 

                                  |
47 | 9, 11, 18, 20, 23, 28, 38, 46 | climsub 13690 |
. . . . . . 7
               |
48 | 14 | subid1d 9972 |
. . . . . . 7
         |
49 | 47, 48 | breqtrd 4426 |
. . . . . 6
             |
50 | 16 | mptex 6134 |
. . . . . . 7
           |
51 | 50 | a1i 11 |
. . . . . 6
             |
52 | 1 | nnrecred 10652 |
. . . . . . . . 9
     |
53 | 52 | adantr 467 |
. . . . . . . 8
 

    |
54 | | nnre 10613 |
. . . . . . . . . 10
   |
55 | 54 | adantl 468 |
. . . . . . . . 9
 

  |
56 | | nnne0 10639 |
. . . . . . . . . 10
   |
57 | 56 | adantl 468 |
. . . . . . . . 9
 

  |
58 | 55, 57 | rereccld 10431 |
. . . . . . . 8
 

    |
59 | 53, 58 | resubcld 10044 |
. . . . . . 7
 

        |
60 | 44, 59 | eqeltrd 2528 |
. . . . . 6
 

              |
61 | | eqidd 2451 |
. . . . . . . 8
 

                      |
62 | | oveq1 6295 |
. . . . . . . . . . 11
       |
63 | 62 | fveq2d 5867 |
. . . . . . . . . 10
               |
64 | | id 22 |
. . . . . . . . . 10
   |
65 | 63, 64 | oveq12d 6306 |
. . . . . . . . 9
                   |
66 | 65 | adantl 468 |
. . . . . . . 8
                       |
67 | | ovex 6316 |
. . . . . . . . 9
         |
68 | 67 | a1i 11 |
. . . . . . . 8
 

          |
69 | 61, 66, 32, 68 | fvmptd 5952 |
. . . . . . 7
 

                        |
70 | 1 | adantr 467 |
. . . . . . . . . 10
 

  |
71 | 55, 70 | nndivred 10655 |
. . . . . . . . 9
 

    |
72 | | reflcl 12029 |
. . . . . . . . 9
           |
73 | 71, 72 | syl 17 |
. . . . . . . 8
 

        |
74 | 73, 55, 57 | redivcld 10432 |
. . . . . . 7
 

          |
75 | 69, 74 | eqeltrd 2528 |
. . . . . 6
 

                |
76 | 71 | recnd 9666 |
. . . . . . . . . . 11
 

    |
77 | | 1cnd 9656 |
. . . . . . . . . . 11
 

  |
78 | | nncn 10614 |
. . . . . . . . . . . 12
   |
79 | 78 | adantl 468 |
. . . . . . . . . . 11
 

  |
80 | 76, 77, 79, 57 | divsubdird 10419 |
. . . . . . . . . 10
 

                |
81 | 12 | adantr 467 |
. . . . . . . . . . . . . 14
 

  |
82 | 13 | adantr 467 |
. . . . . . . . . . . . . 14
 

  |
83 | 79, 81, 82 | divrecd 10383 |
. . . . . . . . . . . . 13
 

        |
84 | 83 | oveq1d 6303 |
. . . . . . . . . . . 12
 

            |
85 | 27, 79, 57 | divcan3d 10385 |
. . . . . . . . . . . 12
 

          |
86 | 84, 85 | eqtrd 2484 |
. . . . . . . . . . 11
 

        |
87 | 86 | oveq1d 6303 |
. . . . . . . . . 10
 

                |
88 | 80, 87 | eqtrd 2484 |
. . . . . . . . 9
 

              |
89 | | 1red 9655 |
. . . . . . . . . . 11
 

  |
90 | 71, 89 | resubcld 10044 |
. . . . . . . . . 10
 

      |
91 | | nnrp 11308 |
. . . . . . . . . . 11
   |
92 | 91 | adantl 468 |
. . . . . . . . . 10
 

  |
93 | 73, 89 | readdcld 9667 |
. . . . . . . . . . . 12
 

          |
94 | | flle 12032 |
. . . . . . . . . . . . . 14
             |
95 | 71, 94 | syl 17 |
. . . . . . . . . . . . 13
 

          |
96 | | flflp1 12040 |
. . . . . . . . . . . . . 14
    
                        |
97 | 71, 71, 96 | syl2anc 666 |
. . . . . . . . . . . . 13
 

        
             |
98 | 95, 97 | mpbid 214 |
. . . . . . . . . . . 12
 

      
     |
99 | 71, 93, 89, 98 | ltsub1dd 10222 |
. . . . . . . . . . 11
 

                |
100 | 73 | recnd 9666 |
. . . . . . . . . . . 12
 

        |
101 | 100, 77 | pncand 9984 |
. . . . . . . . . . 11
 

                  |
102 | 99, 101 | breqtrd 4426 |
. . . . . . . . . 10
 

            |
103 | 90, 73, 92, 102 | ltdiv1dd 11392 |
. . . . . . . . 9
 

          
     |
104 | 88, 103 | eqbrtrrd 4424 |
. . . . . . . 8
 

          
     |
105 | 59, 74, 104 | ltled 9780 |
. . . . . . 7
 

          
     |
106 | | simpr 463 |
. . . . . . . . . . 11
       |
107 | 106 | oveq1d 6303 |
. . . . . . . . . 10
           |
108 | 107 | fveq2d 5867 |
. . . . . . . . 9
                   |
109 | 108, 106 | oveq12d 6306 |
. . . . . . . 8
                       |
110 | 61, 109, 32, 68 | fvmptd 5952 |
. . . . . . 7
 

                        |
111 | 105, 44, 110 | 3brtr4d 4432 |
. . . . . 6
 

                            |
112 | 73, 71, 92, 95 | lediv1dd 11393 |
. . . . . . . 8
 

              |
113 | 112, 86 | breqtrd 4426 |
. . . . . . 7
 

            |
114 | 110, 113 | eqbrtrd 4422 |
. . . . . 6
 

                  |
115 | 9, 11, 49, 51, 60, 75, 111, 114 | climsqz 13697 |
. . . . 5
               |
116 | 16 | mptex 6134 |
. . . . . 6
                     |
117 | 116 | a1i 11 |
. . . . 5
                       |
118 | 3 | zred 11037 |
. . . . . . . . . 10
   |
119 | | 1red 9655 |
. . . . . . . . . 10
   |
120 | 118, 119 | resubcld 10044 |
. . . . . . . . 9
     |
121 | 120, 1 | nndivred 10655 |
. . . . . . . 8
       |
122 | 121 | flcld 12031 |
. . . . . . 7
           |
123 | 122 | zcnd 11038 |
. . . . . 6
           |
124 | | divcnv 13904 |
. . . . . 6
                       |
125 | 123, 124 | syl 17 |
. . . . 5
               |
126 | 75 | recnd 9666 |
. . . . 5
 

                |
127 | | eqidd 2451 |
. . . . . . 7
 

                          |
128 | | oveq2 6296 |
. . . . . . . 8
                       |
129 | 128 | adantl 468 |
. . . . . . 7
                           |
130 | | ovex 6316 |
. . . . . . . 8
           |
131 | 130 | a1i 11 |
. . . . . . 7
 

            |
132 | 127, 129,
32, 131 | fvmptd 5952 |
. . . . . 6
 

                            |
133 | 123 | adantr 467 |
. . . . . . 7
 

          |
134 | 133, 79, 57 | divcld 10380 |
. . . . . 6
 

            |
135 | 132, 134 | eqeltrd 2528 |
. . . . 5
 

                  |
136 | 100, 133,
79, 57 | divsubdird 10419 |
. . . . . 6
 

                                        |
137 | | eqidd 2451 |
. . . . . . 7
 

                                          |
138 | 63 | oveq1d 6303 |
. . . . . . . . 9
                                   |
139 | 138, 64 | oveq12d 6306 |
. . . . . . . 8
                                       |
140 | 139 | adantl 468 |
. . . . . . 7
                                           |
141 | | ovex 6316 |
. . . . . . . 8
                   |
142 | 141 | a1i 11 |
. . . . . . 7
 

                    |
143 | 137, 140,
32, 142 | fvmptd 5952 |
. . . . . 6
 

                                            |
144 | 69, 132 | oveq12d 6306 |
. . . . . 6
 

                                                      |
145 | 136, 143,
144 | 3eqtr4d 2494 |
. . . . 5
 

                                                          |
146 | 9, 11, 115, 117, 125, 126, 135, 145 | climsub 13690 |
. . . 4
                           |
147 | 146, 48 | breqtrd 4426 |
. . 3
                         |
148 | | uzssz 11175 |
. . . . . . 7
   
   |
149 | | resmpt 5153 |
. . . . . . 7
                                       
                       |
150 | 148, 149 | ax-mp 5 |
. . . . . 6
                                
                      |
151 | 150 | breq1i 4408 |
. . . . 5
                     
   
    
                              |
152 | 3, 11 | zsubcld 11042 |
. . . . . 6
     |
153 | | zex 10943 |
. . . . . . 7
 |
154 | 153 | mptex 6134 |
. . . . . 6
                     |
155 | | climres 13632 |
. . . . . 6
                                                       
                         |
156 | 152, 154,
155 | sylancl 667 |
. . . . 5
                               
                         |
157 | 151, 156 | syl5bbr 263 |
. . . 4
                             
                         |
158 | 9 | reseq2i 5101 |
. . . . . 6
                                          
      |
159 | 158 | breq1i 4408 |
. . . . 5
                     
                                 |
160 | | nnssz 10954 |
. . . . . . 7
 |
161 | | resmpt 5153 |
. . . . . . 7

                                            |
162 | 160, 161 | ax-mp 5 |
. . . . . 6
                                           |
163 | 162 | breq1i 4408 |
. . . . 5
                     
                           |
164 | | climres 13632 |
. . . . . 6
                                                   
                         |
165 | 10, 154, 164 | mp2an 677 |
. . . . 5
                     
      
                        |
166 | 159, 163,
165 | 3bitr3i 279 |
. . . 4
                                               |
167 | 157, 166 | syl6bbr 267 |
. . 3
                             
                         |
168 | 147, 167 | mpbird 236 |
. 2
                               |
169 | 8, 168 | eqbrtrd 4422 |
1
            
                |