Step | Hyp | Ref
| Expression |
1 | | stirlinglem14.1 |
. . 3
                       |
2 | | stirlinglem14.2 |
. . 3
           |
3 | 1, 2 | stirlinglem13 38060 |
. 2
  |
4 | | simpl 464 |
. . . . 5
     |
5 | 4 | rpefcld 14236 |
. . . 4
         |
6 | | nnuz 11218 |
. . . . . 6
     |
7 | | 1zzd 10992 |
. . . . . 6
     |
8 | | efcn 23477 |
. . . . . . 7
     |
9 | 8 | a1i 11 |
. . . . . 6
         |
10 | | nnnn0 10900 |
. . . . . . . . . . . . 13
   |
11 | | faccl 12507 |
. . . . . . . . . . . . 13

      |
12 | | nncn 10639 |
. . . . . . . . . . . . 13
           |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . . 12
       |
14 | | 2cnd 10704 |
. . . . . . . . . . . . . . 15
   |
15 | | nncn 10639 |
. . . . . . . . . . . . . . 15
   |
16 | 14, 15 | mulcld 9681 |
. . . . . . . . . . . . . 14
     |
17 | 16 | sqrtcld 13576 |
. . . . . . . . . . . . 13
         |
18 | | epr 14337 |
. . . . . . . . . . . . . . . . 17
 |
19 | | rpcn 11333 |
. . . . . . . . . . . . . . . . 17

  |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
 |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
22 | | 0re 9661 |
. . . . . . . . . . . . . . . . 17
 |
23 | | epos 14336 |
. . . . . . . . . . . . . . . . 17
 |
24 | 22, 23 | gtneii 9764 |
. . . . . . . . . . . . . . . 16
 |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
26 | 15, 21, 25 | divcld 10405 |
. . . . . . . . . . . . . 14
     |
27 | 26, 10 | expcld 12454 |
. . . . . . . . . . . . 13
         |
28 | 17, 27 | mulcld 9681 |
. . . . . . . . . . . 12
                 |
29 | | 2rp 11330 |
. . . . . . . . . . . . . . . . 17
 |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
31 | | nnrp 11334 |
. . . . . . . . . . . . . . . 16
   |
32 | 30, 31 | rpmulcld 11380 |
. . . . . . . . . . . . . . 15
     |
33 | 32 | sqrtgt0d 13551 |
. . . . . . . . . . . . . 14
         |
34 | 33 | gt0ne0d 10199 |
. . . . . . . . . . . . 13
         |
35 | | nnne0 10664 |
. . . . . . . . . . . . . . 15
   |
36 | 15, 21, 35, 25 | divne0d 10421 |
. . . . . . . . . . . . . 14
     |
37 | | nnz 10983 |
. . . . . . . . . . . . . 14
   |
38 | 26, 36, 37 | expne0d 12460 |
. . . . . . . . . . . . 13
         |
39 | 17, 27, 34, 38 | mulne0d 10286 |
. . . . . . . . . . . 12
                 |
40 | 13, 28, 39 | divcld 10405 |
. . . . . . . . . . 11
                       |
41 | 1 | fvmpt2 5972 |
. . . . . . . . . . 11
                                                 |
42 | 40, 41 | mpdan 681 |
. . . . . . . . . 10
                           |
43 | 42, 40 | eqeltrd 2549 |
. . . . . . . . 9
       |
44 | | nnne0 10664 |
. . . . . . . . . . . 12
           |
45 | 10, 11, 44 | 3syl 18 |
. . . . . . . . . . 11
       |
46 | 13, 28, 45, 39 | divne0d 10421 |
. . . . . . . . . 10
                       |
47 | 42, 46 | eqnetrd 2710 |
. . . . . . . . 9
       |
48 | 43, 47 | logcld 23599 |
. . . . . . . 8
           |
49 | 2, 48 | fmpti 6060 |
. . . . . . 7
     |
50 | 49 | a1i 11 |
. . . . . 6
         |
51 | | simpr 468 |
. . . . . 6
     |
52 | 4 | recnd 9687 |
. . . . . 6
     |
53 | 6, 7, 9, 50, 51, 52 | climcncf 22010 |
. . . . 5
           |
54 | 8 | elexi 3041 |
. . . . . . . . 9
 |
55 | | nnex 10637 |
. . . . . . . . . . 11
 |
56 | 55 | mptex 6152 |
. . . . . . . . . 10
           |
57 | 2, 56 | eqeltri 2545 |
. . . . . . . . 9
 |
58 | 54, 57 | coex 6764 |
. . . . . . . 8
   |
59 | 58 | a1i 11 |
. . . . . . 7
    |
60 | 55 | mptex 6152 |
. . . . . . . . 9
                       |
61 | 1, 60 | eqeltri 2545 |
. . . . . . . 8
 |
62 | 61 | a1i 11 |
. . . . . . 7
  |
63 | | 1zzd 10992 |
. . . . . . 7
  |
64 | 2 | funmpt2 5626 |
. . . . . . . . . 10
 |
65 | | id 22 |
. . . . . . . . . . 11
   |
66 | | rabid2 2954 |
. . . . . . . . . . . . 13
                      |
67 | 1 | stirlinglem2 38049 |
. . . . . . . . . . . . . 14
       |
68 | | relogcl 23604 |
. . . . . . . . . . . . . 14
    
          |
69 | | elex 3040 |
. . . . . . . . . . . . . 14
                   |
70 | 67, 68, 69 | 3syl 18 |
. . . . . . . . . . . . 13
           |
71 | 66, 70 | mprgbir 2771 |
. . . . . . . . . . . 12

          |
