Theorem efaddlem25 7304

Description: Lemma for efadd 7308. Convert from the explicit bound for N in efaddlem24 7303 to the existence of a bound m.

Hypotheses

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

Assertion

Ref	Expression
efaddlem25	|- ((x e. RR /\ 0 < x) -> E.m e. NN A.n e. NN (m <_ 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,m,A   B,j,k,m   m,n,R   T,j,k   x,m   j,n,k,x

Proof of Theorem efaddlem25

Step	Hyp	Ref	Expression
1		breq1 2612	. . . . 5 |- (m = ((|_` ((2 x. R) / x)) + 1) -> (m <_ n <-> ((|_` ((2 x. R) / x)) + 1) <_ n))
2	1	imbi1d 611	. . . 4 |- (m = ((|_` ((2 x. R) / x)) + 1) -> ((m <_ 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) <-> (((|_` ((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)))
3	2	ralbidv 1655	. . 3 |- (m = ((|_` ((2 x. R) / x)) + 1) -> (A.n e. NN (m <_ 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) <-> A.n e. NN (((|_` ((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)))
4	3	rcla4ev 1868	. 2 |- ((((|_` ((2 x. R) / x)) + 1) e. NN /\ A.n e. NN (((|_` ((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)) -> E.m e. NN A.n e. NN (m <_ 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))
5		flge0nn0t 6185	. . . 4 |- ((((2 x. R) / x) e. RR /\ 0 <_ ((2 x. R) / x)) -> (|_` ((2 x. R) / x)) e. NN0)
6		redivclt 5756	. . . . 5 |- (((2 x. R) e. RR /\ x e. RR /\ x =/= 0) -> ((2 x. R) / x) e. RR)
7		2re 5926	. . . . . . 7 |- 2 e. RR
8		efaddlem24.1	. . . . . . . . 9 |- A e. CC
9		efaddlem24.2	. . . . . . . . 9 |- B e. CC
10		efaddlem24.3	. . . . . . . . 9 |- T = (((|_` ((abs` A) + 1)) x. (|_` ((abs` B) + 1)))^2)
11		efaddlem24.4	. . . . . . . . 9 |- R = (2 x. ((2^(3^2)) x. ((4 x. T)^((4 x. T) + 3))))
12	8, 9, 10, 11	efaddlem21 7300	. . . . . . . 8 |- R e. NN
13	12	nnre 5879	. . . . . . 7 |- R e. RR
14	7, 13	remulcl 5307	. . . . . 6 |- (2 x. R) e. RR
15	14	a1i 8	. . . . 5 |- ((x e. RR /\ 0 < x) -> (2 x. R) e. RR)
16		pm3.26 319	. . . . 5 |- ((x e. RR /\ 0 < x) -> x e. RR)
17		gt0ne0t 5592	. . . . 5 |- ((x e. RR /\ 0 < x) -> x =/= 0)
18	6, 15, 16, 17	syl3anc 856	. . . 4 |- ((x e. RR /\ 0 < x) -> ((2 x. R) / x) e. RR)
19		0re 5412	. . . . . 6 |- 0 e. RR
20		ltlet 5493	. . . . . 6 |- ((0 e. RR /\ ((2 x. R) / x) e. RR) -> (0 < ((2 x. R) / x) -> 0 <_ ((2 x. R) / x)))
21	19, 20	mpan 693	. . . . 5 |- (((2 x. R) / x) e. RR -> (0 < ((2 x. R) / x) -> 0 <_ ((2 x. R) / x)))
22		2nn 5946	. . . . . . . 8 |- 2 e. NN
23		nnmulclt 5889	. . . . . . . 8 |- ((2 e. NN /\ R e. NN) -> (2 x. R) e. NN)
24	22, 12, 23	mp2an 695	. . . . . . 7 |- (2 x. R) e. NN
25	24	nngt0 5898	. . . . . 6 |- 0 < (2 x. R)
26		divgt0t 5809	. . . . . 6 |- ((((2 x. R) e. RR /\ 0 < (2 x. R)) /\ (x e. RR /\ 0 < x)) -> 0 < ((2 x. R) / x))
27	14, 25, 26	mpanl12 706	. . . . 5 |- ((x e. RR /\ 0 < x) -> 0 < ((2 x. R) / x))
28	21, 18, 27	sylc 68	. . . 4 |- ((x e. RR /\ 0 < x) -> 0 <_ ((2 x. R) / x))
29	5, 18, 28	sylanc 471	. . 3 |- ((x e. RR /\ 0 < x) -> (|_` ((2 x. R) / x)) e. NN0)
30		nn0p1nnt 6122	. . 3 |- ((|_` ((2 x. R) / x)) e. NN0 -> ((|_` ((2 x. R) / x)) + 1) e. NN)
31	29, 30	syl 10	. 2 |- ((x e. RR /\ 0 < x) -> ((|_` ((2 x. R) / x)) + 1) e. NN)
32	8, 9, 10, 11	efaddlem24 7303	. . . 4 |- (((x e. RR /\ 0 < x) /\ n e. NN /\ ((|_` ((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)
33	32	3expia 833	. . 3 |- (((x e. RR /\ 0 < x) /\ n e. NN) -> (((|_` ((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))
34	33	r19.21aiva 1706	. 2 |- ((x e. RR /\ 0 < x) -> A.n e. NN (((|_` ((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))
35	4, 31, 34	sylanc 471	1 |- ((x e. RR /\ 0 < x) -> E.m e. NN A.n e. NN (m <_ 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))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 953   e. wcel 955   =/= wne 1577  A.wral 1637  E.wrex 1638   class class class wbr 2609  ` cfv 3172  (class class class)co 3948  CCcc 5204  RRcr 5205  0cc0 5206  1c1 5207   + caddc 5209   x. cmul 5211   - cmin 5264   / cdiv 5266   <_ cle 5267  NNcn 5268  NN0cn0 5269   < clt 5458  2c2 5908  3c3 5909  4c4 5910  |_cfl 6171  ...cfz 6399  ^cexp 6500  abscabs 6681  !cfa 6868  sum_csu 6917

This theorem is referenced by:  efaddlem27 7306

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-pss 2045  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op