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

Theorem bezoutlemmain 12001
Description: Lemma for Bรฉzout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.)
Hypotheses
Ref Expression
bezout.is-bezout (๐œ‘ โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
bezout.sub-gcd (๐œ“ โ†” โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ)))
bezout.a (๐œƒ โ†’ ๐ด โˆˆ โ„•0)
bezout.b (๐œƒ โ†’ ๐ต โˆˆ โ„•0)
Assertion
Ref Expression
bezoutlemmain (๐œƒ โ†’ โˆ€๐‘ฅ โˆˆ โ„•0 ([๐‘ฅ / ๐‘Ÿ]๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 (๐œ“ โˆง ๐œ‘))))
Distinct variable groups:   ๐œ‘,๐‘ ,๐‘ก,๐‘ฅ,๐‘ฆ,๐‘ง   ๐œ“,๐‘ ,๐‘ก,๐‘ง   ๐‘ ,๐‘Ÿ,๐‘ก,๐‘ฅ,๐‘ฆ,๐‘ง,๐œƒ   ๐ด,๐‘Ÿ,๐‘ ,๐‘ก   ๐ต,๐‘Ÿ,๐‘ ,๐‘ก
Allowed substitution hints:   ๐œ‘(๐‘Ÿ)   ๐œ“(๐‘ฅ,๐‘ฆ,๐‘Ÿ)   ๐ด(๐‘ฅ,๐‘ฆ,๐‘ง)   ๐ต(๐‘ฅ,๐‘ฆ,๐‘ง)

