Metamath Proof Explorer

Theorem mulcanpi

Description: Multiplication cancellation law for positive integers. (Contributed by NM, 4-Feb-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulcanpi ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑵 C ↔ B = C

Proof

Step Hyp Ref Expression
1 mulclpi ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B ∈ 𝑵
2 eleq1 ⊢ A ⋅ 𝑵 B = A ⋅ 𝑵 C → A ⋅ 𝑵 B ∈ 𝑵 ↔ A ⋅ 𝑵 C ∈ 𝑵
3 1 2 imbitrid ⊢ A ⋅ 𝑵 B = A ⋅ 𝑵 C → A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 C ∈ 𝑵
4 3 imp ⊢ A ⋅ 𝑵 B = A ⋅ 𝑵 C ∧ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 C ∈ 𝑵
5 dmmulpi ⊢ dom ⁡ ⋅ 𝑵 = 𝑵 × 𝑵
6 0npi ⊢ ¬ ∅ ∈ 𝑵
7 5 6 ndmovrcl ⊢ A ⋅ 𝑵 C ∈ 𝑵 → A ∈ 𝑵 ∧ C ∈ 𝑵
8 simpr ⊢ A ∈ 𝑵 ∧ C ∈ 𝑵 → C ∈ 𝑵
9 4 7 8 3syl ⊢ A ⋅ 𝑵 B = A ⋅ 𝑵 C ∧ A ∈ 𝑵 ∧ B ∈ 𝑵 → C ∈ 𝑵
10 mulpiord ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑜 B
11 10 adantr ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑜 B
12 mulpiord ⊢ A ∈ 𝑵 ∧ C ∈ 𝑵 → A ⋅ 𝑵 C = A ⋅ 𝑜 C
13 12 adantlr ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ⋅ 𝑵 C = A ⋅ 𝑜 C
14 11 13 eqeq12d ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑵 C ↔ A ⋅ 𝑜 B = A ⋅ 𝑜 C
15 pinn ⊢ A ∈ 𝑵 → A ∈ ω
16 pinn ⊢ B ∈ 𝑵 → B ∈ ω
17 pinn ⊢ C ∈ 𝑵 → C ∈ ω
18 elni2 ⊢ A ∈ 𝑵 ↔ A ∈ ω ∧ ∅ ∈ A
19 18 simprbi ⊢ A ∈ 𝑵 → ∅ ∈ A
20 nnmcan ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ A → A ⋅ 𝑜 B = A ⋅ 𝑜 C ↔ B = C
21 20 biimpd ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ A → A ⋅ 𝑜 B = A ⋅ 𝑜 C → B = C
22 19 21 sylan2 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ A ∈ 𝑵 → A ⋅ 𝑜 B = A ⋅ 𝑜 C → B = C
23 22 ex ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ∈ 𝑵 → A ⋅ 𝑜 B = A ⋅ 𝑜 C → B = C
24 15 16 17 23 syl3an ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ∈ 𝑵 → A ⋅ 𝑜 B = A ⋅ 𝑜 C → B = C
25 24 3exp ⊢ A ∈ 𝑵 → B ∈ 𝑵 → C ∈ 𝑵 → A ∈ 𝑵 → A ⋅ 𝑜 B = A ⋅ 𝑜 C → B = C
26 25 com4r ⊢ A ∈ 𝑵 → A ∈ 𝑵 → B ∈ 𝑵 → C ∈ 𝑵 → A ⋅ 𝑜 B = A ⋅ 𝑜 C → B = C
27 26 pm2.43i ⊢ A ∈ 𝑵 → B ∈ 𝑵 → C ∈ 𝑵 → A ⋅ 𝑜 B = A ⋅ 𝑜 C → B = C
28 27 imp31 ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ⋅ 𝑜 B = A ⋅ 𝑜 C → B = C
29 14 28 sylbid ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑵 C → B = C
30 9 29 sylan2 ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ A ⋅ 𝑵 B = A ⋅ 𝑵 C ∧ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑵 C → B = C
31 30 exp32 ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑵 C → A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑵 C → B = C
32 31 imp4b ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ A ⋅ 𝑵 B = A ⋅ 𝑵 C → A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ A ⋅ 𝑵 B = A ⋅ 𝑵 C → B = C
33 32 pm2.43i ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ A ⋅ 𝑵 B = A ⋅ 𝑵 C → B = C
34 33 ex ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑵 C → B = C
35 oveq2 ⊢ B = C → A ⋅ 𝑵 B = A ⋅ 𝑵 C
36 34 35 impbid1 ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑵 C ↔ B = C