Step | Hyp | Ref
| Expression |
1 | | fsumcl2lem.5 |
. . . 4
|
2 | 1 | neneqd 2361 |
. . 3
|
3 | 2 | pm2.21d 614 |
. 2
|
4 | | fsumcllem.1 |
. . . . . . . . . . . 12
|
5 | 4 | adantr 274 |
. . . . . . . . . . 11
|
6 | | fsumcllem.4 |
. . . . . . . . . . 11
|
7 | 5, 6 | sseldd 3148 |
. . . . . . . . . 10
|
8 | 7 | ralrimiva 2543 |
. . . . . . . . 9
|
9 | | sumfct 11337 |
. . . . . . . . 9
|
10 | 8, 9 | syl 14 |
. . . . . . . 8
|
11 | 10 | adantr 274 |
. . . . . . 7
♯ ♯
|
12 | | fveq2 5496 |
. . . . . . . 8
|
13 | | simprl 526 |
. . . . . . . 8
♯ ♯ ♯ |
14 | | simprr 527 |
. . . . . . . 8
♯ ♯ ♯ |
15 | 4 | ad2antrr 485 |
. . . . . . . . 9
♯ ♯ |
16 | 6 | fmpttd 5651 |
. . . . . . . . . . 11
|
17 | 16 | adantr 274 |
. . . . . . . . . 10
♯ ♯ |
18 | 17 | ffvelrnda 5631 |
. . . . . . . . 9
♯ ♯ |
19 | 15, 18 | sseldd 3148 |
. . . . . . . 8
♯ ♯ |
20 | | f1of 5442 |
. . . . . . . . . 10
♯ ♯ |
21 | 14, 20 | syl 14 |
. . . . . . . . 9
♯ ♯ ♯ |
22 | | fvco3 5567 |
. . . . . . . . 9
♯
♯ |
23 | 21, 22 | sylan 281 |
. . . . . . . 8
♯ ♯ ♯ |
24 | 12, 13, 14, 19, 23 | fsum3 11350 |
. . . . . . 7
♯ ♯ ♯ ♯ |
25 | 11, 24 | eqtr3d 2205 |
. . . . . 6
♯ ♯
♯ ♯ |
26 | | nnuz 9522 |
. . . . . . . 8
|
27 | 13, 26 | eleqtrdi 2263 |
. . . . . . 7
♯ ♯ ♯ |
28 | | elnnuz 9523 |
. . . . . . . . . . 11
|
29 | 28 | biimpri 132 |
. . . . . . . . . 10
|
30 | 29 | adantl 275 |
. . . . . . . . 9
♯ ♯
|
31 | 4 | ad3antrrr 489 |
. . . . . . . . . . . 12
♯ ♯ ♯
|
32 | 17 | ad2antrr 485 |
. . . . . . . . . . . . . 14
♯ ♯ ♯
|
33 | 21 | ad2antrr 485 |
. . . . . . . . . . . . . 14
♯ ♯ ♯
♯ |
34 | | fco 5363 |
. . . . . . . . . . . . . 14
♯ ♯ |
35 | 32, 33, 34 | syl2anc 409 |
. . . . . . . . . . . . 13
♯ ♯ ♯
♯ |
36 | | 1zzd 9239 |
. . . . . . . . . . . . . . 15
♯ ♯ ♯
|
37 | 13 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
♯ ♯ ♯
♯ |
38 | 37 | nnzd 9333 |
. . . . . . . . . . . . . . 15
♯ ♯ ♯
♯ |
39 | | simpr 109 |
. . . . . . . . . . . . . . . . 17
♯ ♯ |
40 | 39 | adantr 274 |
. . . . . . . . . . . . . . . 16
♯ ♯ ♯
|
41 | 40 | nnzd 9333 |
. . . . . . . . . . . . . . 15
♯ ♯ ♯
|
42 | 36, 38, 41 | 3jca 1172 |
. . . . . . . . . . . . . 14
♯ ♯ ♯
♯ |
43 | 40 | nnge1d 8921 |
. . . . . . . . . . . . . . 15
♯ ♯ ♯
|
44 | | simpr 109 |
. . . . . . . . . . . . . . 15
♯ ♯ ♯
♯ |
45 | 43, 44 | jca 304 |
. . . . . . . . . . . . . 14
♯ ♯ ♯
♯ |
46 | | elfz2 9972 |
. . . . . . . . . . . . . 14
♯ ♯ ♯ |
47 | 42, 45, 46 | sylanbrc 415 |
. . . . . . . . . . . . 13
♯ ♯ ♯
♯ |
48 | 35, 47 | ffvelrnd 5632 |
. . . . . . . . . . . 12
♯ ♯ ♯
|
49 | 31, 48 | sseldd 3148 |
. . . . . . . . . . 11
♯ ♯ ♯
|
50 | | 0cnd 7913 |
. . . . . . . . . . 11
♯ ♯ ♯
|
51 | 39 | nnzd 9333 |
. . . . . . . . . . . 12
♯ ♯ |
52 | 13 | adantr 274 |
. . . . . . . . . . . . 13
♯ ♯ ♯ |
53 | 52 | nnzd 9333 |
. . . . . . . . . . . 12
♯ ♯ ♯ |
54 | | zdcle 9288 |
. . . . . . . . . . . 12
♯
DECID
♯ |
55 | 51, 53, 54 | syl2anc 409 |
. . . . . . . . . . 11
♯ ♯
DECID
♯ |
56 | 49, 50, 55 | ifcldadc 3555 |
. . . . . . . . . 10
♯ ♯
♯ |
57 | 30, 56 | syldan 280 |
. . . . . . . . 9
♯ ♯
♯ |
58 | | breq1 3992 |
. . . . . . . . . . 11
♯
♯ |
59 | | fveq2 5496 |
. . . . . . . . . . 11
|
60 | 58, 59 | ifbieq1d 3548 |
. . . . . . . . . 10
♯ ♯ |
61 | | eqid 2170 |
. . . . . . . . . 10
♯ ♯ |
62 | 60, 61 | fvmptg 5572 |
. . . . . . . . 9
♯ ♯ ♯ |
63 | 30, 57, 62 | syl2anc 409 |
. . . . . . . 8
♯ ♯
♯ ♯ |
64 | 4 | adantr 274 |
. . . . . . . . . . . . 13
♯ ♯ |
65 | 17, 64 | fssd 5360 |
. . . . . . . . . . . 12
♯ ♯ |
66 | 65 | ad2antrr 485 |
. . . . . . . . . . 11
♯ ♯
♯ |
67 | 21 | ad2antrr 485 |
. . . . . . . . . . 11
♯ ♯
♯ ♯ |
68 | | fco 5363 |
. . . . . . . . . . 11
♯ ♯ |
69 | 66, 67, 68 | syl2anc 409 |
. . . . . . . . . 10
♯ ♯
♯ ♯ |
70 | | 1zzd 9239 |
. . . . . . . . . . . 12
♯ ♯
♯ |
71 | 13 | ad2antrr 485 |
. . . . . . . . . . . . 13
♯ ♯
♯ ♯ |
72 | 71 | nnzd 9333 |
. . . . . . . . . . . 12
♯ ♯
♯ ♯ |
73 | | eluzelz 9496 |
. . . . . . . . . . . . 13
|
74 | 73 | ad2antlr 486 |
. . . . . . . . . . . 12
♯ ♯
♯
|
75 | 70, 72, 74 | 3jca 1172 |
. . . . . . . . . . 11
♯ ♯
♯ ♯ |
76 | 29 | nnge1d 8921 |
. . . . . . . . . . . . 13
|
77 | 76 | ad2antlr 486 |
. . . . . . . . . . . 12
♯ ♯
♯
|
78 | | simpr 109 |
. . . . . . . . . . . 12
♯ ♯
♯ ♯ |
79 | 77, 78 | jca 304 |
. . . . . . . . . . 11
♯ ♯
♯
♯ |
80 | 75, 79, 46 | sylanbrc 415 |
. . . . . . . . . 10
♯ ♯
♯
♯ |
81 | 69, 80 | ffvelrnd 5632 |
. . . . . . . . 9
♯ ♯
♯ |
82 | | 0cnd 7913 |
. . . . . . . . 9
♯ ♯
♯
|
83 | 30, 55 | syldan 280 |
. . . . . . . . 9
♯ ♯
DECID
♯ |
84 | 81, 82, 83 | ifcldadc 3555 |
. . . . . . . 8
♯ ♯
♯ |
85 | 63, 84 | eqeltrd 2247 |
. . . . . . 7
♯ ♯
♯ |
86 | | elfzle2 9984 |
. . . . . . . . . . 11
♯
♯ |
87 | 86 | adantl 275 |
. . . . . . . . . 10
♯ ♯ ♯ ♯ |
88 | 87 | iftrued 3533 |
. . . . . . . . 9
♯ ♯ ♯ ♯ |
89 | | elfznn 10010 |
. . . . . . . . . . 11
♯
|
90 | 89 | anim2i 340 |
. . . . . . . . . 10
♯ ♯ ♯ ♯ ♯
|
91 | 90, 87, 48 | syl2anc 409 |
. . . . . . . . 9
♯ ♯ ♯ |
92 | 88, 91 | eqeltrd 2247 |
. . . . . . . 8
♯ ♯ ♯ ♯ |
93 | 39, 56, 62 | syl2anc 409 |
. . . . . . . . . 10
♯ ♯ ♯ ♯ |
94 | 93 | eleq1d 2239 |
. . . . . . . . 9
♯ ♯ ♯ ♯ |
95 | 90, 94 | syl 14 |
. . . . . . . 8
♯ ♯ ♯ ♯
♯ |
96 | 92, 95 | mpbird 166 |
. . . . . . 7
♯ ♯ ♯
♯ |
97 | | fsumcllem.2 |
. . . . . . . 8
|
98 | 97 | adantlr 474 |
. . . . . . 7
♯ ♯ |
99 | | addcl 7899 |
. . . . . . . 8
|
100 | 99 | adantl 275 |
. . . . . . 7
♯ ♯ |
101 | 27, 85, 96, 98, 64, 100 | seq3clss 10423 |
. . . . . 6
♯ ♯ ♯ ♯ |
102 | 25, 101 | eqeltrd 2247 |
. . . . 5
♯ ♯ |
103 | 102 | expr 373 |
. . . 4
♯ ♯ |
104 | 103 | exlimdv 1812 |
. . 3
♯ ♯
|
105 | 104 | expimpd 361 |
. 2
♯ ♯
|
106 | | fsumcllem.3 |
. . 3
|
107 | | fz1f1o 11338 |
. . 3
♯ ♯ |
108 | 106, 107 | syl 14 |
. 2
♯ ♯ |
109 | 3, 105, 108 | mpjaod 713 |
1
|