Let me now try to prove a well known limit which in ordinary mathematical books is proved within 5-6 lines. The limit is: lim(1/n)=0 as n-->oo (infinity)
According to the definition of a limit of a sequence we must prove that:
for all e>0 there exists an No ε N (natural numbers) such that for all n, n>=No then
|1/n-0|<e
1) e>0 assumption
2) for all, a (a>0 --> 1/a>0) theorem in inequalities
3) e>0 --> 1/e >0 from 2 and Univ.Elim.
4) 1/e>0 from 1 and 3 and M.Ponens
5) for all h (h>0 --> there exists No (No ε N and No>h)) theorem in real Nos known as Archimedean property
6) 1/e> 0 --> there exists No (No ε N and No>1/e) from 5 and Univ.Elim. where we put h=1/e
7) There exists No (No ε N and No>1/e) from 4 and 6 and M.Ponens
8) No ε N and No>1/e hypothesis for the choose rule
9) No ε N from 8 and conjuction elimination
10) 1/e<No from 8 and conjuction elimination
10a) n>=No hypothesis
11) for all k, (k ε N --> k>0) theorem in natural Nos
12) No ε Ν --> Νο > 0 from 11 and Univ.Elim. where we put k=No
13) No>0 from 9 and 12 and M.Ponens
14) For all a,b [0<a-->(a<=b<-->1/b<=1/a)] theorem in inequalities
15) 0 <No --> (No<=n <--> 1/n<=1/No) from 14 and Univ. Elim. where we put a=No and b=n
16) No <= n <--> 1/n <= 1/No from 15 and 13 and M. Ponens
17) 1/n <= 1/No from 10a and 16 and M.Ponens
18) for all a,b [0<a-->(a<b<-->1/b<1/a)] theorem in inequalities
19) 0 < 1/e --> (1/e<No <--> 1/No<e) from 20 and Univ. Elim. where we put a=1/e and b=No
20) 1/e<No <--> 1/No<e from 4 and 19 and M.Ponens
21) 1/No<e from 10 and 20 and M.Ponens
22) for all,a,b,c (a<=b and b<c ------> a<c) a theorem in real Nos
23) 1/n<= 1/No and 1/No<e ------> 1/n<e from 22 and Univ.Elim. where we put a=1/n,b= 1/No and c=e
24) 1/n<= 1/No and 1/No<e from 17 and 21 and conjuction introduction
25) 1/n<e from 23 and 24 and M.Ponens
26) for all a,b,c (a<b and b<=c-------> a<c) a theorem in inequalities
27) 0<No and No<=n -------->0<n from 26 and Univ.Elim. where we put a=0,b=No and c=n
28) 0<No and No<=n from 10a and 13 and conjuction introduction
29) 0<n from 27 and 28 and M.Ponens
30) 0<n-------> 0< 1/n from 2 and Univ.Elim. where we put a=n
31) 0<1/n from 29 and 30 and M.Ponens
32) for all x, (0<x -------> IxI=x) definition in absolute values
33) 0<1/n -------> I1/nI= I1/n-0I= 1/n from 32 and Univ.Elim. where we put x=1/n
34) I1/nI=I1/n-0I=1/n from 31 and 33 and M.Ponens
35) I1/nI<e by substituting 34 into 25
36) n>=No----------> I1/nI<e from steps 10a to 35 by using the conditional proof rule
37) for all n( n>=No -------------> I1/nI <e) from 36 and Univ.Introduction
38) Noε Ν and for all n( n>=No ------------> I1/nI<e) from 9 and 37 and conjuction introduction
39) there exists No ( No ε Ν and for all n( n>=No----------> I1/nI<e)) from 38 and existential introduction
40) there exists No ( No ε Ν and for all n( n>=No----------> I1/nI<e)) from steps 8 to 39 where according to the choose rule of logic we can discharge the hypothesis of step 8 and be left with the result of 39
41) e> 0--------> there exists No ( No ε Ν and for all n( n>=No----------> I1/nI<e)) from steps 1 to 40 and using the rule of conditional proof
42) for all e [ e>0--------> there exists No ( No ε Ν and for all n( n>=No----------> I1/nI<e)) from 41 and Univ. Introduction
HENCE WE HAVE PROVED lim 1/n =0 as n-----------> 00(infinity)
