Metamath Proof Explorer

Theorem remul02

Description: Real number version of mul02 proven without ax-mulcom . (Contributed by SN, 23-Jan-2024)

Ref Expression
Assertion remul02 
|- ( A e. RR -> ( 0 x. A ) = 0 )

Proof

Step Hyp Ref Expression
1 sn-1ne2 
 |-  1 =/= 2
2 elre0re 
 |-  ( A e. RR -> 0 e. RR )
3 id 
 |-  ( A e. RR -> A e. RR )
4 2 3 remulcld 
 |-  ( A e. RR -> ( 0 x. A ) e. RR )
5 ax-rrecex 
 |-  ( ( ( 0 x. A ) e. RR /\ ( 0 x. A ) =/= 0 ) -> E. x e. RR ( ( 0 x. A ) x. x ) = 1 )
6 4 5 sylan 
 |-  ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) -> E. x e. RR ( ( 0 x. A ) x. x ) = 1 )
7 simprr 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( ( 0 x. A ) x. x ) = 1 )
8 df-2 
 |-  2 = ( 1 + 1 )
9 8 oveq1i 
 |-  ( 2 x. 0 ) = ( ( 1 + 1 ) x. 0 )
10 re0m0e0 
 |-  ( 0 -R 0 ) = 0
11 10 eqcomi 
 |-  0 = ( 0 -R 0 )
12 11 oveq2i 
 |-  ( ( 1 + 1 ) x. 0 ) = ( ( 1 + 1 ) x. ( 0 -R 0 ) )
13 1re 
 |-  1 e. RR
14 13 13 readdcli 
 |-  ( 1 + 1 ) e. RR
15 sn-00idlem1 
 |-  ( ( 1 + 1 ) e. RR -> ( ( 1 + 1 ) x. ( 0 -R 0 ) ) = ( ( 1 + 1 ) -R ( 1 + 1 ) ) )
16 14 15 ax-mp 
 |-  ( ( 1 + 1 ) x. ( 0 -R 0 ) ) = ( ( 1 + 1 ) -R ( 1 + 1 ) )
17 repnpcan 
 |-  ( ( 1 e. RR /\ 1 e. RR /\ 1 e. RR ) -> ( ( 1 + 1 ) -R ( 1 + 1 ) ) = ( 1 -R 1 ) )
18 13 13 13 17 mp3an 
 |-  ( ( 1 + 1 ) -R ( 1 + 1 ) ) = ( 1 -R 1 )
19 re1m1e0m0 
 |-  ( 1 -R 1 ) = ( 0 -R 0 )
20 18 19 10 3eqtri 
 |-  ( ( 1 + 1 ) -R ( 1 + 1 ) ) = 0
21 12 16 20 3eqtri 
 |-  ( ( 1 + 1 ) x. 0 ) = 0
22 9 21 eqtr2i 
 |-  0 = ( 2 x. 0 )
23 22 oveq1i 
 |-  ( 0 x. A ) = ( ( 2 x. 0 ) x. A )
24 23 oveq1i 
 |-  ( ( 0 x. A ) x. x ) = ( ( ( 2 x. 0 ) x. A ) x. x )
25 24 a1i 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( ( 0 x. A ) x. x ) = ( ( ( 2 x. 0 ) x. A ) x. x ) )
26 2cnd 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> 2 e. CC )
27 0cnd 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> 0 e. CC )
28 simpll 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> A e. RR )
29 28 recnd 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> A e. CC )
30 26 27 29 mulassd 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( ( 2 x. 0 ) x. A ) = ( 2 x. ( 0 x. A ) ) )
31 30 oveq1d 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( ( ( 2 x. 0 ) x. A ) x. x ) = ( ( 2 x. ( 0 x. A ) ) x. x ) )
32 4 ad2antrr 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( 0 x. A ) e. RR )
33 32 recnd 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( 0 x. A ) e. CC )
34 simprl 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> x e. RR )
35 34 recnd 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> x e. CC )
36 26 33 35 mulassd 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( ( 2 x. ( 0 x. A ) ) x. x ) = ( 2 x. ( ( 0 x. A ) x. x ) ) )
37 25 31 36 3eqtrd 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( ( 0 x. A ) x. x ) = ( 2 x. ( ( 0 x. A ) x. x ) ) )
38 7 oveq2d 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( 2 x. ( ( 0 x. A ) x. x ) ) = ( 2 x. 1 ) )
39 2re 
 |-  2 e. RR
40 ax-1rid 
 |-  ( 2 e. RR -> ( 2 x. 1 ) = 2 )
41 39 40 mp1i 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( 2 x. 1 ) = 2 )
42 37 38 41 3eqtrd 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> ( ( 0 x. A ) x. x ) = 2 )
43 7 42 eqtr3d 
 |-  ( ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) /\ ( x e. RR /\ ( ( 0 x. A ) x. x ) = 1 ) ) -> 1 = 2 )
44 6 43 rexlimddv 
 |-  ( ( A e. RR /\ ( 0 x. A ) =/= 0 ) -> 1 = 2 )
45 44 ex 
 |-  ( A e. RR -> ( ( 0 x. A ) =/= 0 -> 1 = 2 ) )
46 45 necon1d 
 |-  ( A e. RR -> ( 1 =/= 2 -> ( 0 x. A ) = 0 ) )
47 1 46 mpi 
 |-  ( A e. RR -> ( 0 x. A ) = 0 )