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

Theorem phimullem 16652
Description: Lemma for phimul 16653. (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 7365 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ค โ†’ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = (๐‘ค gcd (๐‘€ ยท ๐‘)))
21eqeq1d 2739 . . . . . . . . . . . . 13 (๐‘ฆ = ๐‘ค โ†’ ((๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1 โ†” (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1))
3 phimul.6 . . . . . . . . . . . . 13 ๐‘Š = {๐‘ฆ โˆˆ ๐‘† โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
42, 3elrab2 3649 . . . . . . . . . . . 12 (๐‘ค โˆˆ ๐‘Š โ†” (๐‘ค โˆˆ ๐‘† โˆง (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1))
54simplbi 499 . . . . . . . . . . 11 (๐‘ค โˆˆ ๐‘Š โ†’ ๐‘ค โˆˆ ๐‘†)
6 oveq1 7365 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ค โ†’ (๐‘ฅ mod ๐‘€) = (๐‘ค mod ๐‘€))
7 oveq1 7365 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ค โ†’ (๐‘ฅ mod ๐‘) = (๐‘ค mod ๐‘))
86, 7opeq12d 4839 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ค โ†’ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
9 crth.3 . . . . . . . . . . . 12 ๐น = (๐‘ฅ โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ)
10 opex 5422 . . . . . . . . . . . 12 โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ โˆˆ V
118, 9, 10fvmpt 6949 . . . . . . . . . . 11 (๐‘ค โˆˆ ๐‘† โ†’ (๐นโ€˜๐‘ค) = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
125, 11syl 17 . . . . . . . . . 10 (๐‘ค โˆˆ ๐‘Š โ†’ (๐นโ€˜๐‘ค) = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
1312adantl 483 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐นโ€˜๐‘ค) = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
14 crth.1 . . . . . . . . . . . . . . 15 ๐‘† = (0..^(๐‘€ ยท ๐‘))
155, 14eleqtrdi 2848 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ ๐‘Š โ†’ ๐‘ค โˆˆ (0..^(๐‘€ ยท ๐‘)))
1615adantl 483 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ค โˆˆ (0..^(๐‘€ ยท ๐‘)))
17 elfzoelz 13573 . . . . . . . . . . . . 13 (๐‘ค โˆˆ (0..^(๐‘€ ยท ๐‘)) โ†’ ๐‘ค โˆˆ โ„ค)
1816, 17syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ค โˆˆ โ„ค)
19 crth.4 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• โˆง (๐‘€ gcd ๐‘) = 1))
2019simp1d 1143 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
2120adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘€ โˆˆ โ„•)
22 zmodfzo 13800 . . . . . . . . . . . 12 ((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•) โ†’ (๐‘ค mod ๐‘€) โˆˆ (0..^๐‘€))
2318, 21, 22syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘€) โˆˆ (0..^๐‘€))
24 modgcd 16414 . . . . . . . . . . . . 13 ((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•) โ†’ ((๐‘ค mod ๐‘€) gcd ๐‘€) = (๐‘ค gcd ๐‘€))
2518, 21, 24syl2anc 585 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘€) gcd ๐‘€) = (๐‘ค gcd ๐‘€))
2621nnzd 12527 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘€ โˆˆ โ„ค)
27 gcddvds 16384 . . . . . . . . . . . . . . . . 17 ((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ ๐‘€))
2818, 26, 27syl2anc 585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ ๐‘€))
2928simpld 496 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆฅ ๐‘ค)
30 nnne0 12188 . . . . . . . . . . . . . . . . . . 19 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โ‰  0)
31 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ค = 0 โˆง ๐‘€ = 0) โ†’ ๐‘€ = 0)
3231necon3ai 2969 . . . . . . . . . . . . . . . . . . 19 (๐‘€ โ‰  0 โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘€ = 0))
3321, 30, 323syl 18 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘€ = 0))
34 gcdn0cl 16383 . . . . . . . . . . . . . . . . . 18 (((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง ๐‘€ = 0)) โ†’ (๐‘ค gcd ๐‘€) โˆˆ โ„•)
3518, 26, 33, 34syl21anc 837 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆˆ โ„•)
3635nnzd 12527 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆˆ โ„ค)
3719simp2d 1144 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
3837adantr 482 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ โˆˆ โ„•)
3938nnzd 12527 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ โˆˆ โ„ค)
4028simprd 497 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆฅ ๐‘€)
4136, 26, 39, 40dvdsmultr1d 16180 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆฅ (๐‘€ ยท ๐‘))
4221, 38nnmulcld 12207 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•)
4342nnzd 12527 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„ค)
44 nnne0 12188 . . . . . . . . . . . . . . . . 17 ((๐‘€ ยท ๐‘) โˆˆ โ„• โ†’ (๐‘€ ยท ๐‘) โ‰  0)
45 simpr 486 . . . . . . . . . . . . . . . . . 18 ((๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0) โ†’ (๐‘€ ยท ๐‘) = 0)
4645necon3ai 2969 . . . . . . . . . . . . . . . . 17 ((๐‘€ ยท ๐‘) โ‰  0 โ†’ ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0))
4742, 44, 463syl 18 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0))
48 dvdslegcd 16385 . . . . . . . . . . . . . . . 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 5132 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โ‰ค 1)
54 nnle1eq1 12184 . . . . . . . . . . . . . 14 ((๐‘ค gcd ๐‘€) โˆˆ โ„• โ†’ ((๐‘ค gcd ๐‘€) โ‰ค 1 โ†” (๐‘ค gcd ๐‘€) = 1))
5535, 54syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘€) โ‰ค 1 โ†” (๐‘ค gcd ๐‘€) = 1))
5653, 55mpbid 231 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) = 1)
5725, 56eqtrd 2777 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘€) gcd ๐‘€) = 1)
58 oveq1 7365 . . . . . . . . . . . . 13 (๐‘ฆ = (๐‘ค mod ๐‘€) โ†’ (๐‘ฆ gcd ๐‘€) = ((๐‘ค mod ๐‘€) gcd ๐‘€))
5958eqeq1d 2739 . . . . . . . . . . . 12 (๐‘ฆ = (๐‘ค mod ๐‘€) โ†’ ((๐‘ฆ gcd ๐‘€) = 1 โ†” ((๐‘ค mod ๐‘€) gcd ๐‘€) = 1))
60 phimul.4 . . . . . . . . . . . 12 ๐‘ˆ = {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1}
6159, 60elrab2 3649 . . . . . . . . . . 11 ((๐‘ค mod ๐‘€) โˆˆ ๐‘ˆ โ†” ((๐‘ค mod ๐‘€) โˆˆ (0..^๐‘€) โˆง ((๐‘ค mod ๐‘€) gcd ๐‘€) = 1))
6223, 57, 61sylanbrc 584 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘€) โˆˆ ๐‘ˆ)
63 zmodfzo 13800 . . . . . . . . . . . 12 ((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ค mod ๐‘) โˆˆ (0..^๐‘))
6418, 38, 63syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘) โˆˆ (0..^๐‘))
65 modgcd 16414 . . . . . . . . . . . . 13 ((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘ค mod ๐‘) gcd ๐‘) = (๐‘ค gcd ๐‘))
6618, 38, 65syl2anc 585 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘) gcd ๐‘) = (๐‘ค gcd ๐‘))
67 gcddvds 16384 . . . . . . . . . . . . . . . . 17 ((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ ๐‘))
6818, 39, 67syl2anc 585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ ๐‘))
6968simpld 496 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆฅ ๐‘ค)
70 nnne0 12188 . . . . . . . . . . . . . . . . . . 19 (๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0)
71 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ค = 0 โˆง ๐‘ = 0) โ†’ ๐‘ = 0)
7271necon3ai 2969 . . . . . . . . . . . . . . . . . . 19 (๐‘ โ‰  0 โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘ = 0))
7338, 70, 723syl 18 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘ = 0))
74 gcdn0cl 16383 . . . . . . . . . . . . . . . . . 18 (((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง ๐‘ = 0)) โ†’ (๐‘ค gcd ๐‘) โˆˆ โ„•)
7518, 39, 73, 74syl21anc 837 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆˆ โ„•)
7675nnzd 12527 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆˆ โ„ค)
7768simprd 497 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆฅ ๐‘)
78 dvdsmul2 16162 . . . . . . . . . . . . . . . . 17 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ๐‘ โˆฅ (๐‘€ ยท ๐‘))
7926, 39, 78syl2anc 585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ โˆฅ (๐‘€ ยท ๐‘))
8076, 39, 43, 77, 79dvdstrd 16178 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘))
81 dvdslegcd 16385 . . . . . . . . . . . . . . . 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 5132 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โ‰ค 1)
85 nnle1eq1 12184 . . . . . . . . . . . . . 14 ((๐‘ค gcd ๐‘) โˆˆ โ„• โ†’ ((๐‘ค gcd ๐‘) โ‰ค 1 โ†” (๐‘ค gcd ๐‘) = 1))
8675, 85syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘) โ‰ค 1 โ†” (๐‘ค gcd ๐‘) = 1))
8784, 86mpbid 231 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) = 1)
8866, 87eqtrd 2777 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘) gcd ๐‘) = 1)
89 oveq1 7365 . . . . . . . . . . . . 13 (๐‘ฆ = (๐‘ค mod ๐‘) โ†’ (๐‘ฆ gcd ๐‘) = ((๐‘ค mod ๐‘) gcd ๐‘))
9089eqeq1d 2739 . . . . . . . . . . . 12 (๐‘ฆ = (๐‘ค mod ๐‘) โ†’ ((๐‘ฆ gcd ๐‘) = 1 โ†” ((๐‘ค mod ๐‘) gcd ๐‘) = 1))
91 phimul.5 . . . . . . . . . . . 12 ๐‘‰ = {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1}
9290, 91elrab2 3649 . . . . . . . . . . 11 ((๐‘ค mod ๐‘) โˆˆ ๐‘‰ โ†” ((๐‘ค mod ๐‘) โˆˆ (0..^๐‘) โˆง ((๐‘ค mod ๐‘) gcd ๐‘) = 1))
9364, 88, 92sylanbrc 584 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘) โˆˆ ๐‘‰)
9462, 93opelxpd 5672 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ โˆˆ (๐‘ˆ ร— ๐‘‰))
9513, 94eqeltrd 2838 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰))
9695ralrimiva 3144 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ค โˆˆ ๐‘Š (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰))
97 crth.2 . . . . . . . . . 10 ๐‘‡ = ((0..^๐‘€) ร— (0..^๐‘))
9814, 97, 9, 19crth 16651 . . . . . . . . 9 (๐œ‘ โ†’ ๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡)
99 f1ofn 6786 . . . . . . . . 9 (๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โ†’ ๐น Fn ๐‘†)
100 fnfun 6603 . . . . . . . . 9 (๐น Fn ๐‘† โ†’ Fun ๐น)
10198, 99, 1003syl 18 . . . . . . . 8 (๐œ‘ โ†’ Fun ๐น)
1023ssrab3 4041 . . . . . . . . 9 ๐‘Š โŠ† ๐‘†
103 fndm 6606 . . . . . . . . . 10 (๐น Fn ๐‘† โ†’ dom ๐น = ๐‘†)
10498, 99, 1033syl 18 . . . . . . . . 9 (๐œ‘ โ†’ dom ๐น = ๐‘†)
105102, 104sseqtrrid 3998 . . . . . . . 8 (๐œ‘ โ†’ ๐‘Š โŠ† dom ๐น)
106 funimass4 6908 . . . . . . . 8 ((Fun ๐น โˆง ๐‘Š โŠ† dom ๐น) โ†’ ((๐น โ€œ ๐‘Š) โŠ† (๐‘ˆ ร— ๐‘‰) โ†” โˆ€๐‘ค โˆˆ ๐‘Š (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰)))
107101, 105, 106syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ ((๐น โ€œ ๐‘Š) โŠ† (๐‘ˆ ร— ๐‘‰) โ†” โˆ€๐‘ค โˆˆ ๐‘Š (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰)))
10896, 107mpbird 257 . . . . . 6 (๐œ‘ โ†’ (๐น โ€œ ๐‘Š) โŠ† (๐‘ˆ ร— ๐‘‰))
10960ssrab3 4041 . . . . . . . . . . 11 ๐‘ˆ โŠ† (0..^๐‘€)
11091ssrab3 4041 . . . . . . . . . . 11 ๐‘‰ โŠ† (0..^๐‘)
111 xpss12 5649 . . . . . . . . . . 11 ((๐‘ˆ โŠ† (0..^๐‘€) โˆง ๐‘‰ โŠ† (0..^๐‘)) โ†’ (๐‘ˆ ร— ๐‘‰) โŠ† ((0..^๐‘€) ร— (0..^๐‘)))
112109, 110, 111mp2an 691 . . . . . . . . . 10 (๐‘ˆ ร— ๐‘‰) โŠ† ((0..^๐‘€) ร— (0..^๐‘))
113112, 97sseqtrri 3982 . . . . . . . . 9 (๐‘ˆ ร— ๐‘‰) โŠ† ๐‘‡
114113sseli 3941 . . . . . . . 8 (๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰) โ†’ ๐‘ง โˆˆ ๐‘‡)
115 f1ocnvfv2 7224 . . . . . . . 8 ((๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โˆง ๐‘ง โˆˆ ๐‘‡) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = ๐‘ง)
11698, 114, 115syl2an 597 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = ๐‘ง)
117 f1ocnv 6797 . . . . . . . . . . 11 (๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โ†’ โ—ก๐น:๐‘‡โ€“1-1-ontoโ†’๐‘†)
118 f1of 6785 . . . . . . . . . . 11 (โ—ก๐น:๐‘‡โ€“1-1-ontoโ†’๐‘† โ†’ โ—ก๐น:๐‘‡โŸถ๐‘†)
11998, 117, 1183syl 18 . . . . . . . . . 10 (๐œ‘ โ†’ โ—ก๐น:๐‘‡โŸถ๐‘†)
120 ffvelcdm 7033 . . . . . . . . . 10 ((โ—ก๐น:๐‘‡โŸถ๐‘† โˆง ๐‘ง โˆˆ ๐‘‡) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘†)
121119, 114, 120syl2an 597 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘†)
122121, 14eleqtrdi 2848 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ (0..^(๐‘€ ยท ๐‘)))
123 elfzoelz 13573 . . . . . . . . . . . . 13 ((โ—ก๐นโ€˜๐‘ง) โˆˆ (0..^(๐‘€ ยท ๐‘)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค)
124122, 123syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค)
12520adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘€ โˆˆ โ„•)
126 modgcd 16414 . . . . . . . . . . . 12 (((โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€))
127124, 125, 126syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€))
128 oveq1 7365 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค = (โ—ก๐นโ€˜๐‘ง) โ†’ (๐‘ค mod ๐‘€) = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€))
129 oveq1 7365 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค = (โ—ก๐นโ€˜๐‘ง) โ†’ (๐‘ค mod ๐‘) = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘))
130128, 129opeq12d 4839 . . . . . . . . . . . . . . . . . . 19 (๐‘ค = (โ—ก๐นโ€˜๐‘ง) โ†’ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
1318cbvmptv 5219 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ) = (๐‘ค โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
1329, 131eqtri 2765 . . . . . . . . . . . . . . . . . . 19 ๐น = (๐‘ค โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
133 opex 5422 . . . . . . . . . . . . . . . . . . 19 โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ โˆˆ V
134130, 132, 133fvmpt 6949 . . . . . . . . . . . . . . . . . 18 ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘† โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
135121, 134syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
136116, 135eqtr3d 2779 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ง = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
137 simpr 486 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰))
138136, 137eqeltrrd 2839 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ โˆˆ (๐‘ˆ ร— ๐‘‰))
139 opelxp 5670 . . . . . . . . . . . . . . 15 (โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ โˆˆ (๐‘ˆ ร— ๐‘‰) โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ โˆง ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰))
140138, 139sylib 217 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ โˆง ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰))
141140simpld 496 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ)
142 oveq1 7365 . . . . . . . . . . . . . . 15 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โ†’ (๐‘ฆ gcd ๐‘€) = (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€))
143142eqeq1d 2739 . . . . . . . . . . . . . 14 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โ†’ ((๐‘ฆ gcd ๐‘€) = 1 โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1))
144143, 60elrab2 3649 . . . . . . . . . . . . 13 (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ (0..^๐‘€) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1))
145141, 144sylib 217 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ (0..^๐‘€) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1))
146145simprd 497 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1)
147127, 146eqtr3d 2779 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€) = 1)
14837adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ โˆˆ โ„•)
149 modgcd 16414 . . . . . . . . . . . 12 (((โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘))
150124, 148, 149syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘))
151140simprd 497 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰)
152 oveq1 7365 . . . . . . . . . . . . . . 15 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โ†’ (๐‘ฆ gcd ๐‘) = (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘))
153152eqeq1d 2739 . . . . . . . . . . . . . 14 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โ†’ ((๐‘ฆ gcd ๐‘) = 1 โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1))
154153, 91elrab2 3649 . . . . . . . . . . . . 13 (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰ โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ (0..^๐‘) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1))
155151, 154sylib 217 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ (0..^๐‘) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1))
156155simprd 497 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1)
157150, 156eqtr3d 2779 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘) = 1)
15820nnzd 12527 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
159158adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘€ โˆˆ โ„ค)
16037nnzd 12527 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
161160adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ โˆˆ โ„ค)
162 rpmul 16536 . . . . . . . . . . 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 7365 . . . . . . . . . . 11 (๐‘ฆ = (โ—ก๐นโ€˜๐‘ง) โ†’ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)))
166165eqeq1d 2739 . . . . . . . . . 10 (๐‘ฆ = (โ—ก๐นโ€˜๐‘ง) โ†’ ((๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1 โ†” ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
167166, 3elrab2 3649 . . . . . . . . 9 ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š โ†” ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘† โˆง ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
168121, 164, 167sylanbrc 584 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š)
169 funfvima2 7182 . . . . . . . . . 10 ((Fun ๐น โˆง ๐‘Š โŠ† dom ๐น) โ†’ ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š)))
170101, 105, 169syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š)))
171170imp 408 . . . . . . . 8 ((๐œ‘ โˆง (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š))
172168, 171syldan 592 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š))
173116, 172eqeltrrd 2839 . . . . . 6 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ง โˆˆ (๐น โ€œ ๐‘Š))
174108, 173eqelssd 3966 . . . . 5 (๐œ‘ โ†’ (๐น โ€œ ๐‘Š) = (๐‘ˆ ร— ๐‘‰))
175 f1of1 6784 . . . . . . 7 (๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โ†’ ๐น:๐‘†โ€“1-1โ†’๐‘‡)
17698, 175syl 17 . . . . . 6 (๐œ‘ โ†’ ๐น:๐‘†โ€“1-1โ†’๐‘‡)
177 fzofi 13880 . . . . . . . . . 10 (0..^(๐‘€ ยท ๐‘)) โˆˆ Fin
17814, 177eqeltri 2834 . . . . . . . . 9 ๐‘† โˆˆ Fin
179 ssfi 9118 . . . . . . . . 9 ((๐‘† โˆˆ Fin โˆง ๐‘Š โŠ† ๐‘†) โ†’ ๐‘Š โˆˆ Fin)
180178, 102, 179mp2an 691 . . . . . . . 8 ๐‘Š โˆˆ Fin
181180elexi 3465 . . . . . . 7 ๐‘Š โˆˆ V
182181f1imaen 8957 . . . . . 6 ((๐น:๐‘†โ€“1-1โ†’๐‘‡ โˆง ๐‘Š โŠ† ๐‘†) โ†’ (๐น โ€œ ๐‘Š) โ‰ˆ ๐‘Š)
183176, 102, 182sylancl 587 . . . . 5 (๐œ‘ โ†’ (๐น โ€œ ๐‘Š) โ‰ˆ ๐‘Š)
184174, 183eqbrtrrd 5130 . . . 4 (๐œ‘ โ†’ (๐‘ˆ ร— ๐‘‰) โ‰ˆ ๐‘Š)
185 fzofi 13880 . . . . . . . 8 (0..^๐‘€) โˆˆ Fin
186 ssrab2 4038 . . . . . . . 8 {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โŠ† (0..^๐‘€)
187 ssfi 9118 . . . . . . . 8 (((0..^๐‘€) โˆˆ Fin โˆง {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โŠ† (0..^๐‘€)) โ†’ {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โˆˆ Fin)
188185, 186, 187mp2an 691 . . . . . . 7 {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โˆˆ Fin
18960, 188eqeltri 2834 . . . . . 6 ๐‘ˆ โˆˆ Fin
190 fzofi 13880 . . . . . . . 8 (0..^๐‘) โˆˆ Fin
191 ssrab2 4038 . . . . . . . 8 {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โŠ† (0..^๐‘)
192 ssfi 9118 . . . . . . . 8 (((0..^๐‘) โˆˆ Fin โˆง {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โŠ† (0..^๐‘)) โ†’ {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โˆˆ Fin)
193190, 191, 192mp2an 691 . . . . . . 7 {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โˆˆ Fin
19491, 193eqeltri 2834 . . . . . 6 ๐‘‰ โˆˆ Fin
195 xpfi 9262 . . . . . 6 ((๐‘ˆ โˆˆ Fin โˆง ๐‘‰ โˆˆ Fin) โ†’ (๐‘ˆ ร— ๐‘‰) โˆˆ Fin)
196189, 194, 195mp2an 691 . . . . 5 (๐‘ˆ ร— ๐‘‰) โˆˆ Fin
197 hashen 14248 . . . . 5 (((๐‘ˆ ร— ๐‘‰) โˆˆ Fin โˆง ๐‘Š โˆˆ Fin) โ†’ ((โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = (โ™ฏโ€˜๐‘Š) โ†” (๐‘ˆ ร— ๐‘‰) โ‰ˆ ๐‘Š))
198196, 180, 197mp2an 691 . . . 4 ((โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = (โ™ฏโ€˜๐‘Š) โ†” (๐‘ˆ ร— ๐‘‰) โ‰ˆ ๐‘Š)
199184, 198sylibr 233 . . 3 (๐œ‘ โ†’ (โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = (โ™ฏโ€˜๐‘Š))
200 hashxp 14335 . . . 4 ((๐‘ˆ โˆˆ Fin โˆง ๐‘‰ โˆˆ Fin) โ†’ (โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰)))
201189, 194, 200mp2an 691 . . 3 (โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰))
202199, 201eqtr3di 2792 . 2 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘Š) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰)))
20320, 37nnmulcld 12207 . . 3 (๐œ‘ โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•)
204 dfphi2 16647 . . . 4 ((๐‘€ ยท ๐‘) โˆˆ โ„• โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}))
20514rabeqi 3421 . . . . . 6 {๐‘ฆ โˆˆ ๐‘† โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1} = {๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
2063, 205eqtri 2765 . . . . 5 ๐‘Š = {๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
207206fveq2i 6846 . . . 4 (โ™ฏโ€˜๐‘Š) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1})
208204, 207eqtr4di 2795 . . 3 ((๐‘€ ยท ๐‘) โˆˆ โ„• โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = (โ™ฏโ€˜๐‘Š))
209203, 208syl 17 . 2 (๐œ‘ โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = (โ™ฏโ€˜๐‘Š))
210 dfphi2 16647 . . . . 5 (๐‘€ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘€) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1}))
21160fveq2i 6846 . . . . 5 (โ™ฏโ€˜๐‘ˆ) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1})
212210, 211eqtr4di 2795 . . . 4 (๐‘€ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘€) = (โ™ฏโ€˜๐‘ˆ))
21320, 212syl 17 . . 3 (๐œ‘ โ†’ (ฯ•โ€˜๐‘€) = (โ™ฏโ€˜๐‘ˆ))
214 dfphi2 16647 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1}))
21591fveq2i 6846 . . . . 5 (โ™ฏโ€˜๐‘‰) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1})
216214, 215eqtr4di 2795 . . . 4 (๐‘ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘) = (โ™ฏโ€˜๐‘‰))
21737, 216syl 17 . . 3 (๐œ‘ โ†’ (ฯ•โ€˜๐‘) = (โ™ฏโ€˜๐‘‰))
218213, 217oveq12d 7376 . 2 (๐œ‘ โ†’ ((ฯ•โ€˜๐‘€) ยท (ฯ•โ€˜๐‘)) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰)))
219202, 209, 2183eqtr4d 2787 1 (๐œ‘ โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = ((ฯ•โ€˜๐‘€) ยท (ฯ•โ€˜๐‘)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆ€wral 3065  {crab 3408   โŠ† wss 3911  โŸจcop 4593   class class class wbr 5106   โ†ฆ cmpt 5189   ร— cxp 5632  โ—กccnv 5633  dom cdm 5634   โ€œ cima 5637  Fun wfun 6491   Fn wfn 6492  โŸถwf 6493  โ€“1-1โ†’wf1 6494  โ€“1-1-ontoโ†’wf1o 6496  โ€˜cfv 6497  (class class class)co 7358   โ‰ˆ cen 8881  Fincfn 8884  0cc0 11052  1c1 11053   ยท cmul 11057   โ‰ค cle 11191  โ„•cn 12154  โ„คcz 12500  ..^cfzo 13568   mod cmo 13775  โ™ฏchash 14231   โˆฅ cdvds 16137   gcd cgcd 16375  ฯ•cphi 16637
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 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129  ax-pre-sup 11130
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  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-int 4909  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-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-oadd 8417  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-sup 9379  df-inf 9380  df-dju 9838  df-card 9876  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-n0 12415  df-xnn0 12487  df-z 12501  df-uz 12765  df-rp 12917  df-fz 13426  df-fzo 13569  df-fl 13698  df-mod 13776  df-seq 13908  df-exp 13969  df-hash 14232  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-dvds 16138  df-gcd 16376  df-phi 16639
This theorem is referenced by:  phimul  16653
  Copyright terms: Public domain W3C validator