Theorem addscan2

Description: Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	addscan2	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) = ( B +s C ) <-> A = B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sleadd1	Could not format ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B <-> ( A +s C ) <_s ( B +s C ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B <-> ( A +s C ) <_s ( B +s C ) ) ) with typecode |-
2		sleadd1	Could not format ( ( B e. No /\ A e. No /\ C e. No ) -> ( B <_s A <-> ( B +s C ) <_s ( A +s C ) ) ) : No typesetting found for |- ( ( B e. No /\ A e. No /\ C e. No ) -> ( B <_s A <-> ( B +s C ) <_s ( A +s C ) ) ) with typecode |-
3	2	3com12	Could not format ( ( A e. No /\ B e. No /\ C e. No ) -> ( B <_s A <-> ( B +s C ) <_s ( A +s C ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> ( B <_s A <-> ( B +s C ) <_s ( A +s C ) ) ) with typecode |-
4	1 3	anbi12d	Could not format ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A <_s B /\ B <_s A ) <-> ( ( A +s C ) <_s ( B +s C ) /\ ( B +s C ) <_s ( A +s C ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A <_s B /\ B <_s A ) <-> ( ( A +s C ) <_s ( B +s C ) /\ ( B +s C ) <_s ( A +s C ) ) ) ) with typecode |-
5		sletri3	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A=B\leftrightarrow \left(A{\le }_{s}B\wedge B{\le }_{s}A\right)\right)$$
6	5	3adant3	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)\to \left(A=B\leftrightarrow \left(A{\le }_{s}B\wedge B{\le }_{s}A\right)\right)$$
7		addscl	Could not format ( ( A e. No /\ C e. No ) -> ( A +s C ) e. No ) : No typesetting found for |- ( ( A e. No /\ C e. No ) -> ( A +s C ) e. No ) with typecode |-
8	7	3adant2	Could not format ( ( A e. No /\ B e. No /\ C e. No ) -> ( A +s C ) e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> ( A +s C ) e. No ) with typecode |-
9		addscl	Could not format ( ( B e. No /\ C e. No ) -> ( B +s C ) e. No ) : No typesetting found for |- ( ( B e. No /\ C e. No ) -> ( B +s C ) e. No ) with typecode |-
10	9	3adant1	Could not format ( ( A e. No /\ B e. No /\ C e. No ) -> ( B +s C ) e. No ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> ( B +s C ) e. No ) with typecode |-
11		sletri3	Could not format ( ( ( A +s C ) e. No /\ ( B +s C ) e. No ) -> ( ( A +s C ) = ( B +s C ) <-> ( ( A +s C ) <_s ( B +s C ) /\ ( B +s C ) <_s ( A +s C ) ) ) ) : No typesetting found for |- ( ( ( A +s C ) e. No /\ ( B +s C ) e. No ) -> ( ( A +s C ) = ( B +s C ) <-> ( ( A +s C ) <_s ( B +s C ) /\ ( B +s C ) <_s ( A +s C ) ) ) ) with typecode |-
12	8 10 11	syl2anc	Could not format ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) = ( B +s C ) <-> ( ( A +s C ) <_s ( B +s C ) /\ ( B +s C ) <_s ( A +s C ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) = ( B +s C ) <-> ( ( A +s C ) <_s ( B +s C ) /\ ( B +s C ) <_s ( A +s C ) ) ) ) with typecode |-
13	4 6 12	3bitr4rd	Could not format ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) = ( B +s C ) <-> A = B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) = ( B +s C ) <-> A = B ) ) with typecode |-