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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
renegmulnnass.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion renegmulnnass ( 𝜑 → ( ( 0 −ℝ 𝐴 ) · 𝑁 ) = ( 0 −ℝ ( 𝐴 · 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 renegmulnnass.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 renegmulnnass.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 oveq2 ⊢ ( 𝑥 = 1 → ( ( 0 −ℝ 𝐴 ) · 𝑥 ) = ( ( 0 −ℝ 𝐴 ) · 1 ) )
4 oveq2 ⊢ ( 𝑥 = 1 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 1 ) )
5 4 oveq2d ⊢ ( 𝑥 = 1 → ( 0 −ℝ ( 𝐴 · 𝑥 ) ) = ( 0 −ℝ ( 𝐴 · 1 ) ) )
6 3 5 eqeq12d ⊢ ( 𝑥 = 1 → ( ( ( 0 −ℝ 𝐴 ) · 𝑥 ) = ( 0 −ℝ ( 𝐴 · 𝑥 ) ) ↔ ( ( 0 −ℝ 𝐴 ) · 1 ) = ( 0 −ℝ ( 𝐴 · 1 ) ) ) )
7 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 0 −ℝ 𝐴 ) · 𝑥 ) = ( ( 0 −ℝ 𝐴 ) · 𝑦 ) )
8 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑦 ) )
9 8 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 0 −ℝ ( 𝐴 · 𝑥 ) ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) )
10 7 9 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 0 −ℝ 𝐴 ) · 𝑥 ) = ( 0 −ℝ ( 𝐴 · 𝑥 ) ) ↔ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) )
11 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 0 −ℝ 𝐴 ) · 𝑥 ) = ( ( 0 −ℝ 𝐴 ) · ( 𝑦 + 1 ) ) )
12 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐴 · 𝑥 ) = ( 𝐴 · ( 𝑦 + 1 ) ) )
13 12 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 0 −ℝ ( 𝐴 · 𝑥 ) ) = ( 0 −ℝ ( 𝐴 · ( 𝑦 + 1 ) ) ) )
14 11 13 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 0 −ℝ 𝐴 ) · 𝑥 ) = ( 0 −ℝ ( 𝐴 · 𝑥 ) ) ↔ ( ( 0 −ℝ 𝐴 ) · ( 𝑦 + 1 ) ) = ( 0 −ℝ ( 𝐴 · ( 𝑦 + 1 ) ) ) ) )
15 oveq2 ⊢ ( 𝑥 = 𝑁 → ( ( 0 −ℝ 𝐴 ) · 𝑥 ) = ( ( 0 −ℝ 𝐴 ) · 𝑁 ) )
16 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑁 ) )
17 16 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 0 −ℝ ( 𝐴 · 𝑥 ) ) = ( 0 −ℝ ( 𝐴 · 𝑁 ) ) )
18 15 17 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( ( 0 −ℝ 𝐴 ) · 𝑥 ) = ( 0 −ℝ ( 𝐴 · 𝑥 ) ) ↔ ( ( 0 −ℝ 𝐴 ) · 𝑁 ) = ( 0 −ℝ ( 𝐴 · 𝑁 ) ) ) )
19 rernegcl ⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℝ )
20 1 19 syl ⊢ ( 𝜑 → ( 0 −ℝ 𝐴 ) ∈ ℝ )
21 ax-1rid ⊢ ( ( 0 −ℝ 𝐴 ) ∈ ℝ → ( ( 0 −ℝ 𝐴 ) · 1 ) = ( 0 −ℝ 𝐴 ) )
22 20 21 syl ⊢ ( 𝜑 → ( ( 0 −ℝ 𝐴 ) · 1 ) = ( 0 −ℝ 𝐴 ) )
23 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
24 1 23 syl ⊢ ( 𝜑 → ( 𝐴 · 1 ) = 𝐴 )
25 24 oveq2d ⊢ ( 𝜑 → ( 0 −ℝ ( 𝐴 · 1 ) ) = ( 0 −ℝ 𝐴 ) )
26 22 25 eqtr4d ⊢ ( 𝜑 → ( ( 0 −ℝ 𝐴 ) · 1 ) = ( 0 −ℝ ( 𝐴 · 1 ) ) )
27 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) )
28 27 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ 𝐴 ) · 𝑦 ) ) = ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) )
29 0red ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → 0 ∈ ℝ )
30 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → 𝐴 ∈ ℝ )
31 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
32 31 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → 𝑦 ∈ ℝ )
33 30 32 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( 𝐴 · 𝑦 ) ∈ ℝ )
34 rernegcl ⊢ ( ( 𝐴 · 𝑦 ) ∈ ℝ → ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ∈ ℝ )
35 33 34 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ∈ ℝ )
36 readdsub ⊢ ( ( 0 ∈ ℝ ∧ ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 + ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) −ℝ 𝐴 ) = ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) )
37 29 35 30 36 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 + ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) −ℝ 𝐴 ) = ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) )
38 readdlid ⊢ ( ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ∈ ℝ → ( 0 + ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) )
39 35 38 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( 0 + ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) )
40 39 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 + ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) −ℝ 𝐴 ) = ( ( 0 −ℝ ( 𝐴 · 𝑦 ) ) −ℝ 𝐴 ) )
41 37 40 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 −ℝ 𝐴 ) + ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) = ( ( 0 −ℝ ( 𝐴 · 𝑦 ) ) −ℝ 𝐴 ) )
42 resubsub4 ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 · 𝑦 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 −ℝ ( 𝐴 · 𝑦 ) ) −ℝ 𝐴 ) = ( 0 −ℝ ( ( 𝐴 · 𝑦 ) + 𝐴 ) ) )
43 29 33 30 42 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 −ℝ ( 𝐴 · 𝑦 ) ) −ℝ 𝐴 ) = ( 0 −ℝ ( ( 𝐴 · 𝑦 ) + 𝐴 ) ) )
44 28 41 43 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ 𝐴 ) · 𝑦 ) ) = ( 0 −ℝ ( ( 𝐴 · 𝑦 ) + 𝐴 ) ) )
45 22 oveq1d ⊢ ( 𝜑 → ( ( ( 0 −ℝ 𝐴 ) · 1 ) + ( ( 0 −ℝ 𝐴 ) · 𝑦 ) ) = ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ 𝐴 ) · 𝑦 ) ) )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( ( 0 −ℝ 𝐴 ) · 1 ) + ( ( 0 −ℝ 𝐴 ) · 𝑦 ) ) = ( ( 0 −ℝ 𝐴 ) + ( ( 0 −ℝ 𝐴 ) · 𝑦 ) ) )
47 24 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) = ( ( 𝐴 · 𝑦 ) + 𝐴 ) )
48 47 oveq2d ⊢ ( 𝜑 → ( 0 −ℝ ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) ) = ( 0 −ℝ ( ( 𝐴 · 𝑦 ) + 𝐴 ) ) )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( 0 −ℝ ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) ) = ( 0 −ℝ ( ( 𝐴 · 𝑦 ) + 𝐴 ) ) )
50 44 46 49 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( ( 0 −ℝ 𝐴 ) · 1 ) + ( ( 0 −ℝ 𝐴 ) · 𝑦 ) ) = ( 0 −ℝ ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) ) )
51 nnadd1com ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) = ( 1 + 𝑦 ) )
52 51 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 0 −ℝ 𝐴 ) · ( 𝑦 + 1 ) ) = ( ( 0 −ℝ 𝐴 ) · ( 1 + 𝑦 ) ) )
53 52 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 −ℝ 𝐴 ) · ( 𝑦 + 1 ) ) = ( ( 0 −ℝ 𝐴 ) · ( 1 + 𝑦 ) ) )
54 20 recnd ⊢ ( 𝜑 → ( 0 −ℝ 𝐴 ) ∈ ℂ )
55 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( 0 −ℝ 𝐴 ) ∈ ℂ )
56 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → 1 ∈ ℂ )
57 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
58 57 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → 𝑦 ∈ ℂ )
59 55 56 58 adddid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 −ℝ 𝐴 ) · ( 1 + 𝑦 ) ) = ( ( ( 0 −ℝ 𝐴 ) · 1 ) + ( ( 0 −ℝ 𝐴 ) · 𝑦 ) ) )
60 53 59 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 −ℝ 𝐴 ) · ( 𝑦 + 1 ) ) = ( ( ( 0 −ℝ 𝐴 ) · 1 ) + ( ( 0 −ℝ 𝐴 ) · 𝑦 ) ) )
61 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
62 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → 𝐴 ∈ ℂ )
63 62 58 56 adddid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( 𝐴 · ( 𝑦 + 1 ) ) = ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) )
64 63 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( 0 −ℝ ( 𝐴 · ( 𝑦 + 1 ) ) ) = ( 0 −ℝ ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) ) )
65 50 60 64 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( ( 0 −ℝ 𝐴 ) · 𝑦 ) = ( 0 −ℝ ( 𝐴 · 𝑦 ) ) ) → ( ( 0 −ℝ 𝐴 ) · ( 𝑦 + 1 ) ) = ( 0 −ℝ ( 𝐴 · ( 𝑦 + 1 ) ) ) )
66 6 10 14 18 26 65 nnindd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( ( 0 −ℝ 𝐴 ) · 𝑁 ) = ( 0 −ℝ ( 𝐴 · 𝑁 ) ) )
67 2 66 mpdan ⊢ ( 𝜑 → ( ( 0 −ℝ 𝐴 ) · 𝑁 ) = ( 0 −ℝ ( 𝐴 · 𝑁 ) ) )