Theorem efcltlem1 7263

Description: Lemma for efclt 7271. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 7207 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 6789	. . . 4 |- (abs` A) e. RR
3		flreclt 6185	. . . . . 6 |- ((abs` A) e. RR -> (|_` (abs` A)) e. RR)
4	2, 3	ax-mp 7	. . . . 5 |- (|_` (abs` A)) e. RR
5		peano2re 5419	. . . . 5 |- ((|_` (abs` A)) e. RR -> ((|_` (abs` A)) + 1) e. RR)
6	4, 5	ax-mp 7	. . . 4 |- ((|_` (abs` A)) + 1) e. RR
7	1	absge0 6790	. . . . . . 7 |- 0 <_ (abs` A)
8		0z 6103	. . . . . . . 8 |- 0 e. ZZ
9		flget 6190	. . . . . . . 8 |- (((abs` A) e. RR /\ 0 e. ZZ) -> (0 <_ (abs` A) <-> 0 <_ (|_` (abs` A))))
10	2, 8, 9	mp2an 696	. . . . . . 7 |- (0 <_ (abs` A) <-> 0 <_ (|_` (abs` A)))
11	7, 10	mpbi 189	. . . . . 6 |- 0 <_ (|_` (abs` A))
12		lt01 5663	. . . . . 6 |- 0 < 1
13		1re 5418	. . . . . . 7 |- 1 e. RR
14	4, 13	addgegt0 5584	. . . . . 6 |- ((0 <_ (|_` (abs` A)) /\ 0 < 1) -> 0 < ((|_` (abs` A)) + 1))
15	11, 12, 14	mp2an 696	. . . . 5 |- 0 < ((|_` (abs` A)) + 1)
16	6, 15	gt0ne0i 5601	. . . 4 |- ((|_` (abs` A)) + 1) =/= 0
17	2, 6, 16	redivcl 5764	. . 3 |- ((abs` A) / ((|_` (abs` A)) + 1)) e. RR
18	2	recn 5297	. . . . . 6 |- (abs` A) e. CC
19	18	div1 5738	. . . . 5 |- ((abs` A) / 1) = (abs` A)
20		flltp1t 6188	. . . . . 6 |- ((abs` A) e. RR -> (abs` A) < ((|_` (abs` A)) + 1))
21	2, 20	ax-mp 7	. . . . 5 |- (abs` A) < ((|_` (abs` A)) + 1)
22	19, 21	eqbrtr 2630	. . . 4 |- ((abs` A) / 1) < ((|_` (abs` A)) + 1)
23	2, 13, 6, 12, 15	ltdiv23i 5853	. . . 4 |- (((abs` A) / 1) < ((|_` (abs` A)) + 1) <-> ((abs` A) / ((|_` (abs` A)) + 1)) < 1)
24	22, 23	mpbi 189	. . 3 |- ((abs` A) / ((|_` (abs` A)) + 1)) < 1
25	17, 24	pm3.2i 285	. 2 |- (((abs` A) / ((|_` (abs` A)) + 1)) e. RR /\ ((abs` A) / ((|_` (abs` A)) + 1)) < 1)
26		flge0nn0t 6197	. . . . 5 |- (((abs` A) e. RR /\ 0 <_ (abs` A)) -> (|_` (abs` A)) e. NN0)
27	2, 7, 26	mp2an 696	. . . 4 |- (|_` (abs` A)) e. NN0
28		nn0p1nnt 6132	. . . 4 |- ((|_` (abs` A)) e. NN0 -> ((|_` (abs` A)) + 1) e. NN)
29	27, 28	ax-mp 7	. . 3 |- ((|_` (abs` A)) + 1) e. NN
30		nnleltp1t 5911	. . . . . . 7 |- ((((|_` (abs` A)) + 1) e. NN /\ w e. NN) -> (((|_` (abs` A)) + 1) <_ w <-> ((|_` (abs` A)) + 1) < (w + 1)))
31	29, 30	mpan 694	. . . . . 6 |- (w e. NN -> (((|_` (abs` A)) + 1) <_ w <-> ((|_` (abs` A)) + 1) < (w + 1)))
32		efcltlem1.3	. . . . . . . . . . . 12 |- A =/= 0
33	1	absgt0 6793	. . . . . . . . . . . 12 |- (A =/= 0 <-> 0 < (abs` A))
34	32, 33	mpbi 189	. . . . . . . . . . 11 |- 0 < (abs` A)
35	2, 34	pm3.2i 285	. . . . . . . . . 10 |- ((abs` A) e. RR /\ 0 < (abs` A))
36		an6 901	. . . . . . . . . . 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))))
37		ltdiv2t 5845	. . . . . . . . . . 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))))
38	36, 37	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))))
39	35, 38	mp3an3 904	. . . . . . . . 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))))
40	6, 15, 39	mpanl12 707	. . . . . . . 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))))
41		peano2nn 5893	. . . . . . . . 9 |- (w e. NN -> (w + 1) e. NN)
42		nncnt 5888	. . . . . . . . 9 |- ((w + 1) e. NN -> (w + 1) e. CC)
43		absclt 6783	. . . . . . . . 9 |- ((w + 1) e. CC -> (abs` (w + 1)) e. RR)
44	41, 42, 43	3syl 20	. . . . . . . 8 |- (w e. NN -> (abs` (w + 1)) e. RR)
45		nngt0t 5904	. . . . . . . . . 10 |- ((w + 1) e. NN -> 0 < (w + 1))
46		absidt 6812	. . . . . . . . . . 11 |- (((w + 1) e. RR /\ 0 <_ (w + 1)) -> (abs` (w + 1)) = (w + 1))
47		nnret 5887	. . . . . . . . . . 11 |- ((w + 1) e. NN -> (w + 1) e. RR)
48		nnnn0t 6063	. . . . . . . . . . . 12 |- ((w + 1) e. NN -> (w + 1) e. NN0)
49		nn0ge0t 6074	. . . . . . . . . . . 12 |- ((w + 1) e. NN0 -> 0 <_ (w + 1))
50	48, 49	syl 10	. . . . . . . . . . 11 |- ((w + 1) e. NN -> 0 <_ (w + 1))
51	46, 47, 50	sylanc 471	. . . . . . . . . 10 |- ((w + 1) e. NN -> (abs` (w + 1)) = (w + 1))
52	45, 51	breqtrrd 2637	. . . . . . . . 9 |- ((w + 1) e. NN -> 0 < (abs` (w + 1)))
53	41, 52	syl 10	. . . . . . . 8 |- (w e. NN -> 0 < (abs` (w + 1)))
54	40, 44, 53	sylanc 471	. . . . . . 7 |- (w e. NN -> (((|_` (abs` A)) + 1) < (abs` (w + 1)) <-> ((abs` A) / (abs` (w + 1))) < ((abs` A) / ((|_` (abs` A)) + 1))))
55	41, 47	syl 10	. . . . . . . . 9 |- (w e. NN -> (w + 1) e. RR)
56		nnnn0t 6063	. . . . . . . . . 10 |- (w e. NN -> w e. NN0)
57		peano2nn0 6081	. . . . . . . . . 10 |- (w e. NN0 -> (w + 1) e. NN0)
58	56, 57, 49	3syl 20	. . . . . . . . 9 |- (w e. NN -> 0 <_ (w + 1))
59	46, 55, 58	sylanc 471	. . . . . . . 8 |- (w e. NN -> (abs` (w + 1)) = (w + 1))
60	59	breq2d 2626	. . . . . . 7 |- (w e. NN -> (((|_` (abs` A)) + 1) < (abs` (w + 1)) <-> ((|_` (abs` A)) + 1) < (w + 1)))
61		flclt 6184	. . . . . . . . . . . . . . . 16 |- ((abs` A) e. RR -> (|_` (abs` A)) e. ZZ)
62	2, 61	ax-mp 7	. . . . . . . . . . . . . . 15 |- (|_` (abs` A)) e. ZZ
63	62	zre 6098	. . . . . . . . . . . . . 14 |- (|_` (abs` A)) e. RR
64	63, 13	addgegt0 5584	. . . . . . . . . . . . 13 |- ((0