HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem efaddlem19 7298
Description: Lemma for efadd 7308. Upper bound for the summation terms on the right-hand side of efaddlem6 7285.
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 6371 . . . . 5 |- NN = (ZZ>` 1)
31, 2eleqtr 1538 . . . 4 |- N e. (ZZ>` 1)
4 fsumclt 6953 . . . . . 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 7280 . . . . . 6 |- (j e. (1...N) -> N e. (ZZ>` ((N - j) + 1)))
6 divclt 5681 . . . . . . . . 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 5245 . . . . . . . . . 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 6513 . . . . . . . . . . 11 |- ((A e. CC /\ j e. NN0) -> (A^j) e. CC)
108, 9mpan 693 . . . . . . . . . 10 |- (j e. NN0 -> (A^j) e. CC)
11 efaddlem17.3 . . . . . . . . . . 11 |- B e. CC
12 expclt 6513 . . . . . . . . . . 11 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
1311, 12mpan 693 . . . . . . . . . 10 |- (k e. NN0 -> (B^k) e. CC)
147, 10, 13syl2an 454 . . . . . . . . 9 |- ((j e. NN0 /\ k e. NN0) -> ((A^j) x. (B^k)) e. CC)
15 nnmulclt 5889 . . . . . . . . . . 11 |- (((!` j) e. NN /\ (!` k) e. NN) -> ((!` j) x. (!` k)) e. NN)
16 facclt 6877 . . . . . . . . . . 11 |- (j e. NN0 -> (!` j) e. NN)
17 facclt 6877 . . . . . . . . . . 11 |- (k e. NN0 -> (!` k) e. NN)
1815, 16, 17syl2an 454 . . . . . . . . . 10 |- ((j e. NN0 /\ k e. NN0) -> ((!` j) x. (!` k)) e. NN)
19 nncnt 5878 . . . . . . . . . 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 5897 . . . . . . . . . 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 856 . . . . . . . 8 |- ((j e. NN0 /\ k e. NN0) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
24 elfznnt 6426 . . . . . . . . . 10 |- (j e. (1...N) -> j e. NN)
2524adantr 389 . . . . . . . . 9 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> j e. NN)
26 nnnn0t 6053 . . . . . . . . 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 7281 . . . . . . . . 9 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> k e. NN)
29 nnnn0t 6053 . . . . . . . . 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 471 . . . . . . 7 |- ((j e. (1...N) /\ k e. (((N - j) + 1)...N)) -> (((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
3231r19.21aiva 1706 . . . . . 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 471 . . . . 5 |- (j e. (1...N) -> sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k))) e. CC)
3433rgen 1690 . . . 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 6981 . . . 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 695 . . 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 6768 . . . . . . 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 6955 . . . . . . 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 6768 . . . . . . . . 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 1706 . . . . . . 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 471 . . . . . 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 6981 . . . . . . 7 |- ((N e. (ZZ>` ((N - j) + 1)) /\ A.k e. (((N - j) + 1)...N)(((A^