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 ∈ No ∧ B ∈ No ∧ N ∈ ℕ s ∧ M ∈ ℕ s ∧ + s ⁡ N < s A ∧ A < s N ∧ + s ⁡ M < s B ∧ B < s M → ∃ p ∈ ℕ s + s ⁡ p < s A ⋅ s B ∧ A ⋅ s B < s p

Proof

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