![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > odcl | Structured version Visualization version GIF version |
Description: The order of a group element is always a nonnegative integer. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.) |
Ref | Expression |
---|---|
odcl.1 | ⊢ 𝑋 = (Base‘𝐺) |
odcl.2 | ⊢ 𝑂 = (od‘𝐺) |
Ref | Expression |
---|---|
odcl | ⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) ∈ ℕ0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | odcl.1 | . . . . 5 ⊢ 𝑋 = (Base‘𝐺) | |
2 | eqid 2692 | . . . . 5 ⊢ (.g‘𝐺) = (.g‘𝐺) | |
3 | eqid 2692 | . . . . 5 ⊢ (0g‘𝐺) = (0g‘𝐺) | |
4 | odcl.2 | . . . . 5 ⊢ 𝑂 = (od‘𝐺) | |
5 | eqid 2692 | . . . . 5 ⊢ {𝑦 ∈ ℕ ∣ (𝑦(.g‘𝐺)𝐴) = (0g‘𝐺)} = {𝑦 ∈ ℕ ∣ (𝑦(.g‘𝐺)𝐴) = (0g‘𝐺)} | |
6 | 1, 2, 3, 4, 5 | odlem1 18043 | . . . 4 ⊢ (𝐴 ∈ 𝑋 → (((𝑂‘𝐴) = 0 ∧ {𝑦 ∈ ℕ ∣ (𝑦(.g‘𝐺)𝐴) = (0g‘𝐺)} = ∅) ∨ (𝑂‘𝐴) ∈ {𝑦 ∈ ℕ ∣ (𝑦(.g‘𝐺)𝐴) = (0g‘𝐺)})) |
7 | simpl 474 | . . . . 5 ⊢ (((𝑂‘𝐴) = 0 ∧ {𝑦 ∈ ℕ ∣ (𝑦(.g‘𝐺)𝐴) = (0g‘𝐺)} = ∅) → (𝑂‘𝐴) = 0) | |
8 | elrabi 3432 | . . . . 5 ⊢ ((𝑂‘𝐴) ∈ {𝑦 ∈ ℕ ∣ (𝑦(.g‘𝐺)𝐴) = (0g‘𝐺)} → (𝑂‘𝐴) ∈ ℕ) | |
9 | 7, 8 | orim12i 539 | . . . 4 ⊢ ((((𝑂‘𝐴) = 0 ∧ {𝑦 ∈ ℕ ∣ (𝑦(.g‘𝐺)𝐴) = (0g‘𝐺)} = ∅) ∨ (𝑂‘𝐴) ∈ {𝑦 ∈ ℕ ∣ (𝑦(.g‘𝐺)𝐴) = (0g‘𝐺)}) → ((𝑂‘𝐴) = 0 ∨ (𝑂‘𝐴) ∈ ℕ)) |
10 | 6, 9 | syl 17 | . . 3 ⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) = 0 ∨ (𝑂‘𝐴) ∈ ℕ)) |
11 | 10 | orcomd 402 | . 2 ⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) ∈ ℕ ∨ (𝑂‘𝐴) = 0)) |
12 | elnn0 11375 | . 2 ⊢ ((𝑂‘𝐴) ∈ ℕ0 ↔ ((𝑂‘𝐴) ∈ ℕ ∨ (𝑂‘𝐴) = 0)) | |
13 | 11, 12 | sylibr 224 | 1 ⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) ∈ ℕ0) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 382 ∧ wa 383 = wceq 1564 ∈ wcel 2071 {crab 2986 ∅c0 3991 ‘cfv 5969 (class class class)co 6733 0cc0 10017 ℕcn 11101 ℕ0cn0 11373 Basecbs 15948 0gc0g 16191 .gcmg 17630 odcod 18033 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1818 ax-5 1920 ax-6 1986 ax-7 2022 ax-8 2073 ax-9 2080 ax-10 2100 ax-11 2115 ax-12 2128 ax-13 2323 ax-ext 2672 ax-rep 4847 ax-sep 4857 ax-nul 4865 ax-pow 4916 ax-pr 4979 ax-un 7034 ax-cnex 10073 ax-resscn 10074 ax-1cn 10075 ax-icn 10076 ax-addcl 10077 ax-addrcl 10078 ax-mulcl 10079 ax-mulrcl 10080 ax-mulcom 10081 ax-addass 10082 ax-mulass 10083 ax-distr 10084 ax-i2m1 10085 ax-1ne0 10086 ax-1rid 10087 ax-rnegex 10088 ax-rrecex 10089 ax-cnre 10090 ax-pre-lttri 10091 ax-pre-lttrn 10092 ax-pre-ltadd 10093 ax-pre-mulgt0 10094 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1567 df-ex 1786 df-nf 1791 df-sb 1979 df-eu 2543 df-mo 2544 df-clab 2679 df-cleq 2685 df-clel 2688 df-nfc 2823 df-ne 2865 df-nel 2968 df-ral 2987 df-rex 2988 df-reu 2989 df-rmo 2990 df-rab 2991 df-v 3274 df-sbc 3510 df-csb 3608 df-dif 3651 df-un 3653 df-in 3655 df-ss 3662 df-pss 3664 df-nul 3992 df-if 4163 df-pw 4236 df-sn 4254 df-pr 4256 df-tp 4258 df-op 4260 df-uni 4513 df-iun 4598 df-br 4729 df-opab 4789 df-mpt 4806 df-tr 4829 df-id 5096 df-eprel 5101 df-po 5107 df-so 5108 df-fr 5145 df-we 5147 df-xp 5192 df-rel 5193 df-cnv 5194 df-co 5195 df-dm 5196 df-rn 5197 df-res 5198 df-ima 5199 df-pred 5761 df-ord 5807 df-on 5808 df-lim 5809 df-suc 5810 df-iota 5932 df-fun 5971 df-fn 5972 df-f 5973 df-f1 5974 df-fo 5975 df-f1o 5976 df-fv 5977 df-riota 6694 df-ov 6736 df-oprab 6737 df-mpt2 6738 df-om 7151 df-wrecs 7495 df-recs 7556 df-rdg 7594 df-er 7830 df-en 8041 df-dom 8042 df-sdom 8043 df-sup 8432 df-inf 8433 df-pnf 10157 df-mnf 10158 df-xr 10159 df-ltxr 10160 df-le 10161 df-sub 10349 df-neg 10350 df-nn 11102 df-n0 11374 df-z 11459 df-uz 11769 df-od 18037 |
This theorem is referenced by: odf 18045 mndodcongi 18051 oddvdsnn0 18052 oddvds 18055 odeq 18058 odval2 18059 odmulg2 18061 odmulg 18062 odmulgeq 18063 odbezout 18064 odinv 18067 odf1 18068 dfod2 18070 odcl2 18071 odhash2 18079 odhash3 18080 gexnnod 18092 odadd1 18340 odadd2 18341 odadd 18342 gexexlem 18344 gexex 18345 torsubg 18346 iscygodd 18379 lt6abl 18385 ablfacrp 18554 ablfac1b 18558 ablfac1eu 18561 pgpfac1lem2 18563 chrcl 19965 |
Copyright terms: Public domain | W3C validator |