Metamath Proof Explorer

Theorem addscutlem

Description: Lemma for addscut . Show the statement with some additional distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Hypotheses addscutlem.1 ⊢ φ → X ∈ No
addscutlem.2 ⊢ φ → Y ∈ No
Assertion addscutlem ⊢ φ → X + s Y ∈ No ∧ p | ∃ l ∈ L ⁡ X p = l + s Y ∪ q | ∃ m ∈ L ⁡ Y q = X + s m ≪ s X + s Y ∧ X + s Y ≪ s w | ∃ r ∈ R ⁡ X w = r + s Y ∪ t | ∃ s ∈ R ⁡ Y t = X + s s

Proof

Step Hyp Ref Expression
1 addscutlem.1 ⊢ φ → X ∈ No
2 addscutlem.2 ⊢ φ → Y ∈ No
3 addsprop ⊢ x ∈ No ∧ y ∈ No ∧ z ∈ No → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
4 3 a1d ⊢ x ∈ No ∧ y ∈ No ∧ z ∈ No → bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ 0 s → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
5 4 rgen3 ⊢ ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ 0 s → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
6 5 a1i ⊢ φ → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ 0 s → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
7 6 1 2 addsproplem3 ⊢ φ → X + s Y ∈ No ∧ p | ∃ l ∈ L ⁡ X p = l + s Y ∪ q | ∃ m ∈ L ⁡ Y q = X + s m ≪ s X + s Y ∧ X + s Y ≪ s w | ∃ r ∈ R ⁡ X w = r + s Y ∪ t | ∃ s ∈ R ⁡ Y t = X + s s