Is the following formal proof, proving $\forall A\forall B \forall C[A+C=B+C\Longrightarrow A=B]$ correct??
Proof
1) $a+c=b+c$.............................................................Hypothesis
2)$\neg(a=b)$......................................................................Hypothesis
3)$\forall A\forall B[\neg(A=B\Longrightarrow A<B \vee B<A)]$..........From trichotomy theorem in real Nos
4)$\neg(a=b\Longrightarrow a<b \vee b<a)$.......From (3) and using Universal Elimination where we put $A=a , B=b$
5)$a<b \vee b<a$................................From (2) & (4) and using Modus Ponens
6)$a<b$.....................................................Hypothesis
7) $\forall A\forall B\forall C[A<B\Longrightarrow A+C<B+C]$................Theorem(Axiom) in real Nos
8)$a<b\Longrightarrow a+c<b+c$......From (7) and using Universal Elimination where we put $A=a,B=b,C=c$
9)$a+c<b+c$....................From (6) & (8) and using Modus Ponens
10)$a+c<a+c$.......................By substituting (1) into (9)
11) $\forall A[\neg(A<A)]$..........................Theorem(Axion) in real Nos
12)$\neg(a+c<a+c)$.......................From (11) and using UE were we put $A=a+c$
13) $\neg(a+c<a+c)\wedge (a+c<a+c)$............From (10) & (12) and using addition introduction
14)$\neg\neg(a=b)$...............................From (2) to (13) and using contradiction
15$a=b$......................................From (14) and using Negation Elimination
16) $a<b\Longrightarrow a=b$
In a similar way we can prove:
17)$b<a\Longrightarrow a=b$
18) $a=b$..................From (5) , (16) , (17) and using Disjunction Elimination
19) $\neg(a=b) \wedge (a=b)$.........................From (2) & (18) and using Addition Introduction
20) $\neg\neg(a=b)$......................................From (2) to (19) and using contradiction
21) $a=b$...............................From (20) and using negation elimination
22) $a+c=b+c\Longrightarrow a=b$........From (1) to (21) and using the law of conditional proof
23) $\forall A\forall B \forall C[A+C=B+C\Longrightarrow A=B]$.................From (22) and using Universal Introduction where we put $a=A,b=B,c=C$
If I stopped at line (19) the conclusion would not had been :$a+c<b+c\Longrightarrow a<b$
BUT, $[(a+c<b+c)\wedge (\neg(a<b)]\Longrightarrow a<b$.
Because the hypothesis $ \neg a<b$ had not been discharged yet
This is a simple application of deduction theoerem ( law of conditional proof).
If we assume P and prove Q ,then we have rpoved :**If P, then Q **
And in our case $P$ IS :$[(a+c<b+c)\wedge (\neg(a<b)]$ AND not only $a+c<b+c$