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 leftssold ⊢ L ⁡ A ⊆ Old ⁡ bday ⁡ A
34 simprl ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ∈ L ⁡ A
35 33 34 sselid ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ∈ Old ⁡ bday ⁡ A
36 3 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → B ∈ No
37 32 35 36 mulsproplem2 ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s B ∈ No
38 2 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A ∈ No
39 leftssold ⊢ L ⁡ B ⊆ Old ⁡ bday ⁡ B
40 simprr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → q ∈ L ⁡ B
41 39 40 sselid ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → q ∈ Old ⁡ bday ⁡ B
42 32 38 41 mulsproplem3 ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → A ⋅ s q ∈ No
43 37 42 addscld ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s B + s A ⋅ s q ∈ No
44 32 35 41 mulsproplem4 ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s q ∈ No
45 43 44 subscld ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → p ⋅ s B + s A ⋅ s q - s p ⋅ s q ∈ No
46 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
47 45 46 syl5ibrcom ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B → g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → g ∈ No
48 47 rexlimdvva ⊢ φ → ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q → g ∈ No
49 48 abssdv ⊢ φ → g | ∃ p ∈ L ⁡ A ∃ q ∈ L ⁡ B g = p ⋅ s B + s A ⋅ s q - s p ⋅ s q ⊆ No
50 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
51 rightssold ⊢ R ⁡ A ⊆ Old ⁡ bday ⁡ A
52 simprl ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ∈ R ⁡ A
53 51 52 sselid ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ∈ Old ⁡ bday ⁡ A
54 3 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → B ∈ No
55 50 53 54 mulsproplem2 ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s B ∈ No
56 2 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A ∈ No
57 rightssold ⊢ R ⁡ B ⊆ Old ⁡ bday ⁡ B
58 simprr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → s ∈ R ⁡ B
59 57 58 sselid ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → s ∈ Old ⁡ bday ⁡ B
60 50 56 59 mulsproplem3 ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → A ⋅ s s ∈ No
61 55 60 addscld ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s B + s A ⋅ s s ∈ No
62 50 53 59 mulsproplem4 ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s s ∈ No
63 61 62 subscld ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → r ⋅ s B + s A ⋅ s s - s r ⋅ s s ∈ No
64 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
65 63 64 syl5ibrcom ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B → h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → h ∈ No
66 65 rexlimdvva ⊢ φ → ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s → h ∈ No
67 66 abssdv ⊢ φ → h | ∃ r ∈ R ⁡ A ∃ s ∈ R ⁡ B h = r ⋅ s B + s A ⋅ s s - s r ⋅ s s ⊆ No
68 49 67 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
69 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
70 simprl ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ L ⁡ A
71 33 70 sselid ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ Old ⁡ bday ⁡ A
72 3 adantr ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → B ∈ No
73 69 71 72 mulsproplem2 ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s B ∈ No
74 2 adantr ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ∈ No
75 simprr ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ R ⁡ B
76 57 75 sselid ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ Old ⁡ bday ⁡ B
77 69 74 76 mulsproplem3 ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ⋅ s u ∈ No
78 73 77 addscld ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s B + s A ⋅ s u ∈ No
79 69 71 76 mulsproplem4 ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s u ∈ No
80 78 79 subscld ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ⋅ s B + s A ⋅ s u - s t ⋅ s u ∈ No
81 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
82 80 81 syl5ibrcom ⊢ φ ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → i ∈ No
83 82 rexlimdvva ⊢ φ → ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u → i ∈ No
84 83 abssdv ⊢ φ → i | ∃ t ∈ L ⁡ A ∃ u ∈ R ⁡ B i = t ⋅ s B + s A ⋅ s u - s t ⋅ s u ⊆ No
85 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
86 simprl ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ R ⁡ A
87 51 86 sselid ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ Old ⁡ bday ⁡ A
88 3 adantr ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → B ∈ No
89 85 87 88 mulsproplem2 ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s B ∈ No
90 2 adantr ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ∈ No
91 simprr ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ L ⁡ B
92 39 91 sselid ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ Old ⁡ bday ⁡ B
93 85 90 92 mulsproplem3 ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ⋅ s w ∈ No
94 89 93 addscld ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s B + s A ⋅ s w ∈ No
95 85 87 92 mulsproplem4 ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s w ∈ No
96 94 95 subscld ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ⋅ s B + s A ⋅ s w - s v ⋅ s w ∈ No
97 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
98 96 97 syl5ibrcom ⊢ φ ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → j ∈ No
99 98 rexlimdvva ⊢ φ → ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w → j ∈ No
100 99 abssdv ⊢ φ → j | ∃ v ∈ R ⁡ A ∃ w ∈ L ⁡ B j = v ⋅ s B + s A ⋅ s w - s v ⋅ s w ⊆ No
101 84 100 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
102 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
103 vex ⊢ x ∈ V
104 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
105 104 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
106 103 105 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
107 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
108 107 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
109 103 108 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
110 106 109 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
111 102 110 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
112 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
113 vex ⊢ y ∈ V
114 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
115 114 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
116 113 115 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
117 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
118 117 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
119 113 118 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
120 116 119 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
121 112 120 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
122 111 121 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
123 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
124 122 123 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
125 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
126 2 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ∈ No
127 3 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → B ∈ No
128 simprll ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → p ∈ L ⁡ A
129 simprlr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → q ∈ L ⁡ B
130 simprrl ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ L ⁡ A
131 simprrr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ R ⁡ B
132 125 126 127 128 129 130 131 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
133 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
134 132 133 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
135 134 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
136 135 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
137 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
138 137 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
139 136 138 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
140 139 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
141 140 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
142 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
143 2 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ∈ No
144 3 adantr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → B ∈ No
145 simprll ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → p ∈ L ⁡ A
146 simprlr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → q ∈ L ⁡ B
147 simprrl ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ R ⁡ A
148 simprrr ⊢ φ ∧ p ∈ L ⁡ A ∧ q ∈ L ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ L ⁡ B
149 142 143 144 145 146 147 148 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
150 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
151 149 150 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
152 151 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
153 152 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
154 137 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
155 153 154 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
156 155 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
157 156 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
158 141 157 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
159 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
160 2 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → A ∈ No
161 3 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → B ∈ No
162 simprll ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → r ∈ R ⁡ A
163 simprlr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → s ∈ R ⁡ B
164 simprrl ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → t ∈ L ⁡ A
165 simprrr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ t ∈ L ⁡ A ∧ u ∈ R ⁡ B → u ∈ R ⁡ B
166 159 160 161 162 163 164 165 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
167 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
168 166 167 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
169 168 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
170 169 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
171 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
172 171 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
173 170 172 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
174 173 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
175 174 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
176 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
177 2 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → A ∈ No
178 3 adantr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → B ∈ No
179 simprll ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → r ∈ R ⁡ A
180 simprlr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → s ∈ R ⁡ B
181 simprrl ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → v ∈ R ⁡ A
182 simprrr ⊢ φ ∧ r ∈ R ⁡ A ∧ s ∈ R ⁡ B ∧ v ∈ R ⁡ A ∧ w ∈ L ⁡ B → w ∈ L ⁡ B
183 176 177 178 179 180 181 182 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
184 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
185 183 184 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
186 185 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
187 186 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
188 171 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
189 187 188 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
190 189 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
191 190 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
192 175 191 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
193 158 192 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
194 124 193 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
195 194 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
196 19 31 68 101 195 ssltd ⊢ φ → 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