ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cncongr1 GIF version

Theorem cncongr1 12106
Description: One direction of the bicondition in cncongr 12108. Theorem 5.4 in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.)
Assertion
Ref Expression
cncongr1 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (((๐ด ยท ๐ถ) mod ๐‘) = ((๐ต ยท ๐ถ) mod ๐‘) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))

Proof of Theorem cncongr1
Dummy variables ๐‘˜ ๐‘Ÿ ๐‘  are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zmulcl 9309 . . . 4 ((๐ด โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐ด ยท ๐ถ) โˆˆ โ„ค)
213adant2 1016 . . 3 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐ด ยท ๐ถ) โˆˆ โ„ค)
3 zmulcl 9309 . . . 4 ((๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐ต ยท ๐ถ) โˆˆ โ„ค)
433adant1 1015 . . 3 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐ต ยท ๐ถ) โˆˆ โ„ค)
5 simpl 109 . . 3 ((๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘))) โ†’ ๐‘ โˆˆ โ„•)
6 congr 12103 . . 3 (((๐ด ยท ๐ถ) โˆˆ โ„ค โˆง (๐ต ยท ๐ถ) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (((๐ด ยท ๐ถ) mod ๐‘) = ((๐ต ยท ๐ถ) mod ๐‘) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘) = ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ))))
72, 4, 5, 6syl2an3an 1298 . 2 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (((๐ด ยท ๐ถ) mod ๐‘) = ((๐ต ยท ๐ถ) mod ๐‘) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘) = ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ))))
8 simpl 109 . . . . . . . . . . . 12 ((๐ถ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ ๐ถ โˆˆ โ„ค)
9 nnz 9275 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ค)
10 nnne0 8950 . . . . . . . . . . . . . 14 (๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0)
119, 10jca 306 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„• โ†’ (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0))
1211adantl 277 . . . . . . . . . . . 12 ((๐ถ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0))
13 eqidd 2178 . . . . . . . . . . . 12 ((๐ถ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (๐ถ gcd ๐‘) = (๐ถ gcd ๐‘))
148, 12, 133jca 1177 . . . . . . . . . . 11 ((๐ถ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (๐ถ โˆˆ โ„ค โˆง (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง (๐ถ gcd ๐‘) = (๐ถ gcd ๐‘)))
1514ex 115 . . . . . . . . . 10 (๐ถ โˆˆ โ„ค โ†’ (๐‘ โˆˆ โ„• โ†’ (๐ถ โˆˆ โ„ค โˆง (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง (๐ถ gcd ๐‘) = (๐ถ gcd ๐‘))))
16153ad2ant3 1020 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐‘ โˆˆ โ„• โ†’ (๐ถ โˆˆ โ„ค โˆง (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง (๐ถ gcd ๐‘) = (๐ถ gcd ๐‘))))
1716com12 30 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐ถ โˆˆ โ„ค โˆง (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง (๐ถ gcd ๐‘) = (๐ถ gcd ๐‘))))
1817adantr 276 . . . . . . 7 ((๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘))) โ†’ ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐ถ โˆˆ โ„ค โˆง (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง (๐ถ gcd ๐‘) = (๐ถ gcd ๐‘))))
1918impcom 125 . . . . . 6 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (๐ถ โˆˆ โ„ค โˆง (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง (๐ถ gcd ๐‘) = (๐ถ gcd ๐‘)))
20 divgcdcoprmex 12105 . . . . . 6 ((๐ถ โˆˆ โ„ค โˆง (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง (๐ถ gcd ๐‘) = (๐ถ gcd ๐‘)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„ค โˆƒ๐‘  โˆˆ โ„ค (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1))
2119, 20syl 14 . . . . 5 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„ค โˆƒ๐‘  โˆˆ โ„ค (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1))
2221adantr 276 . . . 4 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„ค โˆƒ๐‘  โˆˆ โ„ค (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1))
23 oveq2 5886 . . . . . . . . . 10 (๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โ†’ (๐‘˜ ยท ๐‘) = (๐‘˜ ยท ((๐ถ gcd ๐‘) ยท ๐‘ )))
24233ad2ant2 1019 . . . . . . . . 9 ((๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1) โ†’ (๐‘˜ ยท ๐‘) = (๐‘˜ ยท ((๐ถ gcd ๐‘) ยท ๐‘ )))
2524adantl 277 . . . . . . . 8 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ (๐‘˜ ยท ๐‘) = (๐‘˜ ยท ((๐ถ gcd ๐‘) ยท ๐‘ )))
26 oveq2 5886 . . . . . . . . . . 11 (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โ†’ (๐ด ยท ๐ถ) = (๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)))
27 oveq2 5886 . . . . . . . . . . 11 (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โ†’ (๐ต ยท ๐ถ) = (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)))
2826, 27oveq12d 5896 . . . . . . . . . 10 (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โ†’ ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ)) = ((๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) โˆ’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ))))
29283ad2ant1 1018 . . . . . . . . 9 ((๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1) โ†’ ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ)) = ((๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) โˆ’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ))))
3029adantl 277 . . . . . . . 8 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ)) = ((๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) โˆ’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ))))
3125, 30eqeq12d 2192 . . . . . . 7 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ ((๐‘˜ ยท ๐‘) = ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ)) โ†” (๐‘˜ ยท ((๐ถ gcd ๐‘) ยท ๐‘ )) = ((๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) โˆ’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)))))
32 simpr 110 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ๐‘˜ โˆˆ โ„ค)
3332zcnd 9379 . . . . . . . . . . . . 13 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ๐‘˜ โˆˆ โ„‚)
3433adantr 276 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐‘˜ โˆˆ โ„‚)
35 simp3 999 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ ๐ถ โˆˆ โ„ค)
3635adantr 276 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ ๐ถ โˆˆ โ„ค)
379ad2antrl 490 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ ๐‘ โˆˆ โ„ค)
3836, 37gcdcld 11972 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„•0)
3938nn0cnd 9234 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„‚)
4039ad2antrr 488 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„‚)
41 simpr 110 . . . . . . . . . . . . . 14 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค) โ†’ ๐‘  โˆˆ โ„ค)
4241zcnd 9379 . . . . . . . . . . . . 13 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค) โ†’ ๐‘  โˆˆ โ„‚)
4342adantl 277 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐‘  โˆˆ โ„‚)
4434, 40, 43mul12d 8112 . . . . . . . . . . 11 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐‘˜ ยท ((๐ถ gcd ๐‘) ยท ๐‘ )) = ((๐ถ gcd ๐‘) ยท (๐‘˜ ยท ๐‘ )))
45 simp1 997 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ ๐ด โˆˆ โ„ค)
4645zcnd 9379 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ ๐ด โˆˆ โ„‚)
4746ad3antrrr 492 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐ด โˆˆ โ„‚)
4835ad2antrr 488 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ๐ถ โˆˆ โ„ค)
495nnzd 9377 . . . . . . . . . . . . . . . . . 18 ((๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘))) โ†’ ๐‘ โˆˆ โ„ค)
5049adantl 277 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ ๐‘ โˆˆ โ„ค)
5150adantr 276 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ๐‘ โˆˆ โ„ค)
5248, 51gcdcld 11972 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„•0)
5352nn0cnd 9234 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„‚)
5453adantr 276 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„‚)
55 simpl 109 . . . . . . . . . . . . . . 15 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค) โ†’ ๐‘Ÿ โˆˆ โ„ค)
5655zcnd 9379 . . . . . . . . . . . . . 14 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค) โ†’ ๐‘Ÿ โˆˆ โ„‚)
5756adantl 277 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐‘Ÿ โˆˆ โ„‚)
5847, 54, 57mul12d 8112 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) = ((๐ถ gcd ๐‘) ยท (๐ด ยท ๐‘Ÿ)))
59 simp2 998 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ ๐ต โˆˆ โ„ค)
6059zcnd 9379 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ ๐ต โˆˆ โ„‚)
6160ad3antrrr 492 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐ต โˆˆ โ„‚)
6236, 50gcdcld 11972 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„•0)
6362nn0cnd 9234 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„‚)
6463ad2antrr 488 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„‚)
6561, 64, 57mul12d 8112 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) = ((๐ถ gcd ๐‘) ยท (๐ต ยท ๐‘Ÿ)))
6658, 65oveq12d 5896 . . . . . . . . . . 11 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) โˆ’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ))) = (((๐ถ gcd ๐‘) ยท (๐ด ยท ๐‘Ÿ)) โˆ’ ((๐ถ gcd ๐‘) ยท (๐ต ยท ๐‘Ÿ))))
6744, 66eqeq12d 2192 . . . . . . . . . 10 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐‘˜ ยท ((๐ถ gcd ๐‘) ยท ๐‘ )) = ((๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) โˆ’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ))) โ†” ((๐ถ gcd ๐‘) ยท (๐‘˜ ยท ๐‘ )) = (((๐ถ gcd ๐‘) ยท (๐ด ยท ๐‘Ÿ)) โˆ’ ((๐ถ gcd ๐‘) ยท (๐ต ยท ๐‘Ÿ)))))
6845ad3antrrr 492 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐ด โˆˆ โ„ค)
6955adantl 277 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐‘Ÿ โˆˆ โ„ค)
7068, 69zmulcld 9384 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ด ยท ๐‘Ÿ) โˆˆ โ„ค)
7170zcnd 9379 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ด ยท ๐‘Ÿ) โˆˆ โ„‚)
7259ad3antrrr 492 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐ต โˆˆ โ„ค)
7372, 69zmulcld 9384 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ต ยท ๐‘Ÿ) โˆˆ โ„ค)
7473zcnd 9379 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ต ยท ๐‘Ÿ) โˆˆ โ„‚)
7564, 71, 74subdid 8374 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ถ gcd ๐‘) ยท ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ))) = (((๐ถ gcd ๐‘) ยท (๐ด ยท ๐‘Ÿ)) โˆ’ ((๐ถ gcd ๐‘) ยท (๐ต ยท ๐‘Ÿ))))
7675eqcomd 2183 . . . . . . . . . . 11 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (((๐ถ gcd ๐‘) ยท (๐ด ยท ๐‘Ÿ)) โˆ’ ((๐ถ gcd ๐‘) ยท (๐ต ยท ๐‘Ÿ))) = ((๐ถ gcd ๐‘) ยท ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ))))
7776eqeq2d 2189 . . . . . . . . . 10 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (((๐ถ gcd ๐‘) ยท (๐‘˜ ยท ๐‘ )) = (((๐ถ gcd ๐‘) ยท (๐ด ยท ๐‘Ÿ)) โˆ’ ((๐ถ gcd ๐‘) ยท (๐ต ยท ๐‘Ÿ))) โ†” ((๐ถ gcd ๐‘) ยท (๐‘˜ ยท ๐‘ )) = ((๐ถ gcd ๐‘) ยท ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)))))
7832adantr 276 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐‘˜ โˆˆ โ„ค)
79 simprr 531 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐‘  โˆˆ โ„ค)
8078, 79zmulcld 9384 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐‘˜ ยท ๐‘ ) โˆˆ โ„ค)
8180zcnd 9379 . . . . . . . . . . 11 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐‘˜ ยท ๐‘ ) โˆˆ โ„‚)
82 zmulcl 9309 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„ค โˆง ๐‘Ÿ โˆˆ โ„ค) โ†’ (๐ด ยท ๐‘Ÿ) โˆˆ โ„ค)
8382ad2ant2r 509 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ด ยท ๐‘Ÿ) โˆˆ โ„ค)
84 zmulcl 9309 . . . . . . . . . . . . . . . . . 18 ((๐ต โˆˆ โ„ค โˆง ๐‘Ÿ โˆˆ โ„ค) โ†’ (๐ต ยท ๐‘Ÿ) โˆˆ โ„ค)
8584ad2ant2lr 510 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ต ยท ๐‘Ÿ) โˆˆ โ„ค)
8683, 85zsubcld 9383 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) โˆˆ โ„ค)
8786zcnd 9379 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) โˆˆ โ„‚)
8887ex 115 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค) โ†’ ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) โˆˆ โ„‚))
89883adant3 1017 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค) โ†’ ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) โˆˆ โ„‚))
9089ad2antrr 488 . . . . . . . . . . . 12 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค) โ†’ ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) โˆˆ โ„‚))
9190imp 124 . . . . . . . . . . 11 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) โˆˆ โ„‚)
9210ad2antrl 490 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ ๐‘ โ‰  0)
93 gcd2n0cl 11973 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„•)
9436, 50, 92, 93syl3anc 1238 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„•)
9594nnne0d 8967 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (๐ถ gcd ๐‘) โ‰  0)
9695ad2antrr 488 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ถ gcd ๐‘) โ‰  0)
9752adantr 276 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„•0)
9897nn0zd 9376 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ถ gcd ๐‘) โˆˆ โ„ค)
99 0zd 9268 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ 0 โˆˆ โ„ค)
100 zapne 9330 . . . . . . . . . . . . 13 (((๐ถ gcd ๐‘) โˆˆ โ„ค โˆง 0 โˆˆ โ„ค) โ†’ ((๐ถ gcd ๐‘) # 0 โ†” (๐ถ gcd ๐‘) โ‰  0))
10198, 99, 100syl2anc 411 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ถ gcd ๐‘) # 0 โ†” (๐ถ gcd ๐‘) โ‰  0))
10296, 101mpbird 167 . . . . . . . . . . 11 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ถ gcd ๐‘) # 0)
10381, 91, 64, 102mulcanapd 8621 . . . . . . . . . 10 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (((๐ถ gcd ๐‘) ยท (๐‘˜ ยท ๐‘ )) = ((๐ถ gcd ๐‘) ยท ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ))) โ†” (๐‘˜ ยท ๐‘ ) = ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ))))
10467, 77, 1033bitrd 214 . . . . . . . . 9 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐‘˜ ยท ((๐ถ gcd ๐‘) ยท ๐‘ )) = ((๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) โˆ’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ))) โ†” (๐‘˜ ยท ๐‘ ) = ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ))))
105104adantr 276 . . . . . . . 8 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ ((๐‘˜ ยท ((๐ถ gcd ๐‘) ยท ๐‘ )) = ((๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) โˆ’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ))) โ†” (๐‘˜ ยท ๐‘ ) = ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ))))
106 zcn 9261 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„ค โ†’ ๐ด โˆˆ โ„‚)
107 zcn 9261 . . . . . . . . . . . . . . . . . 18 (๐ต โˆˆ โ„ค โ†’ ๐ต โˆˆ โ„‚)
108106, 107anim12i 338 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚))
1091083adant3 1017 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚))
110109ad2antrr 488 . . . . . . . . . . . . . . 15 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚))
111110, 56anim12i 338 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โˆง ๐‘Ÿ โˆˆ โ„‚))
112 df-3an 980 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘Ÿ โˆˆ โ„‚) โ†” ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โˆง ๐‘Ÿ โˆˆ โ„‚))
113111, 112sylibr 134 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘Ÿ โˆˆ โ„‚))
114 subdir 8346 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘Ÿ โˆˆ โ„‚) โ†’ ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) = ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)))
115113, 114syl 14 . . . . . . . . . . . 12 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) = ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)))
116115eqcomd 2183 . . . . . . . . . . 11 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ))
117116adantr 276 . . . . . . . . . 10 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ))
118117eqeq2d 2189 . . . . . . . . 9 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) โ†” (๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ)))
1195nncnd 8936 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘))) โ†’ ๐‘ โˆˆ โ„‚)
120119adantl 277 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ ๐‘ โˆˆ โ„‚)
121120ad2antrr 488 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐‘ โˆˆ โ„‚)
12279zcnd 9379 . . . . . . . . . . . . . . 15 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ๐‘  โˆˆ โ„‚)
123121, 122, 40, 102divmulap2d 8784 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐‘ / (๐ถ gcd ๐‘)) = ๐‘  โ†” ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ )))
124 simpll 527 . . . . . . . . . . . . . . . . 17 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค))
12569adantr 276 . . . . . . . . . . . . . . . . . 18 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ ๐‘Ÿ โˆˆ โ„ค)
1265adantl 277 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ ๐‘ โˆˆ โ„•)
127 divgcdnnr 11980 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ โˆˆ โ„• โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐‘ / (๐ถ gcd ๐‘)) โˆˆ โ„•)
128126, 36, 127syl2anc 411 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (๐‘ / (๐ถ gcd ๐‘)) โˆˆ โ„•)
129128ad3antrrr 492 . . . . . . . . . . . . . . . . . . 19 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ (๐‘ / (๐ถ gcd ๐‘)) โˆˆ โ„•)
130 eleq1 2240 . . . . . . . . . . . . . . . . . . . . 21 (๐‘  = (๐‘ / (๐ถ gcd ๐‘)) โ†’ (๐‘  โˆˆ โ„• โ†” (๐‘ / (๐ถ gcd ๐‘)) โˆˆ โ„•))
131130eqcoms 2180 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ / (๐ถ gcd ๐‘)) = ๐‘  โ†’ (๐‘  โˆˆ โ„• โ†” (๐‘ / (๐ถ gcd ๐‘)) โˆˆ โ„•))
132131adantl 277 . . . . . . . . . . . . . . . . . . 19 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ (๐‘  โˆˆ โ„• โ†” (๐‘ / (๐ถ gcd ๐‘)) โˆˆ โ„•))
133129, 132mpbird 167 . . . . . . . . . . . . . . . . . 18 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ ๐‘  โˆˆ โ„•)
134125, 133jca 306 . . . . . . . . . . . . . . . . 17 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))
135124, 134jca 306 . . . . . . . . . . . . . . . 16 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)))
136 simpr 110 . . . . . . . . . . . . . . . 16 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ )
137 nnz 9275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘  โˆˆ โ„• โ†’ ๐‘  โˆˆ โ„ค)
138137adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•) โ†’ ๐‘  โˆˆ โ„ค)
139138anim2i 342 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ (๐‘˜ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค))
140139adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐‘˜ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค))
141 dvdsmul2 11824 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘˜ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค) โ†’ ๐‘  โˆฅ (๐‘˜ ยท ๐‘ ))
142140, 141syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ๐‘  โˆฅ (๐‘˜ ยท ๐‘ ))
143 breq2 4009 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐‘  โˆฅ (๐‘˜ ยท ๐‘ ) โ†” ๐‘  โˆฅ ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ)))
144 zsubcl 9297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด โˆ’ ๐ต) โˆˆ โ„ค)
145144zcnd 9379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด โˆ’ ๐ต) โˆˆ โ„‚)
146145adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐ด โˆ’ ๐ต) โˆˆ โ„‚)
147 zcn 9261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘Ÿ โˆˆ โ„ค โ†’ ๐‘Ÿ โˆˆ โ„‚)
148147ad2antrl 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ ๐‘Ÿ โˆˆ โ„‚)
149148adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ๐‘Ÿ โˆˆ โ„‚)
150146, 149mulcomd 7982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) = (๐‘Ÿ ยท (๐ด โˆ’ ๐ต)))
151150breq2d 4017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐‘  โˆฅ ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†” ๐‘  โˆฅ (๐‘Ÿ ยท (๐ด โˆ’ ๐ต))))
152137anim2i 342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•) โ†’ (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค))
153 gcdcom 11977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค) โ†’ (๐‘Ÿ gcd ๐‘ ) = (๐‘  gcd ๐‘Ÿ))
154152, 153syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•) โ†’ (๐‘Ÿ gcd ๐‘ ) = (๐‘  gcd ๐‘Ÿ))
155154eqeq1d 2186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†” (๐‘  gcd ๐‘Ÿ) = 1))
156155ad2antll 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†” (๐‘  gcd ๐‘Ÿ) = 1))
157152adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค))
158157ancomd 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ (๐‘  โˆˆ โ„ค โˆง ๐‘Ÿ โˆˆ โ„ค))
159144, 158anim12i 338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐ด โˆ’ ๐ต) โˆˆ โ„ค โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘Ÿ โˆˆ โ„ค)))
160159ancomd 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐‘  โˆˆ โ„ค โˆง ๐‘Ÿ โˆˆ โ„ค) โˆง (๐ด โˆ’ ๐ต) โˆˆ โ„ค))
161 df-3an 980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((๐‘  โˆˆ โ„ค โˆง ๐‘Ÿ โˆˆ โ„ค โˆง (๐ด โˆ’ ๐ต) โˆˆ โ„ค) โ†” ((๐‘  โˆˆ โ„ค โˆง ๐‘Ÿ โˆˆ โ„ค) โˆง (๐ด โˆ’ ๐ต) โˆˆ โ„ค))
162160, 161sylibr 134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐‘  โˆˆ โ„ค โˆง ๐‘Ÿ โˆˆ โ„ค โˆง (๐ด โˆ’ ๐ต) โˆˆ โ„ค))
163 coprmdvds 12095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((๐‘  โˆˆ โ„ค โˆง ๐‘Ÿ โˆˆ โ„ค โˆง (๐ด โˆ’ ๐ต) โˆˆ โ„ค) โ†’ ((๐‘  โˆฅ (๐‘Ÿ ยท (๐ด โˆ’ ๐ต)) โˆง (๐‘  gcd ๐‘Ÿ) = 1) โ†’ ๐‘  โˆฅ (๐ด โˆ’ ๐ต)))
164162, 163syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐‘  โˆฅ (๐‘Ÿ ยท (๐ด โˆ’ ๐ต)) โˆง (๐‘  gcd ๐‘Ÿ) = 1) โ†’ ๐‘  โˆฅ (๐ด โˆ’ ๐ต)))
165 simprr 531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ ๐‘  โˆˆ โ„•)
166165anim2i 342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง ๐‘  โˆˆ โ„•))
167166ancomd 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐‘  โˆˆ โ„• โˆง (๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค)))
168 3anass 982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((๐‘  โˆˆ โ„• โˆง ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†” (๐‘  โˆˆ โ„• โˆง (๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค)))
169167, 168sylibr 134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐‘  โˆˆ โ„• โˆง ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค))
170 moddvds 11809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((๐‘  โˆˆ โ„• โˆง ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ((๐ด mod ๐‘ ) = (๐ต mod ๐‘ ) โ†” ๐‘  โˆฅ (๐ด โˆ’ ๐ต)))
171169, 170syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐ด mod ๐‘ ) = (๐ต mod ๐‘ ) โ†” ๐‘  โˆฅ (๐ด โˆ’ ๐ต)))
172164, 171sylibrd 169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐‘  โˆฅ (๐‘Ÿ ยท (๐ด โˆ’ ๐ต)) โˆง (๐‘  gcd ๐‘Ÿ) = 1) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))
173172expcomd 1441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐‘  gcd ๐‘Ÿ) = 1 โ†’ (๐‘  โˆฅ (๐‘Ÿ ยท (๐ด โˆ’ ๐ต)) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
174156, 173sylbid 150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ (๐‘  โˆฅ (๐‘Ÿ ยท (๐ด โˆ’ ๐ต)) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
175174com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐‘  โˆฅ (๐‘Ÿ ยท (๐ด โˆ’ ๐ต)) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
176151, 175sylbid 150 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐‘  โˆฅ ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
177176com3l 81 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘  โˆฅ ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
178143, 177biimtrdi 163 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐‘  โˆฅ (๐‘˜ ยท ๐‘ ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))))
179178com14 88 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ (๐‘  โˆฅ (๐‘˜ ยท ๐‘ ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))))
180142, 179mpd 13 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•))) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
181180ex 115 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ((๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))))
1821813adant3 1017 . . . . . . . . . . . . . . . . . . . . . 22 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โ†’ ((๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))))
183182adantr 276 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ ((๐‘˜ โˆˆ โ„ค โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))))
184183impl 380 . . . . . . . . . . . . . . . . . . . 20 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
185184adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
186185imp 124 . . . . . . . . . . . . . . . . . 18 (((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1) โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))
187 eqtr2 2196 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐‘ / (๐ถ gcd ๐‘)) = ๐‘€ โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ ๐‘€ = ๐‘ )
188 oveq2 5886 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘€ = ๐‘  โ†’ (๐ด mod ๐‘€) = (๐ด mod ๐‘ ))
189 oveq2 5886 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘€ = ๐‘  โ†’ (๐ต mod ๐‘€) = (๐ต mod ๐‘ ))
190188, 189eqeq12d 2192 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘€ = ๐‘  โ†’ ((๐ด mod ๐‘€) = (๐ต mod ๐‘€) โ†” (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))
191187, 190syl 14 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ / (๐ถ gcd ๐‘)) = ๐‘€ โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ ((๐ด mod ๐‘€) = (๐ต mod ๐‘€) โ†” (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))
192191ex 115 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ / (๐ถ gcd ๐‘)) = ๐‘€ โ†’ ((๐‘ / (๐ถ gcd ๐‘)) = ๐‘  โ†’ ((๐ด mod ๐‘€) = (๐ต mod ๐‘€) โ†” (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
193192eqcoms 2180 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘€ = (๐‘ / (๐ถ gcd ๐‘)) โ†’ ((๐‘ / (๐ถ gcd ๐‘)) = ๐‘  โ†’ ((๐ด mod ๐‘€) = (๐ต mod ๐‘€) โ†” (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
194193ad2antll 491 . . . . . . . . . . . . . . . . . . . . 21 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ ((๐‘ / (๐ถ gcd ๐‘)) = ๐‘  โ†’ ((๐ด mod ๐‘€) = (๐ต mod ๐‘€) โ†” (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
195194ad2antrr 488 . . . . . . . . . . . . . . . . . . . 20 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โ†’ ((๐‘ / (๐ถ gcd ๐‘)) = ๐‘  โ†’ ((๐ด mod ๐‘€) = (๐ต mod ๐‘€) โ†” (๐ด mod ๐‘ ) = (๐ต mod ๐‘ ))))
196195imp 124 . . . . . . . . . . . . . . . . . . 19 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ ((๐ด mod ๐‘€) = (๐ต mod ๐‘€) โ†” (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))
197196adantr 276 . . . . . . . . . . . . . . . . . 18 (((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1) โ†’ ((๐ด mod ๐‘€) = (๐ต mod ๐‘€) โ†” (๐ด mod ๐‘ ) = (๐ต mod ๐‘ )))
198186, 197sylibrd 169 . . . . . . . . . . . . . . . . 17 (((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1) โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))
199198ex 115 . . . . . . . . . . . . . . . 16 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„•)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€))))
200135, 136, 199syl2anc 411 . . . . . . . . . . . . . . 15 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐‘ / (๐ถ gcd ๐‘)) = ๐‘ ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€))))
201200ex 115 . . . . . . . . . . . . . 14 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐‘ / (๐ถ gcd ๐‘)) = ๐‘  โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))))
202123, 201sylbird 170 . . . . . . . . . . . . 13 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ (๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))))
203202com3l 81 . . . . . . . . . . . 12 (๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))))
204203a1i 9 . . . . . . . . . . 11 (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โ†’ (๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โ†’ ((๐‘Ÿ gcd ๐‘ ) = 1 โ†’ (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€))))))
2052043imp 1193 . . . . . . . . . 10 ((๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1) โ†’ (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€))))
206205impcom 125 . . . . . . . . 9 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด โˆ’ ๐ต) ยท ๐‘Ÿ) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))
207118, 206sylbid 150 . . . . . . . 8 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ ((๐‘˜ ยท ๐‘ ) = ((๐ด ยท ๐‘Ÿ) โˆ’ (๐ต ยท ๐‘Ÿ)) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))
208105, 207sylbid 150 . . . . . . 7 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ ((๐‘˜ ยท ((๐ถ gcd ๐‘) ยท ๐‘ )) = ((๐ด ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ)) โˆ’ (๐ต ยท ((๐ถ gcd ๐‘) ยท ๐‘Ÿ))) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))
20931, 208sylbid 150 . . . . . 6 ((((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โˆง (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1)) โ†’ ((๐‘˜ ยท ๐‘) = ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ)) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))
210209ex 115 . . . . 5 (((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โˆง (๐‘Ÿ โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค)) โ†’ ((๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1) โ†’ ((๐‘˜ ยท ๐‘) = ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ)) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€))))
211210rexlimdvva 2602 . . . 4 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„ค โˆƒ๐‘  โˆˆ โ„ค (๐ถ = ((๐ถ gcd ๐‘) ยท ๐‘Ÿ) โˆง ๐‘ = ((๐ถ gcd ๐‘) ยท ๐‘ ) โˆง (๐‘Ÿ gcd ๐‘ ) = 1) โ†’ ((๐‘˜ ยท ๐‘) = ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ)) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€))))
21222, 211mpd 13 . . 3 ((((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โˆง ๐‘˜ โˆˆ โ„ค) โ†’ ((๐‘˜ ยท ๐‘) = ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ)) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))
213212rexlimdva 2594 . 2 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค (๐‘˜ ยท ๐‘) = ((๐ด ยท ๐ถ) โˆ’ (๐ต ยท ๐ถ)) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))
2147, 213sylbid 150 1 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐ถ โˆˆ โ„ค) โˆง (๐‘ โˆˆ โ„• โˆง ๐‘€ = (๐‘ / (๐ถ gcd ๐‘)))) โ†’ (((๐ด ยท ๐ถ) mod ๐‘) = ((๐ต ยท ๐ถ) mod ๐‘) โ†’ (๐ด mod ๐‘€) = (๐ต mod ๐‘€)))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148   โ‰  wne 2347  โˆƒwrex 2456   class class class wbr 4005  (class class class)co 5878  โ„‚cc 7812  0cc0 7814  1c1 7815   ยท cmul 7819   โˆ’ cmin 8131   # cap 8541   / cdiv 8632  โ„•cn 8922  โ„•0cn0 9179  โ„คcz 9256   mod cmo 10325   โˆฅ cdvds 11797   gcd cgcd 11946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7905  ax-resscn 7906  ax-1cn 7907  ax-1re 7908  ax-icn 7909  ax-addcl 7910  ax-addrcl 7911  ax-mulcl 7912  ax-mulrcl 7913  ax-addcom 7914  ax-mulcom 7915  ax-addass 7916  ax-mulass 7917  ax-distr 7918  ax-i2m1 7919  ax-0lt1 7920  ax-1rid 7921  ax-0id 7922  ax-rnegex 7923  ax-precex 7924  ax-cnre 7925  ax-pre-ltirr 7926  ax-pre-ltwlin 7927  ax-pre-lttrn 7928  ax-pre-apti 7929  ax-pre-ltadd 7930  ax-pre-mulgt0 7931  ax-pre-mulext 7932  ax-arch 7933  ax-caucvg 7934
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-riota 5834  df-ov 5881  df-oprab 5882  df-mpo 5883  df-1st 6144  df-2nd 6145  df-recs 6309  df-frec 6395  df-sup 6986  df-pnf 7997  df-mnf 7998  df-xr 7999  df-ltxr 8000  df-le 8001  df-sub 8133  df-neg 8134  df-reap 8535  df-ap 8542  df-div 8633  df-inn 8923  df-2 8981  df-3 8982  df-4 8983  df-n0 9180  df-z 9257  df-uz 9532  df-q 9623  df-rp 9657  df-fz 10012  df-fzo 10146  df-fl 10273  df-mod 10326  df-seqfrec 10449  df-exp 10523  df-cj 10854  df-re 10855  df-im 10856  df-rsqrt 11010  df-abs 11011  df-dvds 11798  df-gcd 11947
This theorem is referenced by:  cncongr  12108
  Copyright terms: Public domain W3C validator