Theorem reccnv 7161

Description: The sequence of reciprocals of natural numbers converges to zero.

Hypothesis

Ref	Expression
reccnv.1	|- F e. V

Assertion

Ref	Expression
reccnv	|- (A.k e. NN (F` k) = (1 / k) -> F ~~> 0)

Distinct variable group:   k,F

Proof of Theorem reccnv

Step	Hyp	Ref	Expression
1		nnreclt 6027	. . . . . 6 |- ((x e. RR /\ 0 < x) -> E.j e. NN (1 / j) < x)
2	1	adantl 388	. . . . 5 |- ((A.k e. NN (F` k) = (1 / k) /\ (x e. RR /\ 0 < x)) -> E.j e. NN (1 / j) < x)
3		absidt 6805	. . . . . . . . . . . . . . . . . . . . 21 |- (((1 / k) e. RR /\ 0 <_ (1 / k)) -> (abs` (1 / k)) = (1 / k))
4		nnrecret 6223	. . . . . . . . . . . . . . . . . . . . 21 |- (k e. NN -> (1 / k) e. RR)
5		0re 5420	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. RR
6		ltlet 5501	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((0 e. RR /\ (1 / k) e. RR) -> (0 < (1 / k) -> 0 <_ (1 / k)))
7	5, 6	mpan 694	. . . . . . . . . . . . . . . . . . . . . 22 |- ((1 / k) e. RR -> (0 < (1 / k) -> 0 <_ (1 / k)))
8		nnrecgt0t 5908	. . . . . . . . . . . . . . . . . . . . . 22 |- (k e. NN -> 0 < (1 / k))
9	7, 4, 8	sylc 68	. . . . . . . . . . . . . . . . . . . . 21 |- (k e. NN -> 0 <_ (1 / k))
10	3, 4, 9	sylanc 471	. . . . . . . . . . . . . . . . . . . 20 |- (k e. NN -> (abs` (1 / k)) = (1 / k))
11	10	ad2antlr 405	. . . . . . . . . . . . . . . . . . 19 |- (((j e. NN /\ k e. NN) /\ j <_ k) -> (abs` (1 / k)) = (1 / k))
12		lerect 5841	. . . . . . . . . . . . . . . . . . . . 21 |- (((j e. RR /\ 0 < j) /\ (k e. RR /\ 0 < k)) -> (j <_ k <-> (1 / k) <_ (1 / j)))
13		nnret 5885	. . . . . . . . . . . . . . . . . . . . . 22 |- (j e. NN -> j e. RR)
14		nngt0t 5902	. . . . . . . . . . . . . . . . . . . . . 22 |- (j e. NN -> 0 < j)
15	13, 14	jca 288	. . . . . . . . . . . . . . . . . . . . 21 |- (j e. NN -> (j e. RR /\ 0 < j))
16		nnret 5885	. . . . . . . . . . . . . . . . . . . . . 22 |- (k e. NN -> k e. RR)
17		nngt0t 5902	. . . . . . . . . . . . . . . . . . . . . 22 |- (k e. NN -> 0 < k)
18	16, 17	jca 288	. . . . . . . . . . . . . . . . . . . . 21 |- (k e. NN -> (k e. RR /\ 0 < k))
19	12, 15, 18	syl2an 454	. . . . . . . . . . . . . . . . . . . 20 |- ((j e. NN /\ k e. NN) -> (j <_ k <-> (1 / k) <_ (1 / j)))
20	19	biimpa 416	. . . . . . . . . . . . . . . . . . 19 |- (((j e. NN /\ k e. NN) /\ j <_ k) -> (1 / k) <_ (1 / j))
21	11, 20	eqbrtrd 2630	. . . . . . . . . . . . . . . . . 18 |- (((j e. NN /\ k e. NN) /\ j <_ k) -> (abs` (1 / k)) <_ (1 / j))
22	21	adantlll 396	. . . . . . . . . . . . . . . . 17 |- (((((x e. RR /\ 0 < x) /\ j e. NN) /\ k e. NN) /\ j <_ k) -> (abs` (1 / k)) <_ (1 / j))
23		lelttrt 5504	. . . . . . . . . . . . . . . . . . . 20 |- (((abs` (1 / k)) e. RR /\ (1 / j) e. RR /\ x e. RR) -> (((abs` (1 / k)) <_ (1 / j) /\ (1 / j) < x) -> (abs` (1 / k)) < x))
24	4	recnd 5295	. . . . . . . . . . . . . . . . . . . . . 22 |- (k e. NN -> (1 / k) e. CC)
25		absclt 6776	. . . . . . . . . . . . . . . . . . . . . 22 |- ((1 / k) e. CC -> (abs` (1 / k)) e. RR)
26	24, 25	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- (k e. NN -> (abs` (1 / k)) e. RR)
27	26	adantl 388	. . . . . . . . . . . . . . . . . . . 20 |- (((x e. RR /\ j e. NN) /\ k e. NN) -> (abs` (1 / k)) e. RR)
28		nnrecret 6223	. . . . . . . . . . . . . . . . . . . . 21 |- (j e. NN -> (1 / j) e. RR)
29	28	ad2antlr 405	. . . . . . . . . . . . . . . . . . . 20 |- (((x e. RR /\ j e. NN) /\ k e. NN) -> (1 / j) e. RR)
30		simpll 412	. . . . . . . . . . . . . . . . . . . 20 |- (((x e. RR /\ j e. NN) /\ k e. NN) -> x e. RR)
31	23, 27, 29, 30	syl3anc 857	. . . . . . . . . . . . . . . . . . 19 |- (((x e. RR /\ j e. NN) /\ k e. NN) -> (((abs` (1 / k)) <_ (1 / j) /\ (1 / j) < x) -> (abs` (1 / k)) < x))
32	31	adantllr 397	. . . . . . . . . . . . . . . . . 18 |- ((((x e. RR /\ 0 < x) /\ j e. NN) /\ k e. NN) -> (((abs` (1 / k)) <_ (1 / j) /\ (1 / j) < x) -> (abs` (1 / k)) < x))
33	32	adantr 389	. . . . . . . . . . . . . . . . 17 |- (((((x e. RR /\ 0 < x) /\ j e. NN) /\ k e. NN) /\ j <_ k) -> (((abs` (1 / k)) <_ (1 / j) /\ (1 / j) < x) -> (abs` (1 / k)) < x))
34	22, 33	mpand 700	. . . . . . . . . . . . . . . 16 |- (((((x e. RR /\ 0 < x) /\ j e. NN) /\ k e. NN) /\ j <_ k) -> ((1 / j) < x -> (abs` (1 / k)) < x))
35	34	exp31 376	. . . . . . . . . . . . . . 15 |- (((x e. RR /\ 0 < x) /\ j e. NN) -> (k e. NN -> (j <_ k -> ((1 / j) < x -> (abs` (1 / k)) < x))))
36	35	com23 32	. . . . . . . . . . . . . 14 |- (((x e. RR /\ 0 < x) /\ j e. NN) -> (j <_ k -> (k e. NN -> ((1 / j) < x -> (abs` (1 / k)) < x))))
37	36	com24 37	. . . . . . . . . . . . 13 |- (((x e. RR /\ 0 < x) /\ j e. NN) -> ((1 / j) < x -> (k e. NN -> (j <_ k -> (abs` (1 / k)) < x))))
38	37	ex 373	. . . . . . . . . . . 12 |- ((x e. RR /\ 0 < x) -> (j e. NN -> ((1 / j) < x -> (k e. NN -> (j <_ k -> (abs` (1 / k)) < x)))))
39	38	imp42 369	. . . . . . . . . . 11 |- ((((x e. RR /\ 0 < x) /\ (j e. NN /\ (1 / j) < x)) /\ k e. NN) -> (j <_ k -> (abs` (1 / k)) < x))
40		fveq2 3715	. . . . . . . . . . . . 13 |- ((F` k) = (1 / k) -> (abs` (F` k)) = (abs` (1 / k)))
41	40	breq1d 2624	. . . . . . . . . . . 12 |- ((F` k) = (1 / k) -> ((abs` (F` k)) < x <-> (abs` (1 / k)) < x))
42	41	biimprd 154	. . . . . . . . . . 11 |- ((F` k) = (1 / k) -> ((abs` (1 / k)) < x -> (abs` (F` k)) < x))
43	39, 42	syl9 57	. . . . . . . . . 10 |- ((((x e. RR /\ 0 < x) /\ (j e. NN /\ (1 / j) < x)) /\ k e. NN) -> ((F` k) = (1 / k) -> (j <_ k -> (abs` (F` k)) < x)))
44	43	r19.20dva 1706	. . . . . . . . 9 |- (((x e. RR /\ 0 < x) /\ (j e. NN /\ (1 / j) < x)) -> (A.k e. NN (F` k) = (1 / k) -> A.k e. NN (j <_ k -> (abs` (F` k)) < x)))
45	44	exp32 377	. . . . . . . 8 |- ((x e. RR /\ 0 < x) -> (j e. NN -> ((1 / j) < x -> (A.k e. NN (F` k) = (1 / k) -> A.k e. NN (j <_ k -> (abs` (F` k)) < x)))))
46	45	com4r 41	. . . . . . 7 |- (A.k e. NN (F` k) = (1 / k) -> ((x e. RR /\ 0 < x) -> (j e. NN -> ((1 / j) < x -> A.k e. NN (j <_ k -> (abs` (F` k)) < x)))))
47	46	imp 350	. . . . . 6 |- ((A.k e. NN (F` k) = (1 / k) /\ (x e. RR /\ 0 < x)) -> (j e. NN -> ((1 / j) < x -> A.k e. NN (j <_ k -> (abs` (F` k)) < x))))
48	47	r19.22dv 1734	. . . . 5 |- ((A.k e. NN (F` k) = (1 / k) /\ (x e. RR /\ 0 < x)) -> (E.j e. NN (1 / j) < x -> E.j e. NN A.k e. NN (j <_ k -> (abs` (F` k)) < x)))
49	2, 48	mpd 26	. . . 4 |- ((A.k e. NN (F` k) = (1 / k) /\ (x e. RR /\ 0 < x)) -> E.j e. NN A.k e. NN (j <_ k -> (abs` (F` k)) < x))
50	49	exp32 377	. . 3 |- (A.k e. NN (F` k) = (1 / k) -> (x e. RR -> (0 < x -> E.j e. NN A.k e. NN (j <_ k -> (abs` (F` k)) < x))))
51	50	r19.21aiv 1710	. 2 |- (A.k e. NN (F` k) = (1 / k) -> A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> (abs` (F` k)) < x)))
52		eleq1 1531	. . . . 5 |- ((F` k) = (1 / k) -> ((F` k) e. CC <-> (1 / k) e. CC))
53	52, 24	syl5cbir 211	. . . 4 |- (k e. NN -> ((F` k) = (1 / k) -> (F` k) e. CC))
54	53	r19.20i 1701	. . 3 |- (A.k e. NN (F` k) = (1 /