Metamath Proof Explorer


Theorem odmulg2

Description: The order of a multiple divides the order of the base point. (Contributed by Stefan O'Rear, 6-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 odmulgid.1 โŠข ๐‘‹ = ( Base โ€˜ ๐บ )
2 odmulgid.2 โŠข ๐‘‚ = ( od โ€˜ ๐บ )
3 odmulgid.3 โŠข ยท = ( .g โ€˜ ๐บ )
4 1 2 odcl โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„•0 )
5 4 nn0zd โŠข ( ๐ด โˆˆ ๐‘‹ โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„ค )
6 5 3ad2ant2 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„ค )
7 simp3 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ๐‘ โˆˆ โ„ค )
8 dvdsmul1 โŠข ( ( ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ( ๐‘‚ โ€˜ ๐ด ) ยท ๐‘ ) )
9 6 7 8 syl2anc โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ( ๐‘‚ โ€˜ ๐ด ) ยท ๐‘ ) )
10 1 2 3 odmulgid โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘‚ โ€˜ ๐ด ) โˆˆ โ„ค ) โ†’ ( ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆฅ ( ๐‘‚ โ€˜ ๐ด ) โ†” ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ( ๐‘‚ โ€˜ ๐ด ) ยท ๐‘ ) ) )
11 6 10 mpdan โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆฅ ( ๐‘‚ โ€˜ ๐ด ) โ†” ( ๐‘‚ โ€˜ ๐ด ) โˆฅ ( ( ๐‘‚ โ€˜ ๐ด ) ยท ๐‘ ) ) )
12 9 11 mpbird โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘‚ โ€˜ ( ๐‘ ยท ๐ด ) ) โˆฅ ( ๐‘‚ โ€˜ ๐ด ) )