Metamath Proof Explorer


Theorem remulid2

Description: Commuted version of ax-1rid without ax-mulcom . (Contributed by SN, 5-Feb-2024)

Ref Expression
Assertion remulid2 A 1 A = A

Proof

Step Hyp Ref Expression
1 df-ne A 0 ¬ A = 0
2 ax-rrecex A A 0 x A x = 1
3 simpll A A 0 x A x = 1 A
4 3 recnd A A 0 x A x = 1 A
5 simprl A A 0 x A x = 1 x
6 5 recnd A A 0 x A x = 1 x
7 4 6 4 mulassd A A 0 x A x = 1 A x A = A x A
8 simprr A A 0 x A x = 1 A x = 1
9 8 oveq1d A A 0 x A x = 1 A x A = 1 A
10 3 5 8 remulinvcom A A 0 x A x = 1 x A = 1
11 10 oveq2d A A 0 x A x = 1 A x A = A 1
12 ax-1rid A A 1 = A
13 3 12 syl A A 0 x A x = 1 A 1 = A
14 11 13 eqtrd A A 0 x A x = 1 A x A = A
15 7 9 14 3eqtr3d A A 0 x A x = 1 1 A = A
16 2 15 rexlimddv A A 0 1 A = A
17 16 ex A A 0 1 A = A
18 1 17 syl5bir A ¬ A = 0 1 A = A
19 1re 1
20 remul01 1 1 0 = 0
21 19 20 mp1i A = 0 1 0 = 0
22 oveq2 A = 0 1 A = 1 0
23 id A = 0 A = 0
24 21 22 23 3eqtr4d A = 0 1 A = A
25 18 24 pm2.61d2 A 1 A = A