Metamath Proof Explorer

Theorem mulsproplem9

Description: Lemma for surreal multiplication. Show that the cut involved in surreal multiplication makes sense. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses mulsproplem.1 ⊢ φ → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
mulsproplem9.1 ⊢ φ → A ∈ No
mulsproplem9.2 ⊢ φ → B ∈ No
Assertion mulsproplem9 ⊢ φ → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w

Proof

Step Hyp Ref Expression
1 mulsproplem.1 ⊢ φ → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
2 mulsproplem9.1 ⊢ φ → A ∈ No
3 mulsproplem9.2 ⊢ φ → B ∈ No
4 eqid ⊢ p ∈ L ⁡ A , q ∈ L ⁡ B ⟼ p ⋅ s B + s A ⋅ s q - s p ⋅ s q = p ∈ L ⁡ A , q ∈ L ⁡ B ⟼ p ⋅ s B + s A ⋅ s q - s p ⋅ s q
5 4 rnmpo ⊢ ran ⁡ p ∈ L ⁡ A , q ∈ L ⁡ B ⟼ p ⋅ s B + s A ⋅ s q - s p ⋅ s q = g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q
6 fvex ⊢ L ⁡ A ∈ V
7 fvex ⊢ L ⁡ B ∈ V
8 6 7 mpoex ⊢ p ∈ L ⁡ A , q ∈ L ⁡ B ⟼ p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∈ V
9 8 rnex ⊢ ran ⁡ p ∈ L ⁡ A , q ∈ L ⁡ B ⟼ p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∈ V
10 5 9 eqeltrri ⊢ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∈ V
11 eqid ⊢ r ∈ R ⁡ A , s ∈ R ⁡ B ⟼ r ⋅ s B + s A ⋅ s s - s r ⋅ s s = r ∈ R ⁡ A , s ∈ R ⁡ B ⟼ r ⋅ s B + s A ⋅ s s - s r ⋅ s s
12 11 rnmpo ⊢ ran ⁡ r ∈ R ⁡ A , s ∈ R ⁡ B ⟼ r ⋅ s B + s A ⋅ s s - s r ⋅ s s = h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
13 fvex ⊢ R ⁡ A ∈ V
14 fvex ⊢ R ⁡ B ∈ V
15 13 14 mpoex ⊢ r ∈ R ⁡ A , s ∈ R ⁡ B ⟼ r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∈ V
16 15 rnex ⊢ ran ⁡ r ∈ R ⁡ A , s ∈ R ⁡ B ⟼ r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∈ V
17 12 16 eqeltrri ⊢ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∈ V
18 10 17 unex ⊢ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∈ V
19 18 a1i ⊢ φ → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∈ V
20 eqid ⊢ t ∈ L ⁡ A , u ∈ R ⁡ B ⟼ t ⋅ s B + s A ⋅ s u - s t ⋅ s u = t ∈ L ⁡ A , u ∈ R ⁡ B ⟼ t ⋅ s B + s A ⋅ s u - s t ⋅ s u
21 20 rnmpo ⊢ ran ⁡ t ∈ L ⁡ A , u ∈ R ⁡ B ⟼ t ⋅ s B + s A ⋅ s u - s t ⋅ s u = i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u
22 6 14 mpoex ⊢ t ∈ L ⁡ A , u ∈ R ⁡ B ⟼ t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∈ V
23 22 rnex ⊢ ran ⁡ t ∈ L ⁡ A , u ∈ R ⁡ B ⟼ t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∈ V
24 21 23 eqeltrri ⊢ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∈ V
25 eqid ⊢ v ∈ R ⁡ A , w ∈ L ⁡ B ⟼ v ⋅ s B + s A ⋅ s w - s v ⋅ s w = v ∈ R ⁡ A , w ∈ L ⁡ B ⟼ v ⋅ s B + s A ⋅ s w - s v ⋅ s w
26 25 rnmpo ⊢ ran ⁡ v ∈ R ⁡ A , w ∈ L ⁡ B ⟼ v ⋅ s B + s A ⋅ s w - s v ⋅ s w = j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
27 13 7 mpoex ⊢ v ∈ R ⁡ A , w ∈ L ⁡ B ⟼ v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ V
28 27 rnex ⊢ ran ⁡ v ∈ R ⁡ A , w ∈ L ⁡ B ⟼ v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ V
29 26 28 eqeltrri ⊢ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ V
30 24 29 unex ⊢ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ V
31 30 a1i ⊢ φ → i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ V
32 1 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
33 simprl ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ∈ L ⁡ A
34 33 leftoldd ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ∈ Old ⁡ bday ⁡ A
35 3 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → B ∈ No
36 32 34 35 mulsproplem2 ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s B ∈ No
37 2 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A ∈ No
38 simprr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → q ∈ L ⁡ B
39 38 leftoldd ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → q ∈ Old ⁡ bday ⁡ B
40 32 37 39 mulsproplem3 ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A ⋅ s q ∈ No
41 36 40 addscld ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s B + s A ⋅ s q ∈ No
42 32 34 39 mulsproplem4 ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s q ∈ No
43 41 42 subscld ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∈ No
44 eleq1 ⊢ g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → g ∈ No ↔ p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∈ No
45 43 44 syl5ibrcom ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → g ∈ No
46 45 rexlimdvva ⊢ φ → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → g ∈ No
47 46 abssdv ⊢ φ → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ⊆ No
48 1 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
49 simprl ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ∈ R ⁡ A
50 49 rightoldd ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ∈ Old ⁡ bday ⁡ A
51 3 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → B ∈ No
52 48 50 51 mulsproplem2 ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s B ∈ No
53 2 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A ∈ No
54 simprr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → s ∈ R ⁡ B
55 54 rightoldd ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → s ∈ Old ⁡ bday ⁡ B
56 48 53 55 mulsproplem3 ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A ⋅ s s ∈ No
57 52 56 addscld ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s B + s A ⋅ s s ∈ No
58 48 50 55 mulsproplem4 ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s s ∈ No
59 57 58 subscld ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∈ No
60 eleq1 ⊢ h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → h ∈ No ↔ r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∈ No
61 59 60 syl5ibrcom ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → h ∈ No
62 61 rexlimdvva ⊢ φ → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → h ∈ No
63 62 abssdv ⊢ φ → h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ⊆ No
64 47 63 unssd ⊢ φ → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ⊆ No
65 1 adantr ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
66 simprl ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ L ⁡ A
67 66 leftoldd ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ Old ⁡ bday ⁡ A
68 3 adantr ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → B ∈ No
69 65 67 68 mulsproplem2 ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s B ∈ No
70 2 adantr ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ∈ No
71 simprr ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ R ⁡ B
72 71 rightoldd ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ Old ⁡ bday ⁡ B
73 65 70 72 mulsproplem3 ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ⋅ s u ∈ No
74 69 73 addscld ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s B + s A ⋅ s u ∈ No
75 65 67 72 mulsproplem4 ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s u ∈ No
76 74 75 subscld ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∈ No
77 eleq1 ⊢ i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → i ∈ No ↔ t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∈ No
78 76 77 syl5ibrcom ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → i ∈ No
79 78 rexlimdvva ⊢ φ → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → i ∈ No
80 79 abssdv ⊢ φ → i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ⊆ No
81 1 adantr ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
82 simprl ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ R ⁡ A
83 82 rightoldd ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ Old ⁡ bday ⁡ A
84 3 adantr ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → B ∈ No
85 81 83 84 mulsproplem2 ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s B ∈ No
86 2 adantr ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ∈ No
87 simprr ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ L ⁡ B
88 87 leftoldd ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ Old ⁡ bday ⁡ B
89 81 86 88 mulsproplem3 ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ⋅ s w ∈ No
90 85 89 addscld ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s B + s A ⋅ s w ∈ No
91 81 83 88 mulsproplem4 ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s w ∈ No
92 90 91 subscld ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ No
93 eleq1 ⊢ j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → j ∈ No ↔ v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ No
94 92 93 syl5ibrcom ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → j ∈ No
95 94 rexlimdvva ⊢ φ → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → j ∈ No
96 95 abssdv ⊢ φ → j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ⊆ No
97 80 96 unssd ⊢ φ → i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ⊆ No
98 elun ⊢ x ∈ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ↔ x ∈ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∨ x ∈ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
99 vex ⊢ x ∈ V
100 eqeq1 ⊢ g = x → g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ↔ x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q
101 100 2rexbidv ⊢ g = x → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q
102 99 101 elab ⊢ x ∈ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q
103 eqeq1 ⊢ h = x → h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ↔ x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
104 103 2rexbidv ⊢ h = x → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ↔ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
105 99 104 elab ⊢ x ∈ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ↔ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
106 102 105 orbi12i ⊢ x ∈ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∨ x ∈ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
107 98 106 bitri ⊢ x ∈ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s
108 elun ⊢ y ∈ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ y ∈ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ y ∈ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
109 vex ⊢ y ∈ V
110 eqeq1 ⊢ i = y → i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ↔ y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u
111 110 2rexbidv ⊢ i = y → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ↔ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u
112 109 111 elab ⊢ y ∈ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ↔ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u
113 eqeq1 ⊢ j = y → j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
114 113 2rexbidv ⊢ j = y → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
115 109 114 elab ⊢ y ∈ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
116 112 115 orbi12i ⊢ y ∈ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ y ∈ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
117 108 116 bitri ⊢ y ∈ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
118 107 117 anbi12i ⊢ x ∈ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ y ∈ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
119 anddi ⊢ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
120 118 119 bitri ⊢ x ∈ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ y ∈ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ↔ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w
121 1 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
122 2 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ∈ No
123 3 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → B ∈ No
124 simprll ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → p ∈ L ⁡ A
125 simprlr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → q ∈ L ⁡ B
126 simprrl ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ L ⁡ A
127 simprrr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ R ⁡ B
128 121 122 123 124 125 126 127 mulsproplem5 ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s t ⋅ s B + s A ⋅ s u - s t ⋅ s u
129 breq2 ⊢ y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y ↔ p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s t ⋅ s B + s A ⋅ s u - s t ⋅ s u
130 128 129 syl5ibrcom ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y
131 130 anassrs ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y
132 131 rexlimdvva ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y
133 breq1 ⊢ x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → x < s y ↔ p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y
134 133 imbi2d ⊢ x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → x < s y ↔ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y
135 132 134 syl5ibrcom ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → x < s y
136 135 rexlimdvva ⊢ φ → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → x < s y
137 136 impd ⊢ φ → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → x < s y
138 1 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
139 2 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ∈ No
140 3 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → B ∈ No
141 simprll ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → p ∈ L ⁡ A
142 simprlr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → q ∈ L ⁡ B
143 simprrl ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ R ⁡ A
144 simprrr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ L ⁡ B
145 138 139 140 141 142 143 144 mulsproplem6 ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s v ⋅ s B + s A ⋅ s w - s v ⋅ s w
146 breq2 ⊢ y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y ↔ p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s v ⋅ s B + s A ⋅ s w - s v ⋅ s w
147 145 146 syl5ibrcom ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y
148 147 anassrs ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y
149 148 rexlimdvva ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y
150 133 imbi2d ⊢ x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y ↔ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → p ⋅ s B + s A ⋅ s q - s p ⋅ s q < s y
151 149 150 syl5ibrcom ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
152 151 rexlimdvva ⊢ φ → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
153 152 impd ⊢ φ → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
154 137 153 jaod ⊢ φ → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
155 1 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
156 2 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ∈ No
157 3 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → B ∈ No
158 simprll ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → r ∈ R ⁡ A
159 simprlr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → s ∈ R ⁡ B
160 simprrl ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ L ⁡ A
161 simprrr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ R ⁡ B
162 155 156 157 158 159 160 161 mulsproplem7 ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s t ⋅ s B + s A ⋅ s u - s t ⋅ s u
163 breq2 ⊢ y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y ↔ r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s t ⋅ s B + s A ⋅ s u - s t ⋅ s u
164 162 163 syl5ibrcom ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y
165 164 anassrs ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y
166 165 rexlimdvva ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y
167 breq1 ⊢ x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → x < s y ↔ r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y
168 167 imbi2d ⊢ x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → x < s y ↔ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y
169 166 168 syl5ibrcom ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → x < s y
170 169 rexlimdvva ⊢ φ → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → x < s y
171 170 impd ⊢ φ → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → x < s y
172 1 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → ∀ a ∈ No ∀ b ∈ No ∀ c ∈ No ∀ d ∈ No ∀ e ∈ No ∀ f ∈ No bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E → a ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
173 2 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ∈ No
174 3 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → B ∈ No
175 simprll ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → r ∈ R ⁡ A
176 simprlr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → s ∈ R ⁡ B
177 simprrl ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ R ⁡ A
178 simprrr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ L ⁡ B
179 172 173 174 175 176 177 178 mulsproplem8 ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s v ⋅ s B + s A ⋅ s w - s v ⋅ s w
180 breq2 ⊢ y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y ↔ r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s v ⋅ s B + s A ⋅ s w - s v ⋅ s w
181 179 180 syl5ibrcom ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y
182 181 anassrs ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y
183 182 rexlimdvva ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y
184 167 imbi2d ⊢ x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y ↔ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → r ⋅ s B + s A ⋅ s s - s r ⋅ s s < s y
185 183 184 syl5ibrcom ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
186 185 rexlimdvva ⊢ φ → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
187 186 impd ⊢ φ → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
188 171 187 jaod ⊢ φ → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
189 154 188 jaod ⊢ φ → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B x = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B y = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∨ ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B x = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B y = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
190 120 189 biimtrid ⊢ φ → x ∈ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ y ∈ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
191 190 3impib ⊢ φ ∧ x ∈ g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∧ y ∈ i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → x < s y
192 19 31 64 97 191 sltsd ⊢ φ → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∪ h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ≪ s i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∪ j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w