Theorem slemul1ad

Description: Multiplication of both sides of surreal less-than or equal by a non-negative number. (Contributed by Scott Fenton, 17-Apr-2025)

	Ref	Expression
Hypotheses	slemul1ad.1	$$⊢\phi \to A\in \mathrm{No}$$
	slemul1ad.2	$$⊢\phi \to B\in \mathrm{No}$$
	slemul1ad.3	$$⊢\phi \to C\in \mathrm{No}$$
	slemul1ad.4	No typesetting found for |- ( ph -> 0s <_s C ) with typecode |-
	slemul1ad.5	$$⊢\phi \to A{\le }_{s}B$$
Assertion	slemul1ad	Could not format assertion : No typesetting found for |- ( ph -> ( A x.s C ) <_s ( B x.s C ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		slemul1ad.1	$$⊢\phi \to A\in \mathrm{No}$$
2		slemul1ad.2	$$⊢\phi \to B\in \mathrm{No}$$
3		slemul1ad.3	$$⊢\phi \to C\in \mathrm{No}$$
4		slemul1ad.4	Could not format ( ph -> 0s <_s C ) : No typesetting found for |- ( ph -> 0s <_s C ) with typecode |-
5		slemul1ad.5	$$⊢\phi \to A{\le }_{s}B$$
6	5	adantr	Could not format ( ( ph /\ 0s A <_s B ) : No typesetting found for |- ( ( ph /\ 0s A <_s B ) with typecode |-
7	1	adantr	Could not format ( ( ph /\ 0s A e. No ) : No typesetting found for |- ( ( ph /\ 0s A e. No ) with typecode |-
8	2	adantr	Could not format ( ( ph /\ 0s B e. No ) : No typesetting found for |- ( ( ph /\ 0s B e. No ) with typecode |-
9	3	adantr	Could not format ( ( ph /\ 0s C e. No ) : No typesetting found for |- ( ( ph /\ 0s C e. No ) with typecode |-
10		simpr	Could not format ( ( ph /\ 0s 0s 0s
11	7 8 9 10	slemul1d	Could not format ( ( ph /\ 0s ( A <_s B <-> ( A x.s C ) <_s ( B x.s C ) ) ) : No typesetting found for |- ( ( ph /\ 0s ( A <_s B <-> ( A x.s C ) <_s ( B x.s C ) ) ) with typecode |-
12	6 11	mpbid	Could not format ( ( ph /\ 0s ( A x.s C ) <_s ( B x.s C ) ) : No typesetting found for |- ( ( ph /\ 0s ( A x.s C ) <_s ( B x.s C ) ) with typecode |-
13		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
14		slerflex	Could not format ( 0s e. No -> 0s <_s 0s ) : No typesetting found for |- ( 0s e. No -> 0s <_s 0s ) with typecode |-
15	13 14	mp1i	Could not format ( ph -> 0s <_s 0s ) : No typesetting found for |- ( ph -> 0s <_s 0s ) with typecode |-
16		muls01	Could not format ( A e. No -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( A e. No -> ( A x.s 0s ) = 0s ) with typecode |-
17	1 16	syl	Could not format ( ph -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( ph -> ( A x.s 0s ) = 0s ) with typecode |-
18		muls01	Could not format ( B e. No -> ( B x.s 0s ) = 0s ) : No typesetting found for |- ( B e. No -> ( B x.s 0s ) = 0s ) with typecode |-
19	2 18	syl	Could not format ( ph -> ( B x.s 0s ) = 0s ) : No typesetting found for |- ( ph -> ( B x.s 0s ) = 0s ) with typecode |-
20	15 17 19	3brtr4d	Could not format ( ph -> ( A x.s 0s ) <_s ( B x.s 0s ) ) : No typesetting found for |- ( ph -> ( A x.s 0s ) <_s ( B x.s 0s ) ) with typecode |-
21		oveq2	Could not format ( 0s = C -> ( A x.s 0s ) = ( A x.s C ) ) : No typesetting found for |- ( 0s = C -> ( A x.s 0s ) = ( A x.s C ) ) with typecode |-
22		oveq2	Could not format ( 0s = C -> ( B x.s 0s ) = ( B x.s C ) ) : No typesetting found for |- ( 0s = C -> ( B x.s 0s ) = ( B x.s C ) ) with typecode |-
23	21 22	breq12d	Could not format ( 0s = C -> ( ( A x.s 0s ) <_s ( B x.s 0s ) <-> ( A x.s C ) <_s ( B x.s C ) ) ) : No typesetting found for |- ( 0s = C -> ( ( A x.s 0s ) <_s ( B x.s 0s ) <-> ( A x.s C ) <_s ( B x.s C ) ) ) with typecode |-
24	20 23	syl5ibcom	Could not format ( ph -> ( 0s = C -> ( A x.s C ) <_s ( B x.s C ) ) ) : No typesetting found for |- ( ph -> ( 0s = C -> ( A x.s C ) <_s ( B x.s C ) ) ) with typecode |-
25	24	imp	Could not format ( ( ph /\ 0s = C ) -> ( A x.s C ) <_s ( B x.s C ) ) : No typesetting found for |- ( ( ph /\ 0s = C ) -> ( A x.s C ) <_s ( B x.s C ) ) with typecode |-
26		sleloe	Could not format ( ( 0s e. No /\ C e. No ) -> ( 0s <_s C <-> ( 0s ( 0s <_s C <-> ( 0s
27	13 3 26	sylancr	Could not format ( ph -> ( 0s <_s C <-> ( 0s ( 0s <_s C <-> ( 0s
28	4 27	mpbid	Could not format ( ph -> ( 0s ( 0s
29	12 25 28	mpjaodan	Could not format ( ph -> ( A x.s C ) <_s ( B x.s C ) ) : No typesetting found for |- ( ph -> ( A x.s C ) <_s ( B x.s C ) ) with typecode |-