MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bezoutlem3 Structured version   Visualization version   GIF version

Theorem bezoutlem3 16427
Description: Lemma for bezout 16429. (Contributed by Mario Carneiro, 22-Feb-2014.) ( Revised by AV, 30-Sep-2020.)
Hypotheses
Ref Expression
bezout.1 ๐‘€ = {๐‘ง โˆˆ โ„• โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))}
bezout.3 (๐œ‘ โ†’ ๐ด โˆˆ โ„ค)
bezout.4 (๐œ‘ โ†’ ๐ต โˆˆ โ„ค)
bezout.2 ๐บ = inf(๐‘€, โ„, < )
bezout.5 (๐œ‘ โ†’ ยฌ (๐ด = 0 โˆง ๐ต = 0))
Assertion
Ref Expression
bezoutlem3 (๐œ‘ โ†’ (๐ถ โˆˆ ๐‘€ โ†’ ๐บ โˆฅ ๐ถ))
Distinct variable groups:   ๐‘ฅ,๐‘ฆ,๐‘ง,๐ด   ๐‘ฅ,๐ต,๐‘ฆ,๐‘ง   ๐‘ฅ,๐บ,๐‘ฆ,๐‘ง   ๐œ‘,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘ฅ,๐ถ,๐‘ฆ,๐‘ง   ๐‘ฅ,๐‘€,๐‘ฆ
Allowed substitution hint:   ๐‘€(๐‘ง)

