Metamath Proof Explorer

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 ⊢ φ → A ∈ No
mulscutlem.2 ⊢ φ → B ∈ No
Assertion mulscutlem ⊢ φ → A ⋅ s B ∈ No ∧ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s A ⋅ s B ∧ A ⋅ s B ≪ s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w

Proof

Step Hyp Ref Expression
1 mulscutlem.1 ⊢ φ → A ∈ No
2 mulscutlem.2 ⊢ φ → B ∈ No
3 mulsprop ⊢ e ∈ No ∧ f ∈ No ∧ g ∈ No ∧ h ∈ No ∧ i ∈ No ∧ j ∈ No → e ⋅ s f ∈ No ∧ g < s h ∧ i < s j → g ⋅ s j - s g ⋅ s i < s h ⋅ s j - s h ⋅ s i
4 3 a1d ⊢ e ∈ No ∧ f ∈ No ∧ g ∈ No ∧ h ∈ No ∧ i ∈ No ∧ j ∈ No → bday ⁡ e + bday ⁡ f ∪ bday ⁡ g + bday ⁡ i ∪ bday ⁡ h + bday ⁡ j ∪ bday ⁡ g + bday ⁡ j ∪ bday ⁡ h + bday ⁡ i ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s → e ⋅ s f ∈ No ∧ g < s h ∧ i < s j → g ⋅ s j - s g ⋅ s i < s h ⋅ s j - s h ⋅ s i
5 4 3expa ⊢ e ∈ No ∧ f ∈ No ∧ g ∈ No ∧ h ∈ No ∧ i ∈ No ∧ j ∈ No → bday ⁡ e + bday ⁡ f ∪ bday ⁡ g + bday ⁡ i ∪ bday ⁡ h + bday ⁡ j ∪ bday ⁡ g + bday ⁡ j ∪ bday ⁡ h + bday ⁡ i ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s → e ⋅ s f ∈ No ∧ g < s h ∧ i < s j → g ⋅ s j - s g ⋅ s i < s h ⋅ s j - s h ⋅ s i
6 5 ralrimivva ⊢ e ∈ No ∧ f ∈ No ∧ g ∈ No ∧ h ∈ No → ∀ i ∈ No ∀ j ∈ No bday ⁡ e + bday ⁡ f ∪ bday ⁡ g + bday ⁡ i ∪ bday ⁡ h + bday ⁡ j ∪ bday ⁡ g + bday ⁡ j ∪ bday ⁡ h + bday ⁡ i ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s → e ⋅ s f ∈ No ∧ g < s h ∧ i < s j → g ⋅ s j - s g ⋅ s i < s h ⋅ s j - s h ⋅ s i
7 6 ralrimivva ⊢ e ∈ No ∧ f ∈ No → ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No bday ⁡ e + bday ⁡ f ∪ bday ⁡ g + bday ⁡ i ∪ bday ⁡ h + bday ⁡ j ∪ bday ⁡ g + bday ⁡ j ∪ bday ⁡ h + bday ⁡ i ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s → e ⋅ s f ∈ No ∧ g < s h ∧ i < s j → g ⋅ s j - s g ⋅ s i < s h ⋅ s j - s h ⋅ s i
8 7 rgen2 ⊢ ∀ e ∈ No ∀ f ∈ No ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No bday ⁡ e + bday ⁡ f ∪ bday ⁡ g + bday ⁡ i ∪ bday ⁡ h + bday ⁡ j ∪ bday ⁡ g + bday ⁡ j ∪ bday ⁡ h + bday ⁡ i ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s → e ⋅ s f ∈ No ∧ g < s h ∧ i < s j → g ⋅ s j - s g ⋅ s i < s h ⋅ s j - s h ⋅ s i
9 8 a1i ⊢ A ∈ No ∧ B ∈ No → ∀ e ∈ No ∀ f ∈ No ∀ g ∈ No ∀ h ∈ No ∀ i ∈ No ∀ j ∈ No bday ⁡ e + bday ⁡ f ∪ bday ⁡ g + bday ⁡ i ∪ bday ⁡ h + bday ⁡ j ∪ bday ⁡ g + bday ⁡ j ∪ bday ⁡ h + bday ⁡ i ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s → e ⋅ s f ∈ No ∧ g < s h ∧ i < s j → g ⋅ s j - s g ⋅ s i < s h ⋅ s j - s h ⋅ s i
10 simpl ⊢ A ∈ No ∧ B ∈ No → A ∈ No
11 simpr ⊢ A ∈ No ∧ B ∈ No → B ∈ No
12 9 10 11 mulsproplem10 ⊢ A ∈ No ∧ B ∈ No → A ⋅ s B ∈ No ∧ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s A ⋅ s B ∧ A ⋅ s B ≪ s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
13 1 2 12 syl2anc ⊢ φ → A ⋅ s B ∈ No ∧ a | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B a = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ b | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B b = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s A ⋅ s B ∧ A ⋅ s B ≪ s c | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B c = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ d | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B d = v ⋅ s B + s A ⋅ s w - s v ⋅ s w