Metamath Proof Explorer


Theorem sn-0lt1

Description: 0lt1 without ax-mulcom . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion sn-0lt1 0 < 1

Proof

Step Hyp Ref Expression
1 ax-1ne0 1 ≠ 0
2 1re 1 ∈ ℝ
3 0re 0 ∈ ℝ
4 2 3 lttri2i ( 1 ≠ 0 ↔ ( 1 < 0 ∨ 0 < 1 ) )
5 1 4 mpbi ( 1 < 0 ∨ 0 < 1 )
6 rernegcl ( 1 ∈ ℝ → ( 0 − 1 ) ∈ ℝ )
7 2 6 mp1i ( 1 < 0 → ( 0 − 1 ) ∈ ℝ )
8 relt0neg1 ( 1 ∈ ℝ → ( 1 < 0 ↔ 0 < ( 0 − 1 ) ) )
9 2 8 ax-mp ( 1 < 0 ↔ 0 < ( 0 − 1 ) )
10 9 biimpi ( 1 < 0 → 0 < ( 0 − 1 ) )
11 7 7 10 10 mulgt0d ( 1 < 0 → 0 < ( ( 0 − 1 ) · ( 0 − 1 ) ) )
12 1red ( 1 ∈ ℝ → 1 ∈ ℝ )
13 6 12 remulneg2d ( 1 ∈ ℝ → ( ( 0 − 1 ) · ( 0 − 1 ) ) = ( 0 − ( ( 0 − 1 ) · 1 ) ) )
14 ax-1rid ( ( 0 − 1 ) ∈ ℝ → ( ( 0 − 1 ) · 1 ) = ( 0 − 1 ) )
15 6 14 syl ( 1 ∈ ℝ → ( ( 0 − 1 ) · 1 ) = ( 0 − 1 ) )
16 15 oveq2d ( 1 ∈ ℝ → ( 0 − ( ( 0 − 1 ) · 1 ) ) = ( 0 − ( 0 − 1 ) ) )
17 renegneg ( 1 ∈ ℝ → ( 0 − ( 0 − 1 ) ) = 1 )
18 13 16 17 3eqtrd ( 1 ∈ ℝ → ( ( 0 − 1 ) · ( 0 − 1 ) ) = 1 )
19 2 18 ax-mp ( ( 0 − 1 ) · ( 0 − 1 ) ) = 1
20 11 19 breqtrdi ( 1 < 0 → 0 < 1 )
21 id ( 0 < 1 → 0 < 1 )
22 20 21 jaoi ( ( 1 < 0 ∨ 0 < 1 ) → 0 < 1 )
23 5 22 ax-mp 0 < 1