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 ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) = ( 𝐴 ·N 𝐶 ) ↔ 𝐵 = 𝐶 ) )

Proof

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