Proof of Theorem bezoutlem3
Dummy variables ๐‘ก ๐‘  ๐‘ข ๐‘ฃ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 486 . . . . . . . . . 10 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ๐ถ โˆˆ ๐‘€)
2 eqeq1 2737 . . . . . . . . . . . . 13 (๐‘ง = ๐ถ โ†’ (๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” ๐ถ = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
322rexbidv 3210 . . . . . . . . . . . 12 (๐‘ง = ๐ถ โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ๐ถ = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
4 oveq2 7366 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘  โ†’ (๐ด ยท ๐‘ฅ) = (๐ด ยท ๐‘ ))
54oveq1d 7373 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘  โ†’ ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ฆ)))
65eqeq2d 2744 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘  โ†’ (๐ถ = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” ๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ฆ))))
7 oveq2 7366 . . . . . . . . . . . . . . 15 (๐‘ฆ = ๐‘ก โ†’ (๐ต ยท ๐‘ฆ) = (๐ต ยท ๐‘ก))
87oveq2d 7374 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ก โ†’ ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ฆ)) = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
98eqeq2d 2744 . . . . . . . . . . . . 13 (๐‘ฆ = ๐‘ก โ†’ (๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ฆ)) โ†” ๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
106, 9cbvrex2vw 3227 . . . . . . . . . . . 12 (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ๐ถ = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
113, 10bitrdi 287 . . . . . . . . . . 11 (๐‘ง = ๐ถ โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
12 bezout.1 . . . . . . . . . . 11 ๐‘€ = {๐‘ง โˆˆ โ„• โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))}
1311, 12elrab2 3649 . . . . . . . . . 10 (๐ถ โˆˆ ๐‘€ โ†” (๐ถ โˆˆ โ„• โˆง โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
141, 13sylib 217 . . . . . . . . 9 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (๐ถ โˆˆ โ„• โˆง โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก))))
1514simpld 496 . . . . . . . 8 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ๐ถ โˆˆ โ„•)
1615nnred 12173 . . . . . . 7 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ๐ถ โˆˆ โ„)
17 bezout.3 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ด โˆˆ โ„ค)
18 bezout.4 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ต โˆˆ โ„ค)
19 bezout.2 . . . . . . . . . . . 12 ๐บ = inf(๐‘€, โ„, < )
20 bezout.5 . . . . . . . . . . . 12 (๐œ‘ โ†’ ยฌ (๐ด = 0 โˆง ๐ต = 0))
2112, 17, 18, 19, 20bezoutlem2 16426 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐บ โˆˆ ๐‘€)
22 oveq2 7366 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘ข โ†’ (๐ด ยท ๐‘ฅ) = (๐ด ยท ๐‘ข))
2322oveq1d 7373 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ข โ†’ ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฆ)))
2423eqeq2d 2744 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ข โ†’ (๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” ๐‘ง = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฆ))))
25 oveq2 7366 . . . . . . . . . . . . . . . 16 (๐‘ฆ = ๐‘ฃ โ†’ (๐ต ยท ๐‘ฆ) = (๐ต ยท ๐‘ฃ))
2625oveq2d 7374 . . . . . . . . . . . . . . 15 (๐‘ฆ = ๐‘ฃ โ†’ ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฆ)) = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
2726eqeq2d 2744 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘ง = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฆ)) โ†” ๐‘ง = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
2824, 27cbvrex2vw 3227 . . . . . . . . . . . . 13 (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ง = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
29 eqeq1 2737 . . . . . . . . . . . . . 14 (๐‘ง = ๐บ โ†’ (๐‘ง = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†” ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
30292rexbidv 3210 . . . . . . . . . . . . 13 (๐‘ง = ๐บ โ†’ (โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐‘ง = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
3128, 30bitrid 283 . . . . . . . . . . . 12 (๐‘ง = ๐บ โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
3231, 12elrab2 3649 . . . . . . . . . . 11 (๐บ โˆˆ ๐‘€ โ†” (๐บ โˆˆ โ„• โˆง โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
3321, 32sylib 217 . . . . . . . . . 10 (๐œ‘ โ†’ (๐บ โˆˆ โ„• โˆง โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))))
3433simpld 496 . . . . . . . . 9 (๐œ‘ โ†’ ๐บ โˆˆ โ„•)
3534nnrpd 12960 . . . . . . . 8 (๐œ‘ โ†’ ๐บ โˆˆ โ„+)
3635adantr 482 . . . . . . 7 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ๐บ โˆˆ โ„+)
37 modlt 13791 . . . . . . 7 ((๐ถ โˆˆ โ„ โˆง ๐บ โˆˆ โ„+) โ†’ (๐ถ mod ๐บ) < ๐บ)
3816, 36, 37syl2anc 585 . . . . . 6 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (๐ถ mod ๐บ) < ๐บ)
3915nnzd 12531 . . . . . . . . 9 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ๐ถ โˆˆ โ„ค)
4034adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ๐บ โˆˆ โ„•)
4139, 40zmodcld 13803 . . . . . . . 8 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (๐ถ mod ๐บ) โˆˆ โ„•0)
4241nn0red 12479 . . . . . . 7 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (๐ถ mod ๐บ) โˆˆ โ„)
4334nnred 12173 . . . . . . . 8 (๐œ‘ โ†’ ๐บ โˆˆ โ„)
4443adantr 482 . . . . . . 7 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ๐บ โˆˆ โ„)
4542, 44ltnled 11307 . . . . . 6 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ((๐ถ mod ๐บ) < ๐บ โ†” ยฌ ๐บ โ‰ค (๐ถ mod ๐บ)))
4638, 45mpbid 231 . . . . 5 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ยฌ ๐บ โ‰ค (๐ถ mod ๐บ))
4714simprd 497 . . . . . . . . 9 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
4833simprd 497 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
4948ad2antrr 725 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โ†’ โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)))
50 simprll 778 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐‘  โˆˆ โ„ค)
51 simprrl 780 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐‘ข โˆˆ โ„ค)
5216, 40nndivred 12212 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (๐ถ / ๐บ) โˆˆ โ„)
5352flcld 13709 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (โŒŠโ€˜(๐ถ / ๐บ)) โˆˆ โ„ค)
5453adantr 482 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (โŒŠโ€˜(๐ถ / ๐บ)) โˆˆ โ„ค)
5551, 54zmulcld 12618 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))) โˆˆ โ„ค)
5650, 55zsubcld 12617 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โˆˆ โ„ค)
57 simprlr 779 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐‘ก โˆˆ โ„ค)
58 simprrr 781 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐‘ฃ โˆˆ โ„ค)
5958, 54zmulcld 12618 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ))) โˆˆ โ„ค)
6057, 59zsubcld 12617 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โˆˆ โ„ค)
6117zcnd 12613 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
6261ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐ด โˆˆ โ„‚)
6350zcnd 12613 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐‘  โˆˆ โ„‚)
6462, 63mulcld 11180 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐ด ยท ๐‘ ) โˆˆ โ„‚)
6518zcnd 12613 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
6665ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐ต โˆˆ โ„‚)
6757zcnd 12613 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐‘ก โˆˆ โ„‚)
6866, 67mulcld 11180 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐ต ยท ๐‘ก) โˆˆ โ„‚)
6955zcnd 12613 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))) โˆˆ โ„‚)
7062, 69mulcld 11180 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐ด ยท (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โˆˆ โ„‚)
7159zcnd 12613 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ))) โˆˆ โ„‚)
7266, 71mulcld 11180 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐ต ยท (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โˆˆ โ„‚)
7364, 68, 70, 72addsub4d 11564 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ ((๐ด ยท (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) + (๐ต ยท (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))) = (((๐ด ยท ๐‘ ) โˆ’ (๐ด ยท (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + ((๐ต ยท ๐‘ก) โˆ’ (๐ต ยท (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))))
7451zcnd 12613 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐‘ข โˆˆ โ„‚)
7562, 74mulcld 11180 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐ด ยท ๐‘ข) โˆˆ โ„‚)
7653zcnd 12613 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (โŒŠโ€˜(๐ถ / ๐บ)) โˆˆ โ„‚)
7776adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (โŒŠโ€˜(๐ถ / ๐บ)) โˆˆ โ„‚)
7858zcnd 12613 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ๐‘ฃ โˆˆ โ„‚)
7966, 78mulcld 11180 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐ต ยท ๐‘ฃ) โˆˆ โ„‚)
8062, 74, 77mulassd 11183 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ((๐ด ยท ๐‘ข) ยท (โŒŠโ€˜(๐ถ / ๐บ))) = (๐ด ยท (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))))
8166, 78, 77mulassd 11183 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ((๐ต ยท ๐‘ฃ) ยท (โŒŠโ€˜(๐ถ / ๐บ))) = (๐ต ยท (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))
8280, 81oveq12d 7376 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (((๐ด ยท ๐‘ข) ยท (โŒŠโ€˜(๐ถ / ๐บ))) + ((๐ต ยท ๐‘ฃ) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) + (๐ต ยท (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ))))))
8375, 77, 79, 82joinlmuladdmuld 11187 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ))) = ((๐ด ยท (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) + (๐ต ยท (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ))))))
8483oveq2d 7374 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ ((๐ด ยท (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) + (๐ต ยท (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))))
8562, 63, 69subdid 11616 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) = ((๐ด ยท ๐‘ ) โˆ’ (๐ด ยท (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))))
8666, 67, 71subdid 11616 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐ต ยท (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ))))) = ((๐ต ยท ๐‘ก) โˆ’ (๐ต ยท (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ))))))
8785, 86oveq12d 7376 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ((๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + (๐ต ยท (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))) = (((๐ด ยท ๐‘ ) โˆ’ (๐ด ยท (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + ((๐ต ยท ๐‘ก) โˆ’ (๐ต ยท (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))))
8873, 84, 873eqtr4d 2783 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + (๐ต ยท (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))))
89 oveq2 7366 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ = (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โ†’ (๐ด ยท ๐‘ฅ) = (๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))))
9089oveq1d 7373 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โ†’ ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) = ((๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + (๐ต ยท ๐‘ฆ)))
9190eqeq2d 2744 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โ†’ ((((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + (๐ต ยท ๐‘ฆ))))
92 oveq2 7366 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ = (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โ†’ (๐ต ยท ๐‘ฆ) = (๐ต ยท (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ))))))
9392oveq2d 7374 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ = (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โ†’ ((๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + (๐ต ยท ๐‘ฆ)) = ((๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + (๐ต ยท (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))))
9493eqeq2d 2744 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ = (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โ†’ ((((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + (๐ต ยท ๐‘ฆ)) โ†” (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + (๐ต ยท (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ))))))))
9591, 94rspc2ev 3591 . . . . . . . . . . . . . . . . 17 (((๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โˆˆ โ„ค โˆง (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โˆˆ โ„ค โˆง (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท (๐‘  โˆ’ (๐‘ข ยท (โŒŠโ€˜(๐ถ / ๐บ))))) + (๐ต ยท (๐‘ก โˆ’ (๐‘ฃ ยท (โŒŠโ€˜(๐ถ / ๐บ))))))) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)))
9656, 60, 88, 95syl3anc 1372 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)))
97 oveq1 7365 . . . . . . . . . . . . . . . . . . 19 (๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ))) = (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ))))
98 oveq12 7367 . . . . . . . . . . . . . . . . . . 19 ((๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆง (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ))) = (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) โ†’ (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))))
9997, 98sylan2 594 . . . . . . . . . . . . . . . . . 18 ((๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆง ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))))
10099eqeq1d 2735 . . . . . . . . . . . . . . . . 17 ((๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆง ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ ((๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
1011002rexbidv 3210 . . . . . . . . . . . . . . . 16 ((๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆง ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆ’ (((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
10296, 101syl5ibrcom 247 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ ((๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โˆง ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ))) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
103102expcomd 418 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โˆง (๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค))) โ†’ (๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†’ (๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)))))
104103expr 458 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โ†’ ((๐‘ข โˆˆ โ„ค โˆง ๐‘ฃ โˆˆ โ„ค) โ†’ (๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†’ (๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))))
105104rexlimdvv 3201 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โ†’ (โˆƒ๐‘ข โˆˆ โ„ค โˆƒ๐‘ฃ โˆˆ โ„ค ๐บ = ((๐ด ยท ๐‘ข) + (๐ต ยท ๐‘ฃ)) โ†’ (๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)))))
10649, 105mpd 15 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โˆง (๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค)) โ†’ (๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
107106ex 414 . . . . . . . . . 10 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ((๐‘  โˆˆ โ„ค โˆง ๐‘ก โˆˆ โ„ค) โ†’ (๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)))))
108107rexlimdvv 3201 . . . . . . . . 9 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐ถ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
10947, 108mpd 15 . . . . . . . 8 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)))
110 modval 13782 . . . . . . . . . . . 12 ((๐ถ โˆˆ โ„ โˆง ๐บ โˆˆ โ„+) โ†’ (๐ถ mod ๐บ) = (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))
11116, 36, 110syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (๐ถ mod ๐บ) = (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))))
112111eqcomd 2739 . . . . . . . . . 10 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = (๐ถ mod ๐บ))
113112eqeq1d 2735 . . . . . . . . 9 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ((๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” (๐ถ mod ๐บ) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
1141132rexbidv 3210 . . . . . . . 8 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ โˆ’ (๐บ ยท (โŒŠโ€˜(๐ถ / ๐บ)))) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ mod ๐บ) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
115109, 114mpbid 231 . . . . . . 7 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ mod ๐บ) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)))
116 eqeq1 2737 . . . . . . . . . 10 (๐‘ง = (๐ถ mod ๐บ) โ†’ (๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” (๐ถ mod ๐บ) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
1171162rexbidv 3210 . . . . . . . . 9 (๐‘ง = (๐ถ mod ๐บ) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ๐‘ง = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†” โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ mod ๐บ) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
118117, 12elrab2 3649 . . . . . . . 8 ((๐ถ mod ๐บ) โˆˆ ๐‘€ โ†” ((๐ถ mod ๐บ) โˆˆ โ„• โˆง โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ mod ๐บ) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ))))
119118simplbi2com 504 . . . . . . 7 (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐ถ mod ๐บ) = ((๐ด ยท ๐‘ฅ) + (๐ต ยท ๐‘ฆ)) โ†’ ((๐ถ mod ๐บ) โˆˆ โ„• โ†’ (๐ถ mod ๐บ) โˆˆ ๐‘€))
120115, 119syl 17 . . . . . 6 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ((๐ถ mod ๐บ) โˆˆ โ„• โ†’ (๐ถ mod ๐บ) โˆˆ ๐‘€))
12112ssrab3 4041 . . . . . . . . 9 ๐‘€ โŠ† โ„•
122 nnuz 12811 . . . . . . . . 9 โ„• = (โ„คโ‰ฅโ€˜1)
123121, 122sseqtri 3981 . . . . . . . 8 ๐‘€ โŠ† (โ„คโ‰ฅโ€˜1)
124 infssuzle 12861 . . . . . . . 8 ((๐‘€ โŠ† (โ„คโ‰ฅโ€˜1) โˆง (๐ถ mod ๐บ) โˆˆ ๐‘€) โ†’ inf(๐‘€, โ„, < ) โ‰ค (๐ถ mod ๐บ))
125123, 124mpan 689 . . . . . . 7 ((๐ถ mod ๐บ) โˆˆ ๐‘€ โ†’ inf(๐‘€, โ„, < ) โ‰ค (๐ถ mod ๐บ))
12619, 125eqbrtrid 5141 . . . . . 6 ((๐ถ mod ๐บ) โˆˆ ๐‘€ โ†’ ๐บ โ‰ค (๐ถ mod ๐บ))
127120, 126syl6 35 . . . . 5 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ((๐ถ mod ๐บ) โˆˆ โ„• โ†’ ๐บ โ‰ค (๐ถ mod ๐บ)))
12846, 127mtod 197 . . . 4 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ยฌ (๐ถ mod ๐บ) โˆˆ โ„•)
129 elnn0 12420 . . . . . 6 ((๐ถ mod ๐บ) โˆˆ โ„•0 โ†” ((๐ถ mod ๐บ) โˆˆ โ„• โˆจ (๐ถ mod ๐บ) = 0))
13041, 129sylib 217 . . . . 5 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ((๐ถ mod ๐บ) โˆˆ โ„• โˆจ (๐ถ mod ๐บ) = 0))
131130ord 863 . . . 4 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (ยฌ (๐ถ mod ๐บ) โˆˆ โ„• โ†’ (๐ถ mod ๐บ) = 0))
132128, 131mpd 15 . . 3 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (๐ถ mod ๐บ) = 0)
133 dvdsval3 16145 . . . 4 ((๐บ โˆˆ โ„• โˆง ๐ถ โˆˆ โ„ค) โ†’ (๐บ โˆฅ ๐ถ โ†” (๐ถ mod ๐บ) = 0))
13440, 39, 133syl2anc 585 . . 3 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ (๐บ โˆฅ ๐ถ โ†” (๐ถ mod ๐บ) = 0))
135132, 134mpbird 257 . 2 ((๐œ‘ โˆง ๐ถ โˆˆ ๐‘€) โ†’ ๐บ โˆฅ ๐ถ)
136135ex 414 1 (๐œ‘ โ†’ (๐ถ โˆˆ ๐‘€ โ†’ ๐บ โˆฅ ๐ถ))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107  โˆƒwrex 3070  {crab 3406   โŠ† wss 3911   class class class wbr 5106  โ€˜cfv 6497  (class class class)co 7358  infcinf 9382  โ„‚cc 11054  โ„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   ยท cmul 11061   < clt 11194   โ‰ค cle 11195   โˆ’ cmin 11390   / cdiv 11817  โ„•cn 12158  โ„•0cn0 12418  โ„คcz 12504  โ„คโ‰ฅcuz 12768  โ„+crp 12920  โŒŠcfl 13701   mod cmo 13780   โˆฅ cdvds 16141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-sup 9383  df-inf 9384  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-n0 12419  df-z 12505  df-uz 12769  df-rp 12921  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-dvds 16142
This theorem is referenced by:  bezoutlem4  16428
  Copyright terms: Public domain W3C validator