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

Theorem bezoutlemnewy 12010
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 3034 . . . 4 ([๐‘Š / ๐‘Ÿ]๐œ‘ โ†” [๐‘Š / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
4 bezoutlemstep.w . . . . 5 (๐œƒ โ†’ ๐‘Š โˆˆ โ„•)
5 eqeq1 2194 . . . . . . 7 (๐‘Ÿ = ๐‘Š โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
652rexbidv 2512 . . . . . 6 (๐‘Ÿ = ๐‘Š โ†’ (โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
76sbcieg 3007 . . . . 5 (๐‘Š โˆˆ โ„• โ†’ ([๐‘Š / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
84, 7syl 14 . . . 4 (๐œƒ โ†’ ([๐‘Š / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
93, 8bitrid 192 . . 3 (๐œƒ โ†’ ([๐‘Š / ๐‘Ÿ]๐œ‘ โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
101, 9mpbid 147 . 2 (๐œƒ โ†’ โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
11 bezoutlemstep.y-is-bezout . . . . . . 7 (๐œƒ โ†’ [๐‘ฆ / ๐‘Ÿ]๐œ‘)
12 oveq2 5896 . . . . . . . . . . . . 13 (๐‘  = ๐‘ข โ†’ (๐ด ยท ๐‘ ) = (๐ด ยท ๐‘ข))
1312oveq1d 5903 . . . . . . . . . . . 12 (๐‘  = ๐‘ข โ†’ ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ก)))
1413eqeq2d 2199 . . . . . . . . . . 11 (๐‘  = ๐‘ข โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ก))))
15 oveq2 5896 . . . . . . . . . . . . 13 (๐‘ก = ๐‘ฃ โ†’ (๐ต ยท ๐‘ก) = (๐ต ยท ๐‘ฃ))
1615oveq2d 5904 . . . . . . . . . . . 12 (๐‘ก = ๐‘ฃ โ†’ ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ก)) = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
1716eqeq2d 2199 . . . . . . . . . . 11 (๐‘ก = ๐‘ฃ โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ก)) โ†” ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
1814, 17cbvrex2v 2729 . . . . . . . . . 10 (โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
192, 18bitri 184 . . . . . . . . 9 (๐œ‘ โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
2019sbbii 1775 . . . . . . . 8 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†” [๐‘ฆ / ๐‘Ÿ]โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
21 nfv 1538 . . . . . . . . 9 โ„ฒ๐‘Ÿโˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))
22 eqeq1 2194 . . . . . . . . . 10 (๐‘Ÿ = ๐‘ฆ โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†” ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
23222rexbidv 2512 . . . . . . . . 9 (๐‘Ÿ = ๐‘ฆ โ†’ (โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
2421, 23sbie 1801 . . . . . . . 8 ([๐‘ฆ / ๐‘Ÿ]โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
2520, 24bitri 184 . . . . . . 7 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
2611, 25sylib 122 . . . . . 6 (๐œƒ โ†’ โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
2726ad2antrr 488 . . . . 5 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
28 bezoutlemstep.y-nn0 . . . . . . . . . . 11 (๐œƒ โ†’ ๐‘ฆ โˆˆ โ„•0)
2928ad4antr 494 . . . . . . . . . 10 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘ฆ โˆˆ โ„•0)
3029nn0zd 9386 . . . . . . . . 9 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘ฆ โˆˆ โ„ค)
314ad4antr 494 . . . . . . . . 9 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘Š โˆˆ โ„•)
3230, 31zmodcld 10358 . . . . . . . . 9 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„•0)
33 zq 9639 . . . . . . . . . . 11 (๐‘ฆ โˆˆ โ„ค โ†’ ๐‘ฆ โˆˆ โ„š)
3430, 33syl 14 . . . . . . . . . 10 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘ฆ โˆˆ โ„š)
3531nnzd 9387 . . . . . . . . . . 11 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘Š โˆˆ โ„ค)
36 zq 9639 . . . . . . . . . . 11 (๐‘Š โˆˆ โ„ค โ†’ ๐‘Š โˆˆ โ„š)
3735, 36syl 14 . . . . . . . . . 10 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ๐‘Š โˆˆ โ„š)
3831nngt0d 8976 . . . . . . . . . 10 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ 0 < ๐‘Š)
39 modqlt 10346 . . . . . . . . . 10 ((๐‘ฆ โˆˆ โ„š โˆง ๐‘Š โˆˆ โ„š โˆง 0 < ๐‘Š) โ†’ (๐‘ฆ mod ๐‘Š) < ๐‘Š)
4034, 37, 38, 39syl3anc 1248 . . . . . . . . 9 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ (๐‘ฆ mod ๐‘Š) < ๐‘Š)
41 eqid 2187 . . . . . . . . . 10 (๐‘ฆ mod ๐‘Š) = (๐‘ฆ mod ๐‘Š)
42 modremain 11947 . . . . . . . . . 10 ((๐‘ฆ โˆˆ โ„ค โˆง ๐‘Š โˆˆ โ„• โˆง ((๐‘ฆ mod ๐‘Š) โˆˆ โ„•0 โˆง (๐‘ฆ mod ๐‘Š) < ๐‘Š)) โ†’ ((๐‘ฆ mod ๐‘Š) = (๐‘ฆ mod ๐‘Š) โ†” โˆƒ๐‘ž โˆˆ โ„ค ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ))
4341, 42mpbii 148 . . . . . . . . 9 ((๐‘ฆ โˆˆ โ„ค โˆง ๐‘Š โˆˆ โ„• โˆง ((๐‘ฆ mod ๐‘Š) โˆˆ โ„•0 โˆง (๐‘ฆ mod ๐‘Š) < ๐‘Š)) โ†’ โˆƒ๐‘ž โˆˆ โ„ค ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)
4430, 31, 32, 40, 43syl112anc 1252 . . . . . . . 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 9394 . . . . . . . . . . . . 13 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘ ) โˆˆ โ„ค)
5146, 50zsubcld 9393 . . . . . . . . . . . 12 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โˆˆ โ„ค)
52 simprr 531 . . . . . . . . . . . . . . 15 ((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โ†’ ๐‘ฃ โˆˆ โ„ค)
5352ad2antrr 488 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฃ โˆˆ โ„ค)
54 simplrr 536 . . . . . . . . . . . . . . . 16 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ ๐‘ก โˆˆ โ„ค)
5554ad3antrrr 492 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ก โˆˆ โ„ค)
5647, 55zmulcld 9394 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘ก) โˆˆ โ„ค)
5753, 56zsubcld 9393 . . . . . . . . . . . . 13 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โˆˆ โ„ค)
58 simplr 528 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
59 simpr 110 . . . . . . . . . . . . . . . . . . 19 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
6059ad3antrrr 492 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
6160oveq2d 5904 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘Š) = (๐‘ž ยท ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
6247zcnd 9389 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ž โˆˆ โ„‚)
63 bezoutlemstep.a . . . . . . . . . . . . . . . . . . . . 21 (๐œƒ โ†’ ๐ด โˆˆ โ„•0)
6463ad5antr 496 . . . . . . . . . . . . . . . . . . . 20 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐ด โˆˆ โ„•0)
6564nn0cnd 9244 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐ด โˆˆ โ„‚)
6649zcnd 9389 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘  โˆˆ โ„‚)
6765, 66mulcld 7991 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ด ยท ๐‘ ) โˆˆ โ„‚)
68 bezoutlemstep.b . . . . . . . . . . . . . . . . . . . . 21 (๐œƒ โ†’ ๐ต โˆˆ โ„•0)
6968ad5antr 496 . . . . . . . . . . . . . . . . . . . 20 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐ต โˆˆ โ„•0)
7069nn0cnd 9244 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐ต โˆˆ โ„‚)
7155zcnd 9389 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ก โˆˆ โ„‚)
7270, 71mulcld 7991 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ต ยท ๐‘ก) โˆˆ โ„‚)
7362, 67, 72adddid 7995 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) = ((๐‘ž ยท (๐ด ยท ๐‘ )) + (๐‘ž ยท (๐ต ยท ๐‘ก))))
7462, 65, 66mul12d 8122 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท (๐ด ยท ๐‘ )) = (๐ด ยท (๐‘ž ยท ๐‘ )))
7562, 70, 71mul12d 8122 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท (๐ต ยท ๐‘ก)) = (๐ต ยท (๐‘ž ยท ๐‘ก)))
7674, 75oveq12d 5906 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ((๐‘ž ยท (๐ด ยท ๐‘ )) + (๐‘ž ยท (๐ต ยท ๐‘ก))) = ((๐ด ยท (๐‘ž ยท ๐‘ )) + (๐ต ยท (๐‘ž ยท ๐‘ก))))
7761, 73, 763eqtrd 2224 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘Š) = ((๐ด ยท (๐‘ž ยท ๐‘ )) + (๐ต ยท (๐‘ž ยท ๐‘ก))))
7858, 77oveq12d 5906 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ โˆ’ (๐‘ž ยท ๐‘Š)) = (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โˆ’ ((๐ด ยท (๐‘ž ยท ๐‘ )) + (๐ต ยท (๐‘ž ยท ๐‘ก)))))
79 simprr 531 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)
8028ad5antr 496 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ โ„•0)
8180nn0cnd 9244 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ โ„‚)
8231adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘Š โˆˆ โ„•)
8382nncnd 8946 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘Š โˆˆ โ„‚)
8462, 83mulcld 7991 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘Š) โˆˆ โ„‚)
8534adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ โ„š)
8637adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘Š โˆˆ โ„š)
8738adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ 0 < ๐‘Š)
8885, 86, 87modqcld 10341 . . . . . . . . . . . . . . . . . 18 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„š)
89 qcn 9647 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ mod ๐‘Š) โˆˆ โ„š โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„‚)
9088, 89syl 14 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„‚)
9181, 84, 90subaddd 8299 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ((๐‘ฆ โˆ’ (๐‘ž ยท ๐‘Š)) = (๐‘ฆ mod ๐‘Š) โ†” ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ))
9279, 91mpbird 167 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ โˆ’ (๐‘ž ยท ๐‘Š)) = (๐‘ฆ mod ๐‘Š))
9346zcnd 9389 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ข โˆˆ โ„‚)
9465, 93mulcld 7991 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ด ยท ๐‘ข) โˆˆ โ„‚)
9553zcnd 9389 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ๐‘ฃ โˆˆ โ„‚)
9670, 95mulcld 7991 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ต ยท ๐‘ฃ) โˆˆ โ„‚)
9762, 66mulcld 7991 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘ ) โˆˆ โ„‚)
9865, 97mulcld 7991 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ด ยท (๐‘ž ยท ๐‘ )) โˆˆ โ„‚)
9962, 71mulcld 7991 . . . . . . . . . . . . . . . . 17 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ž ยท ๐‘ก) โˆˆ โ„‚)
10070, 99mulcld 7991 . . . . . . . . . . . . . . . 16 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ต ยท (๐‘ž ยท ๐‘ก)) โˆˆ โ„‚)
10194, 96, 98, 100addsub4d 8328 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โˆ’ ((๐ด ยท (๐‘ž ยท ๐‘ )) + (๐ต ยท (๐‘ž ยท ๐‘ก)))) = (((๐ด ยท ๐‘ข) โˆ’ (๐ด ยท (๐‘ž ยท ๐‘ ))) + ((๐ต ยท ๐‘ฃ) โˆ’ (๐ต ยท (๐‘ž ยท ๐‘ก)))))
10278, 92, 1013eqtr3d 2228 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) = (((๐ด ยท ๐‘ข) โˆ’ (๐ด ยท (๐‘ž ยท ๐‘ ))) + ((๐ต ยท ๐‘ฃ) โˆ’ (๐ต ยท (๐‘ž ยท ๐‘ก)))))
10365, 93, 97subdid 8384 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) = ((๐ด ยท ๐‘ข) โˆ’ (๐ด ยท (๐‘ž ยท ๐‘ ))))
10470, 95, 99subdid 8384 . . . . . . . . . . . . . . 15 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก))) = ((๐ต ยท ๐‘ฃ) โˆ’ (๐ต ยท (๐‘ž ยท ๐‘ก))))
105103, 104oveq12d 5906 . . . . . . . . . . . . . 14 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)))) = (((๐ด ยท ๐‘ข) โˆ’ (๐ด ยท (๐‘ž ยท ๐‘ ))) + ((๐ต ยท ๐‘ฃ) โˆ’ (๐ต ยท (๐‘ž ยท ๐‘ก)))))
106102, 105eqtr4d 2223 . . . . . . . . . . . . 13 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)))))
107 oveq2 5896 . . . . . . . . . . . . . . . 16 (๐‘˜ = (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โ†’ (๐ต ยท ๐‘˜) = (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก))))
108107oveq2d 5904 . . . . . . . . . . . . . . 15 (๐‘˜ = (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โ†’ ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)))))
109108eqeq2d 2199 . . . . . . . . . . . . . 14 (๐‘˜ = (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โ†’ ((๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก))))))
110109rspcev 2853 . . . . . . . . . . . . 13 (((๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก)) โˆˆ โ„ค โˆง (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท (๐‘ฃ โˆ’ (๐‘ž ยท ๐‘ก))))) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)))
11157, 106, 110syl2anc 411 . . . . . . . . . . . 12 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)))
112 oveq2 5896 . . . . . . . . . . . . . . . 16 (๐‘— = (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โ†’ (๐ด ยท ๐‘—) = (๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))))
113112oveq1d 5903 . . . . . . . . . . . . . . 15 (๐‘— = (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โ†’ ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜)))
114113eqeq2d 2199 . . . . . . . . . . . . . 14 (๐‘— = (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โ†’ ((๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜))))
115114rexbidv 2488 . . . . . . . . . . . . 13 (๐‘— = (๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) โ†” โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜))))
116115rspcev 2853 . . . . . . . . . . . 12 (((๐‘ข โˆ’ (๐‘ž ยท ๐‘ )) โˆˆ โ„ค โˆง โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท (๐‘ข โˆ’ (๐‘ž ยท ๐‘ ))) + (๐ต ยท ๐‘˜))) โ†’ โˆƒ๐‘— โˆˆ โ„ค โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)))
11751, 111, 116syl2anc 411 . . . . . . . . . . 11 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ โˆƒ๐‘— โˆˆ โ„ค โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)))
118 oveq2 5896 . . . . . . . . . . . . . 14 (๐‘— = ๐‘  โ†’ (๐ด ยท ๐‘—) = (๐ด ยท ๐‘ ))
119118oveq1d 5903 . . . . . . . . . . . . 13 (๐‘— = ๐‘  โ†’ ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘˜)))
120119eqeq2d 2199 . . . . . . . . . . . 12 (๐‘— = ๐‘  โ†’ ((๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘˜))))
121 oveq2 5896 . . . . . . . . . . . . . 14 (๐‘˜ = ๐‘ก โ†’ (๐ต ยท ๐‘˜) = (๐ต ยท ๐‘ก))
122121oveq2d 5904 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘ก โ†’ ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘˜)) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
123122eqeq2d 2199 . . . . . . . . . . . 12 (๐‘˜ = ๐‘ก โ†’ ((๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘˜)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
124120, 123cbvrex2v 2729 . . . . . . . . . . 11 (โˆƒ๐‘— โˆˆ โ„ค โˆƒ๐‘˜ โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘—) + (๐ต ยท ๐‘˜)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
125117, 124sylib 122 . . . . . . . . . 10 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
12632adantr 276 . . . . . . . . . . 11 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ (๐‘ฆ mod ๐‘Š) โˆˆ โ„•0)
127 eqeq1 2194 . . . . . . . . . . . . 13 (๐‘Ÿ = (๐‘ฆ mod ๐‘Š) โ†’ (๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
1281272rexbidv 2512 . . . . . . . . . . . 12 (๐‘Ÿ = (๐‘ฆ mod ๐‘Š) โ†’ (โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
129128sbcieg 3007 . . . . . . . . . . 11 ((๐‘ฆ mod ๐‘Š) โˆˆ โ„•0 โ†’ ([(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
130126, 129syl 14 . . . . . . . . . 10 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ ([(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค (๐‘ฆ mod ๐‘Š) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
131125, 130mpbird 167 . . . . . . . . 9 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
1322sbcbii 3034 . . . . . . . . 9 ([(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘ โ†” [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
133131, 132sylibr 134 . . . . . . . 8 ((((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โˆง (๐‘ž โˆˆ โ„ค โˆง ((๐‘ž ยท ๐‘Š) + (๐‘ฆ mod ๐‘Š)) = ๐‘ฆ)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘)
13444, 133rexlimddv 2609 . . . . . . 7 (((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โˆง ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘)
135134ex 115 . . . . . 6 ((((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค)) โ†’ (๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘))
136135rexlimdvva 2612 . . . . 5 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ (โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ฆ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘))
13727, 136mpd 13 . . . 4 (((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โˆง ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘)
138137ex 115 . . 3 ((๐œƒ โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โ†’ (๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘))
139138rexlimdvva 2612 . 2 (๐œƒ โ†’ (โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Š = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘))
14010, 139mpd 13 1 (๐œƒ โ†’ [(๐‘ฆ mod ๐‘Š) / ๐‘Ÿ]๐œ‘)
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 979   = wceq 1363  [wsb 1772   โˆˆ wcel 2158  โˆƒwrex 2466  [wsbc 2974   class class class wbr 4015  (class class class)co 5888  โ„‚cc 7822  0cc0 7824   + caddc 7827   ยท cmul 7829   < clt 8005   โˆ’ cmin 8141  โ„•cn 8932  โ„•0cn0 9189  โ„คcz 9266  โ„šcq 9632   mod cmo 10335
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-frec 6405  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-fl 10283  df-mod 10336  df-seqfrec 10459  df-exp 10533  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-dvds 11808
This theorem is referenced by:  bezoutlemstep  12011
  Copyright terms: Public domain W3C validator