Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . . . 5
|
2 | | 1zzd 11408 |
. . . . 5
|
3 | | emcl.1 |
. . . . . . . 8
|
4 | | emcl.2 |
. . . . . . . 8
|
5 | | emcl.3 |
. . . . . . . 8
|
6 | | emcl.4 |
. . . . . . . 8
|
7 | 3, 4, 5, 6 | emcllem6 24727 |
. . . . . . 7
|
8 | 7 | simpri 478 |
. . . . . 6
|
9 | 8 | a1i 11 |
. . . . 5
|
10 | 3, 4 | emcllem1 24722 |
. . . . . . . 8
|
11 | 10 | simpri 478 |
. . . . . . 7
|
12 | 11 | ffvelrni 6358 |
. . . . . 6
|
13 | 12 | adantl 482 |
. . . . 5
|
14 | 1, 2, 9, 13 | climrecl 14314 |
. . . 4
|
15 | | 1nn 11031 |
. . . . 5
|
16 | | simpr 477 |
. . . . . . 7
|
17 | 8 | a1i 11 |
. . . . . . 7
|
18 | 12 | adantl 482 |
. . . . . . 7
|
19 | 3, 4 | emcllem2 24723 |
. . . . . . . . 9
|
20 | 19 | simprd 479 |
. . . . . . . 8
|
21 | 20 | adantl 482 |
. . . . . . 7
|
22 | 1, 16, 17, 18, 21 | climub 14392 |
. . . . . 6
|
23 | 22 | ralrimiva 2966 |
. . . . 5
|
24 | | fveq2 6191 |
. . . . . . . 8
|
25 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
26 | 25 | sumeq1d 14431 |
. . . . . . . . . . . 12
|
27 | | 1z 11407 |
. . . . . . . . . . . . 13
|
28 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
29 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
30 | | 1div1e1 10717 |
. . . . . . . . . . . . . . 15
|
31 | 29, 30 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
32 | 31 | fsum1 14476 |
. . . . . . . . . . . . 13
|
33 | 27, 28, 32 | mp2an 708 |
. . . . . . . . . . . 12
|
34 | 26, 33 | syl6eq 2672 |
. . . . . . . . . . 11
|
35 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
36 | | df-2 11079 |
. . . . . . . . . . . . 13
|
37 | 35, 36 | syl6eqr 2674 |
. . . . . . . . . . . 12
|
38 | 37 | fveq2d 6195 |
. . . . . . . . . . 11
|
39 | 34, 38 | oveq12d 6668 |
. . . . . . . . . 10
|
40 | | 1re 10039 |
. . . . . . . . . . . 12
|
41 | | 2rp 11837 |
. . . . . . . . . . . . 13
|
42 | | relogcl 24322 |
. . . . . . . . . . . . 13
|
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . 12
|
44 | 40, 43 | resubcli 10343 |
. . . . . . . . . . 11
|
45 | 44 | elexi 3213 |
. . . . . . . . . 10
|
46 | 39, 4, 45 | fvmpt 6282 |
. . . . . . . . 9
|
47 | 15, 46 | ax-mp 5 |
. . . . . . . 8
|
48 | 24, 47 | syl6eq 2672 |
. . . . . . 7
|
49 | 48 | breq1d 4663 |
. . . . . 6
|
50 | 49 | rspcva 3307 |
. . . . 5
|
51 | 15, 23, 50 | sylancr 695 |
. . . 4
|
52 | | fveq2 6191 |
. . . . . . . . . . . 12
|
53 | 52 | negeqd 10275 |
. . . . . . . . . . 11
|
54 | | eqid 2622 |
. . . . . . . . . . 11
|
55 | | negex 10279 |
. . . . . . . . . . 11
|
56 | 53, 54, 55 | fvmpt 6282 |
. . . . . . . . . 10
|
57 | 56 | adantl 482 |
. . . . . . . . 9
|
58 | 7 | simpli 474 |
. . . . . . . . . . . . 13
|
59 | 58 | a1i 11 |
. . . . . . . . . . . 12
|
60 | | 0cnd 10033 |
. . . . . . . . . . . 12
|
61 | | nnex 11026 |
. . . . . . . . . . . . . 14
|
62 | 61 | mptex 6486 |
. . . . . . . . . . . . 13
|
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
|
64 | 10 | simpli 474 |
. . . . . . . . . . . . . . 15
|
65 | 64 | ffvelrni 6358 |
. . . . . . . . . . . . . 14
|
66 | 65 | adantl 482 |
. . . . . . . . . . . . 13
|
67 | 66 | recnd 10068 |
. . . . . . . . . . . 12
|
68 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
69 | 68 | negeqd 10275 |
. . . . . . . . . . . . . . 15
|
70 | | negex 10279 |
. . . . . . . . . . . . . . 15
|
71 | 69, 54, 70 | fvmpt 6282 |
. . . . . . . . . . . . . 14
|
72 | 71 | adantl 482 |
. . . . . . . . . . . . 13
|
73 | | df-neg 10269 |
. . . . . . . . . . . . 13
|
74 | 72, 73 | syl6eq 2672 |
. . . . . . . . . . . 12
|
75 | 1, 2, 59, 60, 63, 67, 74 | climsubc2 14369 |
. . . . . . . . . . 11
|
76 | 75 | adantr 481 |
. . . . . . . . . 10
|
77 | 66 | renegcld 10457 |
. . . . . . . . . . . 12
|
78 | 72, 77 | eqeltrd 2701 |
. . . . . . . . . . 11
|
79 | 78 | adantlr 751 |
. . . . . . . . . 10
|
80 | 19 | simpld 475 |
. . . . . . . . . . . . . 14
|
81 | 80 | adantl 482 |
. . . . . . . . . . . . 13
|
82 | | peano2nn 11032 |
. . . . . . . . . . . . . . . 16
|
83 | 82 | adantl 482 |
. . . . . . . . . . . . . . 15
|
84 | 64 | ffvelrni 6358 |
. . . . . . . . . . . . . . 15
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . 14
|
86 | 85, 66 | lenegd 10606 |
. . . . . . . . . . . . 13
|
87 | 81, 86 | mpbid 222 |
. . . . . . . . . . . 12
|
88 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
89 | 88 | negeqd 10275 |
. . . . . . . . . . . . . 14
|
90 | | negex 10279 |
. . . . . . . . . . . . . 14
|
91 | 89, 54, 90 | fvmpt 6282 |
. . . . . . . . . . . . 13
|
92 | 83, 91 | syl 17 |
. . . . . . . . . . . 12
|
93 | 87, 72, 92 | 3brtr4d 4685 |
. . . . . . . . . . 11
|
94 | 93 | adantlr 751 |
. . . . . . . . . 10
|
95 | 1, 16, 76, 79, 94 | climub 14392 |
. . . . . . . . 9
|
96 | 57, 95 | eqbrtrrd 4677 |
. . . . . . . 8
|
97 | | df-neg 10269 |
. . . . . . . 8
|
98 | 96, 97 | syl6breqr 4695 |
. . . . . . 7
|
99 | 14 | trud 1493 |
. . . . . . . 8
|
100 | 64 | ffvelrni 6358 |
. . . . . . . . 9
|
101 | 100 | adantl 482 |
. . . . . . . 8
|
102 | | leneg 10531 |
. . . . . . . 8
|
103 | 99, 101, 102 | sylancr 695 |
. . . . . . 7
|
104 | 98, 103 | mpbird 247 |
. . . . . 6
|
105 | 104 | ralrimiva 2966 |
. . . . 5
|
106 | | fveq2 6191 |
. . . . . . . 8
|
107 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
108 | | log1 24332 |
. . . . . . . . . . . . 13
|
109 | 107, 108 | syl6eq 2672 |
. . . . . . . . . . . 12
|
110 | 34, 109 | oveq12d 6668 |
. . . . . . . . . . 11
|
111 | | 1m0e1 11131 |
. . . . . . . . . . 11
|
112 | 110, 111 | syl6eq 2672 |
. . . . . . . . . 10
|
113 | 40 | elexi 3213 |
. . . . . . . . . 10
|
114 | 112, 3, 113 | fvmpt 6282 |
. . . . . . . . 9
|
115 | 15, 114 | ax-mp 5 |
. . . . . . . 8
|
116 | 106, 115 | syl6eq 2672 |
. . . . . . 7
|
117 | 116 | breq2d 4665 |
. . . . . 6
|
118 | 117 | rspcva 3307 |
. . . . 5
|
119 | 15, 105, 118 | sylancr 695 |
. . . 4
|
120 | 44, 40 | elicc2i 12239 |
. . . 4
|
121 | 14, 51, 119, 120 | syl3anbrc 1246 |
. . 3
|
122 | | ffn 6045 |
. . . . 5
|
123 | 64, 122 | mp1i 13 |
. . . 4
|
124 | 16, 1 | syl6eleq 2711 |
. . . . . . . 8
|
125 | | elfznn 12370 |
. . . . . . . . . 10
|
126 | 125 | adantl 482 |
. . . . . . . . 9
|
127 | 126, 65 | syl 17 |
. . . . . . . 8
|
128 | | elfznn 12370 |
. . . . . . . . . 10
|
129 | 128 | adantl 482 |
. . . . . . . . 9
|
130 | 129, 80 | syl 17 |
. . . . . . . 8
|
131 | 124, 127,
130 | monoord2 12832 |
. . . . . . 7
|
132 | 131, 115 | syl6breq 4694 |
. . . . . 6
|
133 | 99, 40 | elicc2i 12239 |
. . . . . 6
|
134 | 101, 104,
132, 133 | syl3anbrc 1246 |
. . . . 5
|
135 | 134 | ralrimiva 2966 |
. . . 4
|
136 | | ffnfv 6388 |
. . . 4
|
137 | 123, 135,
136 | sylanbrc 698 |
. . 3
|
138 | | ffn 6045 |
. . . . 5
|
139 | 11, 138 | mp1i 13 |
. . . 4
|
140 | 11 | ffvelrni 6358 |
. . . . . . 7
|
141 | 140 | adantl 482 |
. . . . . 6
|
142 | 126, 12 | syl 17 |
. . . . . . . 8
|
143 | 129, 20 | syl 17 |
. . . . . . . 8
|
144 | 124, 142,
143 | monoord 12831 |
. . . . . . 7
|
145 | 47, 144 | syl5eqbrr 4689 |
. . . . . 6
|
146 | 44, 99 | elicc2i 12239 |
. . . . . 6
|
147 | 141, 145,
22, 146 | syl3anbrc 1246 |
. . . . 5
|
148 | 147 | ralrimiva 2966 |
. . . 4
|
149 | | ffnfv 6388 |
. . . 4
|
150 | 139, 148,
149 | sylanbrc 698 |
. . 3
|
151 | 121, 137,
150 | 3jca 1242 |
. 2
|
152 | 151 | trud 1493 |
1
|