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 0no ⊢ 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 ltmulsd ⊢ 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