Theorem mulscutlem

Description: Lemma for mulscut . State the theorem with extra DV conditions. (Contributed by Scott Fenton, 7-Mar-2025)

	Ref	Expression
Hypotheses	mulscutlem.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulscutlem.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	mulscutlem	Could not format assertion : No typesetting found for |- ( ph -> ( ( A x.s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <

Proof

Step	Hyp	Ref	Expression
1		mulscutlem.1	$$⊢\phi \to A\in \mathrm{No}$$
2		mulscutlem.2	$$⊢\phi \to B\in \mathrm{No}$$
3		mulsprop	Could not format ( ( ( e e. No /\ f e. No ) /\ ( g e. No /\ h e. No ) /\ ( i e. No /\ j e. No ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) ) ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) )
4	3	a1d	Could not format ( ( ( e e. No /\ f e. No ) /\ ( g e. No /\ h e. No ) /\ ( i e. No /\ j e. No ) ) -> ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) ) ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) )
5	4	3expa	Could not format ( ( ( ( e e. No /\ f e. No ) /\ ( g e. No /\ h e. No ) ) /\ ( i e. No /\ j e. No ) ) -> ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) ) ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) )
6	5	ralrimivva	Could not format ( ( ( e e. No /\ f e. No ) /\ ( g e. No /\ h e. No ) ) -> A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) ) A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) )
7	6	ralrimivva	Could not format ( ( e e. No /\ f e. No ) -> A. g e. No A. h e. No A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) ) A. g e. No A. h e. No A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) )
8	7	rgen2	Could not format A. e e. No A. f e. No A. g e. No A. h e. No A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) ) ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) )
9	8	a1i	Could not format ( ( A e. No /\ B e. No ) -> A. e e. No A. f e. No A. g e. No A. h e. No A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) ) A. e e. No A. f e. No A. g e. No A. h e. No A. i e. No A. j e. No ( ( ( ( bday ` e ) +no ( bday ` f ) ) u. ( ( ( ( bday ` g ) +no ( bday ` i ) ) u. ( ( bday ` h ) +no ( bday ` j ) ) ) u. ( ( ( bday ` g ) +no ( bday ` j ) ) u. ( ( bday ` h ) +no ( bday ` i ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) -> ( ( e x.s f ) e. No /\ ( ( g ( ( g x.s j ) -s ( g x.s i ) )
10		simpl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A\in \mathrm{No}$$
11		simpr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to B\in \mathrm{No}$$
12	9 10 11	mulsproplem10	Could not format ( ( A e. No /\ B e. No ) -> ( ( A x.s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( A x.s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
13	1 2 12	syl2anc	Could not format ( ph -> ( ( A x.s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( A x.s B ) e. No /\ ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <