HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem efaddlem19 7356
Description: Lemma for efadd 7366. Upper bound for the summation terms on the right-hand side of efaddlem6 7343.
Hypotheses
Ref Expression
efaddlem17.1 |- N e. NN
efaddlem17.2 |- A e. CC
efaddlem17.3 |- B e. CC
efaddlem17.4 |- S = (|_` ((N + 1) / 2))
efaddlem17.5 |- T = (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)
Assertion
Ref Expression
efaddlem19 |- (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)((T^S) / (!` S))
Distinct variable group:   j,k,N
Proof of Theorem efaddlem19
StepHypRef Expression
1 efaddlem17.1 . . . . 5 |- N e. NN
2 nnuz 6440 . . . . 5 |- NN = (ZZ>` 1)
31, 2eleqtr 1549 . . . 4 |- N e. (ZZ>` 1)
4 fsumclt 7015 . . . . . 6 |- ((N e. (ZZ>` ((N - j) + 1)) /\ A.k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC) -> sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
51efaddlem1 7338 . . . . . 6 |- (j e. (1...N) -> N e. (ZZ>` ((N - j) + 1)))
6 divclt 5724 . . . . . . . . 9 |- ((((A^j) x. (B^k)) e. CC /\ ((!` j) x. (!` k)) e. CC /\ ((!` j) x. (!` k)) =/= 0) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
7 axmulcl 5285 . . . . . . . . . 10 |- (((A^j) e. CC /\ (B^k) e. CC) -> ((A^j) x. (B^k)) e. CC)
8 efaddlem17.2 . . . . . . . . . . 11 |- A e. CC
9 expclt 6582 . . . . . . . . . . 11 |- ((A e. CC /\ j e. NN0) -> (A^j) e. CC)
108, 9mpan 697 . . . . . . . . . 10 |- (j e. NN0 -> (A^j) e. CC)
11 efaddlem17.3 . . . . . . . . . . 11 |- B e. CC
12 expclt 6582 . . . . . . . . . . 11 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
1311, 12mpan 697 . . . . . . . . . 10 |- (k e. NN0 -> (B^k) e. CC)
147, 10, 13syl2an 456 . . . . . . . . 9 |- ((j e. NN0 /\ k e. NN0) -> ((A^j) x. (B^k)) e. CC)
15 nnmulclt 5943 . . . . . . . . . . 11 |- (((!` j) e. NN /\ (!` k) e. NN) -> ((!` j) x. (!` k)) e. NN)
16 facclt 6940 . . . . . . . . . . 11 |- (j e. NN0 -> (!` j) e. NN)
17 facclt 6940 . . . . . . . . . . 11 |- (k e. NN0 -> (!` k) e. NN)
1815, 16, 17syl2an 456 . . . . . . . . . 10 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) x. (!` k)) e. NN)
19 nncnt 5932 . . . . . . . . . 10 |- (((!` j) x. (!` k)) e. NN -> ((!` j) x. (!` k)) e. CC)
2018, 19syl 10 . . . . . . . . 9 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) x. (!` k)) e. CC)
21 nnne0t 5951 . . . . . . . . . 10 |- (((!` j) x. (!` k)) e. NN -> ((!` j) x. (!` k)) =/= 0)
2218, 21syl 10 . . . . . . . . 9 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) x. (!` k)) =/= 0)
236, 14, 20, 22syl3anc 860 . . . . . . . 8 |- ((j e. NN0 /\ k e. NN0) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
24 elfznnt 6495 . . . . . . . . . 10 |- (j e. (1...N) -> j e. NN)
2524adantr 391 . . . . . . . . 9 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> j e. NN)
26 nnnn0t 6108 . . . . . . . . 9 |- (j e. NN -> j e. NN0)
2725, 26syl 10 . . . . . . . 8 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> j e. NN0)
281efaddlem2 7339 . . . . . . . . 9 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> k e. NN)
29 nnnn0t 6108 . . . . . . . . 9 |- (k e. NN -> k e. NN0)
3028, 29syl 10 . . . . . . . 8 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> k e. NN0)
3123, 27, 30sylanc 473 . . . . . . 7 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
3231r19.21aiva 1717 . . . . . 6 |- (j e. (1...N) -> A.k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
334, 5, 32sylanc 473 . . . . 5 |- (j e. (1...N) -> sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
3433rgen 1701 . . . 4 |- A.j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC
35 fsumabs 7043 . . . 4 |- ((N e. (ZZ>` 1) /\ A.j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC) -> (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ sum_j e. (1...N)(abs` sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))))
363, 34, 35mp2an 699 . . 3 |- (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) <_ sum_j e. (1...N)(abs` sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))))
37 absclt 6833 . . . . . . 7 |- (sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC -> (abs` sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR)
3833, 37syl 10 . . . . . 6 |- (j e. (1...N) -> (abs` sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR)
39 fsumreclt 7017 . . . . . . 7 |- ((N e. (ZZ>` ((N - j) + 1)) /\ A.k e. (((N - j) + 1)...N)(abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR) -> sum_k e. (((N - j) + 1)...N)(abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR)
40 absclt 6833 . . . . . . . . 9 |- ((((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC -> (abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR)
4131, 40syl 10 . . . . . . . 8 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR)
4241r19.21aiva 1717 . . . . . . 7 |- (j e. (1...N) -> A.k e. (((N - j) + 1)...N)(abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR)
4339, 5, 42sylanc 473 . . . . . 6 |- (j e. (1...N) -> sum_k e. (((N - j) + 1)...N)(abs` (((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR)
44 fsumabs 7043 . . . . . . 7 |- ((N e. (ZZ>` ((N - j) + 1)) /\ A.k e. (((N - j) + 1)...N)(((A^