Metamath Proof Explorer

Theorem remulscllem2

Description: Lemma for remulscl . Bound A and B above and below. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Assertion remulscllem2 
|- ( ( ( A e. No /\ B e. No ) /\ ( ( N e. NN_s /\ M e. NN_s ) /\ ( ( ( -us ` N )  E. p e. NN_s ( ( -us ` p )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( p = ( N x.s M ) -> ( ( abs_s ` ( A x.s B ) )  ( abs_s ` ( A x.s B ) )
2 nnmulscl 
 |-  ( ( N e. NN_s /\ M e. NN_s ) -> ( N x.s M ) e. NN_s )
3 2 ad2antlr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  ( N x.s M ) e. NN_s )
4 absmuls 
 |-  ( ( A e. No /\ B e. No ) -> ( abs_s ` ( A x.s B ) ) = ( ( abs_s ` A ) x.s ( abs_s ` B ) ) )
5 4 ad2antrr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  ( abs_s ` ( A x.s B ) ) = ( ( abs_s ` A ) x.s ( abs_s ` B ) ) )
6 absscl 
 |-  ( A e. No -> ( abs_s ` A ) e. No )
7 6 ad3antrrr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  ( abs_s ` A ) e. No )
8 simplrl 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  N e. NN_s )
9 8 nnsnod 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  N e. No )
10 absscl 
 |-  ( B e. No -> ( abs_s ` B ) e. No )
11 10 ad3antlr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  ( abs_s ` B ) e. No )
12 simplrr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  M e. NN_s )
13 12 nnsnod 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  M e. No )
14 abssge0 
 |-  ( A e. No -> 0s <_s ( abs_s ` A ) )
15 14 ad3antrrr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  0s <_s ( abs_s ` A ) )
16 simprl 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  ( abs_s ` A )
17 abssge0 
 |-  ( B e. No -> 0s <_s ( abs_s ` B ) )
18 17 ad3antlr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  0s <_s ( abs_s ` B ) )
19 simprr 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  ( abs_s ` B )
20 7 9 11 13 15 16 18 19 sltmul12ad 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  ( ( abs_s ` A ) x.s ( abs_s ` B ) )
21 5 20 eqbrtrd 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  ( abs_s ` ( A x.s B ) )
22 1 3 21 rspcedvdw 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ ( ( abs_s ` A )  E. p e. NN_s ( abs_s ` ( A x.s B ) )
23 22 ex 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) -> ( ( ( abs_s ` A )  E. p e. NN_s ( abs_s ` ( A x.s B ) )
24 nnsno 
 |-  ( N e. NN_s -> N e. No )
25 absslt 
 |-  ( ( A e. No /\ N e. No ) -> ( ( abs_s ` A )  ( ( -us ` N )
26 24 25 sylan2 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( ( abs_s ` A )  ( ( -us ` N )
27 nnsno 
 |-  ( M e. NN_s -> M e. No )
28 absslt 
 |-  ( ( B e. No /\ M e. No ) -> ( ( abs_s ` B )  ( ( -us ` M )
29 27 28 sylan2 
 |-  ( ( B e. No /\ M e. NN_s ) -> ( ( abs_s ` B )  ( ( -us ` M )
30 26 29 bi2anan9 
 |-  ( ( ( A e. No /\ N e. NN_s ) /\ ( B e. No /\ M e. NN_s ) ) -> ( ( ( abs_s ` A )  ( ( ( -us ` N )
31 30 an4s 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) -> ( ( ( abs_s ` A )  ( ( ( -us ` N )
32 mulscl 
 |-  ( ( A e. No /\ B e. No ) -> ( A x.s B ) e. No )
33 32 adantr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) -> ( A x.s B ) e. No )
34 nnsno 
 |-  ( p e. NN_s -> p e. No )
35 absslt 
 |-  ( ( ( A x.s B ) e. No /\ p e. No ) -> ( ( abs_s ` ( A x.s B ) )  ( ( -us ` p )
36 33 34 35 syl2an 
 |-  ( ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) /\ p e. NN_s ) -> ( ( abs_s ` ( A x.s B ) )  ( ( -us ` p )
37 36 rexbidva 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) -> ( E. p e. NN_s ( abs_s ` ( A x.s B ) )  E. p e. NN_s ( ( -us ` p )
38 23 31 37 3imtr3d 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( N e. NN_s /\ M e. NN_s ) ) -> ( ( ( ( -us ` N )  E. p e. NN_s ( ( -us ` p )
39 38 impr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( ( N e. NN_s /\ M e. NN_s ) /\ ( ( ( -us ` N )  E. p e. NN_s ( ( -us ` p )