72 | 2 | dmmpt 5337 |
. . . . . . . . . . . 12
           |
73 | 71, 72 | eqtr4i 2496 |
. . . . . . . . . . 11
 |
74 | 65, 73 | syl6eleq 2559 |
. . . . . . . . . 10
   |
75 | | fvco 5956 |
. . . . . . . . . 10
                   |
76 | 64, 74, 75 | sylancr 676 |
. . . . . . . . 9
  
              |
77 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
                         |
78 | | simpr 468 |
. . . . . . . . . . . . . . . 16
 
   |
79 | 78 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
 
           |
80 | 78 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
 
       |
81 | 80 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
 
               |
82 | 78 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
 
  
    |
83 | 82, 78 | oveq12d 6326 |
. . . . . . . . . . . . . . . 16
 
               |
84 | 81, 83 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
 
                               |
85 | 79, 84 | oveq12d 6326 |
. . . . . . . . . . . . . 14
 
                                           |
86 | | nnnn0 10900 |
. . . . . . . . . . . . . . . 16
   |
87 | | faccl 12507 |
. . . . . . . . . . . . . . . 16

      |
88 | | nncn 10639 |
. . . . . . . . . . . . . . . 16
           |
89 | 86, 87, 88 | 3syl 18 |
. . . . . . . . . . . . . . 15
       |
90 | | 2cnd 10704 |
. . . . . . . . . . . . . . . . . 18
   |
91 | | nncn 10639 |
. . . . . . . . . . . . . . . . . 18
   |
92 | 90, 91 | mulcld 9681 |
. . . . . . . . . . . . . . . . 17
     |
93 | 92 | sqrtcld 13576 |
. . . . . . . . . . . . . . . 16
         |
94 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   |
95 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   |
96 | 91, 94, 95 | divcld 10405 |
. . . . . . . . . . . . . . . . 17
     |
97 | 96, 86 | expcld 12454 |
. . . . . . . . . . . . . . . 16
         |
98 | 93, 97 | mulcld 9681 |
. . . . . . . . . . . . . . 15
                 |
99 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
   |
100 | | nnrp 11334 |
. . . . . . . . . . . . . . . . . . 19
   |
101 | 99, 100 | rpmulcld 11380 |
. . . . . . . . . . . . . . . . . 18
     |
102 | 101 | sqrtgt0d 13551 |
. . . . . . . . . . . . . . . . 17
         |
103 | 102 | gt0ne0d 10199 |
. . . . . . . . . . . . . . . 16
         |
104 | | nnne0 10664 |
. . . . . . . . . . . . . . . . . 18
   |
105 | 91, 94, 104, 95 | divne0d 10421 |
. . . . . . . . . . . . . . . . 17
     |
106 | | nnz 10983 |
. . . . . . . . . . . . . . . . 17
   |
107 | 96, 105, 106 | expne0d 12460 |
. . . . . . . . . . . . . . . 16
         |
108 | 93, 97, 103, 107 | mulne0d 10286 |
. . . . . . . . . . . . . . 15
                 |
109 | 89, 98, 108 | divcld 10405 |
. . . . . . . . . . . . . 14
                       |
110 | 77, 85, 65, 109 | fvmptd 5969 |
. . . . . . . . . . . . 13
                           |
111 | 110, 109 | eqeltrd 2549 |
. . . . . . . . . . . 12
       |
112 | | nnne0 10664 |
. . . . . . . . . . . . . . 15
           |
113 | 86, 87, 112 | 3syl 18 |
. . . . . . . . . . . . . 14
       |
114 | 89, 98, 113, 108 | divne0d 10421 |
. . . . . . . . . . . . 13
                       |
115 | 110, 114 | eqnetrd 2710 |
. . . . . . . . . . . 12
       |
116 | 111, 115 | logcld 23599 |
. . . . . . . . . . 11
           |
117 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
118 | | nfcv 2612 |
. . . . . . . . . . . . 13
   |
119 | | nfmpt1 4485 |
. . . . . . . . . . . . . . 15
                         |
120 | 1, 119 | nfcxfr 2610 |
. . . . . . . . . . . . . 14
   |
121 | 120, 117 | nffv 5886 |
. . . . . . . . . . . . 13
       |
122 | 118, 121 | nffv 5886 |
. . . . . . . . . . . 12
           |
123 | | fveq2 5879 |
. . . . . . . . . . . . 13
           |
124 | 123 | fveq2d 5883 |
. . . . . . . . . . . 12
                   |
125 | 117, 122,
124, 2 | fvmptf 5981 |
. . . . . . . . . . 11
                         |
126 | 116, 125 | mpdan 681 |
. . . . . . . . . 10
               |
127 | 126 | fveq2d 5883 |
. . . . . . . . 9
                       |
128 | | eflog 23605 |
. . . . . . . . . 10
                             |
129 | 111, 115,
128 | syl2anc 673 |
. . . . . . . . 9
                   |
130 | 76, 127, 129 | 3eqtrd 2509 |
. . . . . . . 8
  
          |
131 | 130 | adantl 473 |
. . . . . . 7
   
          |
132 | 6, 59, 62, 63, 131 | climeq 13708 |
. . . . . 6
      
       |
133 | 132 | trud 1461 |
. . . . 5
      
      |
134 | 53, 133 | sylib 201 |
. . . 4
         |
135 | | breq2 4399 |
. . . . 5
    
        |
136 | 135 | rspcev 3136 |
. . . 4
          
   |
137 | 5, 134, 136 | syl2anc 673 |
. . 3
      |
138 | 137 | rexlimiva 2868 |
. 2
     |
139 | 3, 138 | ax-mp 5 |
1
  |