Step | Hyp | Ref
| Expression |
1 | | nconstwlpolemgt0.0 |
. 2
|
2 | | 1zzd 9188 |
. . . . . . 7
|
3 | | simprl 521 |
. . . . . . . . . 10
|
4 | 3 | peano2nnd 8842 |
. . . . . . . . 9
|
5 | 4 | nnzd 9279 |
. . . . . . . 8
|
6 | 5, 2 | zsubcld 9285 |
. . . . . . 7
|
7 | 2, 6 | fzfigd 10323 |
. . . . . 6
|
8 | | elfznn 9949 |
. . . . . . 7
|
9 | | 2rp 9558 |
. . . . . . . . . . . 12
|
10 | 9 | a1i 9 |
. . . . . . . . . . 11
|
11 | | simpr 109 |
. . . . . . . . . . . 12
|
12 | 11 | nnzd 9279 |
. . . . . . . . . . 11
|
13 | 10, 12 | rpexpcld 10568 |
. . . . . . . . . 10
|
14 | 13 | rpreccld 9607 |
. . . . . . . . 9
|
15 | 14 | rpred 9596 |
. . . . . . . 8
|
16 | | 0re 7872 |
. . . . . . . . . 10
|
17 | | 1re 7871 |
. . . . . . . . . 10
|
18 | | prssi 3714 |
. . . . . . . . . 10
|
19 | 16, 17, 18 | mp2an 423 |
. . . . . . . . 9
|
20 | | nconstwlpolem0.g |
. . . . . . . . . . 11
|
21 | 20 | ad2antrr 480 |
. . . . . . . . . 10
|
22 | 21, 11 | ffvelrnd 5602 |
. . . . . . . . 9
|
23 | 19, 22 | sseldi 3126 |
. . . . . . . 8
|
24 | 15, 23 | remulcld 7902 |
. . . . . . 7
|
25 | 8, 24 | sylan2 284 |
. . . . . 6
|
26 | 7, 25 | fsumrecl 11291 |
. . . . 5
|
27 | | eqid 2157 |
. . . . . 6
|
28 | | eqid 2157 |
. . . . . . 7
|
29 | | oveq2 5829 |
. . . . . . . . 9
|
30 | 29 | oveq2d 5837 |
. . . . . . . 8
|
31 | | fveq2 5467 |
. . . . . . . 8
|
32 | 30, 31 | oveq12d 5839 |
. . . . . . 7
|
33 | | eluznn 9504 |
. . . . . . . 8
|
34 | 4, 33 | sylan 281 |
. . . . . . 7
|
35 | 34, 24 | syldan 280 |
. . . . . . 7
|
36 | 28, 32, 34, 35 | fvmptd3 5560 |
. . . . . 6
|
37 | 20, 28 | trilpolemclim 13578 |
. . . . . . . 8
|
38 | 37 | adantr 274 |
. . . . . . 7
|
39 | | nnuz 9468 |
. . . . . . . 8
|
40 | 28, 32, 11, 24 | fvmptd3 5560 |
. . . . . . . . 9
|
41 | 24 | recnd 7900 |
. . . . . . . . 9
|
42 | 40, 41 | eqeltrd 2234 |
. . . . . . . 8
|
43 | 39, 4, 42 | iserex 11229 |
. . . . . . 7
|
44 | 38, 43 | mpbid 146 |
. . . . . 6
|
45 | 27, 5, 36, 35, 44 | isumrecl 11319 |
. . . . 5
|
46 | 3 | nnzd 9279 |
. . . . . . . . . 10
|
47 | | fzofig 10324 |
. . . . . . . . . 10
..^ |
48 | 2, 46, 47 | syl2anc 409 |
. . . . . . . . 9
..^ |
49 | | elfzo1 10082 |
. . . . . . . . . . 11
..^ |
50 | 49 | simp1bi 997 |
. . . . . . . . . 10
..^
|
51 | 50, 24 | sylan2 284 |
. . . . . . . . 9
..^ |
52 | 48, 51 | fsumrecl 11291 |
. . . . . . . 8
..^ |
53 | 9 | a1i 9 |
. . . . . . . . . . . 12
|
54 | 53, 46 | rpexpcld 10568 |
. . . . . . . . . . 11
|
55 | 54 | rpreccld 9607 |
. . . . . . . . . 10
|
56 | 55 | rpred 9596 |
. . . . . . . . 9
|
57 | 20 | adantr 274 |
. . . . . . . . . . 11
|
58 | 57, 3 | ffvelrnd 5602 |
. . . . . . . . . 10
|
59 | 19, 58 | sseldi 3126 |
. . . . . . . . 9
|
60 | 56, 59 | remulcld 7902 |
. . . . . . . 8
|
61 | 14 | rpge0d 9600 |
. . . . . . . . . . 11
|
62 | | 0le0 8916 |
. . . . . . . . . . . . 13
|
63 | | simpr 109 |
. . . . . . . . . . . . 13
|
64 | 62, 63 | breqtrrid 4002 |
. . . . . . . . . . . 12
|
65 | | 0le1 8350 |
. . . . . . . . . . . . 13
|
66 | | simpr 109 |
. . . . . . . . . . . . 13
|
67 | 65, 66 | breqtrrid 4002 |
. . . . . . . . . . . 12
|
68 | | elpri 3583 |
. . . . . . . . . . . . 13
|
69 | 22, 68 | syl 14 |
. . . . . . . . . . . 12
|
70 | 64, 67, 69 | mpjaodan 788 |
. . . . . . . . . . 11
|
71 | 15, 23, 61, 70 | mulge0d 8490 |
. . . . . . . . . 10
|
72 | 50, 71 | sylan2 284 |
. . . . . . . . 9
..^ |
73 | 48, 51, 72 | fsumge0 11349 |
. . . . . . . 8
..^ |
74 | 55 | rpgt0d 9599 |
. . . . . . . . 9
|
75 | | simprr 522 |
. . . . . . . . . . 11
|
76 | 75 | oveq2d 5837 |
. . . . . . . . . 10
|
77 | 56 | recnd 7900 |
. . . . . . . . . . 11
|
78 | 77 | mulid1d 7889 |
. . . . . . . . . 10
|
79 | 76, 78 | eqtrd 2190 |
. . . . . . . . 9
|
80 | 74, 79 | breqtrrd 3992 |
. . . . . . . 8
|
81 | 52, 60, 73, 80 | addgegt0d 8388 |
. . . . . . 7
..^ |
82 | | nfv 1508 |
. . . . . . . 8
|
83 | | nfcv 2299 |
. . . . . . . 8
|
84 | | fzonel 10052 |
. . . . . . . . 9
..^ |
85 | 84 | a1i 9 |
. . . . . . . 8
..^ |
86 | 50, 41 | sylan2 284 |
. . . . . . . 8
..^ |
87 | | oveq2 5829 |
. . . . . . . . . 10
|
88 | 87 | oveq2d 5837 |
. . . . . . . . 9
|
89 | | fveq2 5467 |
. . . . . . . . 9
|
90 | 88, 89 | oveq12d 5839 |
. . . . . . . 8
|
91 | 60 | recnd 7900 |
. . . . . . . 8
|
92 | 82, 83, 48, 3, 85, 86, 90, 91 | fsumsplitsn 11300 |
. . . . . . 7
..^
..^ |
93 | 81, 92 | breqtrrd 3992 |
. . . . . 6
..^ |
94 | 3 | nncnd 8841 |
. . . . . . . . . 10
|
95 | | 1cnd 7888 |
. . . . . . . . . 10
|
96 | 94, 95 | pncand 8181 |
. . . . . . . . 9
|
97 | 96 | oveq2d 5837 |
. . . . . . . 8
|
98 | 3, 39 | eleqtrdi 2250 |
. . . . . . . . 9
|
99 | | fzisfzounsn 10128 |
. . . . . . . . 9
..^ |
100 | 98, 99 | syl 14 |
. . . . . . . 8
..^ |
101 | 97, 100 | eqtrd 2190 |
. . . . . . 7
..^ |
102 | 101 | sumeq1d 11256 |
. . . . . 6
..^ |
103 | 93, 102 | breqtrrd 3992 |
. . . . 5
|
104 | 34, 15 | syldan 280 |
. . . . . . 7
|
105 | 34, 23 | syldan 280 |
. . . . . . 7
|
106 | 34, 14 | syldan 280 |
. . . . . . . 8
|
107 | 106 | rpge0d 9600 |
. . . . . . 7
|
108 | 34, 70 | syldan 280 |
. . . . . . 7
|
109 | 104, 105,
107, 108 | mulge0d 8490 |
. . . . . 6
|
110 | 27, 5, 36, 35, 44, 109 | isumge0 11320 |
. . . . 5
|
111 | 26, 45, 103, 110 | addgtge0d 8389 |
. . . 4
|
112 | 39, 27, 4, 40, 41, 38 | isumsplit 11381 |
. . . 4
|
113 | 111, 112 | breqtrrd 3992 |
. . 3
|
114 | | nconstwlpolem0.a |
. . 3
|
115 | 113, 114 | breqtrrdi 4006 |
. 2
|
116 | 1, 115 | rexlimddv 2579 |
1
|