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 )