Proof of Theorem addasspi
Step | Hyp | Ref
| Expression |
1 | | pinn 10378 |
. . . 4
⊢ (𝐴 ∈ N →
𝐴 ∈
ω) |
2 | | pinn 10378 |
. . . 4
⊢ (𝐵 ∈ N →
𝐵 ∈
ω) |
3 | | pinn 10378 |
. . . 4
⊢ (𝐶 ∈ N →
𝐶 ∈
ω) |
4 | | nnaass 8279 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶))) |
5 | 1, 2, 3, 4 | syl3an 1161 |
. . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → ((𝐴
+o 𝐵)
+o 𝐶) = (𝐴 +o (𝐵 +o 𝐶))) |
6 | | addclpi 10392 |
. . . . . 6
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
+N 𝐵) ∈ N) |
7 | | addpiord 10384 |
. . . . . 6
⊢ (((𝐴 +N
𝐵) ∈ N
∧ 𝐶 ∈
N) → ((𝐴
+N 𝐵) +N 𝐶) = ((𝐴 +N 𝐵) +o 𝐶)) |
8 | 6, 7 | sylan 583 |
. . . . 5
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → ((𝐴
+N 𝐵) +N 𝐶) = ((𝐴 +N 𝐵) +o 𝐶)) |
9 | | addpiord 10384 |
. . . . . . 7
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
+N 𝐵) = (𝐴 +o 𝐵)) |
10 | 9 | oveq1d 7185 |
. . . . . 6
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ((𝐴
+N 𝐵) +o 𝐶) = ((𝐴 +o 𝐵) +o 𝐶)) |
11 | 10 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → ((𝐴
+N 𝐵) +o 𝐶) = ((𝐴 +o 𝐵) +o 𝐶)) |
12 | 8, 11 | eqtrd 2773 |
. . . 4
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → ((𝐴
+N 𝐵) +N 𝐶) = ((𝐴 +o 𝐵) +o 𝐶)) |
13 | 12 | 3impa 1111 |
. . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → ((𝐴
+N 𝐵) +N 𝐶) = ((𝐴 +o 𝐵) +o 𝐶)) |
14 | | addclpi 10392 |
. . . . . 6
⊢ ((𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐵
+N 𝐶) ∈ N) |
15 | | addpiord 10384 |
. . . . . 6
⊢ ((𝐴 ∈ N ∧
(𝐵
+N 𝐶) ∈ N) → (𝐴 +N
(𝐵
+N 𝐶)) = (𝐴 +o (𝐵 +N 𝐶))) |
16 | 14, 15 | sylan2 596 |
. . . . 5
⊢ ((𝐴 ∈ N ∧
(𝐵 ∈ N
∧ 𝐶 ∈
N)) → (𝐴
+N (𝐵 +N 𝐶)) = (𝐴 +o (𝐵 +N 𝐶))) |
17 | | addpiord 10384 |
. . . . . . 7
⊢ ((𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐵
+N 𝐶) = (𝐵 +o 𝐶)) |
18 | 17 | oveq2d 7186 |
. . . . . 6
⊢ ((𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐴 +o
(𝐵
+N 𝐶)) = (𝐴 +o (𝐵 +o 𝐶))) |
19 | 18 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ N ∧
(𝐵 ∈ N
∧ 𝐶 ∈
N)) → (𝐴
+o (𝐵
+N 𝐶)) = (𝐴 +o (𝐵 +o 𝐶))) |
20 | 16, 19 | eqtrd 2773 |
. . . 4
⊢ ((𝐴 ∈ N ∧
(𝐵 ∈ N
∧ 𝐶 ∈
N)) → (𝐴
+N (𝐵 +N 𝐶)) = (𝐴 +o (𝐵 +o 𝐶))) |
21 | 20 | 3impb 1116 |
. . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → (𝐴
+N (𝐵 +N 𝐶)) = (𝐴 +o (𝐵 +o 𝐶))) |
22 | 5, 13, 21 | 3eqtr4d 2783 |
. 2
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → ((𝐴
+N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N
𝐶))) |
23 | | dmaddpi 10390 |
. . 3
⊢ dom
+N = (N ×
N) |
24 | | 0npi 10382 |
. . 3
⊢ ¬
∅ ∈ N |
25 | 23, 24 | ndmovass 7352 |
. 2
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N ∧ 𝐶
∈ N) → ((𝐴 +N 𝐵) +N
𝐶) = (𝐴 +N (𝐵 +N
𝐶))) |
26 | 22, 25 | pm2.61i 185 |
1
⊢ ((𝐴 +N
𝐵)
+N 𝐶) = (𝐴 +N (𝐵 +N
𝐶)) |