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