Theorem efcltlem1 7246

Description: Lemma for efclt 7254. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 7190 is used to show convergence.

Hypotheses

Ref	Expression
efcltlem.1	|- F = {<.y, z>. | (y e. NN /\ z = ((A^y) / (!` y)))}
efcltlem1.2	|- A e. CC
efcltlem1.3	|- A =/= 0

Assertion

Ref	Expression
efcltlem1	|- E.x( + seq1 F) ~~> x

Distinct variable groups:   x,y,z,A   x,F

Proof of Theorem efcltlem1

Step	Hyp	Ref	Expression
1		efcltlem1.2	. . . . 5 |- A e. CC
2	1	abscl 6774	. . . 4 |- (abs` A) e. RR
3		flclt 6174	. . . . . . 7 |- ((abs` A) e. RR -> (|_` (abs` A)) e. ZZ)
4	2, 3	ax-mp 7	. . . . . 6 |- (|_` (abs` A)) e. ZZ
5		peano2z 6113	. . . . . 6 |- ((|_` (abs` A)) e. ZZ -> ((|_` (abs` A)) + 1) e. ZZ)
6	4, 5	ax-mp 7	. . . . 5 |- ((|_` (abs` A)) + 1) e. ZZ
7	6	zre 6088	. . . 4 |- ((|_` (abs` A)) + 1) e. RR
8	1	absge0 6775	. . . . . . 7 |- 0 <_ (abs` A)
9		0z 6093	. . . . . . . 8 |- 0 e. ZZ
10		flget 6178	. . . . . . . 8 |- (((abs` A) e. RR /\ 0 e. ZZ) -> (0 <_ (abs` A) <-> 0 <_ (|_` (abs` A))))
11	2, 9, 10	mp2an 695	. . . . . . 7 |- (0 <_ (abs` A) <-> 0 <_ (|_` (abs` A)))
12	8, 11	mpbi 189	. . . . . 6 |- 0 <_ (|_` (abs` A))
13		lt01 5653	. . . . . 6 |- 0 < 1
14	4	zre 6088	. . . . . . 7 |- (|_` (abs` A)) e. RR
15		1re 5407	. . . . . . 7 |- 1 e. RR
16	14, 15	addgegt0 5574	. . . . . 6 |- ((0 <_ (|_` (abs` A)) /\ 0 < 1) -> 0 < ((|_` (abs` A)) + 1))
17	12, 13, 16	mp2an 695	. . . . 5 |- 0 < ((|_` (abs` A)) + 1)
18	7, 17	gt0ne0i 5591	. . . 4 |- ((|_` (abs` A)) + 1) =/= 0
19	2, 7, 18	redivcl 5754	. . 3 |- ((abs` A) / ((|_` (abs` A)) + 1)) e. RR
20	2	recn 5286	. . . . . 6 |- (abs` A) e. CC
21	20	div1 5728	. . . . 5 |- ((abs` A) / 1) = (abs` A)
22		flltp1t 6177	. . . . . 6 |- ((abs` A) e. RR -> (abs` A) < ((|_` (abs` A)) + 1))
23	2, 22	ax-mp 7	. . . . 5 |- (abs` A) < ((|_` (abs` A)) + 1)
24	21, 23	eqbrtr 2624	. . . 4 |- ((abs` A) / 1) < ((|_` (abs` A)) + 1)
25	2, 15, 7, 13, 17	ltdiv23i 5843	. . . 4 |- (((abs` A) / 1) < ((|_` (abs` A)) + 1) <-> ((abs` A) / ((|_` (abs` A)) + 1)) < 1)
26	24, 25	mpbi 189	. . 3 |- ((abs` A) / ((|_` (abs` A)) + 1)) < 1
27	19, 26	pm3.2i 285	. 2 |- (((abs` A) / ((|_` (abs` A)) + 1)) e. RR /\ ((abs` A) / ((|_` (abs` A)) + 1)) < 1)
28		flge0nn0t 6185	. . . . 5 |- (((abs` A) e. RR /\ 0 <_ (abs` A)) -> (|_` (abs` A)) e. NN0)
29	2, 8, 28	mp2an 695	. . . 4 |- (|_` (abs` A)) e. NN0
30		nn0p1nnt 6122	. . . 4 |- ((|_` (abs` A)) e. NN0 -> ((|_` (abs` A)) + 1) e. NN)
31	29, 30	ax-mp 7	. . 3 |- ((|_` (abs` A)) + 1) e. NN
32		nnleltp1t 5901	. . . . . . 7 |- ((((|_` (abs` A)) + 1) e. NN /\ w e. NN) -> (((|_` (abs` A)) + 1) <_ w <-> ((|_` (abs` A)) + 1) < (w + 1)))
33	31, 32	mpan 693	. . . . . 6 |- (w e. NN -> (((|_` (abs` A)) + 1) <_ w <-> ((|_` (abs` A)) + 1) < (w + 1)))
34		efcltlem1.3	. . . . . . . . . . . 12 |- A =/= 0
35	1	absgt0 6778	. . . . . . . . . . . 12 |- (A =/= 0 <-> 0 < (abs` A))
36	34, 35	mpbi 189	. . . . . . . . . . 11 |- 0 < (abs` A)
37	2, 36	pm3.2i 285	. . . . . . . . . 10 |- ((abs` A) e. RR /\ 0 < (abs` A))
38		an6 899	. . . . . . . . . . 11 |- (((((|_` (abs` A)) + 1) e. RR /\ (abs` (w + 1)) e. RR /\ (abs` A) e. RR) /\ (0 < ((|_` (abs` A)) + 1) /\ 0 < (abs` (w + 1)) /\ 0 < (abs` A))) <-> ((((|_` (abs` A)) + 1) e. RR /\ 0 < ((|_` (abs` A)) + 1)) /\ ((abs` (w + 1)) e. RR /\ 0 < (abs` (w + 1))) /\ ((abs` A) e. RR /\ 0 < (abs` A))))
39		ltdiv2t 5835	. . . . . . . . . . 11 |- (((((|_` (abs` A)) + 1) e. RR /\ (abs` (w + 1)) e. RR /\ (abs` A) e. RR) /\ (0 < ((|_` (abs` A)) + 1) /\ 0 < (abs` (w + 1)) /\ 0 < (abs` A))) -> (((|_` (abs` A)) + 1) < (abs` (w + 1)) <-> ((abs` A) / (abs` (w + 1))) < ((abs` A) / ((|_` (abs` A)) + 1))))
40	38, 39	sylbir 201	. . . . . . . . . 10 |- (((((|_` (abs` A)) + 1) e. RR /\ 0 < ((|_` (abs` A)) + 1)) /\ ((abs` (w + 1)) e. RR /\ 0 < (abs` (w + 1))) /\ ((abs` A) e. RR /\ 0 < (abs` A))) -> (((|_` (abs` A)) + 1) < (abs` (w + 1)) <-> ((abs` A) / (abs` (w + 1))) < ((abs` A) / ((|_` (abs` A)) + 1))))
41	37, 40	mp3an3 902	. . . . . . . . 9 |- (((((|_` (abs` A)) + 1) e. RR /\ 0 < ((|_` (abs` A)) + 1)) /\ ((abs` (w + 1)) e. RR /\ 0 < (abs` (w + 1)))) -> (((|_` (abs` A)) + 1) < (abs` (w + 1)) <-> ((abs` A) / (abs` (w + 1))) < ((abs` A) / ((|_` (abs` A)) + 1))))
42	7, 17, 41	mpanl12 706	. . . . . . . 8 |- (((abs` (w + 1)) e. RR /\ 0 < (abs` (w + 1))) -> (((|_` (abs` A)) + 1) < (abs` (w + 1)) <-> ((abs` A) / (abs` (w + 1))) < ((abs` A) / ((|_` (abs` A)) + 1))))
43		peano2nn 5883	. . . . . . . . 9 |- (w e. NN -> (w + 1) e. NN)
44		nncnt 5878	. . . . . . . . 9 |- ((w + 1) e. NN -> (w + 1) e. CC)
45		absclt 6768	. . . . . . . . 9 |- ((w + 1) e. CC -> (abs` (w + 1)) e. RR)
46	43, 44, 45	3syl 20	. . . . . . . 8 |- (w e. NN -> (abs` (w + 1)) e. RR)
47		nngt0t 5894	. . . . . . . . . 10 |- ((w + 1) e. NN -> 0 < (w + 1))
48		absidt 6797	. . . . . . . . . . 11 |- (((w + 1) e. RR /\ 0 <_ (w + 1)) -> (abs` (w + 1)) = (w + 1))
49		nnret 5877	. . . . . . . . . . 11 |- ((w + 1) e. NN -> (w + 1) e. RR)
50		nnnn0t 6053	. . . . . . . . . . . 12 |- ((w + 1) e. NN -> (w + 1) e. NN0)
51		nn0ge0t 6064	. . . . . . . . . . . 12 |- ((w + 1) e. NN0 -> 0 <_ (w + 1))
52	50, 51	syl 10	. . . . . . . . . . 11 |- ((w + 1) e. NN -> 0 <_ (w + 1))
53	48, 49, 52	sylanc 471	. . . . . . . . . 10 |- ((w + 1) e. NN -> (abs` (w + 1)) = (w + 1))
54	47, 53	breqtrrd 2631	. . . . . . . . 9 |- ((w + 1) e. NN -> 0 < (abs` (w + 1)))
55	43, 54	syl 10	. . . . . . . 8 |- (w e. NN -> 0 < (abs` (w + 1)))
56	42, 46, 55	sylanc 471	. . . . . . 7 |- (w e. NN -> (((|_` (abs` A)) + 1) < (abs` (w + 1)) <-> ((abs` A) / (abs` (w + 1))) < ((abs` A) / ((|_` (abs` A)) + 1))))
57	43, 49	syl 10	. . . . . . . . 9 |- (w e. NN -> (w + 1) e. RR)
58		nnnn0t 6053	. . . . . . . . . 10 |- (w e. NN -> w e. NN0)
59		peano2nn0 6071	. . . . . . . . . 10 |- (w e. NN0 -> (w + 1) e. NN0)
60	58, 59, 51	3syl 20	. . . . . . . . 9 |- (w e. NN -> 0 <_ (w + 1))
61	48, 57, 60	sylanc 471	. . . . . . . 8 |- (w e. NN -> (abs` (w + 1)) = (w + 1))
62	61	breq2d 2620	. . . . . . 7 |- (w e. NN -> (((|_` (abs` A)) + 1) < (abs` (w + 1)) <-> ((|_` (abs` A)) + 1) < (w + 1)))
63		ltmul1t 5786	. . . . . . . . . 10 |- (((((abs` A) / (abs` (w + 1))) e. RR /\ ((abs` A