Metamath Proof Explorer


Theorem mulsgt0

Description: The product of two positive surreals is positive. Theorem 9 of Conway p. 20. (Contributed by Scott Fenton, 6-Mar-2025)

Ref Expression
Assertion mulsgt0 A No 0 s < s A B No 0 s < s B 0 s < s A s B

Proof

Step Hyp Ref Expression
1 0sno 0 s No
2 1 a1i A No 0 s < s A B No 0 s < s B 0 s No
3 simpll A No 0 s < s A B No 0 s < s B A No
4 simprl A No 0 s < s A B No 0 s < s B B No
5 simplr A No 0 s < s A B No 0 s < s B 0 s < s A
6 simprr A No 0 s < s A B No 0 s < s B 0 s < s B
7 2 3 2 4 5 6 sltmuld A No 0 s < s A B No 0 s < s B 0 s s B - s 0 s s 0 s < s A s B - s A s 0 s
8 muls02 B No 0 s s B = 0 s
9 4 8 syl A No 0 s < s A B No 0 s < s B 0 s s B = 0 s
10 muls02 0 s No 0 s s 0 s = 0 s
11 1 10 ax-mp 0 s s 0 s = 0 s
12 11 a1i A No 0 s < s A B No 0 s < s B 0 s s 0 s = 0 s
13 9 12 oveq12d A No 0 s < s A B No 0 s < s B 0 s s B - s 0 s s 0 s = 0 s - s 0 s
14 subsid 0 s No 0 s - s 0 s = 0 s
15 1 14 ax-mp 0 s - s 0 s = 0 s
16 13 15 eqtrdi A No 0 s < s A B No 0 s < s B 0 s s B - s 0 s s 0 s = 0 s
17 muls01 A No A s 0 s = 0 s
18 3 17 syl A No 0 s < s A B No 0 s < s B A s 0 s = 0 s
19 18 oveq2d A No 0 s < s A B No 0 s < s B A s B - s A s 0 s = A s B - s 0 s
20 mulscl A No B No A s B No
21 20 ad2ant2r A No 0 s < s A B No 0 s < s B A s B No
22 subsid1 A s B No A s B - s 0 s = A s B
23 21 22 syl A No 0 s < s A B No 0 s < s B A s B - s 0 s = A s B
24 19 23 eqtrd A No 0 s < s A B No 0 s < s B A s B - s A s 0 s = A s B
25 7 16 24 3brtr3d A No 0 s < s A B No 0 s < s B 0 s < s A s B