Metamath Proof Explorer


Theorem mulscut2

Description: Show that the cut involved in surreal multiplication is actually a cut. (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses mulscut.1 φ A No
mulscut.2 φ B No
Assertion mulscut2 φ 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 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 mulscut.1 φ A No
2 mulscut.2 φ B No
3 1 2 mulscut φ 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
4 3anass 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 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
5 3 4 sylib φ 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
6 5 simprd φ 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
7 ovex A s B V
8 7 snnz A s B
9 sslttr 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 A s B 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 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
10 8 9 mp3an3 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 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 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
11 6 10 syl φ 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 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