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

Theorem bezoutlemnewy 12016
Description: Lemma for Bรฉzout's identity. The is-bezout predicate holds for (๐‘ฆ mod ๐‘Š). (Contributed by Jim Kingdon, 6-Jan-2022.)
Hypotheses
Ref Expression
bezoutlemstep.is-bezout (๐œ‘ โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
bezoutlemstep.a (๐œƒ โ†’ ๐ด โˆˆ โ„•0)
bezoutlemstep.b (๐œƒ โ†’ ๐ต โˆˆ โ„•0)
bezoutlemstep.w (๐œƒ โ†’ ๐‘Š โˆˆ โ„•)
bezoutlemstep.y-is-bezout (๐œƒ โ†’ [๐‘ฆ / ๐‘Ÿ]๐œ‘)
bezoutlemstep.y-nn0 (๐œƒ โ†’ ๐‘ฆ โˆˆ โ„•0)
bezoutlemstep.w-is-bezout (๐œƒ โ†’ [๐‘Š / ๐‘Ÿ]๐œ‘)
Assertion
Ref Expression
bezoutlemnewy (๐œƒ โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘)
Distinct variable groups:   ๐ด,๐‘ ,๐‘Ÿ,๐‘ก   ๐ต,๐‘ ,๐‘Ÿ,๐‘ก   ๐‘Š,๐‘ ,๐‘Ÿ,๐‘ก   ๐‘ฆ,๐‘ ,๐‘ก   ๐œ‘,๐‘ ,๐‘ก   ๐œƒ,๐‘ ,๐‘ก   ๐‘ฆ,๐‘Ÿ
Allowed substitution hints:   ๐œ‘(๐‘ฆ,๐‘Ÿ)   ๐œƒ(๐‘ฆ,๐‘Ÿ)   ๐ด(๐‘ฆ)   ๐ต(๐‘ฆ)   ๐‘Š(๐‘ฆ)

Proof of Theorem bezoutlemnewy
Dummy variables ๐‘— ๐‘˜ ๐‘ž ๐‘ข ๐‘ฃ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bezoutlemstep.w-is-bezout . . 3 (๐œƒ โ†’ [๐‘Š / ๐‘Ÿ]๐œ‘)
2 bezoutlemstep.is-bezout . . . . 5 (๐œ‘ โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
32sbcbii 3037 . . . 4 ([๐‘Š / ๐‘Ÿ]๐œ‘ โ†” [๐‘Š / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
4 bezoutlemstep.w . . . . 5 (๐œƒ โ†’ ๐‘Š โˆˆ โ„•)
5 eqeq1 2196 . . . . . . 7 (๐‘Ÿ = ๐‘Š โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
652rexbidv 2515 . . . . . 6 (๐‘Ÿ = ๐‘Š โ†’ (โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
76sbcieg 3010 . . . . 5 (๐‘Š โˆˆ โ„• โ†’ ([๐‘Š / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
84, 7syl 14 . . . 4 (๐œƒ โ†’ ([๐‘Š / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
93, 8bitrid 192 . . 3 (๐œƒ โ†’ ([๐‘Š / ๐‘Ÿ]๐œ‘ โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
101, 9mpbid 147 . 2 (๐œƒ โ†’ โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
11 bezoutlemstep.y-is-bezout . . . . . . 7 (๐œƒ โ†’ [๐‘ฆ / ๐‘Ÿ]๐œ‘)
12 oveq2 5899 . . . . . . . . . . . . 13 (๐‘  = ๐‘ข โ†’ (๐ด ยท ๐‘ ) = (๐ด ยท ๐‘ข))
1312oveq1d 5906 . . . . . . . . . . . 12 (๐‘  = ๐‘ข โ†’ ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ก)))
1413eqeq2d 2201 . . . . . . . . . . 11 (๐‘  = ๐‘ข โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ก))))
15 oveq2 5899 . . . . . . . . . . . . 13 (๐‘ก = ๐‘ฃ โ†’ (๐ต ยท ๐‘ก) = (๐ต ยท ๐‘ฃ))
1615oveq2d 5907 . . . . . . . . . . . 12 (๐‘ก = ๐‘ฃ โ†’ ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ก)) = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
1716eqeq2d 2201 . . . . . . . . . . 11 (๐‘ก = ๐‘ฃ โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ก)) โ†” ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
1814, 17cbvrex2v 2732 . . . . . . . . . 10 (โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
192, 18bitri 184 . . . . . . . . 9 (๐œ‘ โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
2019sbbii 1776 . . . . . . . 8 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†” [๐‘ฆ / ๐‘Ÿ]โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
21 nfv 1539 . . . . . . . . 9 โ„ฒ๐‘Ÿโˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))
22 eqeq1 2196 . . . . . . . . . 10 (๐‘Ÿ = ๐‘ฆ โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†” ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
23222rexbidv 2515 . . . . . . . . 9 (๐‘Ÿ = ๐‘ฆ โ†’ (โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
2421, 23sbie 1802 . . . . . . . 8 ([๐‘ฆ / ๐‘Ÿ]โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
2520, 24bitri 184 . . . . . . 7 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
2611, 25sylib 122 . . . . . 6 (๐œƒ โ†’ โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
2726ad2antrr 488 . . . . 5 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
28 bezoutlemstep.y-nn0 . . . . . . . . . . 11 (๐œƒ โ†’ ๐‘ฆ โˆˆ โ„•0)
2928ad4antr 494 . . . . . . . . . 10 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘ฆ โˆˆ โ„•0)
3029nn0zd 9392 . . . . . . . . 9 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘ฆ โˆˆ โ„ค)
314ad4antr 494 . . . . . . . . 9 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘Š โˆˆ โ„•)
3230, 31zmodcld 10364 . . . . . . . . 9 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„•0)
33 zq 9645 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„ค โ†’ ๐‘ฆ โˆˆ โ„š)
3430, 33syl 14 . . . . . . . . . 10 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘ฆ โˆˆ โ„š)
3531nnzd 9393 . . . . . . . . . . 11 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘Š โˆˆ โ„ค)
36 zq 9645 . . . . . . . . . . 11 (๐‘Š โˆˆ โ„ค โ†’ ๐‘Š โˆˆ โ„š)
3735, 36syl 14 . . . . . . . . . 10 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘Š โˆˆ โ„š)
3831nngt0d 8982 . . . . . . . . . 10 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ 0 < ๐‘Š)
39 modqlt 10352 . . . . . . . . . 10 ((๐‘ฆ โˆˆ โ„š โˆง ๐‘Š โˆˆ โ„š โˆง 0 < ๐‘Š) โ†’ (๐‘ฆ mod ๐‘Š) < ๐‘Š)
4034, 37, 38, 39syl3anc 1249 . . . . . . . . 9 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ (๐‘ฆ mod ๐‘Š) < ๐‘Š)
41 eqid 2189 . . . . . . . . . 10 (๐‘ฆ mod ๐‘Š) = (๐‘ฆ mod ๐‘Š)
42 modremain 11953 . . . . . . . . . 10 ((๐‘ฆ โˆˆ โ„ค โˆง ๐‘Š โˆˆ โ„• โˆง ((๐‘ฆ mod ๐‘Š) โˆˆ โ„•0 โˆง (๐‘ฆ mod ๐‘Š) < ๐‘Š)) โ†’ ((๐‘ฆ mod ๐‘Š) = (๐‘ฆ mod ๐‘Š) โ†” โˆƒ๐‘ž โˆˆ โ„ค ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ))
4341, 42mpbii 148 . . . . . . . . 9 ((๐‘ฆ โˆˆ โ„ค โˆง ๐‘Š โˆˆ โ„• โˆง ((๐‘ฆ mod ๐‘Š) โˆˆ โ„•0 โˆง (๐‘ฆ mod ๐‘Š) < ๐‘Š)) โ†’ โˆƒ๐‘ž โˆˆ โ„ค ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)
4430, 31, 32, 40, 43syl112anc 1253 . . . . . . . 8 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ โˆƒ๐‘ž โˆˆ โ„ค ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)
45 simprl 529 . . . . . . . . . . . . . 14 ((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โ†’ ๐‘ข โˆˆ โ„ค)
4645ad2antrr 488 . . . . . . . . . . . . 13 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ข โˆˆ โ„ค)
47 simprl 529 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ž โˆˆ โ„ค)
48 simplrl 535 . . . . . . . . . . . . . . 15 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ ๐‘  โˆˆ โ„ค)
4948ad3antrrr 492 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘  โˆˆ โ„ค)
5047, 49zmulcld 9400 . . . . . . . . . . . . 13 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘ ) โˆˆ โ„ค)
5146, 50zsubcld 9399 . . . . . . . . . . . 12 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โˆˆ โ„ค)
52 simprr 531 . . . . . . . . . . . . . . 15 ((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โ†’ ๐‘ฃ โˆˆ โ„ค)
5352ad2antrr 488 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฃ โˆˆ โ„ค)
54 simplrr 536 . . . . . . . . . . . . . . . 16 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ ๐‘ก โˆˆ โ„ค)
5554ad3antrrr 492 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ก โˆˆ โ„ค)
5647, 55zmulcld 9400 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘ก) โˆˆ โ„ค)
5753, 56zsubcld 9399 . . . . . . . . . . . . 13 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โˆˆ โ„ค)
58 simplr 528 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
59 simpr 110 . . . . . . . . . . . . . . . . . . 19 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
6059ad3antrrr 492 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
6160oveq2d 5907 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘Š) = (๐‘ž ยท ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
6247zcnd 9395 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ž โˆˆ โ„‚)
63 bezoutlemstep.a . . . . . . . . . . . . . . . . . . . . 21 (๐œƒ โ†’ ๐ด โˆˆ โ„•0)
6463ad5antr 496 . . . . . . . . . . . . . . . . . . . 20 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐ด โˆˆ โ„•0)
6564nn0cnd 9250 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐ด โˆˆ โ„‚)
6649zcnd 9395 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘  โˆˆ โ„‚)
6765, 66mulcld 7997 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ด ยท ๐‘ ) โˆˆ โ„‚)
68 bezoutlemstep.b . . . . . . . . . . . . . . . . . . . . 21 (๐œƒ โ†’ ๐ต โˆˆ โ„•0)
6968ad5antr 496 . . . . . . . . . . . . . . . . . . . 20 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐ต โˆˆ โ„•0)
7069nn0cnd 9250 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐ต โˆˆ โ„‚)
7155zcnd 9395 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ก โˆˆ โ„‚)
7270, 71mulcld 7997 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ต ยท ๐‘ก) โˆˆ โ„‚)
7362, 67, 72adddid 8001 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) = ((๐‘ž ยท (๐ด ยท ๐‘ )) + (๐‘ž ยท (๐ต ยท ๐‘ก))))
7462, 65, 66mul12d 8128 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท (๐ด ยท ๐‘ )) = (๐ด ยท (๐‘ž ยท ๐‘ )))
7562, 70, 71mul12d 8128 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท (๐ต ยท ๐‘ก)) = (๐ต ยท (๐‘ž ยท ๐‘ก)))
7674, 75oveq12d 5909 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ((๐‘ž ยท (๐ด ยท ๐‘ )) + (๐‘ž ยท (๐ต ยท ๐‘ก))) = ((๐ด ยท (๐‘ž ยท ๐‘ )) + (๐ต ยท (๐‘ž ยท ๐‘ก))))
7761, 73, 763eqtrd 2226 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘Š) = ((๐ด ยท (๐‘ž ยท ๐‘ )) + (๐ต ยท (๐‘ž ยท ๐‘ก))))
7858, 77oveq12d 5909 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ โˆ’ (๐‘ž ยท ๐‘Š)) = (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โˆ’ ((๐ด ยท (๐‘ž ยท ๐‘ )) + (๐ต ยท (๐‘ž ยท ๐‘ก)))))
79 simprr 531 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)
8028ad5antr 496 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ โ„•0)
8180nn0cnd 9250 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ โ„‚)
8231adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘Š โˆˆ โ„•)
8382nncnd 8952 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘Š โˆˆ โ„‚)
8462, 83mulcld 7997 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘Š) โˆˆ โ„‚)
8534adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ โ„š)
8637adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘Š โˆˆ โ„š)
8738adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ 0 < ๐‘Š)
8885, 86, 87modqcld 10347 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„š)
89 qcn 9653 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ mod ๐‘Š) โˆˆ โ„š โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„‚)
9088, 89syl 14 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„‚)
9181, 84, 90subaddd 8305 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ((๐‘ฆ โˆ’ (๐‘ž ยท ๐‘Š)) = (๐‘ฆ mod ๐‘Š) โ†” ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ))
9279, 91mpbird 167 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ โˆ’ (๐‘ž ยท ๐‘Š)) = (๐‘ฆ mod ๐‘Š))
9346zcnd 9395 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ข โˆˆ โ„‚)
9465, 93mulcld 7997 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ด ยท ๐‘ข) โˆˆ โ„‚)
9553zcnd 9395 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฃ โˆˆ โ„‚)
9670, 95mulcld 7997 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ต ยท ๐‘ฃ) โˆˆ โ„‚)
9762, 66mulcld 7997 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘ ) โˆˆ โ„‚)
9865, 97mulcld 7997 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ด ยท (๐‘ž ยท ๐‘ )) โˆˆ โ„‚)
9962, 71mulcld 7997 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘ก) โˆˆ โ„‚)
10070, 99mulcld 7997 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ต ยท (๐‘ž ยท ๐‘ก)) โˆˆ โ„‚)
10194, 96, 98, 100addsub4d 8334 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โˆ’ ((๐ด ยท (๐‘ž ยท ๐‘ )) + (๐ต ยท (๐‘ž ยท ๐‘ก)))) = (((๐ด ยท ๐‘ข) โˆ’ (๐ด ยท (๐‘ž ยท ๐‘ ))) + ((๐ต ยท ๐‘ฃ) โˆ’ (๐ต ยท (๐‘ž ยท ๐‘ก)))))
10278, 92, 1013eqtr3d 2230 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) = (((๐ด ยท ๐‘ข) โˆ’ (๐ด ยท (๐‘ž ยท ๐‘ ))) + ((๐ต ยท ๐‘ฃ) โˆ’ (๐ต ยท (๐‘ž ยท ๐‘ก)))))
10365, 93, 97subdid 8390 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) = ((๐ด ยท ๐‘ข) โˆ’ (๐ด ยท (๐‘ž ยท ๐‘ ))))
10470, 95, 99subdid 8390 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก))) = ((๐ต ยท ๐‘ฃ) โˆ’ (๐ต ยท (๐‘ž ยท ๐‘ก))))
105103, 104oveq12d 5909 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)))) = (((๐ด ยท ๐‘ข) โˆ’ (๐ด ยท (๐‘ž ยท ๐‘ ))) + ((๐ต ยท ๐‘ฃ) โˆ’ (๐ต ยท (๐‘ž ยท ๐‘ก)))))
106102, 105eqtr4d 2225 . . . . . . . . . . . . 13 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)))))
107 oveq2 5899 . . . . . . . . . . . . . . . 16 (๐‘˜ = (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โ†’ (๐ต ยท ๐‘˜) = (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก))))
108107oveq2d 5907 . . . . . . . . . . . . . . 15 (๐‘˜ = (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โ†’ ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)))))
109108eqeq2d 2201 . . . . . . . . . . . . . 14 (๐‘˜ = (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โ†’ ((๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก))))))
110109rspcev 2856 . . . . . . . . . . . . 13 (((๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โˆˆ โ„ค โˆง (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก))))) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)))
11157, 106, 110syl2anc 411 . . . . . . . . . . . 12 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)))
112 oveq2 5899 . . . . . . . . . . . . . . . 16 (๐‘— = (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โ†’ (๐ด ยท ๐‘—) = (๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))))
113112oveq1d 5906 . . . . . . . . . . . . . . 15 (๐‘— = (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โ†’ ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)))
114113eqeq2d 2201 . . . . . . . . . . . . . 14 (๐‘— = (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โ†’ ((๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜))))
115114rexbidv 2491 . . . . . . . . . . . . 13 (๐‘— = (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜))))
116115rspcev 2856 . . . . . . . . . . . 12 (((๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โˆˆ โ„ค โˆง โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜))) โ†’ โˆƒ๐‘— โˆˆ โ„ค โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)))
11751, 111, 116syl2anc 411 . . . . . . . . . . 11 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ โˆƒ๐‘— โˆˆ โ„ค โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)))
118 oveq2 5899 . . . . . . . . . . . . . 14 (๐‘— = ๐‘  โ†’ (๐ด ยท ๐‘—) = (๐ด ยท ๐‘ ))
119118oveq1d 5906 . . . . . . . . . . . . 13 (๐‘— = ๐‘  โ†’ ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘˜)))
120119eqeq2d 2201 . . . . . . . . . . . 12 (๐‘— = ๐‘  โ†’ ((๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘˜))))
121 oveq2 5899 . . . . . . . . . . . . . 14 (๐‘˜ = ๐‘ก โ†’ (๐ต ยท ๐‘˜) = (๐ต ยท ๐‘ก))
122121oveq2d 5907 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘ก โ†’ ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘˜)) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
123122eqeq2d 2201 . . . . . . . . . . . 12 (๐‘˜ = ๐‘ก โ†’ ((๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘˜)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
124120, 123cbvrex2v 2732 . . . . . . . . . . 11 (โˆƒ๐‘— โˆˆ โ„ค โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
125117, 124sylib 122 . . . . . . . . . 10 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
12632adantr 276 . . . . . . . . . . 11 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„•0)
127 eqeq1 2196 . . . . . . . . . . . . 13 (๐‘Ÿ = (๐‘ฆ mod ๐‘Š) โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
1281272rexbidv 2515 . . . . . . . . . . . 12 (๐‘Ÿ = (๐‘ฆ mod ๐‘Š) โ†’ (โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
129128sbcieg 3010 . . . . . . . . . . 11 ((๐‘ฆ mod ๐‘Š) โˆˆ โ„•0 โ†’ ([(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
130126, 129syl 14 . . . . . . . . . 10 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ([(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
131125, 130mpbird 167 . . . . . . . . 9 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
1322sbcbii 3037 . . . . . . . . 9 ([(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘ โ†” [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
133131, 132sylibr 134 . . . . . . . 8 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘)
13444, 133rexlimddv 2612 . . . . . . 7 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘)
135134ex 115 . . . . . 6 ((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โ†’ (๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘))
136135rexlimdvva 2615 . . . . 5 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ (โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘))
13727, 136mpd 13 . . . 4 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘)
138137ex 115 . . 3 ((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โ†’ (๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘))
139138rexlimdvva 2615 . 2 (๐œƒ โ†’ (โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘))
14010, 139mpd 13 1 (๐œƒ โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘)
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 980   = wceq 1364  [wsb 1773   โˆˆ wcel 2160  โˆƒwrex 2469  [wsbc 2977   class class class wbr 4018  (class class class)co 5891  โ„‚cc 7828  0cc0 7830   + caddc 7833   ยท cmul 7835   < clt 8011   โˆ’ cmin 8147  โ„•cn 8938  โ„•0cn0 9195  โ„คcz 9272  โ„šcq 9638   mod cmo 10341
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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602  ax-cnex 7921  ax-resscn 7922  ax-1cn 7923  ax-1re 7924  ax-icn 7925  ax-addcl 7926  ax-addrcl 7927  ax-mulcl 7928  ax-mulrcl 7929  ax-addcom 7930  ax-mulcom 7931  ax-addass 7932  ax-mulass 7933  ax-distr 7934  ax-i2m1 7935  ax-0lt1 7936  ax-1rid 7937  ax-0id 7938  ax-rnegex 7939  ax-precex 7940  ax-cnre 7941  ax-pre-ltirr 7942  ax-pre-ltwlin 7943  ax-pre-lttrn 7944  ax-pre-apti 7945  ax-pre-ltadd 7946  ax-pre-mulgt0 7947  ax-pre-mulext 7948  ax-arch 7949
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4308  df-po 4311  df-iso 4312  df-iord 4381  df-on 4383  df-ilim 4384  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-f1 5236  df-fo 5237  df-f1o 5238  df-fv 5239  df-riota 5847  df-ov 5894  df-oprab 5895  df-mpo 5896  df-1st 6159  df-2nd 6160  df-recs 6324  df-frec 6410  df-pnf 8013  df-mnf 8014  df-xr 8015  df-ltxr 8016  df-le 8017  df-sub 8149  df-neg 8150  df-reap 8551  df-ap 8558  df-div 8649  df-inn 8939  df-2 8997  df-n0 9196  df-z 9273  df-uz 9548  df-q 9639  df-rp 9673  df-fl 10289  df-mod 10342  df-seqfrec 10465  df-exp 10539  df-cj 10870  df-re 10871  df-im 10872  df-rsqrt 11026  df-abs 11027  df-dvds 11814
This theorem is referenced by:  bezoutlemstep  12017
  Copyright terms: Public domain W3C validator