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 ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → 0s <s ( 𝐴 ·s 𝐵 ) )

Proof

Step Hyp Ref Expression
1 0no ⊢ 0s ∈ No
2 1 a1i ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → 0s ∈ No )
3 simpll ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → 𝐴 ∈ No )
4 simprl ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → 𝐵 ∈ No )
5 simplr ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → 0s <s 𝐴 )
6 simprr ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → 0s <s 𝐵 )
7 2 3 2 4 5 6 ltmulsd ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( ( 0s ·s 𝐵 ) -s ( 0s ·s 0s ) ) <s ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 0s ) ) )
8 muls02 ⊢ ( 𝐵 ∈ No → ( 0s ·s 𝐵 ) = 0s )
9 4 8 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( 0s ·s 𝐵 ) = 0s )
10 muls02 ⊢ ( 0s ∈ No → ( 0s ·s 0s ) = 0s )
11 1 10 ax-mp ⊢ ( 0s ·s 0s ) = 0s
12 11 a1i ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( 0s ·s 0s ) = 0s )
13 9 12 oveq12d ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( ( 0s ·s 𝐵 ) -s ( 0s ·s 0s ) ) = ( 0s -s 0s ) )
14 subsid ⊢ ( 0s ∈ No → ( 0s -s 0s ) = 0s )
15 1 14 ax-mp ⊢ ( 0s -s 0s ) = 0s
16 13 15 eqtrdi ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( ( 0s ·s 𝐵 ) -s ( 0s ·s 0s ) ) = 0s )
17 muls01 ⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 0s ) = 0s )
18 3 17 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( 𝐴 ·s 0s ) = 0s )
19 18 oveq2d ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 0s ) ) = ( ( 𝐴 ·s 𝐵 ) -s 0s ) )
20 mulscl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ·s 𝐵 ) ∈ No )
21 20 ad2ant2r ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( 𝐴 ·s 𝐵 ) ∈ No )
22 subsid1 ⊢ ( ( 𝐴 ·s 𝐵 ) ∈ No → ( ( 𝐴 ·s 𝐵 ) -s 0s ) = ( 𝐴 ·s 𝐵 ) )
23 21 22 syl ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( ( 𝐴 ·s 𝐵 ) -s 0s ) = ( 𝐴 ·s 𝐵 ) )
24 19 23 eqtrd ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 0s ) ) = ( 𝐴 ·s 𝐵 ) )
25 7 16 24 3brtr3d ⊢ ( ( ( 𝐴 ∈ No ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ No ∧ 0s <s 𝐵 ) ) → 0s <s ( 𝐴 ·s 𝐵 ) )