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 ax-mp ⊢ ( 0 −ℝ 1 ) ∈ ℝ
8 7 a1i ⊢ ( 1 < 0 → ( 0 −ℝ 1 ) ∈ ℝ )
9 relt0neg1 ⊢ ( 1 ∈ ℝ → ( 1 < 0 ↔ 0 < ( 0 −ℝ 1 ) ) )
10 2 9 ax-mp ⊢ ( 1 < 0 ↔ 0 < ( 0 −ℝ 1 ) )
11 10 biimpi ⊢ ( 1 < 0 → 0 < ( 0 −ℝ 1 ) )
12 8 8 11 11 mulgt0d ⊢ ( 1 < 0 → 0 < ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) )
13 resubdi ⊢ ( ( ( 0 −ℝ 1 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) = ( ( ( 0 −ℝ 1 ) · 0 ) −ℝ ( ( 0 −ℝ 1 ) · 1 ) ) )
14 7 3 2 13 mp3an ⊢ ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) = ( ( ( 0 −ℝ 1 ) · 0 ) −ℝ ( ( 0 −ℝ 1 ) · 1 ) )
15 remul01 ⊢ ( ( 0 −ℝ 1 ) ∈ ℝ → ( ( 0 −ℝ 1 ) · 0 ) = 0 )
16 7 15 ax-mp ⊢ ( ( 0 −ℝ 1 ) · 0 ) = 0
17 ax-1rid ⊢ ( ( 0 −ℝ 1 ) ∈ ℝ → ( ( 0 −ℝ 1 ) · 1 ) = ( 0 −ℝ 1 ) )
18 7 17 ax-mp ⊢ ( ( 0 −ℝ 1 ) · 1 ) = ( 0 −ℝ 1 )
19 16 18 oveq12i ⊢ ( ( ( 0 −ℝ 1 ) · 0 ) −ℝ ( ( 0 −ℝ 1 ) · 1 ) ) = ( 0 −ℝ ( 0 −ℝ 1 ) )
20 renegneg ⊢ ( 1 ∈ ℝ → ( 0 −ℝ ( 0 −ℝ 1 ) ) = 1 )
21 2 20 ax-mp ⊢ ( 0 −ℝ ( 0 −ℝ 1 ) ) = 1
22 14 19 21 3eqtri ⊢ ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) = 1
23 12 22 breqtrdi ⊢ ( 1 < 0 → 0 < 1 )
24 id ⊢ ( 0 < 1 → 0 < 1 )
25 23 24 jaoi ⊢ ( ( 1 < 0 ∨ 0 < 1 ) → 0 < 1 )
26 5 25 ax-mp ⊢ 0 < 1