This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem renegmulnnass

Description: Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025)

Ref Expression
Hypotheses renegmulnnass.a 
|- ( ph -> A e. RR )
renegmulnnass.n 
|- ( ph -> N e. NN )
Assertion renegmulnnass 
|- ( ph -> ( ( 0 -R A ) x. N ) = ( 0 -R ( A x. N ) ) )

Proof

Step Hyp Ref Expression
1 renegmulnnass.a 
 |-  ( ph -> A e. RR )
2 renegmulnnass.n 
 |-  ( ph -> N e. NN )
3 oveq2 
 |-  ( x = 1 -> ( ( 0 -R A ) x. x ) = ( ( 0 -R A ) x. 1 ) )
4 oveq2 
 |-  ( x = 1 -> ( A x. x ) = ( A x. 1 ) )
5 4 oveq2d 
 |-  ( x = 1 -> ( 0 -R ( A x. x ) ) = ( 0 -R ( A x. 1 ) ) )
6 3 5 eqeq12d 
 |-  ( x = 1 -> ( ( ( 0 -R A ) x. x ) = ( 0 -R ( A x. x ) ) <-> ( ( 0 -R A ) x. 1 ) = ( 0 -R ( A x. 1 ) ) ) )
7 oveq2 
 |-  ( x = y -> ( ( 0 -R A ) x. x ) = ( ( 0 -R A ) x. y ) )
8 oveq2 
 |-  ( x = y -> ( A x. x ) = ( A x. y ) )
9 8 oveq2d 
 |-  ( x = y -> ( 0 -R ( A x. x ) ) = ( 0 -R ( A x. y ) ) )
10 7 9 eqeq12d 
 |-  ( x = y -> ( ( ( 0 -R A ) x. x ) = ( 0 -R ( A x. x ) ) <-> ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) )
11 oveq2 
 |-  ( x = ( y + 1 ) -> ( ( 0 -R A ) x. x ) = ( ( 0 -R A ) x. ( y + 1 ) ) )
12 oveq2 
 |-  ( x = ( y + 1 ) -> ( A x. x ) = ( A x. ( y + 1 ) ) )
13 12 oveq2d 
 |-  ( x = ( y + 1 ) -> ( 0 -R ( A x. x ) ) = ( 0 -R ( A x. ( y + 1 ) ) ) )
14 11 13 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( ( 0 -R A ) x. x ) = ( 0 -R ( A x. x ) ) <-> ( ( 0 -R A ) x. ( y + 1 ) ) = ( 0 -R ( A x. ( y + 1 ) ) ) ) )
15 oveq2 
 |-  ( x = N -> ( ( 0 -R A ) x. x ) = ( ( 0 -R A ) x. N ) )
16 oveq2 
 |-  ( x = N -> ( A x. x ) = ( A x. N ) )
17 16 oveq2d 
 |-  ( x = N -> ( 0 -R ( A x. x ) ) = ( 0 -R ( A x. N ) ) )
18 15 17 eqeq12d 
 |-  ( x = N -> ( ( ( 0 -R A ) x. x ) = ( 0 -R ( A x. x ) ) <-> ( ( 0 -R A ) x. N ) = ( 0 -R ( A x. N ) ) ) )
19 rernegcl 
 |-  ( A e. RR -> ( 0 -R A ) e. RR )
20 1 19 syl 
 |-  ( ph -> ( 0 -R A ) e. RR )
21 ax-1rid 
 |-  ( ( 0 -R A ) e. RR -> ( ( 0 -R A ) x. 1 ) = ( 0 -R A ) )
22 20 21 syl 
 |-  ( ph -> ( ( 0 -R A ) x. 1 ) = ( 0 -R A ) )
23 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
24 1 23 syl 
 |-  ( ph -> ( A x. 1 ) = A )
25 24 oveq2d 
 |-  ( ph -> ( 0 -R ( A x. 1 ) ) = ( 0 -R A ) )
26 22 25 eqtr4d 
 |-  ( ph -> ( ( 0 -R A ) x. 1 ) = ( 0 -R ( A x. 1 ) ) )
27 simpr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) )
28 27 oveq2d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 -R A ) + ( ( 0 -R A ) x. y ) ) = ( ( 0 -R A ) + ( 0 -R ( A x. y ) ) ) )
29 0red 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> 0 e. RR )
30 1 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> A e. RR )
31 nnre 
 |-  ( y e. NN -> y e. RR )
32 31 ad2antlr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> y e. RR )
33 30 32 remulcld 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( A x. y ) e. RR )
34 rernegcl 
 |-  ( ( A x. y ) e. RR -> ( 0 -R ( A x. y ) ) e. RR )
35 33 34 syl 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( 0 -R ( A x. y ) ) e. RR )
36 readdsub 
 |-  ( ( 0 e. RR /\ ( 0 -R ( A x. y ) ) e. RR /\ A e. RR ) -> ( ( 0 + ( 0 -R ( A x. y ) ) ) -R A ) = ( ( 0 -R A ) + ( 0 -R ( A x. y ) ) ) )
