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