Theorem efaddlem23 7310

Description: Lemma for efadd 7316. Given any positive x, no matter how small, there is an N such that the difference between the truncated series for (exp` A) x. (exp` B) and exp` (A + B) is less than x. Here we show an explicit lower bound for N.

Hypotheses

Ref	Expression
efaddlem23.1	|- N e. NN
efaddlem23.2	|- A e. CC
efaddlem23.3	|- B e. CC
efaddlem23.4	|- T = (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)
efaddlem23.5	|- R = (2 x. ((2^(3^2)) x. ((4 x. T)^((4 x. T) + 3))))

Assertion

Ref	Expression
efaddlem23	|- (((x e. RR /\ 0 < x) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> (abs` ((sum_j e. (0...N)((A^j) / (!` j)) x. sum_k e. (0...N)((B^k) / (!` k))) - sum_j e. (0...N)(((A + B)^j) / (!` j)))) < x)

Distinct variable groups:   j,k,A   B,j,k   j,N,k   T,j,k

Proof of Theorem efaddlem23

Step	Hyp	Ref	Expression
1		efaddlem23.1	. . . . 5 |- N e. NN
2		efaddlem23.2	. . . . 5 |- A e. CC
3		efaddlem23.3	. . . . 5 |- B e. CC
4	1, 2, 3	efaddlem4 7291	. . . 4 |- (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR
5	4	a1i 8	. . 3 |- (((x e. RR /\ 0 < x) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) e. RR)
6		2re 5934	. . . . . 6 |- 2 e. RR
7		efaddlem23.4	. . . . . . . 8 |- T = (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)
8		efaddlem23.5	. . . . . . . 8 |- R = (2 x. ((2^(3^2)) x. ((4 x. T)^((4 x. T) + 3))))
9	2, 3, 7, 8	efaddlem21 7308	. . . . . . 7 |- R e. NN
10	9	nnre 5887	. . . . . 6 |- R e. RR
11	6, 10	remulcl 5315	. . . . 5 |- (2 x. R) e. RR
12	1	nnre 5887	. . . . 5 |- N e. RR
13	1	nnne0 5907	. . . . 5 |- N =/= 0
14	11, 12, 13	redivcl 5762	. . . 4 |- ((2 x. R) / N) e. RR
15	14	a1i 8	. . 3 |- (((x e. RR /\ 0 < x) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> ((2 x. R) / N) e. RR)
16		simpll 412	. . 3 |- (((x e. RR /\ 0 < x) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> x e. RR)
17		eqid 1473	. . . . 5 |- (|_` ((N + 1) / 2)) = (|_` ((N + 1) / 2))
18	1, 2, 3, 17, 7, 8	efaddlem22 7309	. . . 4 |- (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) < ((2 x. R) / N)
19	18	a1i 8	. . 3 |- (((x e. RR /\ 0 < x) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) < ((2 x. R) / N))
20		redivclt 5764	. . . . . . . 8 |- (((2 x. R) e. RR /\ x e. RR /\ x =/= 0) -> ((2 x. R) / x) e. RR)
21	11	a1i 8	. . . . . . . 8 |- ((x e. RR /\ 0 < x) -> (2 x. R) e. RR)
22		pm3.26 319	. . . . . . . 8 |- ((x e. RR /\ 0 < x) -> x e. RR)
23		gt0ne0t 5600	. . . . . . . 8 |- ((x e. RR /\ 0 < x) -> x =/= 0)
24	20, 21, 22, 23	syl3anc 857	. . . . . . 7 |- ((x e. RR /\ 0 < x) -> ((2 x. R) / x) e. RR)
25		flltp1t 6185	. . . . . . 7 |- (((2 x. R) / x) e. RR -> ((2 x. R) / x) < ((|_` ((2 x. R) / x)) + 1))
26	24, 25	syl 10	. . . . . 6 |- ((x e. RR /\ 0 < x) -> ((2 x. R) / x) < ((|_` ((2 x. R) / x)) + 1))
27		ltletrt 5505	. . . . . . 7 |- ((((2 x. R) / x) e. RR /\ ((|_` ((2 x. R) / x)) + 1) e. RR /\ N e. RR) -> ((((2 x. R) / x) < ((|_` ((2 x. R) / x)) + 1) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> ((2 x. R) / x) < N))
28		flclt 6182	. . . . . . . . . 10 |- (((2 x. R) / x) e. RR -> (|_` ((2 x. R) / x)) e. ZZ)
29	24, 28	syl 10	. . . . . . . . 9 |- ((x e. RR /\ 0 < x) -> (|_` ((2 x. R) / x)) e. ZZ)
30		zret 6094	. . . . . . . . 9 |- ((|_` ((2 x. R) / x)) e. ZZ -> (|_` ((2 x. R) / x)) e. RR)
31	29, 30	syl 10	. . . . . . . 8 |- ((x e. RR /\ 0 < x) -> (|_` ((2 x. R) / x)) e. RR)
32		peano2re 5416	. . . . . . . 8 |- ((|_` ((2 x. R) / x)) e. RR -> ((|_` ((2 x. R) / x)) + 1) e. RR)
33	31, 32	syl 10	. . . . . . 7 |- ((x e. RR /\ 0 < x) -> ((|_` ((2 x. R) / x)) + 1) e. RR)
34	12	a1i 8	. . . . . . 7 |- ((x e. RR /\ 0 < x) -> N e. RR)
35	27, 24, 33, 34	syl3anc 857	. . . . . 6 |- ((x e. RR /\ 0 < x) -> ((((2 x. R) / x) < ((|_` ((2 x. R) / x)) + 1) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> ((2 x. R) / x) < N))
36	26, 35	mpand 700	. . . . 5 |- ((x e. RR /\ 0 < x) -> (((|_` ((2 x. R) / x)) + 1) <_ N -> ((2 x. R) / x) < N))
37	36	imp 350	. . . 4 |- (((x e. RR /\ 0 < x) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> ((2 x. R) / x) < N)
38		ltdiv23t 5848	. . . . . 6 |- ((((2 x. R) e. RR /\ x e. RR /\ N e. RR) /\ (0 < x /\ 0 < N)) -> (((2 x. R) / x) < N <-> ((2 x. R) / N) < x))
39	21, 22, 34	3jca 818	. . . . . 6 |- ((x e. RR /\ 0 < x) -> ((2 x. R) e. RR /\ x e. RR /\ N e. RR))
40		pm3.27 323	. . . . . . 7 |- ((x e. RR /\ 0 < x) -> 0 < x)
41	1	nngt0 5906	. . . . . . 7 |- 0 < N
42	40, 41	jctir 293	. . . . . 6 |- ((x e. RR /\ 0 < x) -> (0 < x /\ 0 < N))
43	38, 39, 42	sylanc 471	. . . . 5 |- ((x e. RR /\ 0 < x) -> (((2 x. R) / x) < N <-> ((2 x. R) / N) < x))
44	43	adantr 389	. . . 4 |- (((x e. RR /\ 0 < x) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> (((2 x. R) / x) < N <-> ((2 x. R) / N) < x))
45	37, 44	mpbid 195	. . 3 |- (((x e. RR /\ 0 < x) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> ((2 x. R) / N) < x)
46	5, 15, 16, 19, 45	lttrd 5510	. 2 |- (((x e. RR /\ 0 < x) /\ ((|_` ((2 x. R) / x)) + 1) <_ N) -> (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))) < x)
47	1, 2, 3	efaddlem6 7293	. . 3 |- ((sum_j e. (0...N)((A^j) / (!` j)) x. sum_k e. (0...N)((B^k) / (!` k))) - sum_j e. (0...N)(((A + B)^j) / (!` j))) = sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k)) / ((!` j) x. (!` k)))
48	47	fveq2i 3718	. 2 |- (abs` ((sum_j e. (0...N)((A^j) / (!` j)) x. sum_k e. (0...N)((B^k) / (!` k))) - sum_j e. (0...N)(((A + B)^j) / (!` j)))) = (abs` sum_j e. (1...N)sum_k e. (((N - j) + 1)...N)(((A^j) x. (B^k