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 ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑁 ) <s 𝐴 ∧ 𝐴 <s 𝑁 ) ∧ ( ( -us ‘ 𝑀 ) <s 𝐵 ∧ 𝐵 <s 𝑀 ) ) ) ) → ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 ·s 𝐵 ) ∧ ( 𝐴 ·s 𝐵 ) <s 𝑝 ) )

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝑝 = ( 𝑁 ·s 𝑀 ) → ( ( abss ‘ ( 𝐴 ·s 𝐵 ) ) <s 𝑝 ↔ ( abss ‘ ( 𝐴 ·s 𝐵 ) ) <s ( 𝑁 ·s 𝑀 ) ) )
2 nnmulscl ⊢ ( ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) → ( 𝑁 ·s 𝑀 ) ∈ ℕs )
3 2 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → ( 𝑁 ·s 𝑀 ) ∈ ℕs )
4 absmuls ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( abss ‘ ( 𝐴 ·s 𝐵 ) ) = ( ( abss ‘ 𝐴 ) ·s ( abss ‘ 𝐵 ) ) )
5 4 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → ( abss ‘ ( 𝐴 ·s 𝐵 ) ) = ( ( abss ‘ 𝐴 ) ·s ( abss ‘ 𝐵 ) ) )
6 absscl ⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) ∈ No )
7 6 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → ( abss ‘ 𝐴 ) ∈ No )
8 simplrl ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → 𝑁 ∈ ℕs )
9 8 nnnod ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → 𝑁 ∈ No )
10 absscl ⊢ ( 𝐵 ∈ No → ( abss ‘ 𝐵 ) ∈ No )
11 10 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → ( abss ‘ 𝐵 ) ∈ No )
12 simplrr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → 𝑀 ∈ ℕs )
13 12 nnnod ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → 𝑀 ∈ No )
14 abssge0 ⊢ ( 𝐴 ∈ No → 0s ≤s ( abss ‘ 𝐴 ) )
15 14 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → 0s ≤s ( abss ‘ 𝐴 ) )
16 simprl ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → ( abss ‘ 𝐴 ) <s 𝑁 )
17 abssge0 ⊢ ( 𝐵 ∈ No → 0s ≤s ( abss ‘ 𝐵 ) )
18 17 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → 0s ≤s ( abss ‘ 𝐵 ) )
19 simprr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → ( abss ‘ 𝐵 ) <s 𝑀 )
20 7 9 11 13 15 16 18 19 ltmuls12ad ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → ( ( abss ‘ 𝐴 ) ·s ( abss ‘ 𝐵 ) ) <s ( 𝑁 ·s 𝑀 ) )
21 5 20 eqbrtrd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → ( abss ‘ ( 𝐴 ·s 𝐵 ) ) <s ( 𝑁 ·s 𝑀 ) )
22 1 3 21 rspcedvdw ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ) → ∃ 𝑝 ∈ ℕs ( abss ‘ ( 𝐴 ·s 𝐵 ) ) <s 𝑝 )
23 22 ex ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) → ( ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) → ∃ 𝑝 ∈ ℕs ( abss ‘ ( 𝐴 ·s 𝐵 ) ) <s 𝑝 ) )
24 nnno ⊢ ( 𝑁 ∈ ℕs → 𝑁 ∈ No )
25 abslts ⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ No ) → ( ( abss ‘ 𝐴 ) <s 𝑁 ↔ ( ( -us ‘ 𝑁 ) <s 𝐴 ∧ 𝐴 <s 𝑁 ) ) )
26 24 25 sylan2 ⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ( ( abss ‘ 𝐴 ) <s 𝑁 ↔ ( ( -us ‘ 𝑁 ) <s 𝐴 ∧ 𝐴 <s 𝑁 ) ) )
27 nnno ⊢ ( 𝑀 ∈ ℕs → 𝑀 ∈ No )
28 abslts ⊢ ( ( 𝐵 ∈ No ∧ 𝑀 ∈ No ) → ( ( abss ‘ 𝐵 ) <s 𝑀 ↔ ( ( -us ‘ 𝑀 ) <s 𝐵 ∧ 𝐵 <s 𝑀 ) ) )
29 27 28 sylan2 ⊢ ( ( 𝐵 ∈ No ∧ 𝑀 ∈ ℕs ) → ( ( abss ‘ 𝐵 ) <s 𝑀 ↔ ( ( -us ‘ 𝑀 ) <s 𝐵 ∧ 𝐵 <s 𝑀 ) ) )
30 26 29 bi2anan9 ⊢ ( ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) ∧ ( 𝐵 ∈ No ∧ 𝑀 ∈ ℕs ) ) → ( ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ↔ ( ( ( -us ‘ 𝑁 ) <s 𝐴 ∧ 𝐴 <s 𝑁 ) ∧ ( ( -us ‘ 𝑀 ) <s 𝐵 ∧ 𝐵 <s 𝑀 ) ) ) )
31 30 an4s ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) → ( ( ( abss ‘ 𝐴 ) <s 𝑁 ∧ ( abss ‘ 𝐵 ) <s 𝑀 ) ↔ ( ( ( -us ‘ 𝑁 ) <s 𝐴 ∧ 𝐴 <s 𝑁 ) ∧ ( ( -us ‘ 𝑀 ) <s 𝐵 ∧ 𝐵 <s 𝑀 ) ) ) )
32 mulscl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ·s 𝐵 ) ∈ No )
33 32 adantr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) → ( 𝐴 ·s 𝐵 ) ∈ No )
34 nnno ⊢ ( 𝑝 ∈ ℕs → 𝑝 ∈ No )
35 abslts ⊢ ( ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ 𝑝 ∈ No ) → ( ( abss ‘ ( 𝐴 ·s 𝐵 ) ) <s 𝑝 ↔ ( ( -us ‘ 𝑝 ) <s ( 𝐴 ·s 𝐵 ) ∧ ( 𝐴 ·s 𝐵 ) <s 𝑝 ) ) )
36 33 34 35 syl2an ⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) ∧ 𝑝 ∈ ℕs ) → ( ( abss ‘ ( 𝐴 ·s 𝐵 ) ) <s 𝑝 ↔ ( ( -us ‘ 𝑝 ) <s ( 𝐴 ·s 𝐵 ) ∧ ( 𝐴 ·s 𝐵 ) <s 𝑝 ) ) )
37 36 rexbidva ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) → ( ∃ 𝑝 ∈ ℕs ( abss ‘ ( 𝐴 ·s 𝐵 ) ) <s 𝑝 ↔ ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 ·s 𝐵 ) ∧ ( 𝐴 ·s 𝐵 ) <s 𝑝 ) ) )
38 23 31 37 3imtr3d ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ) → ( ( ( ( -us ‘ 𝑁 ) <s 𝐴 ∧ 𝐴 <s 𝑁 ) ∧ ( ( -us ‘ 𝑀 ) <s 𝐵 ∧ 𝐵 <s 𝑀 ) ) → ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 ·s 𝐵 ) ∧ ( 𝐴 ·s 𝐵 ) <s 𝑝 ) ) )
39 38 impr ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( 𝑁 ∈ ℕs ∧ 𝑀 ∈ ℕs ) ∧ ( ( ( -us ‘ 𝑁 ) <s 𝐴 ∧ 𝐴 <s 𝑁 ) ∧ ( ( -us ‘ 𝑀 ) <s 𝐵 ∧ 𝐵 <s 𝑀 ) ) ) ) → ∃ 𝑝 ∈ ℕs ( ( -us ‘ 𝑝 ) <s ( 𝐴 ·s 𝐵 ) ∧ ( 𝐴 ·s 𝐵 ) <s 𝑝 ) )