Metamath Proof Explorer


Theorem rei4

Description: i4 without ax-mulcom . (Contributed by SN, 27-May-2024)

Ref Expression
Assertion rei4 i i i i = 1

Proof

Step Hyp Ref Expression
1 reixi i i = 0 - 1
2 1 1 oveq12i i i i i = 0 - 1 0 - 1
3 1re 1
4 rernegcl 1 0 - 1
5 1red 1 1
6 4 5 remulneg2d 1 0 - 1 0 - 1 = 0 - 0 - 1 1
7 ax-1rid 0 - 1 0 - 1 1 = 0 - 1
8 4 7 syl 1 0 - 1 1 = 0 - 1
9 8 oveq2d 1 0 - 0 - 1 1 = 0 - 0 - 1
10 renegneg 1 0 - 0 - 1 = 1
11 6 9 10 3eqtrd 1 0 - 1 0 - 1 = 1
12 3 11 ax-mp 0 - 1 0 - 1 = 1
13 2 12 eqtri i i i i = 1