Step Hyp Ref
Expression 1 bcxmaslem1 13646 . . . . 5
2 oveq2 6304 . . . . . 6
3 2 sumeq1d 13523 . . . . 5
4 1 , 3 eqeq12d 2479 . . . 4
5 4 imbi2d 316 . . 3
6 bcxmaslem1 13646 . . . . 5
7 oveq2 6304 . . . . . 6
8 7 sumeq1d 13523 . . . . 5
9 6 , 8 eqeq12d 2479 . . . 4
10 9 imbi2d 316 . . 3
11 bcxmaslem1 13646 . . . . 5
12 oveq2 6304 . . . . . 6
13 12 sumeq1d 13523 . . . . 5
14 11 , 13 eqeq12d 2479 . . . 4
15 14 imbi2d 316 . . 3
16 bcxmaslem1 13646 . . . . 5
17 oveq2 6304 . . . . . 6
18 17 sumeq1d 13523 . . . . 5
19 16 , 18 eqeq12d 2479 . . . 4
20 19 imbi2d 316 . . 3
21 0nn0 10835 . . . . 5
22 nn0addcl 10856 . . . . . 6
23 bcn0 12388 . . . . . 6
24 22 , 23 syl 16 . . . . 5
25 21 , 24 mpan2 671 . . . 4
26 0z 10900 . . . . 5
27 1nn0 10836 . . . . . . 7
28 25 , 27 syl6eqel 2553 . . . . . 6
29 28 nn0cnd 10879 . . . . 5
30 bcxmaslem1 13646 . . . . . 6
31 30 fsum1 13564 . . . . 5
32 26 , 29 , 31 sylancr 663 . . . 4
33 peano2nn0 10861 . . . . . 6
34 nn0addcl 10856 . . . . . 6
35 33 , 21 , 34 sylancl 662 . . . . 5
36 bcn0 12388 . . . . 5
37 35 , 36 syl 16 . . . 4
38 25 , 32 , 37 3eqtr4rd 2509 . . 3
39 simpr 461 . . . . . . . . . . 11
40 elnn0uz 11147 . . . . . . . . . . 11
41 39 , 40 sylib 196 . . . . . . . . . 10
42 simpl 457 . . . . . . . . . . . . 13
43 elfznn0 11800 . . . . . . . . . . . . 13
44 nn0addcl 10856 . . . . . . . . . . . . 13
45 42 , 43 , 44 syl2an 477 . . . . . . . . . . . 12
46 elfzelz 11717 . . . . . . . . . . . . 13
47 46 adantl 466 . . . . . . . . . . . 12
48 bccl 12400 . . . . . . . . . . . 12
49 45 , 47 , 48 syl2anc 661 . . . . . . . . . . 11
50 49 nn0cnd 10879 . . . . . . . . . 10
51 bcxmaslem1 13646 . . . . . . . . . 10
52 41 , 50 , 51 fsump1 13571 . . . . . . . . 9
53 nn0cn 10830 . . . . . . . . . . . . 13
54 53 adantr 465 . . . . . . . . . . . 12
55 nn0cn 10830 . . . . . . . . . . . . 13
56 55 adantl 466 . . . . . . . . . . . 12
57 1cnd 9633 . . . . . . . . . . . 12
58 add32r 9816 . . . . . . . . . . . 12
59 54 , 56 , 57 , 58 syl3anc 1228 . . . . . . . . . . 11
60 59 oveq1d 6311 . . . . . . . . . 10
61 60 oveq2d 6312 . . . . . . . . 9
62 52 , 61 eqtrd 2498 . . . . . . . 8
63 62 adantr 465 . . . . . . 7
64 oveq1 6303 . . . . . . . 8
65 64 adantl 466 . . . . . . 7
66 ax-1cn 9571 . . . . . . . . . . . . 13
67 pncan 9849 . . . . . . . . . . . . 13
68 56 , 66 , 67 sylancl 662 . . . . . . . . . . . 12
69 68 oveq2d 6312 . . . . . . . . . . 11
70 69 oveq2d 6312 . . . . . . . . . 10
71 nn0addcl 10856 . . . . . . . . . . . 12
72 33 , 71 sylan 471 . . . . . . . . . . 11
73 nn0p1nn 10860 . . . . . . . . . . . . 13
74 73 adantl 466 . . . . . . . . . . . 12
75 74 nnzd 10993 . . . . . . . . . . 11
76 bcpasc 12399 . . . . . . . . . . 11
77 72 , 75 , 76 syl2anc 661 . . . . . . . . . 10
78 70 , 77 eqtr3d 2500 . . . . . . . . 9
79 nn0p1nn 10860 . . . . . . . . . . . . . 14
80 nnnn0addcl 10851 . . . . . . . . . . . . . 14
81 79 , 80 sylan 471 . . . . . . . . . . . . 13
82 81 nnnn0d 10877 . . . . . . . . . . . 12
83 bccl 12400 . . . . . . . . . . . 12
84 82 , 75 , 83 syl2anc 661 . . . . . . . . . . 11
85 84 nn0cnd 10879 . . . . . . . . . 10
86 nn0z 10912 . . . . . . . . . . . . . 14
87 86 adantl 466 . . . . . . . . . . . . 13
88 bccl 12400 . . . . . . . . . . . . 13
89 71 , 87 , 88 syl2anc 661 . . . . . . . . . . . 12
90 33 , 89 sylan 471 . . . . . . . . . . 11
91 90 nn0cnd 10879 . . . . . . . . . 10
92 85 , 91 addcomd 9803 . . . . . . . . 9
93 peano2cn 9773 . . . . . . . . . . . . 13
94 53 , 93 syl 16 . . . . . . . . . . . 12
95 94 adantr 465 . . . . . . . . . . 11
96 95 , 56 , 57 addassd 9639 . . . . . . . . . 10
97 96 oveq1d 6311 . . . . . . . . 9
98 78 , 92 , 97 3eqtr3d 2506 . . . . . . . 8
99 98 adantr 465 . . . . . . 7
100 63 , 65 , 99 3eqtr2rd 2505 . . . . . 6
101 100 ex 434 . . . . 5
102 101 expcom 435 . . . 4
103 102 a2d 26 . . 3
104 5 , 10 , 15 , 20 , 38 , 103 nn0ind 10984 . 2
105 104 impcom 430 1
