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

Theorem phimullem 16712
Description: Lemma for phimul 16713. (Contributed by Mario Carneiro, 24-Feb-2014.)
Hypotheses
Ref Expression
crth.1 ๐‘† = (0..^(๐‘€ ยท ๐‘))
crth.2 ๐‘‡ = ((0..^๐‘€) ร— (0..^๐‘))
crth.3 ๐น = (๐‘ฅ โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ)
crth.4 (๐œ‘ โ†’ (๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• โˆง (๐‘€ gcd ๐‘) = 1))
phimul.4 ๐‘ˆ = {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1}
phimul.5 ๐‘‰ = {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1}
phimul.6 ๐‘Š = {๐‘ฆ โˆˆ ๐‘† โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
Assertion
Ref Expression
phimullem (๐œ‘ โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = ((ฯ•โ€˜๐‘€) ยท (ฯ•โ€˜๐‘)))
Distinct variable groups:   ๐‘ฆ,๐น   ๐‘ฅ,๐‘ฆ,๐‘€   ๐œ‘,๐‘ฅ,๐‘ฆ   ๐‘ฅ,๐‘†,๐‘ฆ   ๐‘ฅ,๐‘‡   ๐‘ฅ,๐‘,๐‘ฆ
Allowed substitution hints:   ๐‘‡(๐‘ฆ)   ๐‘ˆ(๐‘ฅ,๐‘ฆ)   ๐น(๐‘ฅ)   ๐‘‰(๐‘ฅ,๐‘ฆ)   ๐‘Š(๐‘ฅ,๐‘ฆ)

Proof of Theorem phimullem
Dummy variables ๐‘ค ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7416 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ค โ†’ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = (๐‘ค gcd (๐‘€ ยท ๐‘)))
21eqeq1d 2735 . . . . . . . . . . . . 13 (๐‘ฆ = ๐‘ค โ†’ ((๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1 โ†” (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1))
3 phimul.6 . . . . . . . . . . . . 13 ๐‘Š = {๐‘ฆ โˆˆ ๐‘† โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
42, 3elrab2 3687 . . . . . . . . . . . 12 (๐‘ค โˆˆ ๐‘Š โ†” (๐‘ค โˆˆ ๐‘† โˆง (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1))
54simplbi 499 . . . . . . . . . . 11 (๐‘ค โˆˆ ๐‘Š โ†’ ๐‘ค โˆˆ ๐‘†)
6 oveq1 7416 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ค โ†’ (๐‘ฅ mod ๐‘€) = (๐‘ค mod ๐‘€))
7 oveq1 7416 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ค โ†’ (๐‘ฅ mod ๐‘) = (๐‘ค mod ๐‘))
86, 7opeq12d 4882 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ค โ†’ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
9 crth.3 . . . . . . . . . . . 12 ๐น = (๐‘ฅ โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ)
10 opex 5465 . . . . . . . . . . . 12 โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ โˆˆ V
118, 9, 10fvmpt 6999 . . . . . . . . . . 11 (๐‘ค โˆˆ ๐‘† โ†’ (๐นโ€˜๐‘ค) = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
125, 11syl 17 . . . . . . . . . 10 (๐‘ค โˆˆ ๐‘Š โ†’ (๐นโ€˜๐‘ค) = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
1312adantl 483 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐นโ€˜๐‘ค) = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
14 crth.1 . . . . . . . . . . . . . . 15 ๐‘† = (0..^(๐‘€ ยท ๐‘))
155, 14eleqtrdi 2844 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ ๐‘Š โ†’ ๐‘ค โˆˆ (0..^(๐‘€ ยท ๐‘)))
1615adantl 483 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ค โˆˆ (0..^(๐‘€ ยท ๐‘)))
17 elfzoelz 13632 . . . . . . . . . . . . 13 (๐‘ค โˆˆ (0..^(๐‘€ ยท ๐‘)) โ†’ ๐‘ค โˆˆ โ„ค)
1816, 17syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ค โˆˆ โ„ค)
19 crth.4 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• โˆง (๐‘€ gcd ๐‘) = 1))
2019simp1d 1143 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
2120adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘€ โˆˆ โ„•)
22 zmodfzo 13859 . . . . . . . . . . . 12 ((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•) โ†’ (๐‘ค mod ๐‘€) โˆˆ (0..^๐‘€))
2318, 21, 22syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘€) โˆˆ (0..^๐‘€))
24 modgcd 16474 . . . . . . . . . . . . 13 ((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•) โ†’ ((๐‘ค mod ๐‘€) gcd ๐‘€) = (๐‘ค gcd ๐‘€))
2518, 21, 24syl2anc 585 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘€) gcd ๐‘€) = (๐‘ค gcd ๐‘€))
2621nnzd 12585 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘€ โˆˆ โ„ค)
27 gcddvds 16444 . . . . . . . . . . . . . . . . 17 ((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ ๐‘€))
2818, 26, 27syl2anc 585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ ๐‘€))
2928simpld 496 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆฅ ๐‘ค)
30 nnne0 12246 . . . . . . . . . . . . . . . . . . 19 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โ‰  0)
31 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ค = 0 โˆง ๐‘€ = 0) โ†’ ๐‘€ = 0)
3231necon3ai 2966 . . . . . . . . . . . . . . . . . . 19 (๐‘€ โ‰  0 โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘€ = 0))
3321, 30, 323syl 18 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘€ = 0))
34 gcdn0cl 16443 . . . . . . . . . . . . . . . . . 18 (((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง ๐‘€ = 0)) โ†’ (๐‘ค gcd ๐‘€) โˆˆ โ„•)
3518, 26, 33, 34syl21anc 837 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆˆ โ„•)
3635nnzd 12585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆˆ โ„ค)
3719simp2d 1144 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
3837adantr 482 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ โˆˆ โ„•)
3938nnzd 12585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ โˆˆ โ„ค)
4028simprd 497 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆฅ ๐‘€)
4136, 26, 39, 40dvdsmultr1d 16240 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆฅ (๐‘€ ยท ๐‘))
4221, 38nnmulcld 12265 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•)
4342nnzd 12585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„ค)
44 nnne0 12246 . . . . . . . . . . . . . . . . 17 ((๐‘€ ยท ๐‘) โˆˆ โ„• โ†’ (๐‘€ ยท ๐‘) โ‰  0)
45 simpr 486 . . . . . . . . . . . . . . . . . 18 ((๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0) โ†’ (๐‘€ ยท ๐‘) = 0)
4645necon3ai 2966 . . . . . . . . . . . . . . . . 17 ((๐‘€ ยท ๐‘) โ‰  0 โ†’ ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0))
4742, 44, 463syl 18 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0))
48 dvdslegcd 16445 . . . . . . . . . . . . . . . 16 ((((๐‘ค gcd ๐‘€) โˆˆ โ„ค โˆง ๐‘ค โˆˆ โ„ค โˆง (๐‘€ ยท ๐‘) โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0)) โ†’ (((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ (๐‘€ ยท ๐‘)) โ†’ (๐‘ค gcd ๐‘€) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘))))
4936, 18, 43, 47, 48syl31anc 1374 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ (๐‘€ ยท ๐‘)) โ†’ (๐‘ค gcd ๐‘€) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘))))
5029, 41, 49mp2and 698 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘)))
514simprbi 498 . . . . . . . . . . . . . . 15 (๐‘ค โˆˆ ๐‘Š โ†’ (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1)
5251adantl 483 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1)
5350, 52breqtrd 5175 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โ‰ค 1)
54 nnle1eq1 12242 . . . . . . . . . . . . . 14 ((๐‘ค gcd ๐‘€) โˆˆ โ„• โ†’ ((๐‘ค gcd ๐‘€) โ‰ค 1 โ†” (๐‘ค gcd ๐‘€) = 1))
5535, 54syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘€) โ‰ค 1 โ†” (๐‘ค gcd ๐‘€) = 1))
5653, 55mpbid 231 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) = 1)
5725, 56eqtrd 2773 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘€) gcd ๐‘€) = 1)
58 oveq1 7416 . . . . . . . . . . . . 13 (๐‘ฆ = (๐‘ค mod ๐‘€) โ†’ (๐‘ฆ gcd ๐‘€) = ((๐‘ค mod ๐‘€) gcd ๐‘€))
5958eqeq1d 2735 . . . . . . . . . . . 12 (๐‘ฆ = (๐‘ค mod ๐‘€) โ†’ ((๐‘ฆ gcd ๐‘€) = 1 โ†” ((๐‘ค mod ๐‘€) gcd ๐‘€) = 1))
60 phimul.4 . . . . . . . . . . . 12 ๐‘ˆ = {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1}
6159, 60elrab2 3687 . . . . . . . . . . 11 ((๐‘ค mod ๐‘€) โˆˆ ๐‘ˆ โ†” ((๐‘ค mod ๐‘€) โˆˆ (0..^๐‘€) โˆง ((๐‘ค mod ๐‘€) gcd ๐‘€) = 1))
6223, 57, 61sylanbrc 584 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘€) โˆˆ ๐‘ˆ)
63 zmodfzo 13859 . . . . . . . . . . . 12 ((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ค mod ๐‘) โˆˆ (0..^๐‘))
6418, 38, 63syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘) โˆˆ (0..^๐‘))
65 modgcd 16474 . . . . . . . . . . . . 13 ((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘ค mod ๐‘) gcd ๐‘) = (๐‘ค gcd ๐‘))
6618, 38, 65syl2anc 585 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘) gcd ๐‘) = (๐‘ค gcd ๐‘))
67 gcddvds 16444 . . . . . . . . . . . . . . . . 17 ((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ ๐‘))
6818, 39, 67syl2anc 585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ ๐‘))
6968simpld 496 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆฅ ๐‘ค)
70 nnne0 12246 . . . . . . . . . . . . . . . . . . 19 (๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0)
71 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ค = 0 โˆง ๐‘ = 0) โ†’ ๐‘ = 0)
7271necon3ai 2966 . . . . . . . . . . . . . . . . . . 19 (๐‘ โ‰  0 โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘ = 0))
7338, 70, 723syl 18 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘ = 0))
74 gcdn0cl 16443 . . . . . . . . . . . . . . . . . 18 (((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง ๐‘ = 0)) โ†’ (๐‘ค gcd ๐‘) โˆˆ โ„•)
7518, 39, 73, 74syl21anc 837 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆˆ โ„•)
7675nnzd 12585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆˆ โ„ค)
7768simprd 497 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆฅ ๐‘)
78 dvdsmul2 16222 . . . . . . . . . . . . . . . . 17 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ๐‘ โˆฅ (๐‘€ ยท ๐‘))
7926, 39, 78syl2anc 585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ โˆฅ (๐‘€ ยท ๐‘))
8076, 39, 43, 77, 79dvdstrd 16238 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘))
81 dvdslegcd 16445 . . . . . . . . . . . . . . . 16 ((((๐‘ค gcd ๐‘) โˆˆ โ„ค โˆง ๐‘ค โˆˆ โ„ค โˆง (๐‘€ ยท ๐‘) โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0)) โ†’ (((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)) โ†’ (๐‘ค gcd ๐‘) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘))))
8276, 18, 43, 47, 81syl31anc 1374 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)) โ†’ (๐‘ค gcd ๐‘) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘))))
8369, 80, 82mp2and 698 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘)))
8483, 52breqtrd 5175 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โ‰ค 1)
85 nnle1eq1 12242 . . . . . . . . . . . . . 14 ((๐‘ค gcd ๐‘) โˆˆ โ„• โ†’ ((๐‘ค gcd ๐‘) โ‰ค 1 โ†” (๐‘ค gcd ๐‘) = 1))
8675, 85syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘) โ‰ค 1 โ†” (๐‘ค gcd ๐‘) = 1))
8784, 86mpbid 231 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) = 1)
8866, 87eqtrd 2773 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘) gcd ๐‘) = 1)
89 oveq1 7416 . . . . . . . . . . . . 13 (๐‘ฆ = (๐‘ค mod ๐‘) โ†’ (๐‘ฆ gcd ๐‘) = ((๐‘ค mod ๐‘) gcd ๐‘))
9089eqeq1d 2735 . . . . . . . . . . . 12 (๐‘ฆ = (๐‘ค mod ๐‘) โ†’ ((๐‘ฆ gcd ๐‘) = 1 โ†” ((๐‘ค mod ๐‘) gcd ๐‘) = 1))
91 phimul.5 . . . . . . . . . . . 12 ๐‘‰ = {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1}
9290, 91elrab2 3687 . . . . . . . . . . 11 ((๐‘ค mod ๐‘) โˆˆ ๐‘‰ โ†” ((๐‘ค mod ๐‘) โˆˆ (0..^๐‘) โˆง ((๐‘ค mod ๐‘) gcd ๐‘) = 1))
9364, 88, 92sylanbrc 584 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘) โˆˆ ๐‘‰)
9462, 93opelxpd 5716 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ โˆˆ (๐‘ˆ ร— ๐‘‰))
9513, 94eqeltrd 2834 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰))
9695ralrimiva 3147 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ค โˆˆ ๐‘Š (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰))
97 crth.2 . . . . . . . . . 10 ๐‘‡ = ((0..^๐‘€) ร— (0..^๐‘))
9814, 97, 9, 19crth 16711 . . . . . . . . 9 (๐œ‘ โ†’ ๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡)
99 f1ofn 6835 . . . . . . . . 9 (๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โ†’ ๐น Fn ๐‘†)
100 fnfun 6650 . . . . . . . . 9 (๐น Fn ๐‘† โ†’ Fun ๐น)
10198, 99, 1003syl 18 . . . . . . . 8 (๐œ‘ โ†’ Fun ๐น)
1023ssrab3 4081 . . . . . . . . 9 ๐‘Š โŠ† ๐‘†
103 fndm 6653 . . . . . . . . . 10 (๐น Fn ๐‘† โ†’ dom ๐น = ๐‘†)
10498, 99, 1033syl 18 . . . . . . . . 9 (๐œ‘ โ†’ dom ๐น = ๐‘†)
105102, 104sseqtrrid 4036 . . . . . . . 8 (๐œ‘ โ†’ ๐‘Š โŠ† dom ๐น)
106 funimass4 6957 . . . . . . . 8 ((Fun ๐น โˆง ๐‘Š โŠ† dom ๐น) โ†’ ((๐น โ€œ ๐‘Š) โŠ† (๐‘ˆ ร— ๐‘‰) โ†” โˆ€๐‘ค โˆˆ ๐‘Š (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰)))
107101, 105, 106syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ ((๐น โ€œ ๐‘Š) โŠ† (๐‘ˆ ร— ๐‘‰) โ†” โˆ€๐‘ค โˆˆ ๐‘Š (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰)))
10896, 107mpbird 257 . . . . . 6 (๐œ‘ โ†’ (๐น โ€œ ๐‘Š) โŠ† (๐‘ˆ ร— ๐‘‰))
10960ssrab3 4081 . . . . . . . . . . 11 ๐‘ˆ โŠ† (0..^๐‘€)
11091ssrab3 4081 . . . . . . . . . . 11 ๐‘‰ โŠ† (0..^๐‘)
111 xpss12 5692 . . . . . . . . . . 11 ((๐‘ˆ โŠ† (0..^๐‘€) โˆง ๐‘‰ โŠ† (0..^๐‘)) โ†’ (๐‘ˆ ร— ๐‘‰) โŠ† ((0..^๐‘€) ร— (0..^๐‘)))
112109, 110, 111mp2an 691 . . . . . . . . . 10 (๐‘ˆ ร— ๐‘‰) โŠ† ((0..^๐‘€) ร— (0..^๐‘))
113112, 97sseqtrri 4020 . . . . . . . . 9 (๐‘ˆ ร— ๐‘‰) โŠ† ๐‘‡
114113sseli 3979 . . . . . . . 8 (๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰) โ†’ ๐‘ง โˆˆ ๐‘‡)
115 f1ocnvfv2 7275 . . . . . . . 8 ((๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โˆง ๐‘ง โˆˆ ๐‘‡) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = ๐‘ง)
11698, 114, 115syl2an 597 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = ๐‘ง)
117 f1ocnv 6846 . . . . . . . . . . 11 (๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โ†’ โ—ก๐น:๐‘‡โ€“1-1-ontoโ†’๐‘†)
118 f1of 6834 . . . . . . . . . . 11 (โ—ก๐น:๐‘‡โ€“1-1-ontoโ†’๐‘† โ†’ โ—ก๐น:๐‘‡โŸถ๐‘†)
11998, 117, 1183syl 18 . . . . . . . . . 10 (๐œ‘ โ†’ โ—ก๐น:๐‘‡โŸถ๐‘†)
120 ffvelcdm 7084 . . . . . . . . . 10 ((โ—ก๐น:๐‘‡โŸถ๐‘† โˆง ๐‘ง โˆˆ ๐‘‡) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘†)
121119, 114, 120syl2an 597 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘†)
122121, 14eleqtrdi 2844 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ (0..^(๐‘€ ยท ๐‘)))
123 elfzoelz 13632 . . . . . . . . . . . . 13 ((โ—ก๐นโ€˜๐‘ง) โˆˆ (0..^(๐‘€ ยท ๐‘)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค)
124122, 123syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค)
12520adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘€ โˆˆ โ„•)
126 modgcd 16474 . . . . . . . . . . . 12 (((โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€))
127124, 125, 126syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€))
128 oveq1 7416 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค = (โ—ก๐นโ€˜๐‘ง) โ†’ (๐‘ค mod ๐‘€) = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€))
129 oveq1 7416 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค = (โ—ก๐นโ€˜๐‘ง) โ†’ (๐‘ค mod ๐‘) = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘))
130128, 129opeq12d 4882 . . . . . . . . . . . . . . . . . . 19 (๐‘ค = (โ—ก๐นโ€˜๐‘ง) โ†’ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
1318cbvmptv 5262 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ) = (๐‘ค โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
1329, 131eqtri 2761 . . . . . . . . . . . . . . . . . . 19 ๐น = (๐‘ค โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
133 opex 5465 . . . . . . . . . . . . . . . . . . 19 โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ โˆˆ V
134130, 132, 133fvmpt 6999 . . . . . . . . . . . . . . . . . 18 ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘† โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
135121, 134syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
136116, 135eqtr3d 2775 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ง = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
137 simpr 486 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰))
138136, 137eqeltrrd 2835 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ โˆˆ (๐‘ˆ ร— ๐‘‰))
139 opelxp 5713 . . . . . . . . . . . . . . 15 (โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ โˆˆ (๐‘ˆ ร— ๐‘‰) โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ โˆง ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰))
140138, 139sylib 217 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ โˆง ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰))
141140simpld 496 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ)
142 oveq1 7416 . . . . . . . . . . . . . . 15 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โ†’ (๐‘ฆ gcd ๐‘€) = (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€))
143142eqeq1d 2735 . . . . . . . . . . . . . 14 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โ†’ ((๐‘ฆ gcd ๐‘€) = 1 โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1))
144143, 60elrab2 3687 . . . . . . . . . . . . 13 (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ (0..^๐‘€) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1))
145141, 144sylib 217 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ (0..^๐‘€) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1))
146145simprd 497 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1)
147127, 146eqtr3d 2775 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€) = 1)
14837adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ โˆˆ โ„•)
149 modgcd 16474 . . . . . . . . . . . 12 (((โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘))
150124, 148, 149syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘))
151140simprd 497 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰)
152 oveq1 7416 . . . . . . . . . . . . . . 15 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โ†’ (๐‘ฆ gcd ๐‘) = (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘))
153152eqeq1d 2735 . . . . . . . . . . . . . 14 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โ†’ ((๐‘ฆ gcd ๐‘) = 1 โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1))
154153, 91elrab2 3687 . . . . . . . . . . . . 13 (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰ โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ (0..^๐‘) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1))
155151, 154sylib 217 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ (0..^๐‘) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1))
156155simprd 497 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1)
157150, 156eqtr3d 2775 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘) = 1)
15820nnzd 12585 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
159158adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘€ โˆˆ โ„ค)
16037nnzd 12585 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
161160adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ โˆˆ โ„ค)
162 rpmul 16596 . . . . . . . . . . 11 (((โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€) = 1 โˆง ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘) = 1) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
163124, 159, 161, 162syl3anc 1372 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€) = 1 โˆง ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘) = 1) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
164147, 157, 163mp2and 698 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1)
165 oveq1 7416 . . . . . . . . . . 11 (๐‘ฆ = (โ—ก๐นโ€˜๐‘ง) โ†’ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)))
166165eqeq1d 2735 . . . . . . . . . 10 (๐‘ฆ = (โ—ก๐นโ€˜๐‘ง) โ†’ ((๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1 โ†” ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
167166, 3elrab2 3687 . . . . . . . . 9 ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š โ†” ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘† โˆง ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
168121, 164, 167sylanbrc 584 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š)
169 funfvima2 7233 . . . . . . . . . 10 ((Fun ๐น โˆง ๐‘Š โŠ† dom ๐น) โ†’ ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š)))
170101, 105, 169syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š)))
171170imp 408 . . . . . . . 8 ((๐œ‘ โˆง (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š))
172168, 171syldan 592 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š))
173116, 172eqeltrrd 2835 . . . . . 6 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ง โˆˆ (๐น โ€œ ๐‘Š))
174108, 173eqelssd 4004 . . . . 5 (๐œ‘ โ†’ (๐น โ€œ ๐‘Š) = (๐‘ˆ ร— ๐‘‰))
175 f1of1 6833 . . . . . . 7 (๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โ†’ ๐น:๐‘†โ€“1-1โ†’๐‘‡)
17698, 175syl 17 . . . . . 6 (๐œ‘ โ†’ ๐น:๐‘†โ€“1-1โ†’๐‘‡)
177 fzofi 13939 . . . . . . . . . 10 (0..^(๐‘€ ยท ๐‘)) โˆˆ Fin
17814, 177eqeltri 2830 . . . . . . . . 9 ๐‘† โˆˆ Fin
179 ssfi 9173 . . . . . . . . 9 ((๐‘† โˆˆ Fin โˆง ๐‘Š โŠ† ๐‘†) โ†’ ๐‘Š โˆˆ Fin)
180178, 102, 179mp2an 691 . . . . . . . 8 ๐‘Š โˆˆ Fin
181180elexi 3494 . . . . . . 7 ๐‘Š โˆˆ V
182181f1imaen 9012 . . . . . 6 ((๐น:๐‘†โ€“1-1โ†’๐‘‡ โˆง ๐‘Š โŠ† ๐‘†) โ†’ (๐น โ€œ ๐‘Š) โ‰ˆ ๐‘Š)
183176, 102, 182sylancl 587 . . . . 5 (๐œ‘ โ†’ (๐น โ€œ ๐‘Š) โ‰ˆ ๐‘Š)
184174, 183eqbrtrrd 5173 . . . 4 (๐œ‘ โ†’ (๐‘ˆ ร— ๐‘‰) โ‰ˆ ๐‘Š)
185 fzofi 13939 . . . . . . . 8 (0..^๐‘€) โˆˆ Fin
186 ssrab2 4078 . . . . . . . 8 {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โŠ† (0..^๐‘€)
187 ssfi 9173 . . . . . . . 8 (((0..^๐‘€) โˆˆ Fin โˆง {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โŠ† (0..^๐‘€)) โ†’ {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โˆˆ Fin)
188185, 186, 187mp2an 691 . . . . . . 7 {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โˆˆ Fin
18960, 188eqeltri 2830 . . . . . 6 ๐‘ˆ โˆˆ Fin
190 fzofi 13939 . . . . . . . 8 (0..^๐‘) โˆˆ Fin
191 ssrab2 4078 . . . . . . . 8 {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โŠ† (0..^๐‘)
192 ssfi 9173 . . . . . . . 8 (((0..^๐‘) โˆˆ Fin โˆง {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โŠ† (0..^๐‘)) โ†’ {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โˆˆ Fin)
193190, 191, 192mp2an 691 . . . . . . 7 {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โˆˆ Fin
19491, 193eqeltri 2830 . . . . . 6 ๐‘‰ โˆˆ Fin
195 xpfi 9317 . . . . . 6 ((๐‘ˆ โˆˆ Fin โˆง ๐‘‰ โˆˆ Fin) โ†’ (๐‘ˆ ร— ๐‘‰) โˆˆ Fin)
196189, 194, 195mp2an 691 . . . . 5 (๐‘ˆ ร— ๐‘‰) โˆˆ Fin
197 hashen 14307 . . . . 5 (((๐‘ˆ ร— ๐‘‰) โˆˆ Fin โˆง ๐‘Š โˆˆ Fin) โ†’ ((โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = (โ™ฏโ€˜๐‘Š) โ†” (๐‘ˆ ร— ๐‘‰) โ‰ˆ ๐‘Š))
198196, 180, 197mp2an 691 . . . 4 ((โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = (โ™ฏโ€˜๐‘Š) โ†” (๐‘ˆ ร— ๐‘‰) โ‰ˆ ๐‘Š)
199184, 198sylibr 233 . . 3 (๐œ‘ โ†’ (โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = (โ™ฏโ€˜๐‘Š))
200 hashxp 14394 . . . 4 ((๐‘ˆ โˆˆ Fin โˆง ๐‘‰ โˆˆ Fin) โ†’ (โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰)))
201189, 194, 200mp2an 691 . . 3 (โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰))
202199, 201eqtr3di 2788 . 2 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘Š) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰)))
20320, 37nnmulcld 12265 . . 3 (๐œ‘ โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•)
204 dfphi2 16707 . . . 4 ((๐‘€ ยท ๐‘) โˆˆ โ„• โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}))
20514rabeqi 3446 . . . . . 6 {๐‘ฆ โˆˆ ๐‘† โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1} = {๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
2063, 205eqtri 2761 . . . . 5 ๐‘Š = {๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
207206fveq2i 6895 . . . 4 (โ™ฏโ€˜๐‘Š) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1})
208204, 207eqtr4di 2791 . . 3 ((๐‘€ ยท ๐‘) โˆˆ โ„• โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = (โ™ฏโ€˜๐‘Š))
209203, 208syl 17 . 2 (๐œ‘ โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = (โ™ฏโ€˜๐‘Š))
210 dfphi2 16707 . . . . 5 (๐‘€ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘€) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1}))
21160fveq2i 6895 . . . . 5 (โ™ฏโ€˜๐‘ˆ) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1})
212210, 211eqtr4di 2791 . . . 4 (๐‘€ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘€) = (โ™ฏโ€˜๐‘ˆ))
21320, 212syl 17 . . 3 (๐œ‘ โ†’ (ฯ•โ€˜๐‘€) = (โ™ฏโ€˜๐‘ˆ))
214 dfphi2 16707 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1}))
21591fveq2i 6895 . . . . 5 (โ™ฏโ€˜๐‘‰) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1})
216214, 215eqtr4di 2791 . . . 4 (๐‘ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘) = (โ™ฏโ€˜๐‘‰))
21737, 216syl 17 . . 3 (๐œ‘ โ†’ (ฯ•โ€˜๐‘) = (โ™ฏโ€˜๐‘‰))
218213, 217oveq12d 7427 . 2 (๐œ‘ โ†’ ((ฯ•โ€˜๐‘€) ยท (ฯ•โ€˜๐‘)) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰)))
219202, 209, 2183eqtr4d 2783 1 (๐œ‘ โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = ((ฯ•โ€˜๐‘€) ยท (ฯ•โ€˜๐‘)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941  โˆ€wral 3062  {crab 3433   โŠ† wss 3949  โŸจcop 4635   class class class wbr 5149   โ†ฆ cmpt 5232   ร— cxp 5675  โ—กccnv 5676  dom cdm 5677   โ€œ cima 5680  Fun wfun 6538   Fn wfn 6539  โŸถwf 6540  โ€“1-1โ†’wf1 6541  โ€“1-1-ontoโ†’wf1o 6543  โ€˜cfv 6544  (class class class)co 7409   โ‰ˆ cen 8936  Fincfn 8939  0cc0 11110  1c1 11111   ยท cmul 11115   โ‰ค cle 11249  โ„•cn 12212  โ„คcz 12558  ..^cfzo 13627   mod cmo 13834  โ™ฏchash 14290   โˆฅ cdvds 16197   gcd cgcd 16435  ฯ•cphi 16697
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-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
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 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-inf 9438  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-xnn0 12545  df-z 12559  df-uz 12823  df-rp 12975  df-fz 13485  df-fzo 13628  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-dvds 16198  df-gcd 16436  df-phi 16699
This theorem is referenced by:  phimul  16713
  Copyright terms: Public domain W3C validator