MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oddvdsnn0 Unicode version

Theorem oddvdsnn0 16135
Description: The only multiples of that are equal to the identity are the multiples of the order of . (Contributed by Mario Carneiro, 23-Sep-2015.)
Hypotheses
Ref Expression
odcl.1
odcl.2
odid.3
odid.4
Assertion
Ref Expression
oddvdsnn0

Proof of Theorem oddvdsnn0
StepHypRef Expression
1 0nn0 10679 . . . . 5
2 odcl.1 . . . . . . 7
3 odcl.2 . . . . . . 7
4 odid.3 . . . . . . 7
5 odid.4 . . . . . . 7
62, 3, 4, 5mndodcong 16133 . . . . . 6
763expia 1190 . . . . 5
81, 7mpanr2 684 . . . 4
983impa 1183 . . 3
10 nn0cn 10674 . . . . . . 7
11103ad2ant3 1011 . . . . . 6
1211subid1d 9793 . . . . 5
1312breq2d 4386 . . . 4
142, 5, 4mulg0 15718 . . . . . 6
15143ad2ant2 1010 . . . . 5
1615eqeq2d 2463 . . . 4
1713, 16bibi12d 321 . . 3
189, 17sylibd 214 . 2
19 simpr 461 . . . . 5
2019breq1d 4384 . . . 4
21 simpl3 993 . . . . 5
22 nn0z 10754 . . . . 5
23 0dvds 13639 . . . . 5
2421, 22, 233syl 20 . . . 4
2515adantr 465 . . . . . 6
26 oveq1 6181 . . . . . . 7
2726eqeq1d 2452 . . . . . 6
2825, 27syl5ibrcom 222 . . . . 5
292, 3, 4, 5odlem2 16130 . . . . . . . . . . . 12
30293com23 1194 . . . . . . . . . . 11
31 elfznn 11563 . . . . . . . . . . 11
32 nnne0 10439 . . . . . . . . . . 11
3330, 31, 323syl 20 . . . . . . . . . 10
34333expia 1190 . . . . . . . . 9
35343ad2antl2 1151 . . . . . . . 8
3635necon2bd 2660 . . . . . . 7
37 simpl3 993 . . . . . . . . 9
38 elnn0 10666 . . . . . . . . 9
3937, 38sylib 196 . . . . . . . 8
4039ord 377 . . . . . . 7
4136, 40syld 44 . . . . . 6
4241impancom 440 . . . . 5
4328, 42impbid 191 . . . 4
4420, 24, 433bitrd 279 . . 3
4544ex 434 . 2
462, 3odcl 16127 . . . 4
47463ad2ant2 1010 . . 3
48 elnn0 10666 . . 3
4947, 48sylib 196 . 2
5018, 45, 49mpjaod 381 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  /\w3a 965  =wceq 1370  e.wcel 1757  =/=wne 2641   class class class wbr 4374  `cfv 5500  (class class class)co 6174   cc 9365  0cc0 9367  1c1 9368   cmin 9680   cn 10407   cn0 10664   cz 10731   cfz 11522   cdivides 13621   cbs 14260   c0g 14464   cmnd 15495   cmg 15500   cod 16116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456  ax-inf2 7932  ax-cnex 9423  ax-resscn 9424  ax-1cn 9425  ax-icn 9426  ax-addcl 9427  ax-addrcl 9428  ax-mulcl 9429  ax-mulrcl 9430  ax-mulcom 9431  ax-addass 9432  ax-mulass 9433  ax-distr 9434  ax-i2m1 9435  ax-1ne0 9436  ax-1rid 9437  ax-rnegex 9438  ax-rrecex 9439  ax-cnre 9440  ax-pre-lttri 9441  ax-pre-lttrn 9442  ax-pre-ltadd 9443  ax-pre-mulgt0 9444  ax-pre-sup 9445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-pss 3426  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4174  df-iun 4255  df-br 4375  df-opab 4433  df-mpt 4434  df-tr 4468  df-eprel 4714  df-id 4718  df-po 4723  df-so 4724  df-fr 4761  df-we 4763  df-ord 4804  df-on 4805  df-lim 4806  df-suc 4807  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-om 6561  df-1st 6661  df-2nd 6662  df-recs 6916  df-rdg 6950  df-er 7185  df-en 7395  df-dom 7396  df-sdom 7397  df-sup 7776  df-pnf 9505  df-mnf 9506  df-xr 9507  df-ltxr 9508  df-le 9509  df-sub 9682  df-neg 9683  df-div 10079  df-nn 10408  df-n0 10665  df-z 10732  df-uz 10947  df-rp 11077  df-fz 11523  df-fl 11727  df-mod 11794  df-seq 11892  df-dvds 13622  df-0g 14466  df-mnd 15501  df-mulg 15634  df-od 16120
  Copyright terms: Public domain W3C validator