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

Theorem oddvds 18685
 Description: The only multiples of 𝐴 that are equal to the identity are the multiples of the order of 𝐴. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
Hypotheses
Ref Expression
odcl.1 𝑋 = (Base‘𝐺)
odcl.2 𝑂 = (od‘𝐺)
odid.3 · = (.g𝐺)
odid.4 0 = (0g𝐺)
Assertion
Ref Expression
oddvds ((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) → ((𝑂𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 ))

Proof of Theorem oddvds
StepHypRef Expression
1 simpr 488 . . . 4 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (𝑂𝐴) ∈ ℕ)
2 simpl3 1190 . . . 4 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → 𝑁 ∈ ℤ)
3 dvdsval3 15620 . . . 4 (((𝑂𝐴) ∈ ℕ ∧ 𝑁 ∈ ℤ) → ((𝑂𝐴) ∥ 𝑁 ↔ (𝑁 mod (𝑂𝐴)) = 0))
41, 2, 3syl2anc 587 . . 3 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → ((𝑂𝐴) ∥ 𝑁 ↔ (𝑁 mod (𝑂𝐴)) = 0))
5 simpl2 1189 . . . . . 6 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → 𝐴𝑋)
6 odcl.1 . . . . . . 7 𝑋 = (Base‘𝐺)
7 odid.4 . . . . . . 7 0 = (0g𝐺)
8 odid.3 . . . . . . 7 · = (.g𝐺)
96, 7, 8mulg0 18241 . . . . . 6 (𝐴𝑋 → (0 · 𝐴) = 0 )
105, 9syl 17 . . . . 5 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (0 · 𝐴) = 0 )
11 oveq1 7149 . . . . . 6 ((𝑁 mod (𝑂𝐴)) = 0 → ((𝑁 mod (𝑂𝐴)) · 𝐴) = (0 · 𝐴))
1211eqeq1d 2800 . . . . 5 ((𝑁 mod (𝑂𝐴)) = 0 → (((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 ↔ (0 · 𝐴) = 0 ))
1310, 12syl5ibrcom 250 . . . 4 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → ((𝑁 mod (𝑂𝐴)) = 0 → ((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 ))
142zred 12092 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → 𝑁 ∈ ℝ)
151nnrpd 12434 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (𝑂𝐴) ∈ ℝ+)
16 modlt 13260 . . . . . . . 8 ((𝑁 ∈ ℝ ∧ (𝑂𝐴) ∈ ℝ+) → (𝑁 mod (𝑂𝐴)) < (𝑂𝐴))
1714, 15, 16syl2anc 587 . . . . . . 7 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (𝑁 mod (𝑂𝐴)) < (𝑂𝐴))
182, 1zmodcld 13272 . . . . . . . . 9 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (𝑁 mod (𝑂𝐴)) ∈ ℕ0)
1918nn0red 11961 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (𝑁 mod (𝑂𝐴)) ∈ ℝ)
201nnred 11655 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (𝑂𝐴) ∈ ℝ)
2119, 20ltnled 10791 . . . . . . 7 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → ((𝑁 mod (𝑂𝐴)) < (𝑂𝐴) ↔ ¬ (𝑂𝐴) ≤ (𝑁 mod (𝑂𝐴))))
2217, 21mpbid 235 . . . . . 6 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → ¬ (𝑂𝐴) ≤ (𝑁 mod (𝑂𝐴)))
23 odcl.2 . . . . . . . . . . . 12 𝑂 = (od‘𝐺)
246, 23, 8, 7odlem2 18677 . . . . . . . . . . 11 ((𝐴𝑋 ∧ (𝑁 mod (𝑂𝐴)) ∈ ℕ ∧ ((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 ) → (𝑂𝐴) ∈ (1...(𝑁 mod (𝑂𝐴))))
25 elfzle2 12923 . . . . . . . . . . 11 ((𝑂𝐴) ∈ (1...(𝑁 mod (𝑂𝐴))) → (𝑂𝐴) ≤ (𝑁 mod (𝑂𝐴)))
2624, 25syl 17 . . . . . . . . . 10 ((𝐴𝑋 ∧ (𝑁 mod (𝑂𝐴)) ∈ ℕ ∧ ((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 ) → (𝑂𝐴) ≤ (𝑁 mod (𝑂𝐴)))
27263com23 1123 . . . . . . . . 9 ((𝐴𝑋 ∧ ((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 ∧ (𝑁 mod (𝑂𝐴)) ∈ ℕ) → (𝑂𝐴) ≤ (𝑁 mod (𝑂𝐴)))
28273expia 1118 . . . . . . . 8 ((𝐴𝑋 ∧ ((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 ) → ((𝑁 mod (𝑂𝐴)) ∈ ℕ → (𝑂𝐴) ≤ (𝑁 mod (𝑂𝐴))))
2928con3d 155 . . . . . . 7 ((𝐴𝑋 ∧ ((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 ) → (¬ (𝑂𝐴) ≤ (𝑁 mod (𝑂𝐴)) → ¬ (𝑁 mod (𝑂𝐴)) ∈ ℕ))
3029impancom 455 . . . . . 6 ((𝐴𝑋 ∧ ¬ (𝑂𝐴) ≤ (𝑁 mod (𝑂𝐴))) → (((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 → ¬ (𝑁 mod (𝑂𝐴)) ∈ ℕ))
315, 22, 30syl2anc 587 . . . . 5 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 → ¬ (𝑁 mod (𝑂𝐴)) ∈ ℕ))
32 elnn0 11902 . . . . . . 7 ((𝑁 mod (𝑂𝐴)) ∈ ℕ0 ↔ ((𝑁 mod (𝑂𝐴)) ∈ ℕ ∨ (𝑁 mod (𝑂𝐴)) = 0))
3318, 32sylib 221 . . . . . 6 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → ((𝑁 mod (𝑂𝐴)) ∈ ℕ ∨ (𝑁 mod (𝑂𝐴)) = 0))
3433ord 861 . . . . 5 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (¬ (𝑁 mod (𝑂𝐴)) ∈ ℕ → (𝑁 mod (𝑂𝐴)) = 0))
3531, 34syld 47 . . . 4 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 → (𝑁 mod (𝑂𝐴)) = 0))
3613, 35impbid 215 . . 3 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → ((𝑁 mod (𝑂𝐴)) = 0 ↔ ((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 ))
376, 23, 8, 7odmod 18684 . . . 4 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → ((𝑁 mod (𝑂𝐴)) · 𝐴) = (𝑁 · 𝐴))
3837eqeq1d 2800 . . 3 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → (((𝑁 mod (𝑂𝐴)) · 𝐴) = 0 ↔ (𝑁 · 𝐴) = 0 ))
394, 36, 383bitrd 308 . 2 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) ∈ ℕ) → ((𝑂𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 ))
40 simpr 488 . . . 4 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → (𝑂𝐴) = 0)
4140breq1d 5043 . . 3 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → ((𝑂𝐴) ∥ 𝑁 ↔ 0 ∥ 𝑁))
42 simpl3 1190 . . . 4 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → 𝑁 ∈ ℤ)
43 0dvds 15639 . . . 4 (𝑁 ∈ ℤ → (0 ∥ 𝑁𝑁 = 0))
4442, 43syl 17 . . 3 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → (0 ∥ 𝑁𝑁 = 0))
45 simpl2 1189 . . . . . 6 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → 𝐴𝑋)
4645, 9syl 17 . . . . 5 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → (0 · 𝐴) = 0 )
47 oveq1 7149 . . . . . 6 (𝑁 = 0 → (𝑁 · 𝐴) = (0 · 𝐴))
4847eqeq1d 2800 . . . . 5 (𝑁 = 0 → ((𝑁 · 𝐴) = 0 ↔ (0 · 𝐴) = 0 ))
4946, 48syl5ibrcom 250 . . . 4 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → (𝑁 = 0 → (𝑁 · 𝐴) = 0 ))
506, 23, 8, 7odnncl 18683 . . . . . . . . 9 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑁 ≠ 0 ∧ (𝑁 · 𝐴) = 0 )) → (𝑂𝐴) ∈ ℕ)
5150nnne0d 11690 . . . . . . . 8 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑁 ≠ 0 ∧ (𝑁 · 𝐴) = 0 )) → (𝑂𝐴) ≠ 0)
5251expr 460 . . . . . . 7 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ((𝑁 · 𝐴) = 0 → (𝑂𝐴) ≠ 0))
5352impancom 455 . . . . . 6 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑁 · 𝐴) = 0 ) → (𝑁 ≠ 0 → (𝑂𝐴) ≠ 0))
5453necon4d 3011 . . . . 5 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑁 · 𝐴) = 0 ) → ((𝑂𝐴) = 0 → 𝑁 = 0))
5554impancom 455 . . . 4 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → ((𝑁 · 𝐴) = 0𝑁 = 0))
5649, 55impbid 215 . . 3 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → (𝑁 = 0 ↔ (𝑁 · 𝐴) = 0 ))
5741, 44, 563bitrd 308 . 2 (((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) ∧ (𝑂𝐴) = 0) → ((𝑂𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 ))
586, 23odcl 18674 . . . 4 (𝐴𝑋 → (𝑂𝐴) ∈ ℕ0)
59583ad2ant2 1131 . . 3 ((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) → (𝑂𝐴) ∈ ℕ0)
60 elnn0 11902 . . 3 ((𝑂𝐴) ∈ ℕ0 ↔ ((𝑂𝐴) ∈ ℕ ∨ (𝑂𝐴) = 0))
6159, 60sylib 221 . 2 ((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) → ((𝑂𝐴) ∈ ℕ ∨ (𝑂𝐴) = 0))
6239, 57, 61mpjaodan 956 1 ((𝐺 ∈ Grp ∧ 𝐴𝑋𝑁 ∈ ℤ) → ((𝑂𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987   class class class wbr 5033  ‘cfv 6329  (class class class)co 7142  ℝcr 10540  0cc0 10541  1c1 10542   < clt 10679   ≤ cle 10680  ℕcn 11640  ℕ0cn0 11900  ℤcz 11986  ℝ+crp 12394  ...cfz 12902   mod cmo 13249   ∥ cdvds 15616  Basecbs 16492  0gc0g 16722  Grpcgrp 18112  .gcmg 18234  odcod 18662 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618  ax-pre-sup 10619 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7571  df-1st 7681  df-2nd 7682  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-er 8287  df-en 8508  df-dom 8509  df-sdom 8510  df-sup 8905  df-inf 8906  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-div 11302  df-nn 11641  df-2 11703  df-3 11704  df-n0 11901  df-z 11987  df-uz 12249  df-rp 12395  df-fz 12903  df-fl 13174  df-mod 13250  df-seq 13382  df-exp 13443  df-cj 14467  df-re 14468  df-im 14469  df-sqrt 14603  df-abs 14604  df-dvds 15617  df-0g 16724  df-mgm 17861  df-sgrp 17910  df-mnd 17921  df-grp 18115  df-minusg 18116  df-sbg 18117  df-mulg 18235  df-od 18666 This theorem is referenced by:  oddvdsi  18686  odcong  18687  odeq  18688  odmulgid  18691  odbezout  18695  gexdvds2  18720  gexod  18721  gexcl3  18722  odadd1  18979  odadd2  18980  oddvdssubg  18986  pgpfac1lem3a  19209  ablsimpgfindlem2  19241  chrdvds  20239  dchrfi  25880  dchrabs  25885  dchrptlem2  25890  idomodle  40227
 Copyright terms: Public domain W3C validator