Proof of Theorem mulcanpi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mulclpi 10934 | . . . . . . . . . 10
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
·N 𝐵) ∈ N) | 
| 2 |  | eleq1 2828 | . . . . . . . . . 10
⊢ ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) → ((𝐴 ·N 𝐵) ∈ N ↔
(𝐴
·N 𝐶) ∈ N)) | 
| 3 | 1, 2 | imbitrid 244 | . . . . . . . . 9
⊢ ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) → ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
·N 𝐶) ∈ N)) | 
| 4 | 3 | imp 406 | . . . . . . . 8
⊢ (((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) ∧ (𝐴 ∈ N ∧ 𝐵 ∈ N)) →
(𝐴
·N 𝐶) ∈ N) | 
| 5 |  | dmmulpi 10932 | . . . . . . . . 9
⊢ dom
·N = (N ×
N) | 
| 6 |  | 0npi 10923 | . . . . . . . . 9
⊢  ¬
∅ ∈ N | 
| 7 | 5, 6 | ndmovrcl 7620 | . . . . . . . 8
⊢ ((𝐴
·N 𝐶) ∈ N → (𝐴 ∈ N ∧
𝐶 ∈
N)) | 
| 8 |  | simpr 484 | . . . . . . . 8
⊢ ((𝐴 ∈ N ∧
𝐶 ∈ N)
→ 𝐶 ∈
N) | 
| 9 | 4, 7, 8 | 3syl 18 | . . . . . . 7
⊢ (((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) ∧ (𝐴 ∈ N ∧ 𝐵 ∈ N)) →
𝐶 ∈
N) | 
| 10 |  | mulpiord 10926 | . . . . . . . . . 10
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
·N 𝐵) = (𝐴 ·o 𝐵)) | 
| 11 | 10 | adantr 480 | . . . . . . . . 9
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → (𝐴
·N 𝐵) = (𝐴 ·o 𝐵)) | 
| 12 |  | mulpiord 10926 | . . . . . . . . . 10
⊢ ((𝐴 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
·N 𝐶) = (𝐴 ·o 𝐶)) | 
| 13 | 12 | adantlr 715 | . . . . . . . . 9
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → (𝐴
·N 𝐶) = (𝐴 ·o 𝐶)) | 
| 14 | 11, 13 | eqeq12d 2752 | . . . . . . . 8
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) ↔ (𝐴 ·o 𝐵) = (𝐴 ·o 𝐶))) | 
| 15 |  | pinn 10919 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ N →
𝐴 ∈
ω) | 
| 16 |  | pinn 10919 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ N →
𝐵 ∈
ω) | 
| 17 |  | pinn 10919 | . . . . . . . . . . . . 13
⊢ (𝐶 ∈ N →
𝐶 ∈
ω) | 
| 18 |  | elni2 10918 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ N ↔
(𝐴 ∈ ω ∧
∅ ∈ 𝐴)) | 
| 19 | 18 | simprbi 496 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ N →
∅ ∈ 𝐴) | 
| 20 |  | nnmcan 8673 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ 𝐵 = 𝐶)) | 
| 21 | 20 | biimpd 229 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) → 𝐵 = 𝐶)) | 
| 22 | 19, 21 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ 𝐴 ∈ N) →
((𝐴 ·o
𝐵) = (𝐴 ·o 𝐶) → 𝐵 = 𝐶)) | 
| 23 | 22 | ex 412 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ N →
((𝐴 ·o
𝐵) = (𝐴 ·o 𝐶) → 𝐵 = 𝐶))) | 
| 24 | 15, 16, 17, 23 | syl3an 1160 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → (𝐴
∈ N → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) → 𝐵 = 𝐶))) | 
| 25 | 24 | 3exp 1119 | . . . . . . . . . . 11
⊢ (𝐴 ∈ N →
(𝐵 ∈ N
→ (𝐶 ∈
N → (𝐴
∈ N → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) → 𝐵 = 𝐶))))) | 
| 26 | 25 | com4r 94 | . . . . . . . . . 10
⊢ (𝐴 ∈ N →
(𝐴 ∈ N
→ (𝐵 ∈
N → (𝐶
∈ N → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) → 𝐵 = 𝐶))))) | 
| 27 | 26 | pm2.43i 52 | . . . . . . . . 9
⊢ (𝐴 ∈ N →
(𝐵 ∈ N
→ (𝐶 ∈
N → ((𝐴
·o 𝐵) =
(𝐴 ·o
𝐶) → 𝐵 = 𝐶)))) | 
| 28 | 27 | imp31 417 | . . . . . . . 8
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → ((𝐴
·o 𝐵) =
(𝐴 ·o
𝐶) → 𝐵 = 𝐶)) | 
| 29 | 14, 28 | sylbid 240 | . . . . . . 7
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ 𝐶 ∈
N) → ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) → 𝐵 = 𝐶)) | 
| 30 | 9, 29 | sylan2 593 | . . . . . 6
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) ∧ (𝐴 ∈ N ∧ 𝐵 ∈ N)))
→ ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) → 𝐵 = 𝐶)) | 
| 31 | 30 | exp32 420 | . . . . 5
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) → ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) → 𝐵 = 𝐶)))) | 
| 32 | 31 | imp4b 421 | . . . 4
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐴
·N 𝐵) = (𝐴 ·N 𝐶)) → (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐴
·N 𝐵) = (𝐴 ·N 𝐶)) → 𝐵 = 𝐶)) | 
| 33 | 32 | pm2.43i 52 | . . 3
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐴
·N 𝐵) = (𝐴 ·N 𝐶)) → 𝐵 = 𝐶) | 
| 34 | 33 | ex 412 | . 2
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) → 𝐵 = 𝐶)) | 
| 35 |  | oveq2 7440 | . 2
⊢ (𝐵 = 𝐶 → (𝐴 ·N 𝐵) = (𝐴 ·N 𝐶)) | 
| 36 | 34, 35 | impbid1 225 | 1
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) ↔ 𝐵 = 𝐶)) |