Proof of Theorem bezoutlemmain
Dummy variables ๐‘Ž ๐‘ค are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sbequ 1840 . . . . . . 7 (๐‘ค = ๐‘ง โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†” [๐‘ง / ๐‘Ÿ]๐œ‘))
21anbi2d 464 . . . . . 6 (๐‘ค = ๐‘ง โ†’ ((๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘) โ†” (๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘)))
3 sbequ 1840 . . . . . . . . . 10 (๐‘ค = ๐‘ง โ†’ ([๐‘ค / ๐‘ฅ]๐œ“ โ†” [๐‘ง / ๐‘ฅ]๐œ“))
43anbi1d 465 . . . . . . . . 9 (๐‘ค = ๐‘ง โ†’ (([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘) โ†” ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
54rexbidv 2478 . . . . . . . 8 (๐‘ค = ๐‘ง โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘) โ†” โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
65imbi2d 230 . . . . . . 7 (๐‘ค = ๐‘ง โ†’ (([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)) โ†” ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))))
76ralbidv 2477 . . . . . 6 (๐‘ค = ๐‘ง โ†’ (โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)) โ†” โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))))
82, 7imbi12d 234 . . . . 5 (๐‘ค = ๐‘ง โ†’ (((๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘))) โ†” ((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))))
9 sbequ 1840 . . . . . . 7 (๐‘ค = ๐‘ฅ โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†” [๐‘ฅ / ๐‘Ÿ]๐œ‘))
109anbi2d 464 . . . . . 6 (๐‘ค = ๐‘ฅ โ†’ ((๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘) โ†” (๐œƒ โˆง [๐‘ฅ / ๐‘Ÿ]๐œ‘)))
11 sbequ12r 1772 . . . . . . . . . 10 (๐‘ค = ๐‘ฅ โ†’ ([๐‘ค / ๐‘ฅ]๐œ“ โ†” ๐œ“))
1211anbi1d 465 . . . . . . . . 9 (๐‘ค = ๐‘ฅ โ†’ (([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘) โ†” (๐œ“ โˆง ๐œ‘)))
1312rexbidv 2478 . . . . . . . 8 (๐‘ค = ๐‘ฅ โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘) โ†” โˆƒ๐‘Ÿ โˆˆ โ„•0 (๐œ“ โˆง ๐œ‘)))
1413imbi2d 230 . . . . . . 7 (๐‘ค = ๐‘ฅ โ†’ (([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)) โ†” ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 (๐œ“ โˆง ๐œ‘))))
1514ralbidv 2477 . . . . . 6 (๐‘ค = ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)) โ†” โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 (๐œ“ โˆง ๐œ‘))))
1610, 15imbi12d 234 . . . . 5 (๐‘ค = ๐‘ฅ โ†’ (((๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘))) โ†” ((๐œƒ โˆง [๐‘ฅ / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 (๐œ“ โˆง ๐œ‘)))))
17 nfv 1528 . . . . . . . . . . 11 โ„ฒ๐‘ฆ ๐‘ค โˆˆ โ„•0
18 nfcv 2319 . . . . . . . . . . . 12 โ„ฒ๐‘ฆ(0...(๐‘ค โˆ’ 1))
19 nfv 1528 . . . . . . . . . . . . 13 โ„ฒ๐‘ฆ(๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘)
20 nfra1 2508 . . . . . . . . . . . . 13 โ„ฒ๐‘ฆโˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
2119, 20nfim 1572 . . . . . . . . . . . 12 โ„ฒ๐‘ฆ((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
2218, 21nfralxy 2515 . . . . . . . . . . 11 โ„ฒ๐‘ฆโˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
2317, 22nfan 1565 . . . . . . . . . 10 โ„ฒ๐‘ฆ(๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))))
24 nfv 1528 . . . . . . . . . 10 โ„ฒ๐‘ฆ(๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)
2523, 24nfan 1565 . . . . . . . . 9 โ„ฒ๐‘ฆ((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘))
26 nfv 1528 . . . . . . . . 9 โ„ฒ๐‘ฆ ๐‘ค = 0
2725, 26nfan 1565 . . . . . . . 8 โ„ฒ๐‘ฆ(((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง ๐‘ค = 0)
28 simplr 528 . . . . . . . . . 10 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง ๐‘ค = 0) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ ๐‘ฆ โˆˆ โ„•0)
29 nfv 1528 . . . . . . . . . . . . . 14 โ„ฒ๐‘Ÿโˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘ฆ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ))
30 breq2 4009 . . . . . . . . . . . . . . . 16 (๐‘Ÿ = ๐‘ฆ โ†’ (๐‘ง โˆฅ ๐‘Ÿ โ†” ๐‘ง โˆฅ ๐‘ฆ))
3130imbi1d 231 . . . . . . . . . . . . . . 15 (๐‘Ÿ = ๐‘ฆ โ†’ ((๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ)) โ†” (๐‘ง โˆฅ ๐‘ฆ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ))))
3231ralbidv 2477 . . . . . . . . . . . . . 14 (๐‘Ÿ = ๐‘ฆ โ†’ (โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ)) โ†” โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘ฆ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ))))
3329, 32sbie 1791 . . . . . . . . . . . . 13 ([๐‘ฆ / ๐‘Ÿ]โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ)) โ†” โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘ฆ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ)))
34 nn0z 9275 . . . . . . . . . . . . . . . 16 (๐‘ง โˆˆ โ„•0 โ†’ ๐‘ง โˆˆ โ„ค)
35 dvds0 11815 . . . . . . . . . . . . . . . 16 (๐‘ง โˆˆ โ„ค โ†’ ๐‘ง โˆฅ 0)
3634, 35syl 14 . . . . . . . . . . . . . . 15 (๐‘ง โˆˆ โ„•0 โ†’ ๐‘ง โˆฅ 0)
3736biantrurd 305 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ โ„•0 โ†’ (๐‘ง โˆฅ ๐‘ฆ โ†” (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ)))
3837biimpd 144 . . . . . . . . . . . . 13 (๐‘ง โˆˆ โ„•0 โ†’ (๐‘ง โˆฅ ๐‘ฆ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ)))
3933, 38mprgbir 2535 . . . . . . . . . . . 12 [๐‘ฆ / ๐‘Ÿ]โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ))
40 nfv 1528 . . . . . . . . . . . . 13 โ„ฒ๐‘Ÿ ๐‘ค = 0
41 dfsbcq2 2967 . . . . . . . . . . . . . 14 (๐‘ค = 0 โ†’ ([๐‘ค / ๐‘ฅ]๐œ“ โ†” [0 / ๐‘ฅ]๐œ“))
42 bezout.sub-gcd . . . . . . . . . . . . . . . 16 (๐œ“ โ†” โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ)))
4342sbcbii 3024 . . . . . . . . . . . . . . 15 ([0 / ๐‘ฅ]๐œ“ โ†” [0 / ๐‘ฅ]โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ)))
44 c0ex 7953 . . . . . . . . . . . . . . . 16 0 โˆˆ V
45 breq2 4009 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = 0 โ†’ (๐‘ง โˆฅ ๐‘ฅ โ†” ๐‘ง โˆฅ 0))
4645anbi1d 465 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = 0 โ†’ ((๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ) โ†” (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ)))
4746imbi2d 230 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = 0 โ†’ ((๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ)) โ†” (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ))))
4847ralbidv 2477 . . . . . . . . . . . . . . . 16 (๐‘ฅ = 0 โ†’ (โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ)) โ†” โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ))))
4944, 48sbcie 2999 . . . . . . . . . . . . . . 15 ([0 / ๐‘ฅ]โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ)) โ†” โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ)))
5043, 49bitri 184 . . . . . . . . . . . . . 14 ([0 / ๐‘ฅ]๐œ“ โ†” โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ)))
5141, 50bitrdi 196 . . . . . . . . . . . . 13 (๐‘ค = 0 โ†’ ([๐‘ค / ๐‘ฅ]๐œ“ โ†” โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ))))
5240, 51sbbid 1846 . . . . . . . . . . . 12 (๐‘ค = 0 โ†’ ([๐‘ฆ / ๐‘Ÿ][๐‘ค / ๐‘ฅ]๐œ“ โ†” [๐‘ฆ / ๐‘Ÿ]โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ 0 โˆง ๐‘ง โˆฅ ๐‘ฆ))))
5339, 52mpbiri 168 . . . . . . . . . . 11 (๐‘ค = 0 โ†’ [๐‘ฆ / ๐‘Ÿ][๐‘ค / ๐‘ฅ]๐œ“)
5453ad3antlr 493 . . . . . . . . . 10 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง ๐‘ค = 0) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ [๐‘ฆ / ๐‘Ÿ][๐‘ค / ๐‘ฅ]๐œ“)
55 simpr 110 . . . . . . . . . 10 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง ๐‘ค = 0) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ [๐‘ฆ / ๐‘Ÿ]๐œ‘)
56 nfs1v 1939 . . . . . . . . . . . 12 โ„ฒ๐‘Ÿ[๐‘ฆ / ๐‘Ÿ][๐‘ค / ๐‘ฅ]๐œ“
57 nfs1v 1939 . . . . . . . . . . . 12 โ„ฒ๐‘Ÿ[๐‘ฆ / ๐‘Ÿ]๐œ‘
5856, 57nfan 1565 . . . . . . . . . . 11 โ„ฒ๐‘Ÿ([๐‘ฆ / ๐‘Ÿ][๐‘ค / ๐‘ฅ]๐œ“ โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘)
59 sbequ12 1771 . . . . . . . . . . . 12 (๐‘Ÿ = ๐‘ฆ โ†’ ([๐‘ค / ๐‘ฅ]๐œ“ โ†” [๐‘ฆ / ๐‘Ÿ][๐‘ค / ๐‘ฅ]๐œ“))
60 sbequ12 1771 . . . . . . . . . . . 12 (๐‘Ÿ = ๐‘ฆ โ†’ (๐œ‘ โ†” [๐‘ฆ / ๐‘Ÿ]๐œ‘))
6159, 60anbi12d 473 . . . . . . . . . . 11 (๐‘Ÿ = ๐‘ฆ โ†’ (([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘) โ†” ([๐‘ฆ / ๐‘Ÿ][๐‘ค / ๐‘ฅ]๐œ“ โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘)))
6258, 61rspce 2838 . . . . . . . . . 10 ((๐‘ฆ โˆˆ โ„•0 โˆง ([๐‘ฆ / ๐‘Ÿ][๐‘ค / ๐‘ฅ]๐œ“ โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
6328, 54, 55, 62syl12anc 1236 . . . . . . . . 9 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง ๐‘ค = 0) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
6463exp31 364 . . . . . . . 8 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง ๐‘ค = 0) โ†’ (๐‘ฆ โˆˆ โ„•0 โ†’ ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘))))
6527, 64ralrimi 2548 . . . . . . 7 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง ๐‘ค = 0) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
66 nfv 1528 . . . . . . . . . 10 โ„ฒ๐‘ฆ0 < ๐‘ค
6725, 66nfan 1565 . . . . . . . . 9 โ„ฒ๐‘ฆ(((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค)
68 bezout.is-bezout . . . . . . . . . . 11 (๐œ‘ โ†” โˆƒ๐‘  โˆˆ โ„ค โˆƒ๐‘ก โˆˆ โ„ค ๐‘Ÿ = ((๐ด ยท ๐‘ ) + (๐ต ยท ๐‘ก)))
69 simplrl 535 . . . . . . . . . . . . 13 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ ๐œƒ)
70 bezout.a . . . . . . . . . . . . 13 (๐œƒ โ†’ ๐ด โˆˆ โ„•0)
7169, 70syl 14 . . . . . . . . . . . 12 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ ๐ด โˆˆ โ„•0)
7271ad2antrr 488 . . . . . . . . . . 11 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ ๐ด โˆˆ โ„•0)
73 bezout.b . . . . . . . . . . . . 13 (๐œƒ โ†’ ๐ต โˆˆ โ„•0)
7469, 73syl 14 . . . . . . . . . . . 12 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ ๐ต โˆˆ โ„•0)
7574ad2antrr 488 . . . . . . . . . . 11 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ ๐ต โˆˆ โ„•0)
76 simplll 533 . . . . . . . . . . . . 13 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ ๐‘ค โˆˆ โ„•0)
77 simpr 110 . . . . . . . . . . . . 13 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ 0 < ๐‘ค)
78 elnnnn0b 9222 . . . . . . . . . . . . 13 (๐‘ค โˆˆ โ„• โ†” (๐‘ค โˆˆ โ„•0 โˆง 0 < ๐‘ค))
7976, 77, 78sylanbrc 417 . . . . . . . . . . . 12 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ ๐‘ค โˆˆ โ„•)
8079ad2antrr 488 . . . . . . . . . . 11 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ ๐‘ค โˆˆ โ„•)
81 simpr 110 . . . . . . . . . . 11 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ [๐‘ฆ / ๐‘Ÿ]๐œ‘)
82 simplr 528 . . . . . . . . . . 11 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ ๐‘ฆ โˆˆ โ„•0)
83 simplrr 536 . . . . . . . . . . . . 13 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ [๐‘ค / ๐‘Ÿ]๐œ‘)
84 sbsbc 2968 . . . . . . . . . . . . 13 ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†” [๐‘ค / ๐‘Ÿ]๐œ‘)
8583, 84sylib 122 . . . . . . . . . . . 12 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ [๐‘ค / ๐‘Ÿ]๐œ‘)
8685ad2antrr 488 . . . . . . . . . . 11 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ [๐‘ค / ๐‘Ÿ]๐œ‘)
87 breq1 4008 . . . . . . . . . . . . . 14 (๐‘ง = ๐‘Ž โ†’ (๐‘ง โˆฅ ๐‘Ÿ โ†” ๐‘Ž โˆฅ ๐‘Ÿ))
88 breq1 4008 . . . . . . . . . . . . . . 15 (๐‘ง = ๐‘Ž โ†’ (๐‘ง โˆฅ ๐‘ฅ โ†” ๐‘Ž โˆฅ ๐‘ฅ))
89 breq1 4008 . . . . . . . . . . . . . . 15 (๐‘ง = ๐‘Ž โ†’ (๐‘ง โˆฅ ๐‘ฆ โ†” ๐‘Ž โˆฅ ๐‘ฆ))
9088, 89anbi12d 473 . . . . . . . . . . . . . 14 (๐‘ง = ๐‘Ž โ†’ ((๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ) โ†” (๐‘Ž โˆฅ ๐‘ฅ โˆง ๐‘Ž โˆฅ ๐‘ฆ)))
9187, 90imbi12d 234 . . . . . . . . . . . . 13 (๐‘ง = ๐‘Ž โ†’ ((๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ)) โ†” (๐‘Ž โˆฅ ๐‘Ÿ โ†’ (๐‘Ž โˆฅ ๐‘ฅ โˆง ๐‘Ž โˆฅ ๐‘ฆ))))
9291cbvralv 2705 . . . . . . . . . . . 12 (โˆ€๐‘ง โˆˆ โ„•0 (๐‘ง โˆฅ ๐‘Ÿ โ†’ (๐‘ง โˆฅ ๐‘ฅ โˆง ๐‘ง โˆฅ ๐‘ฆ)) โ†” โˆ€๐‘Ž โˆˆ โ„•0 (๐‘Ž โˆฅ ๐‘Ÿ โ†’ (๐‘Ž โˆฅ ๐‘ฅ โˆง ๐‘Ž โˆฅ ๐‘ฆ)))
9342, 92bitri 184 . . . . . . . . . . 11 (๐œ“ โ†” โˆ€๐‘Ž โˆˆ โ„•0 (๐‘Ž โˆฅ ๐‘Ÿ โ†’ (๐‘Ž โˆฅ ๐‘ฅ โˆง ๐‘Ž โˆฅ ๐‘ฆ)))
9469ad3antrrr 492 . . . . . . . . . . . . 13 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ ๐œƒ)
95 simpr 110 . . . . . . . . . . . . 13 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘)
9694, 95jca 306 . . . . . . . . . . . 12 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ (๐œƒ โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘))
9783ad3antrrr 492 . . . . . . . . . . . 12 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ [๐‘ค / ๐‘Ÿ]๐œ‘)
98 dfsbcq2 2967 . . . . . . . . . . . . . . 15 (๐‘ง = (๐‘ฆ mod ๐‘ค) โ†’ ([๐‘ง / ๐‘Ÿ]๐œ‘ โ†” [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘))
9998anbi2d 464 . . . . . . . . . . . . . 14 (๐‘ง = (๐‘ฆ mod ๐‘ค) โ†’ ((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†” (๐œƒ โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘)))
100 sbsbc 2968 . . . . . . . . . . . . . . . . . . 19 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โ†” [๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“)
101 sbsbc 2968 . . . . . . . . . . . . . . . . . . . 20 ([๐‘ค / ๐‘ฆ]๐œ“ โ†” [๐‘ค / ๐‘ฆ]๐œ“)
102101sbcbii 3024 . . . . . . . . . . . . . . . . . . 19 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โ†” [๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“)
103100, 102bitri 184 . . . . . . . . . . . . . . . . . 18 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โ†” [๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“)
104103anbi1i 458 . . . . . . . . . . . . . . . . 17 (([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘) โ†” ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))
105 dfsbcq 2966 . . . . . . . . . . . . . . . . . 18 (๐‘ง = (๐‘ฆ mod ๐‘ค) โ†’ ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โ†” [(๐‘ฆ mod ๐‘ค) / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“))
106105anbi1d 465 . . . . . . . . . . . . . . . . 17 (๐‘ง = (๐‘ฆ mod ๐‘ค) โ†’ (([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘) โ†” ([(๐‘ฆ mod ๐‘ค) / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)))
107104, 106bitrid 192 . . . . . . . . . . . . . . . 16 (๐‘ง = (๐‘ฆ mod ๐‘ค) โ†’ (([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘) โ†” ([(๐‘ฆ mod ๐‘ค) / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)))
108107rexbidv 2478 . . . . . . . . . . . . . . 15 (๐‘ง = (๐‘ฆ mod ๐‘ค) โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘) โ†” โˆƒ๐‘Ÿ โˆˆ โ„•0 ([(๐‘ฆ mod ๐‘ค) / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)))
109108imbi2d 230 . . . . . . . . . . . . . 14 (๐‘ง = (๐‘ฆ mod ๐‘ค) โ†’ (([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)) โ†” ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([(๐‘ฆ mod ๐‘ค) / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))))
11099, 109imbi12d 234 . . . . . . . . . . . . 13 (๐‘ง = (๐‘ฆ mod ๐‘ค) โ†’ (((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))) โ†” ((๐œƒ โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([(๐‘ฆ mod ๐‘ค) / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)))))
111 simpll 527 . . . . . . . . . . . . . 14 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ (((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค))
112 simpr 110 . . . . . . . . . . . . . . . 16 ((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โ†’ โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))))
113112ad3antrrr 492 . . . . . . . . . . . . . . 15 (((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))))
114 nfv 1528 . . . . . . . . . . . . . . . . . . . 20 โ„ฒ๐‘ฆ[๐‘ค / ๐‘Ÿ]๐œ‘
115 nfcv 2319 . . . . . . . . . . . . . . . . . . . . 21 โ„ฒ๐‘ฆโ„•0
116 nfs1v 1939 . . . . . . . . . . . . . . . . . . . . . . 23 โ„ฒ๐‘ฆ[๐‘ค / ๐‘ฆ]๐œ“
117116nfsbxy 1942 . . . . . . . . . . . . . . . . . . . . . 22 โ„ฒ๐‘ฆ[๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“
118 nfv 1528 . . . . . . . . . . . . . . . . . . . . . 22 โ„ฒ๐‘ฆ๐œ‘
119117, 118nfan 1565 . . . . . . . . . . . . . . . . . . . . 21 โ„ฒ๐‘ฆ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)
120115, 119nfrexxy 2516 . . . . . . . . . . . . . . . . . . . 20 โ„ฒ๐‘ฆโˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)
121114, 120nfim 1572 . . . . . . . . . . . . . . . . . . 19 โ„ฒ๐‘ฆ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))
122 sbequ 1840 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ = ๐‘ค โ†’ ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†” [๐‘ค / ๐‘Ÿ]๐œ‘))
123 nfv 1528 . . . . . . . . . . . . . . . . . . . . . . 23 โ„ฒ๐‘ฅ ๐‘ฆ = ๐‘ค
124 sbequ12 1771 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ = ๐‘ค โ†’ (๐œ“ โ†” [๐‘ค / ๐‘ฆ]๐œ“))
125123, 124sbbid 1846 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ = ๐‘ค โ†’ ([๐‘ง / ๐‘ฅ]๐œ“ โ†” [๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“))
126125anbi1d 465 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ = ๐‘ค โ†’ (([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘) โ†” ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)))
127126rexbidv 2478 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ = ๐‘ค โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘) โ†” โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)))
128122, 127imbi12d 234 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ = ๐‘ค โ†’ (([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)) โ†” ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))))
129121, 128rspc 2837 . . . . . . . . . . . . . . . . . 18 (๐‘ค โˆˆ โ„•0 โ†’ (โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)) โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))))
130129imim2d 54 . . . . . . . . . . . . . . . . 17 (๐‘ค โˆˆ โ„•0 โ†’ (((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))) โ†’ ((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)))))
131130ralimdv 2545 . . . . . . . . . . . . . . . 16 (๐‘ค โˆˆ โ„•0 โ†’ (โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))) โ†’ โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)))))
132131ad4antr 494 . . . . . . . . . . . . . . 15 (((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ (โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))) โ†’ โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘)))))
133113, 132mpd 13 . . . . . . . . . . . . . 14 (((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))))
134111, 133sylan 283 . . . . . . . . . . . . 13 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))))
135 simpllr 534 . . . . . . . . . . . . . . 15 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ ๐‘ฆ โˆˆ โ„•0)
136135nn0zd 9375 . . . . . . . . . . . . . 14 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ ๐‘ฆ โˆˆ โ„ค)
13779ad3antrrr 492 . . . . . . . . . . . . . 14 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ ๐‘ค โˆˆ โ„•)
138 zmodfz 10348 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆˆ โ„ค โˆง ๐‘ค โˆˆ โ„•) โ†’ (๐‘ฆ mod ๐‘ค) โˆˆ (0...(๐‘ค โˆ’ 1)))
139136, 137, 138syl2anc 411 . . . . . . . . . . . . 13 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ (๐‘ฆ mod ๐‘ค) โˆˆ (0...(๐‘ค โˆ’ 1)))
140110, 134, 139rspcdva 2848 . . . . . . . . . . . 12 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ ((๐œƒ โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ ([๐‘ค / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([(๐‘ฆ mod ๐‘ค) / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))))
14196, 97, 140mp2d 47 . . . . . . . . . . 11 (((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โˆง [(๐‘ฆ mod ๐‘ค) / ๐‘Ÿ]๐œ‘) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([(๐‘ฆ mod ๐‘ค) / ๐‘ฅ][๐‘ค / ๐‘ฆ]๐œ“ โˆง ๐œ‘))
142 nfv 1528 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘ฅ ๐‘ค โˆˆ โ„•0
143 nfcv 2319 . . . . . . . . . . . . . . . . 17 โ„ฒ๐‘ฅ(0...(๐‘ค โˆ’ 1))
144 nfv 1528 . . . . . . . . . . . . . . . . . 18 โ„ฒ๐‘ฅ(๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘)
145 nfcv 2319 . . . . . . . . . . . . . . . . . . 19 โ„ฒ๐‘ฅโ„•0
146 nfv 1528 . . . . . . . . . . . . . . . . . . . . 21 โ„ฒ๐‘ฅ๐œ‘
147146nfsbxy 1942 . . . . . . . . . . . . . . . . . . . 20 โ„ฒ๐‘ฅ[๐‘ฆ / ๐‘Ÿ]๐œ‘
148 nfs1v 1939 . . . . . . . . . . . . . . . . . . . . . 22 โ„ฒ๐‘ฅ[๐‘ง / ๐‘ฅ]๐œ“
149148, 146nfan 1565 . . . . . . . . . . . . . . . . . . . . 21 โ„ฒ๐‘ฅ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)
150145, 149nfrexxy 2516 . . . . . . . . . . . . . . . . . . . 20 โ„ฒ๐‘ฅโˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)
151147, 150nfim 1572 . . . . . . . . . . . . . . . . . . 19 โ„ฒ๐‘ฅ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
152145, 151nfralxy 2515 . . . . . . . . . . . . . . . . . 18 โ„ฒ๐‘ฅโˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
153144, 152nfim 1572 . . . . . . . . . . . . . . . . 17 โ„ฒ๐‘ฅ((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
154143, 153nfralxy 2515 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘ฅโˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
155142, 154nfan 1565 . . . . . . . . . . . . . . 15 โ„ฒ๐‘ฅ(๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))))
156 nfv 1528 . . . . . . . . . . . . . . 15 โ„ฒ๐‘ฅ(๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)
157155, 156nfan 1565 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฅ((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘))
158 nfv 1528 . . . . . . . . . . . . . 14 โ„ฒ๐‘ฅ0 < ๐‘ค
159157, 158nfan 1565 . . . . . . . . . . . . 13 โ„ฒ๐‘ฅ(((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค)
160 nfv 1528 . . . . . . . . . . . . 13 โ„ฒ๐‘ฅ ๐‘ฆ โˆˆ โ„•0
161159, 160nfan 1565 . . . . . . . . . . . 12 โ„ฒ๐‘ฅ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0)
162161, 147nfan 1565 . . . . . . . . . . 11 โ„ฒ๐‘ฅ(((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘)
163 nfv 1528 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘Ÿ ๐‘ค โˆˆ โ„•0
164 nfcv 2319 . . . . . . . . . . . . . . . . 17 โ„ฒ๐‘Ÿ(0...(๐‘ค โˆ’ 1))
165 nfv 1528 . . . . . . . . . . . . . . . . . . 19 โ„ฒ๐‘Ÿ๐œƒ
166 nfs1v 1939 . . . . . . . . . . . . . . . . . . 19 โ„ฒ๐‘Ÿ[๐‘ง / ๐‘Ÿ]๐œ‘
167165, 166nfan 1565 . . . . . . . . . . . . . . . . . 18 โ„ฒ๐‘Ÿ(๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘)
168 nfcv 2319 . . . . . . . . . . . . . . . . . . 19 โ„ฒ๐‘Ÿโ„•0
169 nfre1 2520 . . . . . . . . . . . . . . . . . . . 20 โ„ฒ๐‘Ÿโˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)
17057, 169nfim 1572 . . . . . . . . . . . . . . . . . . 19 โ„ฒ๐‘Ÿ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
171168, 170nfralxy 2515 . . . . . . . . . . . . . . . . . 18 โ„ฒ๐‘Ÿโˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
172167, 171nfim 1572 . . . . . . . . . . . . . . . . 17 โ„ฒ๐‘Ÿ((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
173164, 172nfralxy 2515 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘Ÿโˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
174163, 173nfan 1565 . . . . . . . . . . . . . . 15 โ„ฒ๐‘Ÿ(๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))))
175 nfs1v 1939 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘Ÿ[๐‘ค / ๐‘Ÿ]๐œ‘
176165, 175nfan 1565 . . . . . . . . . . . . . . 15 โ„ฒ๐‘Ÿ(๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)
177174, 176nfan 1565 . . . . . . . . . . . . . 14 โ„ฒ๐‘Ÿ((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘))
178 nfv 1528 . . . . . . . . . . . . . 14 โ„ฒ๐‘Ÿ0 < ๐‘ค
179177, 178nfan 1565 . . . . . . . . . . . . 13 โ„ฒ๐‘Ÿ(((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค)
180 nfv 1528 . . . . . . . . . . . . 13 โ„ฒ๐‘Ÿ ๐‘ฆ โˆˆ โ„•0
181179, 180nfan 1565 . . . . . . . . . . . 12 โ„ฒ๐‘Ÿ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0)
182181, 57nfan 1565 . . . . . . . . . . 11 โ„ฒ๐‘Ÿ(((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘)
18368, 72, 75, 80, 81, 82, 86, 93, 141, 162, 182bezoutlemstep 12000 . . . . . . . . . 10 ((((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง [๐‘ฆ / ๐‘Ÿ]๐œ‘) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
184183exp31 364 . . . . . . . . 9 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ (๐‘ฆ โˆˆ โ„•0 โ†’ ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘))))
18567, 184ralrimi 2548 . . . . . . . 8 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
186 sbsbc 2968 . . . . . . . . . . . 12 ([๐‘ค / ๐‘ฅ]๐œ“ โ†” [๐‘ค / ๐‘ฅ]๐œ“)
187186anbi1i 458 . . . . . . . . . . 11 (([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘) โ†” ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
188187rexbii 2484 . . . . . . . . . 10 (โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘) โ†” โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘))
189188imbi2i 226 . . . . . . . . 9 (([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)) โ†” ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
190189ralbii 2483 . . . . . . . 8 (โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)) โ†” โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
191185, 190sylibr 134 . . . . . . 7 ((((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โˆง 0 < ๐‘ค) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
192 nn0nlt0 9204 . . . . . . . . 9 (๐‘ค โˆˆ โ„•0 โ†’ ยฌ ๐‘ค < 0)
193 nn0z 9275 . . . . . . . . . . . 12 (๐‘ค โˆˆ โ„•0 โ†’ ๐‘ค โˆˆ โ„ค)
194 ztri3or0 9297 . . . . . . . . . . . 12 (๐‘ค โˆˆ โ„ค โ†’ (๐‘ค < 0 โˆจ ๐‘ค = 0 โˆจ 0 < ๐‘ค))
195193, 194syl 14 . . . . . . . . . . 11 (๐‘ค โˆˆ โ„•0 โ†’ (๐‘ค < 0 โˆจ ๐‘ค = 0 โˆจ 0 < ๐‘ค))
196 3orass 981 . . . . . . . . . . 11 ((๐‘ค < 0 โˆจ ๐‘ค = 0 โˆจ 0 < ๐‘ค) โ†” (๐‘ค < 0 โˆจ (๐‘ค = 0 โˆจ 0 < ๐‘ค)))
197195, 196sylib 122 . . . . . . . . . 10 (๐‘ค โˆˆ โ„•0 โ†’ (๐‘ค < 0 โˆจ (๐‘ค = 0 โˆจ 0 < ๐‘ค)))
198197orcomd 729 . . . . . . . . 9 (๐‘ค โˆˆ โ„•0 โ†’ ((๐‘ค = 0 โˆจ 0 < ๐‘ค) โˆจ ๐‘ค < 0))
199192, 198ecased 1349 . . . . . . . 8 (๐‘ค โˆˆ โ„•0 โ†’ (๐‘ค = 0 โˆจ 0 < ๐‘ค))
200199ad2antrr 488 . . . . . . 7 (((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โ†’ (๐‘ค = 0 โˆจ 0 < ๐‘ค))
20165, 191, 200mpjaodan 798 . . . . . 6 (((๐‘ค โˆˆ โ„•0 โˆง โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))) โˆง (๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘)) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))
202201exp31 364 . . . . 5 (๐‘ค โˆˆ โ„•0 โ†’ (โˆ€๐‘ง โˆˆ (0...(๐‘ค โˆ’ 1))((๐œƒ โˆง [๐‘ง / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ง / ๐‘ฅ]๐œ“ โˆง ๐œ‘))) โ†’ ((๐œƒ โˆง [๐‘ค / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 ([๐‘ค / ๐‘ฅ]๐œ“ โˆง ๐œ‘)))))
2038, 16, 202nn0sinds 10446 . . . 4 (๐‘ฅ โˆˆ โ„•0 โ†’ ((๐œƒ โˆง [๐‘ฅ / ๐‘Ÿ]๐œ‘) โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 (๐œ“ โˆง ๐œ‘))))
204203expd 258 . . 3 (๐‘ฅ โˆˆ โ„•0 โ†’ (๐œƒ โ†’ ([๐‘ฅ / ๐‘Ÿ]๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 (๐œ“ โˆง ๐œ‘)))))
205204impcom 125 . 2 ((๐œƒ โˆง ๐‘ฅ โˆˆ โ„•0) โ†’ ([๐‘ฅ / ๐‘Ÿ]๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 (๐œ“ โˆง ๐œ‘))))
206205ralrimiva 2550 1 (๐œƒ โ†’ โˆ€๐‘ฅ โˆˆ โ„•0 ([๐‘ฅ / ๐‘Ÿ]๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ โ„•0 ([๐‘ฆ / ๐‘Ÿ]๐œ‘ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„•0 (๐œ“ โˆง ๐œ‘))))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 708   โˆจ w3o 977   = wceq 1353  [wsb 1762   โˆˆ wcel 2148  โˆ€wral 2455  โˆƒwrex 2456  [wsbc 2964   class class class wbr 4005  (class class class)co 5877  0cc0 7813  1c1 7814   + caddc 7816   ยท cmul 7818   < clt 7994   โˆ’ cmin 8130  โ„•cn 8921  โ„•0cn0 9178  โ„คcz 9255  ...cfz 10010   mod cmo 10324   โˆฅ cdvds 11796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-mulrcl 7912  ax-addcom 7913  ax-mulcom 7914  ax-addass 7915  ax-mulass 7916  ax-distr 7917  ax-i2m1 7918  ax-0lt1 7919  ax-1rid 7920  ax-0id 7921  ax-rnegex 7922  ax-precex 7923  ax-cnre 7924  ax-pre-ltirr 7925  ax-pre-ltwlin 7926  ax-pre-lttrn 7927  ax-pre-apti 7928  ax-pre-ltadd 7929  ax-pre-mulgt0 7930  ax-pre-mulext 7931  ax-arch 7932
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-recs 6308  df-frec 6394  df-pnf 7996  df-mnf 7997  df-xr 7998  df-ltxr 7999  df-le 8000  df-sub 8132  df-neg 8133  df-reap 8534  df-ap 8541  df-div 8632  df-inn 8922  df-2 8980  df-n0 9179  df-z 9256  df-uz 9531  df-q 9622  df-rp 9656  df-fz 10011  df-fl 10272  df-mod 10325  df-seqfrec 10448  df-exp 10522  df-cj 10853  df-re 10854  df-im 10855  df-rsqrt 11009  df-abs 11010  df-dvds 11797
This theorem is referenced by:  bezoutlemex  12004
  Copyright terms: Public domain W3C validator