Proof of Theorem addcanpi
Step | Hyp | Ref
| Expression |
1 | | addclpi 10506 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
+N 𝐵) ∈ N) |
2 | | eleq1 2825 |
. . . . . . . . . 10
⊢ ((𝐴 +N
𝐵) = (𝐴 +N 𝐶) → ((𝐴 +N 𝐵) ∈ N ↔
(𝐴
+N 𝐶) ∈ N)) |
3 | 1, 2 | syl5ib 247 |
. . . . . . . . 9
⊢ ((𝐴 +N
𝐵) = (𝐴 +N 𝐶) → ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
+N 𝐶) ∈ N)) |
4 | 3 | imp 410 |
. . . . . . . 8
⊢ (((𝐴 +N
𝐵) = (𝐴 +N 𝐶) ∧ (𝐴 ∈ N ∧ 𝐵 ∈ N)) →
(𝐴
+N 𝐶) ∈ N) |
5 | | dmaddpi 10504 |
. . . . . . . . 9
⊢ dom
+N = (N ×
N) |
6 | | 0npi 10496 |
. . . . . . . . 9
⊢ ¬
∅ ∈ N |
7 | 5, 6 | ndmovrcl 7394 |
. . . . . . . 8
⊢ ((𝐴 +N
𝐶) ∈ N
→ (𝐴 ∈
N ∧ 𝐶
∈ N)) |
8 | | simpr 488 |
. . . . . . . 8
⊢ ((𝐴 ∈ N ∧
𝐶 ∈ N)
→ 𝐶 ∈
N) |
9 | 4, 7, 8 | 3syl 18 |
. . . . . . 7
⊢ (((𝐴 +N
𝐵) = (𝐴 +N 𝐶) ∧ (𝐴 ∈ N ∧ 𝐵 ∈ N)) →
𝐶 ∈
N) |
10 | | addpiord 10498 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
+N 𝐵) = (𝐴 +o 𝐵)) |
11 | 10 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → (𝐴
+N 𝐵) = (𝐴 +o 𝐵)) |
12 | | addpiord 10498 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
+N 𝐶) = (𝐴 +o 𝐶)) |
13 | 12 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → (𝐴
+N 𝐶) = (𝐴 +o 𝐶)) |
14 | 11, 13 | eqeq12d 2753 |
. . . . . . . 8
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → ((𝐴
+N 𝐵) = (𝐴 +N 𝐶) ↔ (𝐴 +o 𝐵) = (𝐴 +o 𝐶))) |
15 | | pinn 10492 |
. . . . . . . . . 10
⊢ (𝐴 ∈ N →
𝐴 ∈
ω) |
16 | | pinn 10492 |
. . . . . . . . . 10
⊢ (𝐵 ∈ N →
𝐵 ∈
ω) |
17 | | pinn 10492 |
. . . . . . . . . 10
⊢ (𝐶 ∈ N →
𝐶 ∈
ω) |
18 | | nnacan 8356 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) = (𝐴 +o 𝐶) ↔ 𝐵 = 𝐶)) |
19 | 18 | biimpd 232 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) = (𝐴 +o 𝐶) → 𝐵 = 𝐶)) |
20 | 15, 16, 17, 19 | syl3an 1162 |
. . . . . . . . 9
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → ((𝐴
+o 𝐵) = (𝐴 +o 𝐶) → 𝐵 = 𝐶)) |
21 | 20 | 3expa 1120 |
. . . . . . . 8
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → ((𝐴
+o 𝐵) = (𝐴 +o 𝐶) → 𝐵 = 𝐶)) |
22 | 14, 21 | sylbid 243 |
. . . . . . 7
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → ((𝐴
+N 𝐵) = (𝐴 +N 𝐶) → 𝐵 = 𝐶)) |
23 | 9, 22 | sylan2 596 |
. . . . . 6
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ ((𝐴
+N 𝐵) = (𝐴 +N 𝐶) ∧ (𝐴 ∈ N ∧ 𝐵 ∈ N)))
→ ((𝐴
+N 𝐵) = (𝐴 +N 𝐶) → 𝐵 = 𝐶)) |
24 | 23 | exp32 424 |
. . . . 5
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ((𝐴
+N 𝐵) = (𝐴 +N 𝐶) → ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
((𝐴
+N 𝐵) = (𝐴 +N 𝐶) → 𝐵 = 𝐶)))) |
25 | 24 | imp4b 425 |
. . . 4
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐴
+N 𝐵) = (𝐴 +N 𝐶)) → (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐴
+N 𝐵) = (𝐴 +N 𝐶)) → 𝐵 = 𝐶)) |
26 | 25 | pm2.43i 52 |
. . 3
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐴
+N 𝐵) = (𝐴 +N 𝐶)) → 𝐵 = 𝐶) |
27 | 26 | ex 416 |
. 2
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ((𝐴
+N 𝐵) = (𝐴 +N 𝐶) → 𝐵 = 𝐶)) |
28 | | oveq2 7221 |
. 2
⊢ (𝐵 = 𝐶 → (𝐴 +N 𝐵) = (𝐴 +N 𝐶)) |
29 | 27, 28 | impbid1 228 |
1
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ((𝐴
+N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶)) |