Metamath Proof Explorer


Theorem cncongrcoprm

Description: Corollary 1 of Cancellability of Congruences: Two products with a common factor are congruent modulo an integer being coprime to the common factor iff the other factors are congruent modulo the integer. (Contributed by AV, 13-Jul-2021)

Ref Expression
Assertion cncongrcoprm ( ( ( ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„• โˆง ( ๐ถ gcd ๐‘ ) = 1 ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) mod ๐‘ ) = ( ( ๐ต ยท ๐ถ ) mod ๐‘ ) โ†” ( ๐ด mod ๐‘ ) = ( ๐ต mod ๐‘ ) ) )

Proof

Step Hyp Ref Expression
1 simpl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ถ gcd ๐‘ ) = 1 ) โ†’ ๐‘ โˆˆ โ„• )
2 nncn โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚ )
3 2 div1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ / 1 ) = ๐‘ )
4 oveq2 โŠข ( ( ๐ถ gcd ๐‘ ) = 1 โ†’ ( ๐‘ / ( ๐ถ gcd ๐‘ ) ) = ( ๐‘ / 1 ) )
5 4 eqcomd โŠข ( ( ๐ถ gcd ๐‘ ) = 1 โ†’ ( ๐‘ / 1 ) = ( ๐‘ / ( ๐ถ gcd ๐‘ ) ) )
6 3 5 sylan9req โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ถ gcd ๐‘ ) = 1 ) โ†’ ๐‘ = ( ๐‘ / ( ๐ถ gcd ๐‘ ) ) )
7 1 6 jca โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ถ gcd ๐‘ ) = 1 ) โ†’ ( ๐‘ โˆˆ โ„• โˆง ๐‘ = ( ๐‘ / ( ๐ถ gcd ๐‘ ) ) ) )
8 cncongr โŠข ( ( ( ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„• โˆง ๐‘ = ( ๐‘ / ( ๐ถ gcd ๐‘ ) ) ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) mod ๐‘ ) = ( ( ๐ต ยท ๐ถ ) mod ๐‘ ) โ†” ( ๐ด mod ๐‘ ) = ( ๐ต mod ๐‘ ) ) )
9 7 8 sylan2 โŠข ( ( ( ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„• โˆง ( ๐ถ gcd ๐‘ ) = 1 ) ) โ†’ ( ( ( ๐ด ยท ๐ถ ) mod ๐‘ ) = ( ( ๐ต ยท ๐ถ ) mod ๐‘ ) โ†” ( ๐ด mod ๐‘ ) = ( ๐ต mod ๐‘ ) ) )