Now i will start giving formal proofs of theorems concering the real Nos
So let us prove : For all xεR 0x=0
1) for all x, 1.x=x............ ......An axiom on real Nos2
2) 1.x=x ..............................from 1 and using Univ. Elim.
3) for all x,y,z (y+z).x= yx +zx................................... An axiom on real Nos (distributive property)
4) (0+1).x= 0x+1x...................... from 3and using Univ.Elim. where we put y=0,z=1,x=x
5) for all x,0+x=x .....................An axiom in real Nos
6) 0+1=1 ................................from 5 and using Univ.Elim.where we put x=1
7) 1x= 0x+1x........................ by substituting 6 into 4
8) x=0x+x ...........................by substituting 1 into 7
9) for all a,b,c a=b ----> a+c=b+c ..............................An axiom in equality
10) x=ox+x -------> x+(-x)= (0x+x)+(-x) ....................................from 9 and using Univ.Elim.where we put a=x,b= 0x+x,c=(-x)
11) x+(-x)= (0x+x)+(-x) ...............from 8 and 10 and using M.Ponens
12) for all a,b,c (a+b)+c= a+(b+c)...... An axiom in real Nos
13) (0x+x)+(-x) =0x +(x+(-x)) ...........from 12 and using Univ,Elim. where we put a=0x,b=x,c=(-x)
14) x+(-x) =0x +(x+(-x))................ by substituting 13 into 11
15) for all x, x+(-x) =0 ................An axiom in real Nos
16) x+(-x)=0............................. from 15 and using Univ.Elim.
17) 0 = 0x +0 ............................by substituting 16 into 14
18) 0x + 0 = 0x........................... from 5 and using Univ.Elim. where we put x=0x