AXIOMS

******

1 ~0=1/5

Axiom

2 ALL(x):[x e real => [1/x=5 <=> x=1/5]]

Axiom

PROOF

*****

Prove: ALL(a):[a e real => [a=0 => 1/a=5 <=> ~a=0]]

Suppose...

3 a e real

Premise

Prove: a=0 => ~[a=0 => 1/a=5]

Suppose...

4 a=0

Premise

Prove: ~[a=0 => 1/a=5]

Suppose to the contrary...

5 a=0 => 1/a=5

Premise

6 1/a=5

Detach, 5, 4

7 a e real => [1/a=5 <=> a=1/5]

U Spec, 2

8 1/a=5 <=> a=1/5

Detach, 7, 3

9 [1/a=5 => a=1/5] & [a=1/5 => 1/a=5]

Iff-And, 8

10 1/a=5 => a=1/5

Split, 9

11 a=1/5 => 1/a=5

Split, 9

12 a=1/5

Detach, 10, 6

13 0=1/5

Substitute, 4, 12

14 0=1/5 & ~0=1/5

Join, 13, 1

As Required:

15 ~[a=0 => 1/a=5]

4 Conclusion, 5

As Required:

16 a=0 => ~[a=0 => 1/a=5]

4 Conclusion, 4

17 ~~[a=0 => 1/a=5] => ~a=0

Contra, 16

18 a=0 => 1/a=5 => ~a=0

Rem DNeg, 17

Prove: ~a=0 => [a=0 => 1/a=5]

Suppose...

19 ~a=0

Premise

20 ~~a=0 => 1/a=5

Arb Cons, 19

21 a=0 => 1/a=5

Rem DNeg, 20

As Required:

22 ~a=0 => [a=0 => 1/a=5]

4 Conclusion, 19

23 [a=0 => 1/a=5 => ~a=0] & [~a=0 => [a=0 => 1/a=5]]

Join, 18, 22

24 a=0 => 1/a=5 <=> ~a=0

Iff-And, 23

As Required:

25 ALL(a):[a e real => [a=0 => 1/a=5 <=> ~a=0]]

4 Conclusion, 3