Metamath Proof Explorer

Theorem remul01

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

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( ( A x. 0 ) = 1 -> ( 2 x. ( A x. 0 ) ) = ( 2 x. 1 ) )
2 1 adantl 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> ( 2 x. ( A x. 0 ) ) = ( 2 x. 1 ) )
3 2re 
 |-  2 e. RR
4 ax-1rid 
 |-  ( 2 e. RR -> ( 2 x. 1 ) = 2 )
5 3 4 mp1i 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> ( 2 x. 1 ) = 2 )
6 2 5 eqtrd 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> ( 2 x. ( A x. 0 ) ) = 2 )
7 3 a1i 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> 2 e. RR )
8 simpl 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> A e. RR )
9 0red 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> 0 e. RR )
10 8 9 remulcld 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> ( A x. 0 ) e. RR )
11 7 10 remulcld 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> ( 2 x. ( A x. 0 ) ) e. RR )
12 sn-0ne2 
 |-  0 =/= 2
13 12 necomi 
 |-  2 =/= 0
14 13 a1i 
 |-  ( ( 2 x. ( A x. 0 ) ) = 2 -> 2 =/= 0 )
15 eqtr2 
 |-  ( ( ( 2 x. ( A x. 0 ) ) = 2 /\ ( 2 x. ( A x. 0 ) ) = 0 ) -> 2 = 0 )
16 14 15 mteqand 
 |-  ( ( 2 x. ( A x. 0 ) ) = 2 -> ( 2 x. ( A x. 0 ) ) =/= 0 )
17 ax-rrecex 
 |-  ( ( ( 2 x. ( A x. 0 ) ) e. RR /\ ( 2 x. ( A x. 0 ) ) =/= 0 ) -> E. x e. RR ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 )
18 11 16 17 syl2an 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) -> E. x e. RR ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 )
19 2cnd 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> 2 e. CC )
20 simplll 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> A e. RR )
21 0red 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> 0 e. RR )
22 20 21 remulcld 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( A x. 0 ) e. RR )
23 22 recnd 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( A x. 0 ) e. CC )
24 simprl 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> x e. RR )
25 24 recnd 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> x e. CC )
26 19 23 25 mulassd 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( ( 2 x. ( A x. 0 ) ) x. x ) = ( 2 x. ( ( A x. 0 ) x. x ) ) )
27 simprr 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 )
28 20 recnd 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> A e. CC )
29 0cnd 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> 0 e. CC )
30 28 29 25 mulassd 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( ( A x. 0 ) x. x ) = ( A x. ( 0 x. x ) ) )
31 remul02 
 |-  ( x e. RR -> ( 0 x. x ) = 0 )
32 31 ad2antrl 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( 0 x. x ) = 0 )
33 32 oveq2d 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( A x. ( 0 x. x ) ) = ( A x. 0 ) )
34 30 33 eqtrd 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( ( A x. 0 ) x. x ) = ( A x. 0 ) )
35 34 oveq2d 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( 2 x. ( ( A x. 0 ) x. x ) ) = ( 2 x. ( A x. 0 ) ) )
36 26 27 35 3eqtr3rd 
 |-  ( ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) /\ ( x e. RR /\ ( ( 2 x. ( A x. 0 ) ) x. x ) = 1 ) ) -> ( 2 x. ( A x. 0 ) ) = 1 )
37 18 36 rexlimddv 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) = 1 ) /\ ( 2 x. ( A x. 0 ) ) = 2 ) -> ( 2 x. ( A x. 0 ) ) = 1 )
38 6 37 mpdan 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> ( 2 x. ( A x. 0 ) ) = 1 )
39 sn-1ne2 
 |-  1 =/= 2
40 39 a1i 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> 1 =/= 2 )
41 38 40 eqnetrd 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> ( 2 x. ( A x. 0 ) ) =/= 2 )
42 6 41 pm2.21ddne 
 |-  ( ( A e. RR /\ ( A x. 0 ) = 1 ) -> -. ( A x. 0 ) = 1 )
43 42 ex 
 |-  ( A e. RR -> ( ( A x. 0 ) = 1 -> -. ( A x. 0 ) = 1 ) )
44 pm2.01 
 |-  ( ( ( A x. 0 ) = 1 -> -. ( A x. 0 ) = 1 ) -> -. ( A x. 0 ) = 1 )
45 44 neqned 
 |-  ( ( ( A x. 0 ) = 1 -> -. ( A x. 0 ) = 1 ) -> ( A x. 0 ) =/= 1 )
46 43 45 syl 
 |-  ( A e. RR -> ( A x. 0 ) =/= 1 )
47 id 
 |-  ( A e. RR -> A e. RR )
48 elre0re 
 |-  ( A e. RR -> 0 e. RR )
49 47 48 remulcld 
 |-  ( A e. RR -> ( A x. 0 ) e. RR )
50 ax-rrecex 
 |-  ( ( ( A x. 0 ) e. RR /\ ( A x. 0 ) =/= 0 ) -> E. x e. RR ( ( A x. 0 ) x. x ) = 1 )
51 49 50 sylan 
 |-  ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) -> E. x e. RR ( ( A x. 0 ) x. x ) = 1 )
52 simpll 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) /\ ( x e. RR /\ ( ( A x. 0 ) x. x ) = 1 ) ) -> A e. RR )
53 52 recnd 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) /\ ( x e. RR /\ ( ( A x. 0 ) x. x ) = 1 ) ) -> A e. CC )
54 0cnd 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) /\ ( x e. RR /\ ( ( A x. 0 ) x. x ) = 1 ) ) -> 0 e. CC )
55 simprl 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) /\ ( x e. RR /\ ( ( A x. 0 ) x. x ) = 1 ) ) -> x e. RR )
56 55 recnd 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) /\ ( x e. RR /\ ( ( A x. 0 ) x. x ) = 1 ) ) -> x e. CC )
57 53 54 56 mulassd 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) /\ ( x e. RR /\ ( ( A x. 0 ) x. x ) = 1 ) ) -> ( ( A x. 0 ) x. x ) = ( A x. ( 0 x. x ) ) )
58 simprr 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) /\ ( x e. RR /\ ( ( A x. 0 ) x. x ) = 1 ) ) -> ( ( A x. 0 ) x. x ) = 1 )
59 31 oveq2d 
 |-  ( x e. RR -> ( A x. ( 0 x. x ) ) = ( A x. 0 ) )
60 59 ad2antrl 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) /\ ( x e. RR /\ ( ( A x. 0 ) x. x ) = 1 ) ) -> ( A x. ( 0 x. x ) ) = ( A x. 0 ) )
61 57 58 60 3eqtr3rd 
 |-  ( ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) /\ ( x e. RR /\ ( ( A x. 0 ) x. x ) = 1 ) ) -> ( A x. 0 ) = 1 )
62 51 61 rexlimddv 
 |-  ( ( A e. RR /\ ( A x. 0 ) =/= 0 ) -> ( A x. 0 ) = 1 )
63 62 ex 
 |-  ( A e. RR -> ( ( A x. 0 ) =/= 0 -> ( A x. 0 ) = 1 ) )
64 63 necon1d 
 |-  ( A e. RR -> ( ( A x. 0 ) =/= 1 -> ( A x. 0 ) = 0 ) )
65 46 64 mpd 
 |-  ( A e. RR -> ( A x. 0 ) = 0 )