Theorem efaddlem25 7312

Description: Lemma for efadd 7316. Convert from the explicit bound for N in efaddlem24 7311 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 2617	. . . . 5 |- (m = ((|_` ((2 x. R) / x)) + 1) -> (m <_ n <-> ((|_` ((2 x. R) / x)) + 1) <_ n))
2	1	imbi1d 612	. . . 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 1660	. . 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 1873	. 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 6193	. . . 4 |- ((((2 x. R) / x) e. RR /\ 0 <_ ((2 x. R) / x)) -> (|_` ((2 x. R) / x)) e. NN0)
6		redivclt 5764	. . . . 5 |- (((2 x. R) e. RR /\ x e. RR /\ x =/= 0) -> ((2 x. R) / x) e. RR)
7		2re 5934	. . . . . . 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 7308	. . . . . . . 8 |- R e. NN
13	12	nnre 5887	. . . . . . 7 |- R e. RR
14	7, 13	remulcl 5315	. . . . . 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 5600	. . . . 5 |- ((x e. RR /\ 0 < x) -> x =/= 0)
18	6, 15, 16, 17	syl3anc 857	. . . 4 |- ((x e. RR /\ 0 < x) -> ((2 x. R) / x) e. RR)
19		0re 5420	. . . . . 6 |- 0 e. RR
20		ltlet 5501	. . . . . 6 |- ((0 e. RR /\ ((2 x. R) / x) e. RR) -> (0 < ((2 x. R) / x) -> 0 <_ ((2 x. R) / x)))
21	19, 20	mpan 694	. . . . 5 |- (((2 x. R) / x) e. RR -> (0 < ((2 x. R) / x) -> 0 <_ ((2 x. R) / x)))
22		2nn 5954	. . . . . . . 8 |- 2 e. NN
23		nnmulclt 5897	. . . . . . . 8 |- ((2 e. NN /\ R e. NN) -> (2 x. R) e. NN)
24	22, 12, 23	mp2an 696	. . . . . . 7 |- (2 x. R) e. NN
25	24	nngt0 5906	. . . . . 6 |- 0 < (2 x. R)
26		divgt0t 5817	. . . . . 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 707	. . . . 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 6130	. . 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 7311	. . . 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 834	. . 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 1711	. 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 954   e. wcel 956   =/= wne 1582  A.wral 1642  E.wrex 1643   class class class wbr 2614  ` cfv 3177  (class class class)co 3954  CCcc 5212  RRcr 5213  0cc0 5214  1c1 5215   + caddc 5217   x. cmul 5219   - cmin 5272   / cdiv 5274   <_ cle 5275  NNcn 5276  NN0cn0 5277   < clt 5466  2c2 5916  3c3 5917  4c4 5918  |_cfl 6179  ...cfz 6407  ^cexp 6508  abscabs 6689  !cfa 6876  sum_csu 6925

This theorem is referenced by:  efaddlem27 7314

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-nel 1585  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op