Theorem sltmul12ad

Description: Comparison of the product of two positive surreals. (Contributed by Scott Fenton, 17-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		sltmul12ad.1	$$⊢\phi \to A\in \mathrm{No}$$
2		sltmul12ad.2	$$⊢\phi \to B\in \mathrm{No}$$
3		sltmul12ad.3	$$⊢\phi \to C\in \mathrm{No}$$
4		sltmul12ad.4	$$⊢\phi \to D\in \mathrm{No}$$
5		sltmul12ad.5	Could not format ( ph -> 0s <_s A ) : No typesetting found for |- ( ph -> 0s <_s A ) with typecode |-
6		sltmul12ad.6	$$⊢\phi \to A{<}_{s}B$$
7		sltmul12ad.7	Could not format ( ph -> 0s <_s C ) : No typesetting found for |- ( ph -> 0s <_s C ) with typecode |-
8		sltmul12ad.8	$$⊢\phi \to C{<}_{s}D$$
9	1 3	mulscld	Could not format ( ph -> ( A x.s C ) e. No ) : No typesetting found for |- ( ph -> ( A x.s C ) e. No ) with typecode |-
10	2 3	mulscld	Could not format ( ph -> ( B x.s C ) e. No ) : No typesetting found for |- ( ph -> ( B x.s C ) e. No ) with typecode |-
11	2 4	mulscld	Could not format ( ph -> ( B x.s D ) e. No ) : No typesetting found for |- ( ph -> ( B x.s D ) e. No ) with typecode |-
12	1 2 6	sltled	$$⊢\phi \to A{\le }_{s}B$$
13	1 2 3 7 12	slemul1ad	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 |-
14		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
15	14	a1i	Could not format ( ph -> 0s e. No ) : No typesetting found for |- ( ph -> 0s e. No ) with typecode |-
16	15 1 2 5 6	slelttrd	Could not format ( ph -> 0s 0s
17	3 4 2 16	sltmul2d	Could not format ( ph -> ( C ( B x.s C ) ( C ( B x.s C )
18	8 17	mpbid	Could not format ( ph -> ( B x.s C ) ( B x.s C )
19	9 10 11 13 18	slelttrd	Could not format ( ph -> ( A x.s C ) ( A x.s C )