Theorem efaddlem10 7347

Description: Lemma for efadd 7366. Properties of A (or B) in the summation terms on the right-hand side of efaddlem6 7343.

Hypotheses

Ref	Expression
efaddlem10.1	|- N e. NN
efaddlem10.2	|- A e. CC

Assertion

Ref	Expression
efaddlem10	|- ((j e. NN0 /\ j <_ N) -> (((abs` (A^j)) e. RR /\ ((|_` ((abs` A) + 1))^N) e. RR) /\ (0 <_ (abs` (A^j)) /\ (abs` (A^j)) <_ ((|_` ((abs` A) + 1))^N))))

Proof of Theorem efaddlem10

Step	Hyp	Ref	Expression
1		efaddlem10.2	. . . . . 6 |- A e. CC
2		expclt 6581	. . . . . 6 |- ((A e. CC /\ j e. NN0) -> (A^j) e. CC)
3	1, 2	mpan 695	. . . . 5 |- (j e. NN0 -> (A^j) e. CC)
4		absclt 6833	. . . . 5 |- ((A^j) e. CC -> (abs` (A^j)) e. RR)
5	3, 4	syl 10	. . . 4 |- (j e. NN0 -> (abs` (A^j)) e. RR)
6	1	abscl 6839	. . . . . . 7 |- (abs` A) e. RR
7		1re 5435	. . . . . . 7 |- 1 e. RR
8	6, 7	readdcl 5334	. . . . . 6 |- ((abs` A) + 1) e. RR
9		flreclt 6227	. . . . . 6 |- (((abs` A) + 1) e. RR -> (|_` ((abs` A) + 1)) e. RR)
10	8, 9	ax-mp 7	. . . . 5 |- (|_` ((abs` A) + 1)) e. RR
11		efaddlem10.1	. . . . . 6 |- N e. NN
12	11	nnnn0 6107	. . . . 5 |- N e. NN0
13		reexpclt 6580	. . . . 5 |- (((|_` ((abs` A) + 1)) e. RR /\ N e. NN0) -> ((|_` ((abs` A) + 1))^N) e. RR)
14	10, 12, 13	mp2an 697	. . . 4 |- ((|_` ((abs` A) + 1))^N) e. RR
15	5, 14	jctir 293	. . 3 |- (j e. NN0 -> ((abs` (A^j)) e. RR /\ ((|_` ((abs` A) + 1))^N) e. RR))
16	15	adantr 389	. 2 |- ((j e. NN0 /\ j <_ N) -> ((abs` (A^j)) e. RR /\ ((|_` ((abs` A) + 1))^N) e. RR))
17		absge0t 6854	. . . . 5 |- ((A^j) e. CC -> 0 <_ (abs` (A^j)))
18	3, 17	syl 10	. . . 4 |- (j e. NN0 -> 0 <_ (abs` (A^j)))
19	18	adantr 389	. . 3 |- ((j e. NN0 /\ j <_ N) -> 0 <_ (abs` (A^j)))
20		absexpt 6868	. . . . . 6 |- ((A e. CC /\ j e. NN0) -> (abs` (A^j)) = ((abs` A)^j))
21	1, 20	mpan 695	. . . . 5 |- (j e. NN0 -> (abs` (A^j)) = ((abs` A)^j))
22	21	adantr 389	. . . 4 |- ((j e. NN0 /\ j <_ N) -> (abs` (A^j)) = ((abs` A)^j))
23		reexpclt 6580	. . . . . . 7 |- (((abs` A) e. RR /\ j e. NN0) -> ((abs` A)^j) e. RR)
24	6, 23	mpan 695	. . . . . 6 |- (j e. NN0 -> ((abs` A)^j) e. RR)
25	24	adantr 389	. . . . 5 |- ((j e. NN0 /\ j <_ N) -> ((abs` A)^j) e. RR)
26		reexpclt 6580	. . . . . . 7 |- (((|_` ((abs` A) + 1)) e. RR /\ j e. NN0) -> ((|_` ((abs` A) + 1))^j) e. RR)
27	10, 26	mpan 695	. . . . . 6 |- (j e. NN0 -> ((|_` ((abs` A) + 1))^j) e. RR)
28	27	adantr 389	. . . . 5 |- ((j e. NN0 /\ j <_ N) -> ((|_` ((abs` A) + 1))^j) e. RR)
29	14	a1i 8	. . . . 5 |- ((j e. NN0 /\ j <_ N) -> ((|_` ((abs` A) + 1))^N) e. RR)
30		expmwordit 6606	. . . . . . 7 |- ((((abs` A) e. RR /\ (|_` ((abs` A) + 1)) e. RR /\ j e. NN0) /\ (0 <_ (abs` A) /\ (abs` A) <_ (|_` ((abs` A) + 1)))) -> ((abs` A)^j) <_ ((|_` ((abs` A) + 1))^j))
31	6	a1i 8	. . . . . . . 8 |- (j e. NN0 -> (abs` A) e. RR)
32	10	a1i 8	. . . . . . . 8 |- (j e. NN0 -> (|_` ((abs` A) + 1)) e. RR)
33		id 59	. . . . . . . 8 |- (j e. NN0 -> j e. NN0)
34	31, 32, 33	3jca 819	. . . . . . 7 |- (j e. NN0 -> ((abs` A) e. RR /\ (|_` ((abs` A) + 1)) e. RR /\ j e. NN0))
35	1	absge0 6840	. . . . . . . . 9 |- 0 <_ (abs` A)
36		flreclt 6227	. . . . . . . . . . . . 13 |- ((abs` A) e. RR -> (|_` (abs` A)) e. RR)
37	6, 36	ax-mp 7	. . . . . . . . . . . 12 |- (|_` (abs` A)) e. RR
38	37, 7	readdcl 5334	. . . . . . . . . . 11 |- ((|_` (abs` A)) + 1) e. RR
39		flltp1t 6230	. . . . . . . . . . . 12 |- ((abs` A) e. RR -> (abs` A) < ((|_` (abs` A)) + 1))
40	6, 39	ax-mp 7	. . . . . . . . . . 11 |- (abs` A) < ((|_` (abs` A)) + 1)
41	6, 38, 40	ltlei 5581	. . . . . . . . . 10 |- (abs` A) <_ ((|_` (abs` A)) + 1)
42		1z 6159	. . . . . . . . . . 11 |- 1 e. ZZ
43		fladdzt 6244	. . . . . . . . . . 11 |- (((abs` A) e. RR /\ 1 e. ZZ) -> (|_` ((abs` A) + 1)) = ((|_` (abs` A)) + 1))
44	6, 42, 43	mp2an 697	. . . . . . . . . 10 |- (|_` ((abs` A) + 1)) = ((|_` (abs` A)) + 1)
45	41, 44	breqtrr 2640	. . . . . . . . 9 |- (abs` A) <_ (|_` ((abs` A) + 1))
46	35, 45	pm3.2i 285	. . . . . . . 8 |- (0 <_ (abs` A) /\ (abs` A) <_ (|_` ((abs` A) + 1)))
47	46	a1i 8	. . . . . . 7 |- (j e. NN0 -> (0 <_ (abs` A) /\ (abs` A) <_ (|_` ((abs` A) + 1))))
48	30, 34, 47	sylanc 471	. . . . . 6 |- (j e. NN0 -> ((abs` A)^j) <_ ((|_` ((abs` A) + 1))^j))
49	48	adantr 389	. . . . 5 |- ((j e. NN0 /\ j <_ N) -> ((abs` A)^j) <_ ((|_` ((abs` A) + 1))^j))
50		expwordit 6603	. . . . . . 7 |- ((((|_` ((abs` A) + 1)) e. RR /\ j e. NN0 /\ N e. NN0) /\ (1 <_ (|_` ((abs` A) + 1)) /\ j <_ N)) -> ((|_` ((abs` A) + 1))^j) <_ ((|_` ((abs` A) + 1))^N))
51	12, 50	mp3anl3 912	. . . . . 6 |- ((((|_` ((abs` A) + 1)) e. RR /\ j e. NN0) /\ (1 <_ (|_` ((abs` A) + 1)) /\ j <_ N)) -> ((|_` ((abs` A) + 1))^j) <_ ((|_` ((abs` A) + 1))^N))
52		pm3.26 319	. . . . . . 7 |- ((j e. NN0 /\ j <_ N) -> j e. NN0)
53	52, 10	jctil 292	. . . . . 6 |- ((j e. NN0 /\ j <_ N) -> ((|_` ((abs` A) + 1)) e. RR /\ j e. NN0))
54		pm3.27 323	. . . . . . 7 |- ((j e. NN0 /\ j <_ N) -> j <_ N)
55		addge02t 5673	. . . . . . . . . 10 |- ((1 e. RR /\ (abs` A) e. RR) -> (0 <_ (abs` A) <-> 1 <_ ((abs` A) + 1)))
56	7, 6, 55	mp2an 697	. . . . . . . . 9 |- (0 <_ (abs` A) <-> 1 <_ ((abs` A) + 1))
57	35, 56	mpbi 189	. . . . . . . 8 |- 1 <_ ((abs` A) + 1)
58		flget 6233	. . . . . . . . 9 |- ((((abs` A) + 1) e. RR /\ 1 e. ZZ) -> (1 <_ ((abs` A) + 1) <-> 1 <_ (|_` ((abs` A) + 1))))
59	8, 42, 58	mp2an 697	. . . . . . . 8 |- (1 <_ ((abs` A) + 1) <-> 1 <_ (|_` ((abs` A) + 1)))
60	57, 59	mpbi 189	. . . . . . 7 |- 1 <_ (|_` ((abs` A) + 1))
61	54, 60	jctil 292	. . . . . 6 |- ((j e. NN0 /\ j <_ N) -> (1 <_ (|_` ((abs` A) + 1)) /\ j <_ N))
62	51, 53, 61	sylanc 471	. . . . 5 |- ((j e. NN0 /\ j <_ N) -> ((|_` ((abs` A) + 1))^j) <_ ((|_` ((abs` A) + 1))^N))
63	25, 28, 29, 49, 62	letrd 5526	. . . 4 |- ((j e. NN0 /\ j <_ N) -> ((abs` A)^j) <_ ((|_` ((abs` A) + 1))^N))
64	22, 63	eqbrtrd 2635	. . 3 |- ((j e. NN0 /\ j <_ N) -> (abs` (A^j)) <_ ((|_` ((abs` A) + 1))^N))
65	19, 64	jca 288	. 2 |- ((j e. NN0 /\ j <_ N) -> (0 <_ (abs` (A^j)) /\ (abs` (A^j)) <_ ((|_` ((abs` A) + 1))^N)))
66	16, 65	jca 288	1 |- ((j e. NN0 /\ j <_ N) -> (((abs` (A^j)) e. RR /\ ((|_` ((abs` A) + 1))^N) e. RR) /\ (0 <_ (abs` (