Metamath Proof Explorer


Theorem oddvdsnn0

Description: The only multiples of A that are equal to the identity are the multiples of the order of A . (Contributed by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses odcl.1 X = Base G
odcl.2 O = od G
odid.3 · ˙ = G
odid.4 0 ˙ = 0 G
Assertion oddvdsnn0 G Mnd A X N 0 O A N N · ˙ A = 0 ˙

Proof

Step Hyp Ref Expression
1 odcl.1 X = Base G
2 odcl.2 O = od G
3 odid.3 · ˙ = G
4 odid.4 0 ˙ = 0 G
5 0nn0 0 0
6 1 2 3 4 mndodcong G Mnd A X N 0 0 0 O A O A N 0 N · ˙ A = 0 · ˙ A
7 6 3expia G Mnd A X N 0 0 0 O A O A N 0 N · ˙ A = 0 · ˙ A
8 5 7 mpanr2 G Mnd A X N 0 O A O A N 0 N · ˙ A = 0 · ˙ A
9 8 3impa G Mnd A X N 0 O A O A N 0 N · ˙ A = 0 · ˙ A
10 nn0cn N 0 N
11 10 3ad2ant3 G Mnd A X N 0 N
12 11 subid1d G Mnd A X N 0 N 0 = N
13 12 breq2d G Mnd A X N 0 O A N 0 O A N
14 1 4 3 mulg0 A X 0 · ˙ A = 0 ˙
15 14 3ad2ant2 G Mnd A X N 0 0 · ˙ A = 0 ˙
16 15 eqeq2d G Mnd A X N 0 N · ˙ A = 0 · ˙ A N · ˙ A = 0 ˙
17 13 16 bibi12d G Mnd A X N 0 O A N 0 N · ˙ A = 0 · ˙ A O A N N · ˙ A = 0 ˙
18 9 17 sylibd G Mnd A X N 0 O A O A N N · ˙ A = 0 ˙
19 simpr G Mnd A X N 0 O A = 0 O A = 0
20 19 breq1d G Mnd A X N 0 O A = 0 O A N 0 N
21 simpl3 G Mnd A X N 0 O A = 0 N 0
22 nn0z N 0 N
23 0dvds N 0 N N = 0
24 21 22 23 3syl G Mnd A X N 0 O A = 0 0 N N = 0
25 15 adantr G Mnd A X N 0 O A = 0 0 · ˙ A = 0 ˙
26 oveq1 N = 0 N · ˙ A = 0 · ˙ A
27 26 eqeq1d N = 0 N · ˙ A = 0 ˙ 0 · ˙ A = 0 ˙
28 25 27 syl5ibrcom G Mnd A X N 0 O A = 0 N = 0 N · ˙ A = 0 ˙
29 1 2 3 4 odlem2 A X N N · ˙ A = 0 ˙ O A 1 N
30 29 3com23 A X N · ˙ A = 0 ˙ N O A 1 N
31 elfznn O A 1 N O A
32 nnne0 O A O A 0
33 30 31 32 3syl A X N · ˙ A = 0 ˙ N O A 0
34 33 3expia A X N · ˙ A = 0 ˙ N O A 0
35 34 3ad2antl2 G Mnd A X N 0 N · ˙ A = 0 ˙ N O A 0
36 35 necon2bd G Mnd A X N 0 N · ˙ A = 0 ˙ O A = 0 ¬ N
37 simpl3 G Mnd A X N 0 N · ˙ A = 0 ˙ N 0
38 elnn0 N 0 N N = 0
39 37 38 sylib G Mnd A X N 0 N · ˙ A = 0 ˙ N N = 0
40 39 ord G Mnd A X N 0 N · ˙ A = 0 ˙ ¬ N N = 0
41 36 40 syld G Mnd A X N 0 N · ˙ A = 0 ˙ O A = 0 N = 0
42 41 impancom G Mnd A X N 0 O A = 0 N · ˙ A = 0 ˙ N = 0
43 28 42 impbid G Mnd A X N 0 O A = 0 N = 0 N · ˙ A = 0 ˙
44 20 24 43 3bitrd G Mnd A X N 0 O A = 0 O A N N · ˙ A = 0 ˙
45 44 ex G Mnd A X N 0 O A = 0 O A N N · ˙ A = 0 ˙
46 1 2 odcl A X O A 0
47 46 3ad2ant2 G Mnd A X N 0 O A 0
48 elnn0 O A 0 O A O A = 0
49 47 48 sylib G Mnd A X N 0 O A O A = 0
50 18 45 49 mpjaod G Mnd A X N 0 O A N N · ˙ A = 0 ˙