Step | Hyp | Ref
| Expression |
1 | | renegmulnnass.n |
. 2
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | oveq2 7359 |
. . . 4
⊢ (𝑥 = 1 → ((0
−ℝ 𝐴) · 𝑥) = ((0 −ℝ 𝐴) · 1)) |
3 | | oveq2 7359 |
. . . . 5
⊢ (𝑥 = 1 → (𝐴 · 𝑥) = (𝐴 · 1)) |
4 | 3 | oveq2d 7367 |
. . . 4
⊢ (𝑥 = 1 → (0
−ℝ (𝐴 · 𝑥)) = (0 −ℝ (𝐴 · 1))) |
5 | 2, 4 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 1 → (((0
−ℝ 𝐴) · 𝑥) = (0 −ℝ (𝐴 · 𝑥)) ↔ ((0 −ℝ 𝐴) · 1) = (0
−ℝ (𝐴 · 1)))) |
6 | | oveq2 7359 |
. . . 4
⊢ (𝑥 = 𝑦 → ((0 −ℝ 𝐴) · 𝑥) = ((0 −ℝ 𝐴) · 𝑦)) |
7 | | oveq2 7359 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) |
8 | 7 | oveq2d 7367 |
. . . 4
⊢ (𝑥 = 𝑦 → (0 −ℝ (𝐴 · 𝑥)) = (0 −ℝ (𝐴 · 𝑦))) |
9 | 6, 8 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 𝑦 → (((0 −ℝ 𝐴) · 𝑥) = (0 −ℝ (𝐴 · 𝑥)) ↔ ((0 −ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦)))) |
10 | | oveq2 7359 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((0 −ℝ
𝐴) · 𝑥) = ((0
−ℝ 𝐴) · (𝑦 + 1))) |
11 | | oveq2 7359 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝐴 · 𝑥) = (𝐴 · (𝑦 + 1))) |
12 | 11 | oveq2d 7367 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (0 −ℝ
(𝐴 · 𝑥)) = (0
−ℝ (𝐴 · (𝑦 + 1)))) |
13 | 10, 12 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → (((0 −ℝ
𝐴) · 𝑥) = (0 −ℝ
(𝐴 · 𝑥)) ↔ ((0
−ℝ 𝐴) · (𝑦 + 1)) = (0 −ℝ (𝐴 · (𝑦 + 1))))) |
14 | | oveq2 7359 |
. . . 4
⊢ (𝑥 = 𝑁 → ((0 −ℝ 𝐴) · 𝑥) = ((0 −ℝ 𝐴) · 𝑁)) |
15 | | oveq2 7359 |
. . . . 5
⊢ (𝑥 = 𝑁 → (𝐴 · 𝑥) = (𝐴 · 𝑁)) |
16 | 15 | oveq2d 7367 |
. . . 4
⊢ (𝑥 = 𝑁 → (0 −ℝ (𝐴 · 𝑥)) = (0 −ℝ (𝐴 · 𝑁))) |
17 | 14, 16 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 𝑁 → (((0 −ℝ 𝐴) · 𝑥) = (0 −ℝ (𝐴 · 𝑥)) ↔ ((0 −ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁)))) |
18 | | renegmulnnass.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
19 | | rernegcl 40742 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0
−ℝ 𝐴) ∈ ℝ) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → (0
−ℝ 𝐴) ∈ ℝ) |
21 | | ax-1rid 11079 |
. . . . 5
⊢ ((0
−ℝ 𝐴) ∈ ℝ → ((0
−ℝ 𝐴) · 1) = (0 −ℝ
𝐴)) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ (𝜑 → ((0
−ℝ 𝐴) · 1) = (0 −ℝ
𝐴)) |
23 | | ax-1rid 11079 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) |
24 | 18, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 · 1) = 𝐴) |
25 | 24 | oveq2d 7367 |
. . . 4
⊢ (𝜑 → (0
−ℝ (𝐴 · 1)) = (0 −ℝ
𝐴)) |
26 | 22, 25 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → ((0
−ℝ 𝐴) · 1) = (0 −ℝ
(𝐴 ·
1))) |
27 | | simpr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 −ℝ
𝐴) · 𝑦) = (0 −ℝ
(𝐴 · 𝑦))) |
28 | 27 | oveq2d 7367 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 −ℝ
𝐴) + ((0
−ℝ 𝐴) · 𝑦)) = ((0 −ℝ 𝐴) + (0 −ℝ
(𝐴 · 𝑦)))) |
29 | | 0red 11116 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → 0 ∈ ℝ) |
30 | 18 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → 𝐴 ∈ ℝ) |
31 | | nnre 12118 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
32 | 31 | ad2antlr 725 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → 𝑦 ∈ ℝ) |
33 | 30, 32 | remulcld 11143 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → (𝐴 · 𝑦) ∈ ℝ) |
34 | | rernegcl 40742 |
. . . . . . . . 9
⊢ ((𝐴 · 𝑦) ∈ ℝ → (0
−ℝ (𝐴 · 𝑦)) ∈ ℝ) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → (0 −ℝ
(𝐴 · 𝑦)) ∈
ℝ) |
36 | | readdsub 40755 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ (0 −ℝ (𝐴 · 𝑦)) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((0 + (0
−ℝ (𝐴 · 𝑦))) −ℝ 𝐴) = ((0
−ℝ 𝐴) + (0 −ℝ (𝐴 · 𝑦)))) |
37 | 29, 35, 30, 36 | syl3anc 1371 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 + (0 −ℝ
(𝐴 · 𝑦))) −ℝ
𝐴) = ((0
−ℝ 𝐴) + (0 −ℝ (𝐴 · 𝑦)))) |
38 | | readdid2 40774 |
. . . . . . . . 9
⊢ ((0
−ℝ (𝐴 · 𝑦)) ∈ ℝ → (0 + (0
−ℝ (𝐴 · 𝑦))) = (0 −ℝ (𝐴 · 𝑦))) |
39 | 35, 38 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → (0 + (0 −ℝ
(𝐴 · 𝑦))) = (0
−ℝ (𝐴 · 𝑦))) |
40 | 39 | oveq1d 7366 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 + (0 −ℝ
(𝐴 · 𝑦))) −ℝ
𝐴) = ((0
−ℝ (𝐴 · 𝑦)) −ℝ 𝐴)) |
41 | 37, 40 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 −ℝ
𝐴) + (0
−ℝ (𝐴 · 𝑦))) = ((0 −ℝ (𝐴 · 𝑦)) −ℝ 𝐴)) |
42 | | resubsub4 40760 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ (𝐴
· 𝑦) ∈ ℝ
∧ 𝐴 ∈ ℝ)
→ ((0 −ℝ (𝐴 · 𝑦)) −ℝ 𝐴) = (0 −ℝ
((𝐴 · 𝑦) + 𝐴))) |
43 | 29, 33, 30, 42 | syl3anc 1371 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 −ℝ
(𝐴 · 𝑦)) −ℝ
𝐴) = (0
−ℝ ((𝐴 · 𝑦) + 𝐴))) |
44 | 28, 41, 43 | 3eqtrd 2781 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 −ℝ
𝐴) + ((0
−ℝ 𝐴) · 𝑦)) = (0 −ℝ ((𝐴 · 𝑦) + 𝐴))) |
45 | 22 | oveq1d 7366 |
. . . . . 6
⊢ (𝜑 → (((0
−ℝ 𝐴) · 1) + ((0
−ℝ 𝐴) · 𝑦)) = ((0 −ℝ 𝐴) + ((0
−ℝ 𝐴) · 𝑦))) |
46 | 45 | ad2antrr 724 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → (((0 −ℝ
𝐴) · 1) + ((0
−ℝ 𝐴) · 𝑦)) = ((0 −ℝ 𝐴) + ((0
−ℝ 𝐴) · 𝑦))) |
47 | 24 | oveq2d 7367 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 · 𝑦) + (𝐴 · 1)) = ((𝐴 · 𝑦) + 𝐴)) |
48 | 47 | oveq2d 7367 |
. . . . . 6
⊢ (𝜑 → (0
−ℝ ((𝐴 · 𝑦) + (𝐴 · 1))) = (0
−ℝ ((𝐴 · 𝑦) + 𝐴))) |
49 | 48 | ad2antrr 724 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → (0 −ℝ
((𝐴 · 𝑦) + (𝐴 · 1))) = (0
−ℝ ((𝐴 · 𝑦) + 𝐴))) |
50 | 44, 46, 49 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → (((0 −ℝ
𝐴) · 1) + ((0
−ℝ 𝐴) · 𝑦)) = (0 −ℝ ((𝐴 · 𝑦) + (𝐴 · 1)))) |
51 | | nnadd1com 40685 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) = (1 + 𝑦)) |
52 | 51 | oveq2d 7367 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → ((0
−ℝ 𝐴) · (𝑦 + 1)) = ((0 −ℝ 𝐴) · (1 + 𝑦))) |
53 | 52 | ad2antlr 725 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 −ℝ
𝐴) · (𝑦 + 1)) = ((0
−ℝ 𝐴) · (1 + 𝑦))) |
54 | 20 | recnd 11141 |
. . . . . . 7
⊢ (𝜑 → (0
−ℝ 𝐴) ∈ ℂ) |
55 | 54 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → (0 −ℝ 𝐴) ∈
ℂ) |
56 | | 1cnd 11108 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → 1 ∈ ℂ) |
57 | | nncn 12119 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
58 | 57 | ad2antlr 725 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → 𝑦 ∈ ℂ) |
59 | 55, 56, 58 | adddid 11137 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 −ℝ
𝐴) · (1 + 𝑦)) = (((0
−ℝ 𝐴) · 1) + ((0
−ℝ 𝐴) · 𝑦))) |
60 | 53, 59 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → ((0 −ℝ
𝐴) · (𝑦 + 1)) = (((0
−ℝ 𝐴) · 1) + ((0
−ℝ 𝐴) · 𝑦))) |
61 | 18 | recnd 11141 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
62 | 61 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → 𝐴 ∈ ℂ) |
63 | 62, 58, 56 | adddid 11137 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ ((0
−ℝ 𝐴) · 𝑦) = (0 −ℝ (𝐴 · 𝑦))) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + (𝐴 · 1))) |
64 | 63 | oveq2d 7367 |
. . . 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 12131 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((0
−ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁))) |
67 | 1, 66 | mpdan 685 |
1
⊢ (𝜑 → ((0
−ℝ 𝐴) · 𝑁) = (0 −ℝ (𝐴 · 𝑁))) |