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