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

Theorem phimullem 16716
Description: Lemma for phimul 16717. (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 7418 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ค โ†’ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = (๐‘ค gcd (๐‘€ ยท ๐‘)))
21eqeq1d 2732 . . . . . . . . . . . . 13 (๐‘ฆ = ๐‘ค โ†’ ((๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1 โ†” (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1))
3 phimul.6 . . . . . . . . . . . . 13 ๐‘Š = {๐‘ฆ โˆˆ ๐‘† โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
42, 3elrab2 3685 . . . . . . . . . . . 12 (๐‘ค โˆˆ ๐‘Š โ†” (๐‘ค โˆˆ ๐‘† โˆง (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1))
54simplbi 496 . . . . . . . . . . 11 (๐‘ค โˆˆ ๐‘Š โ†’ ๐‘ค โˆˆ ๐‘†)
6 oveq1 7418 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ค โ†’ (๐‘ฅ mod ๐‘€) = (๐‘ค mod ๐‘€))
7 oveq1 7418 . . . . . . . . . . . . 13 (๐‘ฅ = ๐‘ค โ†’ (๐‘ฅ mod ๐‘) = (๐‘ค mod ๐‘))
86, 7opeq12d 4880 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ค โ†’ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
9 crth.3 . . . . . . . . . . . 12 ๐น = (๐‘ฅ โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ)
10 opex 5463 . . . . . . . . . . . 12 โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ โˆˆ V
118, 9, 10fvmpt 6997 . . . . . . . . . . 11 (๐‘ค โˆˆ ๐‘† โ†’ (๐นโ€˜๐‘ค) = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
125, 11syl 17 . . . . . . . . . 10 (๐‘ค โˆˆ ๐‘Š โ†’ (๐นโ€˜๐‘ค) = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
1312adantl 480 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐นโ€˜๐‘ค) = โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
14 crth.1 . . . . . . . . . . . . . . 15 ๐‘† = (0..^(๐‘€ ยท ๐‘))
155, 14eleqtrdi 2841 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ ๐‘Š โ†’ ๐‘ค โˆˆ (0..^(๐‘€ ยท ๐‘)))
1615adantl 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ค โˆˆ (0..^(๐‘€ ยท ๐‘)))
17 elfzoelz 13636 . . . . . . . . . . . . 13 (๐‘ค โˆˆ (0..^(๐‘€ ยท ๐‘)) โ†’ ๐‘ค โˆˆ โ„ค)
1816, 17syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ค โˆˆ โ„ค)
19 crth.4 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• โˆง (๐‘€ gcd ๐‘) = 1))
2019simp1d 1140 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
2120adantr 479 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘€ โˆˆ โ„•)
22 zmodfzo 13863 . . . . . . . . . . . 12 ((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•) โ†’ (๐‘ค mod ๐‘€) โˆˆ (0..^๐‘€))
2318, 21, 22syl2anc 582 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘€) โˆˆ (0..^๐‘€))
24 modgcd 16478 . . . . . . . . . . . . 13 ((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•) โ†’ ((๐‘ค mod ๐‘€) gcd ๐‘€) = (๐‘ค gcd ๐‘€))
2518, 21, 24syl2anc 582 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘€) gcd ๐‘€) = (๐‘ค gcd ๐‘€))
2621nnzd 12589 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘€ โˆˆ โ„ค)
27 gcddvds 16448 . . . . . . . . . . . . . . . . 17 ((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ ๐‘€))
2818, 26, 27syl2anc 582 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ ๐‘€))
2928simpld 493 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆฅ ๐‘ค)
30 nnne0 12250 . . . . . . . . . . . . . . . . . . 19 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โ‰  0)
31 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ค = 0 โˆง ๐‘€ = 0) โ†’ ๐‘€ = 0)
3231necon3ai 2963 . . . . . . . . . . . . . . . . . . 19 (๐‘€ โ‰  0 โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘€ = 0))
3321, 30, 323syl 18 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘€ = 0))
34 gcdn0cl 16447 . . . . . . . . . . . . . . . . . 18 (((๐‘ค โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง ๐‘€ = 0)) โ†’ (๐‘ค gcd ๐‘€) โˆˆ โ„•)
3518, 26, 33, 34syl21anc 834 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆˆ โ„•)
3635nnzd 12589 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆˆ โ„ค)
3719simp2d 1141 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
3837adantr 479 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ โˆˆ โ„•)
3938nnzd 12589 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ โˆˆ โ„ค)
4028simprd 494 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆฅ ๐‘€)
4136, 26, 39, 40dvdsmultr1d 16244 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โˆฅ (๐‘€ ยท ๐‘))
4221, 38nnmulcld 12269 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•)
4342nnzd 12589 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„ค)
44 nnne0 12250 . . . . . . . . . . . . . . . . 17 ((๐‘€ ยท ๐‘) โˆˆ โ„• โ†’ (๐‘€ ยท ๐‘) โ‰  0)
45 simpr 483 . . . . . . . . . . . . . . . . . 18 ((๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0) โ†’ (๐‘€ ยท ๐‘) = 0)
4645necon3ai 2963 . . . . . . . . . . . . . . . . 17 ((๐‘€ ยท ๐‘) โ‰  0 โ†’ ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0))
4742, 44, 463syl 18 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0))
48 dvdslegcd 16449 . . . . . . . . . . . . . . . 16 ((((๐‘ค gcd ๐‘€) โˆˆ โ„ค โˆง ๐‘ค โˆˆ โ„ค โˆง (๐‘€ ยท ๐‘) โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0)) โ†’ (((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ (๐‘€ ยท ๐‘)) โ†’ (๐‘ค gcd ๐‘€) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘))))
4936, 18, 43, 47, 48syl31anc 1371 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (((๐‘ค gcd ๐‘€) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘€) โˆฅ (๐‘€ ยท ๐‘)) โ†’ (๐‘ค gcd ๐‘€) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘))))
5029, 41, 49mp2and 695 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘)))
514simprbi 495 . . . . . . . . . . . . . . 15 (๐‘ค โˆˆ ๐‘Š โ†’ (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1)
5251adantl 480 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd (๐‘€ ยท ๐‘)) = 1)
5350, 52breqtrd 5173 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) โ‰ค 1)
54 nnle1eq1 12246 . . . . . . . . . . . . . 14 ((๐‘ค gcd ๐‘€) โˆˆ โ„• โ†’ ((๐‘ค gcd ๐‘€) โ‰ค 1 โ†” (๐‘ค gcd ๐‘€) = 1))
5535, 54syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘€) โ‰ค 1 โ†” (๐‘ค gcd ๐‘€) = 1))
5653, 55mpbid 231 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘€) = 1)
5725, 56eqtrd 2770 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘€) gcd ๐‘€) = 1)
58 oveq1 7418 . . . . . . . . . . . . 13 (๐‘ฆ = (๐‘ค mod ๐‘€) โ†’ (๐‘ฆ gcd ๐‘€) = ((๐‘ค mod ๐‘€) gcd ๐‘€))
5958eqeq1d 2732 . . . . . . . . . . . 12 (๐‘ฆ = (๐‘ค mod ๐‘€) โ†’ ((๐‘ฆ gcd ๐‘€) = 1 โ†” ((๐‘ค mod ๐‘€) gcd ๐‘€) = 1))
60 phimul.4 . . . . . . . . . . . 12 ๐‘ˆ = {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1}
6159, 60elrab2 3685 . . . . . . . . . . 11 ((๐‘ค mod ๐‘€) โˆˆ ๐‘ˆ โ†” ((๐‘ค mod ๐‘€) โˆˆ (0..^๐‘€) โˆง ((๐‘ค mod ๐‘€) gcd ๐‘€) = 1))
6223, 57, 61sylanbrc 581 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘€) โˆˆ ๐‘ˆ)
63 zmodfzo 13863 . . . . . . . . . . . 12 ((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ค mod ๐‘) โˆˆ (0..^๐‘))
6418, 38, 63syl2anc 582 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘) โˆˆ (0..^๐‘))
65 modgcd 16478 . . . . . . . . . . . . 13 ((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘ค mod ๐‘) gcd ๐‘) = (๐‘ค gcd ๐‘))
6618, 38, 65syl2anc 582 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘) gcd ๐‘) = (๐‘ค gcd ๐‘))
67 gcddvds 16448 . . . . . . . . . . . . . . . . 17 ((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ ๐‘))
6818, 39, 67syl2anc 582 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ ๐‘))
6968simpld 493 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆฅ ๐‘ค)
70 nnne0 12250 . . . . . . . . . . . . . . . . . . 19 (๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0)
71 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ค = 0 โˆง ๐‘ = 0) โ†’ ๐‘ = 0)
7271necon3ai 2963 . . . . . . . . . . . . . . . . . . 19 (๐‘ โ‰  0 โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘ = 0))
7338, 70, 723syl 18 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ยฌ (๐‘ค = 0 โˆง ๐‘ = 0))
74 gcdn0cl 16447 . . . . . . . . . . . . . . . . . 18 (((๐‘ค โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง ๐‘ = 0)) โ†’ (๐‘ค gcd ๐‘) โˆˆ โ„•)
7518, 39, 73, 74syl21anc 834 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆˆ โ„•)
7675nnzd 12589 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆˆ โ„ค)
7768simprd 494 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆฅ ๐‘)
78 dvdsmul2 16226 . . . . . . . . . . . . . . . . 17 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ๐‘ โˆฅ (๐‘€ ยท ๐‘))
7926, 39, 78syl2anc 582 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ๐‘ โˆฅ (๐‘€ ยท ๐‘))
8076, 39, 43, 77, 79dvdstrd 16242 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘))
81 dvdslegcd 16449 . . . . . . . . . . . . . . . 16 ((((๐‘ค gcd ๐‘) โˆˆ โ„ค โˆง ๐‘ค โˆˆ โ„ค โˆง (๐‘€ ยท ๐‘) โˆˆ โ„ค) โˆง ยฌ (๐‘ค = 0 โˆง (๐‘€ ยท ๐‘) = 0)) โ†’ (((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)) โ†’ (๐‘ค gcd ๐‘) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘))))
8276, 18, 43, 47, 81syl31anc 1371 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (((๐‘ค gcd ๐‘) โˆฅ ๐‘ค โˆง (๐‘ค gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)) โ†’ (๐‘ค gcd ๐‘) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘))))
8369, 80, 82mp2and 695 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โ‰ค (๐‘ค gcd (๐‘€ ยท ๐‘)))
8483, 52breqtrd 5173 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) โ‰ค 1)
85 nnle1eq1 12246 . . . . . . . . . . . . . 14 ((๐‘ค gcd ๐‘) โˆˆ โ„• โ†’ ((๐‘ค gcd ๐‘) โ‰ค 1 โ†” (๐‘ค gcd ๐‘) = 1))
8675, 85syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค gcd ๐‘) โ‰ค 1 โ†” (๐‘ค gcd ๐‘) = 1))
8784, 86mpbid 231 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค gcd ๐‘) = 1)
8866, 87eqtrd 2770 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ ((๐‘ค mod ๐‘) gcd ๐‘) = 1)
89 oveq1 7418 . . . . . . . . . . . . 13 (๐‘ฆ = (๐‘ค mod ๐‘) โ†’ (๐‘ฆ gcd ๐‘) = ((๐‘ค mod ๐‘) gcd ๐‘))
9089eqeq1d 2732 . . . . . . . . . . . 12 (๐‘ฆ = (๐‘ค mod ๐‘) โ†’ ((๐‘ฆ gcd ๐‘) = 1 โ†” ((๐‘ค mod ๐‘) gcd ๐‘) = 1))
91 phimul.5 . . . . . . . . . . . 12 ๐‘‰ = {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1}
9290, 91elrab2 3685 . . . . . . . . . . 11 ((๐‘ค mod ๐‘) โˆˆ ๐‘‰ โ†” ((๐‘ค mod ๐‘) โˆˆ (0..^๐‘) โˆง ((๐‘ค mod ๐‘) gcd ๐‘) = 1))
9364, 88, 92sylanbrc 581 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐‘ค mod ๐‘) โˆˆ ๐‘‰)
9462, 93opelxpd 5714 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ โˆˆ (๐‘ˆ ร— ๐‘‰))
9513, 94eqeltrd 2831 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ค โˆˆ ๐‘Š) โ†’ (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰))
9695ralrimiva 3144 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ค โˆˆ ๐‘Š (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰))
97 crth.2 . . . . . . . . . 10 ๐‘‡ = ((0..^๐‘€) ร— (0..^๐‘))
9814, 97, 9, 19crth 16715 . . . . . . . . 9 (๐œ‘ โ†’ ๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡)
99 f1ofn 6833 . . . . . . . . 9 (๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โ†’ ๐น Fn ๐‘†)
100 fnfun 6648 . . . . . . . . 9 (๐น Fn ๐‘† โ†’ Fun ๐น)
10198, 99, 1003syl 18 . . . . . . . 8 (๐œ‘ โ†’ Fun ๐น)
1023ssrab3 4079 . . . . . . . . 9 ๐‘Š โІ ๐‘†
103 fndm 6651 . . . . . . . . . 10 (๐น Fn ๐‘† โ†’ dom ๐น = ๐‘†)
10498, 99, 1033syl 18 . . . . . . . . 9 (๐œ‘ โ†’ dom ๐น = ๐‘†)
105102, 104sseqtrrid 4034 . . . . . . . 8 (๐œ‘ โ†’ ๐‘Š โІ dom ๐น)
106 funimass4 6955 . . . . . . . 8 ((Fun ๐น โˆง ๐‘Š โІ dom ๐น) โ†’ ((๐น โ€œ ๐‘Š) โІ (๐‘ˆ ร— ๐‘‰) โ†” โˆ€๐‘ค โˆˆ ๐‘Š (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰)))
107101, 105, 106syl2anc 582 . . . . . . 7 (๐œ‘ โ†’ ((๐น โ€œ ๐‘Š) โІ (๐‘ˆ ร— ๐‘‰) โ†” โˆ€๐‘ค โˆˆ ๐‘Š (๐นโ€˜๐‘ค) โˆˆ (๐‘ˆ ร— ๐‘‰)))
10896, 107mpbird 256 . . . . . 6 (๐œ‘ โ†’ (๐น โ€œ ๐‘Š) โІ (๐‘ˆ ร— ๐‘‰))
10960ssrab3 4079 . . . . . . . . . . 11 ๐‘ˆ โІ (0..^๐‘€)
11091ssrab3 4079 . . . . . . . . . . 11 ๐‘‰ โІ (0..^๐‘)
111 xpss12 5690 . . . . . . . . . . 11 ((๐‘ˆ โІ (0..^๐‘€) โˆง ๐‘‰ โІ (0..^๐‘)) โ†’ (๐‘ˆ ร— ๐‘‰) โІ ((0..^๐‘€) ร— (0..^๐‘)))
112109, 110, 111mp2an 688 . . . . . . . . . 10 (๐‘ˆ ร— ๐‘‰) โІ ((0..^๐‘€) ร— (0..^๐‘))
113112, 97sseqtrri 4018 . . . . . . . . 9 (๐‘ˆ ร— ๐‘‰) โІ ๐‘‡
114113sseli 3977 . . . . . . . 8 (๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰) โ†’ ๐‘ง โˆˆ ๐‘‡)
115 f1ocnvfv2 7277 . . . . . . . 8 ((๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โˆง ๐‘ง โˆˆ ๐‘‡) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = ๐‘ง)
11698, 114, 115syl2an 594 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = ๐‘ง)
117 f1ocnv 6844 . . . . . . . . . . 11 (๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โ†’ โ—ก๐น:๐‘‡โ€“1-1-ontoโ†’๐‘†)
118 f1of 6832 . . . . . . . . . . 11 (โ—ก๐น:๐‘‡โ€“1-1-ontoโ†’๐‘† โ†’ โ—ก๐น:๐‘‡โŸถ๐‘†)
11998, 117, 1183syl 18 . . . . . . . . . 10 (๐œ‘ โ†’ โ—ก๐น:๐‘‡โŸถ๐‘†)
120 ffvelcdm 7082 . . . . . . . . . 10 ((โ—ก๐น:๐‘‡โŸถ๐‘† โˆง ๐‘ง โˆˆ ๐‘‡) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘†)
121119, 114, 120syl2an 594 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘†)
122121, 14eleqtrdi 2841 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ (0..^(๐‘€ ยท ๐‘)))
123 elfzoelz 13636 . . . . . . . . . . . . 13 ((โ—ก๐นโ€˜๐‘ง) โˆˆ (0..^(๐‘€ ยท ๐‘)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค)
124122, 123syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค)
12520adantr 479 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘€ โˆˆ โ„•)
126 modgcd 16478 . . . . . . . . . . . 12 (((โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„•) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€))
127124, 125, 126syl2anc 582 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€))
128 oveq1 7418 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค = (โ—ก๐นโ€˜๐‘ง) โ†’ (๐‘ค mod ๐‘€) = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€))
129 oveq1 7418 . . . . . . . . . . . . . . . . . . . 20 (๐‘ค = (โ—ก๐นโ€˜๐‘ง) โ†’ (๐‘ค mod ๐‘) = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘))
130128, 129opeq12d 4880 . . . . . . . . . . . . . . . . . . 19 (๐‘ค = (โ—ก๐นโ€˜๐‘ง) โ†’ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
1318cbvmptv 5260 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ฅ mod ๐‘€), (๐‘ฅ mod ๐‘)โŸฉ) = (๐‘ค โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
1329, 131eqtri 2758 . . . . . . . . . . . . . . . . . . 19 ๐น = (๐‘ค โˆˆ ๐‘† โ†ฆ โŸจ(๐‘ค mod ๐‘€), (๐‘ค mod ๐‘)โŸฉ)
133 opex 5463 . . . . . . . . . . . . . . . . . . 19 โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ โˆˆ V
134130, 132, 133fvmpt 6997 . . . . . . . . . . . . . . . . . 18 ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘† โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
135121, 134syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
136116, 135eqtr3d 2772 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ง = โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ)
137 simpr 483 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰))
138136, 137eqeltrrd 2832 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ โˆˆ (๐‘ˆ ร— ๐‘‰))
139 opelxp 5711 . . . . . . . . . . . . . . 15 (โŸจ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€), ((โ—ก๐นโ€˜๐‘ง) mod ๐‘)โŸฉ โˆˆ (๐‘ˆ ร— ๐‘‰) โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ โˆง ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰))
140138, 139sylib 217 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ โˆง ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰))
141140simpld 493 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ)
142 oveq1 7418 . . . . . . . . . . . . . . 15 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โ†’ (๐‘ฆ gcd ๐‘€) = (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€))
143142eqeq1d 2732 . . . . . . . . . . . . . 14 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โ†’ ((๐‘ฆ gcd ๐‘€) = 1 โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1))
144143, 60elrab2 3685 . . . . . . . . . . . . 13 (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ ๐‘ˆ โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ (0..^๐‘€) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1))
145141, 144sylib 217 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) โˆˆ (0..^๐‘€) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1))
146145simprd 494 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘€) gcd ๐‘€) = 1)
147127, 146eqtr3d 2772 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€) = 1)
14837adantr 479 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ โˆˆ โ„•)
149 modgcd 16478 . . . . . . . . . . . 12 (((โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„•) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘))
150124, 148, 149syl2anc 582 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘))
151140simprd 494 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰)
152 oveq1 7418 . . . . . . . . . . . . . . 15 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โ†’ (๐‘ฆ gcd ๐‘) = (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘))
153152eqeq1d 2732 . . . . . . . . . . . . . 14 (๐‘ฆ = ((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โ†’ ((๐‘ฆ gcd ๐‘) = 1 โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1))
154153, 91elrab2 3685 . . . . . . . . . . . . 13 (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ ๐‘‰ โ†” (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ (0..^๐‘) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1))
155151, 154sylib 217 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) โˆˆ (0..^๐‘) โˆง (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1))
156155simprd 494 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (((โ—ก๐นโ€˜๐‘ง) mod ๐‘) gcd ๐‘) = 1)
157150, 156eqtr3d 2772 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘) = 1)
15820nnzd 12589 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
159158adantr 479 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘€ โˆˆ โ„ค)
16037nnzd 12589 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
161160adantr 479 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ โˆˆ โ„ค)
162 rpmul 16600 . . . . . . . . . . 11 (((โ—ก๐นโ€˜๐‘ง) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€) = 1 โˆง ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘) = 1) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
163124, 159, 161, 162syl3anc 1369 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((((โ—ก๐นโ€˜๐‘ง) gcd ๐‘€) = 1 โˆง ((โ—ก๐นโ€˜๐‘ง) gcd ๐‘) = 1) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
164147, 157, 163mp2and 695 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1)
165 oveq1 7418 . . . . . . . . . . 11 (๐‘ฆ = (โ—ก๐นโ€˜๐‘ง) โ†’ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)))
166165eqeq1d 2732 . . . . . . . . . 10 (๐‘ฆ = (โ—ก๐นโ€˜๐‘ง) โ†’ ((๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1 โ†” ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
167166, 3elrab2 3685 . . . . . . . . 9 ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š โ†” ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘† โˆง ((โ—ก๐นโ€˜๐‘ง) gcd (๐‘€ ยท ๐‘)) = 1))
168121, 164, 167sylanbrc 581 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š)
169 funfvima2 7234 . . . . . . . . . 10 ((Fun ๐น โˆง ๐‘Š โІ dom ๐น) โ†’ ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š)))
170101, 105, 169syl2anc 582 . . . . . . . . 9 (๐œ‘ โ†’ ((โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š)))
171170imp 405 . . . . . . . 8 ((๐œ‘ โˆง (โ—ก๐นโ€˜๐‘ง) โˆˆ ๐‘Š) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š))
172168, 171syldan 589 . . . . . . 7 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘ง)) โˆˆ (๐น โ€œ ๐‘Š))
173116, 172eqeltrrd 2832 . . . . . 6 ((๐œ‘ โˆง ๐‘ง โˆˆ (๐‘ˆ ร— ๐‘‰)) โ†’ ๐‘ง โˆˆ (๐น โ€œ ๐‘Š))
174108, 173eqelssd 4002 . . . . 5 (๐œ‘ โ†’ (๐น โ€œ ๐‘Š) = (๐‘ˆ ร— ๐‘‰))
175 f1of1 6831 . . . . . . 7 (๐น:๐‘†โ€“1-1-ontoโ†’๐‘‡ โ†’ ๐น:๐‘†โ€“1-1โ†’๐‘‡)
17698, 175syl 17 . . . . . 6 (๐œ‘ โ†’ ๐น:๐‘†โ€“1-1โ†’๐‘‡)
177 fzofi 13943 . . . . . . . . . 10 (0..^(๐‘€ ยท ๐‘)) โˆˆ Fin
17814, 177eqeltri 2827 . . . . . . . . 9 ๐‘† โˆˆ Fin
179 ssfi 9175 . . . . . . . . 9 ((๐‘† โˆˆ Fin โˆง ๐‘Š โІ ๐‘†) โ†’ ๐‘Š โˆˆ Fin)
180178, 102, 179mp2an 688 . . . . . . . 8 ๐‘Š โˆˆ Fin
181180elexi 3492 . . . . . . 7 ๐‘Š โˆˆ V
182181f1imaen 9014 . . . . . 6 ((๐น:๐‘†โ€“1-1โ†’๐‘‡ โˆง ๐‘Š โІ ๐‘†) โ†’ (๐น โ€œ ๐‘Š) โ‰ˆ ๐‘Š)
183176, 102, 182sylancl 584 . . . . 5 (๐œ‘ โ†’ (๐น โ€œ ๐‘Š) โ‰ˆ ๐‘Š)
184174, 183eqbrtrrd 5171 . . . 4 (๐œ‘ โ†’ (๐‘ˆ ร— ๐‘‰) โ‰ˆ ๐‘Š)
185 fzofi 13943 . . . . . . . 8 (0..^๐‘€) โˆˆ Fin
186 ssrab2 4076 . . . . . . . 8 {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โІ (0..^๐‘€)
187 ssfi 9175 . . . . . . . 8 (((0..^๐‘€) โˆˆ Fin โˆง {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โІ (0..^๐‘€)) โ†’ {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โˆˆ Fin)
188185, 186, 187mp2an 688 . . . . . . 7 {๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1} โˆˆ Fin
18960, 188eqeltri 2827 . . . . . 6 ๐‘ˆ โˆˆ Fin
190 fzofi 13943 . . . . . . . 8 (0..^๐‘) โˆˆ Fin
191 ssrab2 4076 . . . . . . . 8 {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โІ (0..^๐‘)
192 ssfi 9175 . . . . . . . 8 (((0..^๐‘) โˆˆ Fin โˆง {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โІ (0..^๐‘)) โ†’ {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โˆˆ Fin)
193190, 191, 192mp2an 688 . . . . . . 7 {๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1} โˆˆ Fin
19491, 193eqeltri 2827 . . . . . 6 ๐‘‰ โˆˆ Fin
195 xpfi 9319 . . . . . 6 ((๐‘ˆ โˆˆ Fin โˆง ๐‘‰ โˆˆ Fin) โ†’ (๐‘ˆ ร— ๐‘‰) โˆˆ Fin)
196189, 194, 195mp2an 688 . . . . 5 (๐‘ˆ ร— ๐‘‰) โˆˆ Fin
197 hashen 14311 . . . . 5 (((๐‘ˆ ร— ๐‘‰) โˆˆ Fin โˆง ๐‘Š โˆˆ Fin) โ†’ ((โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = (โ™ฏโ€˜๐‘Š) โ†” (๐‘ˆ ร— ๐‘‰) โ‰ˆ ๐‘Š))
198196, 180, 197mp2an 688 . . . 4 ((โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = (โ™ฏโ€˜๐‘Š) โ†” (๐‘ˆ ร— ๐‘‰) โ‰ˆ ๐‘Š)
199184, 198sylibr 233 . . 3 (๐œ‘ โ†’ (โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = (โ™ฏโ€˜๐‘Š))
200 hashxp 14398 . . . 4 ((๐‘ˆ โˆˆ Fin โˆง ๐‘‰ โˆˆ Fin) โ†’ (โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰)))
201189, 194, 200mp2an 688 . . 3 (โ™ฏโ€˜(๐‘ˆ ร— ๐‘‰)) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰))
202199, 201eqtr3di 2785 . 2 (๐œ‘ โ†’ (โ™ฏโ€˜๐‘Š) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰)))
20320, 37nnmulcld 12269 . . 3 (๐œ‘ โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•)
204 dfphi2 16711 . . . 4 ((๐‘€ ยท ๐‘) โˆˆ โ„• โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}))
20514rabeqi 3443 . . . . . 6 {๐‘ฆ โˆˆ ๐‘† โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1} = {๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
2063, 205eqtri 2758 . . . . 5 ๐‘Š = {๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1}
207206fveq2i 6893 . . . 4 (โ™ฏโ€˜๐‘Š) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^(๐‘€ ยท ๐‘)) โˆฃ (๐‘ฆ gcd (๐‘€ ยท ๐‘)) = 1})
208204, 207eqtr4di 2788 . . 3 ((๐‘€ ยท ๐‘) โˆˆ โ„• โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = (โ™ฏโ€˜๐‘Š))
209203, 208syl 17 . 2 (๐œ‘ โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = (โ™ฏโ€˜๐‘Š))
210 dfphi2 16711 . . . . 5 (๐‘€ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘€) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1}))
21160fveq2i 6893 . . . . 5 (โ™ฏโ€˜๐‘ˆ) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘€) โˆฃ (๐‘ฆ gcd ๐‘€) = 1})
212210, 211eqtr4di 2788 . . . 4 (๐‘€ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘€) = (โ™ฏโ€˜๐‘ˆ))
21320, 212syl 17 . . 3 (๐œ‘ โ†’ (ฯ•โ€˜๐‘€) = (โ™ฏโ€˜๐‘ˆ))
214 dfphi2 16711 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1}))
21591fveq2i 6893 . . . . 5 (โ™ฏโ€˜๐‘‰) = (โ™ฏโ€˜{๐‘ฆ โˆˆ (0..^๐‘) โˆฃ (๐‘ฆ gcd ๐‘) = 1})
216214, 215eqtr4di 2788 . . . 4 (๐‘ โˆˆ โ„• โ†’ (ฯ•โ€˜๐‘) = (โ™ฏโ€˜๐‘‰))
21737, 216syl 17 . . 3 (๐œ‘ โ†’ (ฯ•โ€˜๐‘) = (โ™ฏโ€˜๐‘‰))
218213, 217oveq12d 7429 . 2 (๐œ‘ โ†’ ((ฯ•โ€˜๐‘€) ยท (ฯ•โ€˜๐‘)) = ((โ™ฏโ€˜๐‘ˆ) ยท (โ™ฏโ€˜๐‘‰)))
219202, 209, 2183eqtr4d 2780 1 (๐œ‘ โ†’ (ฯ•โ€˜(๐‘€ ยท ๐‘)) = ((ฯ•โ€˜๐‘€) ยท (ฯ•โ€˜๐‘)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆง w3a 1085   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2938  โˆ€wral 3059  {crab 3430   โІ wss 3947  โŸจcop 4633   class class class wbr 5147   โ†ฆ cmpt 5230   ร— cxp 5673  โ—กccnv 5674  dom cdm 5675   โ€œ cima 5678  Fun wfun 6536   Fn wfn 6537  โŸถwf 6538  โ€“1-1โ†’wf1 6539  โ€“1-1-ontoโ†’wf1o 6541  โ€˜cfv 6542  (class class class)co 7411   โ‰ˆ cen 8938  Fincfn 8941  0cc0 11112  1c1 11113   ยท cmul 11117   โ‰ค cle 11253  โ„•cn 12216  โ„คcz 12562  ..^cfzo 13631   mod cmo 13838  โ™ฏchash 14294   โˆฅ cdvds 16201   gcd cgcd 16439  ฯ•cphi 16701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-rp 12979  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-hash 14295  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-dvds 16202  df-gcd 16440  df-phi 16703
This theorem is referenced by:  phimul  16717
  Copyright terms: Public domain W3C validator