Metamath Proof Explorer


Theorem odmulg

Description: Relationship between the order of an element and that of a multiple. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odmulgid.1 โŠข ๐‘‹ = ( Base โ€˜ ๐บ )
odmulgid.2 โŠข ๐‘‚ = ( od โ€˜ ๐บ )
odmulgid.3 โŠข ยท = ( .g โ€˜ ๐บ )
Assertion odmulg ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) = ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) )

Proof

Step Hyp Ref Expression
1 odmulgid.1 โŠข ๐‘‹ = ( Base โ€˜ ๐บ )
2 odmulgid.2 โŠข ๐‘‚ = ( od โ€˜ ๐บ )
3 odmulgid.3 โŠข ยท = ( .g โ€˜ ๐บ )
4 1 3 mulgcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ โˆˆ โ„ค โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ๐‘ ยท ๐ด ) โˆˆ ๐‘‹ )
5 4 3com23 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ ยท ๐ด ) โˆˆ ๐‘‹ )
6 1 2 odcl โŠข ( ( ๐‘ ยท ๐ด ) โˆˆ ๐‘‹ โ†’ ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„•0 )
7 5 6 syl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„•0 )
8 7 nn0cnd โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„‚ )
9 8 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) = 0 ) โ†’ ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„‚ )
10 9 mul02d โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) = 0 ) โ†’ ( 0 ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) = 0 )
11 simpr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) = 0 ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) = 0 )
12 11 oveq1d โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) = 0 ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) = ( 0 ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) )
13 simp3 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ๐‘ โˆˆ โ„ค )
14 1 2 odcl โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„•0 )
15 14 3ad2ant2 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„•0 )
16 15 nn0zd โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„ค )
17 gcdeq0 โŠข ( ( ๐‘ โˆˆ โ„ค โˆง ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„ค ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) = 0 โ†” ( ๐‘ = 0 โˆง ( ๐‘‚ โ€˜ ๐ด ) = 0 ) ) )
18 13 16 17 syl2anc โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) = 0 โ†” ( ๐‘ = 0 โˆง ( ๐‘‚ โ€˜ ๐ด ) = 0 ) ) )
19 18 simplbda โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) = 0 ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) = 0 )
20 10 12 19 3eqtr4rd โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) = 0 ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) = ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) )
21 simpll3 โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ๐‘ โˆˆ โ„ค )
22 16 ad2antrr โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„ค )
23 gcddvds โŠข ( ( ๐‘ โˆˆ โ„ค โˆง ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„ค ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ( ๐‘‚ โ€˜ ๐ด ) ) )
24 21 22 23 syl2anc โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ( ๐‘‚ โ€˜ ๐ด ) ) )
25 24 simprd โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ( ๐‘‚ โ€˜ ๐ด ) )
26 13 16 gcdcld โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„•0 )
27 26 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„•0 )
28 27 nn0zd โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„ค )
29 28 adantr โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„ค )
30 nn0z โŠข ( ๐‘ฅ โˆˆ โ„•0 โ†’ ๐‘ฅ โˆˆ โ„ค )
31 30 adantl โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ๐‘ฅ โˆˆ โ„ค )
32 dvdstr โŠข ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„ค โˆง ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ( ๐‘‚ โ€˜ ๐ด ) โˆง ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ ) )
33 29 22 31 32 syl3anc โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ( ๐‘‚ โ€˜ ๐ด ) โˆง ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ ) )
34 25 33 mpand โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ ) )
35 7 nn0zd โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„ค )
36 35 ad2antrr โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„ค )
37 muldvds1 โŠข ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„ค โˆง ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ ) )
38 29 36 31 37 syl3anc โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ ) )
39 dvdszrcl โŠข ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค ) )
40 divides โŠข ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ โ†” โˆƒ ๐‘ฆ โˆˆ โ„ค ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) = ๐‘ฅ ) )
41 39 40 syl โŠข ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ โ†” โˆƒ ๐‘ฆ โˆˆ โ„ค ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) = ๐‘ฅ ) )
42 41 ibi โŠข ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ โ†’ โˆƒ ๐‘ฆ โˆˆ โ„ค ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) = ๐‘ฅ )
43 35 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„ค )
44 simprr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ๐‘ฆ โˆˆ โ„ค )
45 28 adantrr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„ค )
46 simprl โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 )
47 dvdscmulr โŠข ( ( ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„ค โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) ) โ†’ ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ๐‘ฆ ) โ†” ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆฅ ๐‘ฆ ) )
48 43 44 45 46 47 syl112anc โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ๐‘ฆ ) โ†” ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆฅ ๐‘ฆ ) )
49 1 2 3 odmulgid โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ๐‘ฆ โˆˆ โ„ค ) โ†’ ( ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆฅ ๐‘ฆ โ†” ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ๐‘ ) ) )
50 49 adantrl โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆฅ ๐‘ฆ โ†” ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ๐‘ ) ) )
51 simpl3 โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ๐‘ โˆˆ โ„ค )
52 dvdsmulgcd โŠข ( ( ๐‘ฆ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ๐‘ ) โ†” ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) ) )
53 44 51 52 syl2anc โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ๐‘ ) โ†” ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) ) )
54 48 50 53 3bitrrd โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ๐‘ฆ ) ) )
55 45 zcnd โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆˆ โ„‚ )
56 44 zcnd โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ๐‘ฆ โˆˆ โ„‚ )
57 55 56 mulcomd โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ๐‘ฆ ) = ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) )
58 57 breq2d โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ๐‘ฆ ) โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) ) )
59 54 58 bitrd โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) ) )
60 59 anassrs โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฆ โˆˆ โ„ค ) โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) ) )
61 breq2 โŠข ( ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) = ๐‘ฅ โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) โ†” ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ ) )
62 breq2 โŠข ( ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) = ๐‘ฅ โ†’ ( ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) )
63 61 62 bibi12d โŠข ( ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) = ๐‘ฅ โ†’ ( ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) ) โ†” ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) ) )
64 60 63 syl5ibcom โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฆ โˆˆ โ„ค ) โ†’ ( ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) = ๐‘ฅ โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) ) )
65 64 rexlimdva โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ ( โˆƒ ๐‘ฆ โˆˆ โ„ค ( ๐‘ฆ ยท ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ) = ๐‘ฅ โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) ) )
66 42 65 syl5 โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) ) )
67 66 adantr โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โˆฅ ๐‘ฅ โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) ) )
68 34 38 67 pm5.21ndd โŠข ( ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โˆง ๐‘ฅ โˆˆ โ„•0 ) โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) )
69 68 ralrimiva โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„•0 ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) )
70 15 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„•0 )
71 7 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆˆ โ„•0 )
72 27 71 nn0mulcld โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆˆ โ„•0 )
73 dvdsext โŠข ( ( ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„•0 โˆง ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆˆ โ„•0 ) โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) = ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„•0 ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) ) )
74 70 72 73 syl2anc โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ ( ( ๐‘‚ โ€˜ ๐ด ) = ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„•0 ( ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ๐‘ฅ โ†” ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) โˆฅ ๐‘ฅ ) ) )
75 69 74 mpbird โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) โ‰  0 ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) = ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) )
76 20 75 pm2.61dane โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) = ( ( ๐‘ gcd ( ๐‘‚ โ€˜ ๐ด ) ) ยท ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) ) )