37 29 35 30 36 syl3anc 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 + ( 0 -R ( A x. y ) ) ) -R A ) = ( ( 0 -R A ) + ( 0 -R ( A x. y ) ) ) )
38 readdlid 
 |-  ( ( 0 -R ( A x. y ) ) e. RR -> ( 0 + ( 0 -R ( A x. y ) ) ) = ( 0 -R ( A x. y ) ) )
39 35 38 syl 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( 0 + ( 0 -R ( A x. y ) ) ) = ( 0 -R ( A x. y ) ) )
40 39 oveq1d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 + ( 0 -R ( A x. y ) ) ) -R A ) = ( ( 0 -R ( A x. y ) ) -R A ) )
41 37 40 eqtr3d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 -R A ) + ( 0 -R ( A x. y ) ) ) = ( ( 0 -R ( A x. y ) ) -R A ) )
42 resubsub4 
 |-  ( ( 0 e. RR /\ ( A x. y ) e. RR /\ A e. RR ) -> ( ( 0 -R ( A x. y ) ) -R A ) = ( 0 -R ( ( A x. y ) + A ) ) )
43 29 33 30 42 syl3anc 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 -R ( A x. y ) ) -R A ) = ( 0 -R ( ( A x. y ) + A ) ) )
44 28 41 43 3eqtrd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 -R A ) + ( ( 0 -R A ) x. y ) ) = ( 0 -R ( ( A x. y ) + A ) ) )
45 22 oveq1d 
 |-  ( ph -> ( ( ( 0 -R A ) x. 1 ) + ( ( 0 -R A ) x. y ) ) = ( ( 0 -R A ) + ( ( 0 -R A ) x. y ) ) )
46 45 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( ( 0 -R A ) x. 1 ) + ( ( 0 -R A ) x. y ) ) = ( ( 0 -R A ) + ( ( 0 -R A ) x. y ) ) )
47 24 oveq2d 
 |-  ( ph -> ( ( A x. y ) + ( A x. 1 ) ) = ( ( A x. y ) + A ) )
48 47 oveq2d 
 |-  ( ph -> ( 0 -R ( ( A x. y ) + ( A x. 1 ) ) ) = ( 0 -R ( ( A x. y ) + A ) ) )
49 48 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( 0 -R ( ( A x. y ) + ( A x. 1 ) ) ) = ( 0 -R ( ( A x. y ) + A ) ) )
50 44 46 49 3eqtr4d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( ( 0 -R A ) x. 1 ) + ( ( 0 -R A ) x. y ) ) = ( 0 -R ( ( A x. y ) + ( A x. 1 ) ) ) )
51 nnadd1com 
 |-  ( y e. NN -> ( y + 1 ) = ( 1 + y ) )
52 51 oveq2d 
 |-  ( y e. NN -> ( ( 0 -R A ) x. ( y + 1 ) ) = ( ( 0 -R A ) x. ( 1 + y ) ) )
53 52 ad2antlr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 -R A ) x. ( y + 1 ) ) = ( ( 0 -R A ) x. ( 1 + y ) ) )
54 20 recnd 
 |-  ( ph -> ( 0 -R A ) e. CC )
55 54 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( 0 -R A ) e. CC )
56 1cnd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> 1 e. CC )
57 nncn 
 |-  ( y e. NN -> y e. CC )
58 57 ad2antlr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> y e. CC )
59 55 56 58 adddid 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 -R A ) x. ( 1 + y ) ) = ( ( ( 0 -R A ) x. 1 ) + ( ( 0 -R A ) x. y ) ) )
60 53 59 eqtrd 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 -R A ) x. ( y + 1 ) ) = ( ( ( 0 -R A ) x. 1 ) + ( ( 0 -R A ) x. y ) ) )
61 1 recnd 
 |-  ( ph -> A e. CC )
62 61 ad2antrr 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> A e. CC )
63 62 58 56 adddid 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( A x. ( y + 1 ) ) = ( ( A x. y ) + ( A x. 1 ) ) )
64 63 oveq2d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( 0 -R ( A x. ( y + 1 ) ) ) = ( 0 -R ( ( A x. y ) + ( A x. 1 ) ) ) )
65 50 60 64 3eqtr4d 
 |-  ( ( ( ph /\ y e. NN ) /\ ( ( 0 -R A ) x. y ) = ( 0 -R ( A x. y ) ) ) -> ( ( 0 -R A ) x. ( y + 1 ) ) = ( 0 -R ( A x. ( y + 1 ) ) ) )
66 6 10 14 18 26 65 nnindd 
 |-  ( ( ph /\ N e. NN ) -> ( ( 0 -R A ) x. N ) = ( 0 -R ( A x. N ) ) )
67 2 66 mpdan 
 |-  ( ph -> ( ( 0 -R A ) x. N ) = ( 0 -R ( A x. N ) ) )