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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odid.3 ⊢ · = ( .g ‘ 𝐺 )
odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion oddvdsnn0 ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odid.3 ⊢ · = ( .g ‘ 𝐺 )
4 odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 0nn0 ⊢ 0 ∈ ℕ0
6 1 2 3 4 mndodcong ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑁 − 0 ) ↔ ( 𝑁 · 𝐴 ) = ( 0 · 𝐴 ) ) )
7 6 3expia ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑁 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑁 − 0 ) ↔ ( 𝑁 · 𝐴 ) = ( 0 · 𝐴 ) ) ) )
8 5 7 mpanr2 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑁 − 0 ) ↔ ( 𝑁 · 𝐴 ) = ( 0 · 𝐴 ) ) ) )
9 8 3impa ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑁 − 0 ) ↔ ( 𝑁 · 𝐴 ) = ( 0 · 𝐴 ) ) ) )
10 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
11 10 3ad2ant3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
12 11 subid1d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 − 0 ) = 𝑁 )
13 12 breq2d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑁 − 0 ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ) )
14 1 4 3 mulg0 ⊢ ( 𝐴 ∈ 𝑋 → ( 0 · 𝐴 ) = 0 )
15 14 3ad2ant2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 0 · 𝐴 ) = 0 )
16 15 eqeq2d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 · 𝐴 ) = ( 0 · 𝐴 ) ↔ ( 𝑁 · 𝐴 ) = 0 ) )
17 13 16 bibi12d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑁 − 0 ) ↔ ( 𝑁 · 𝐴 ) = ( 0 · 𝐴 ) ) ↔ ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) ) )
18 9 17 sylibd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) ) )
19 simpr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) = 0 )
20 19 breq1d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ 0 ∥ 𝑁 ) )
21 simpl3 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → 𝑁 ∈ ℕ0 )
22 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
23 0dvds ⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )
24 21 22 23 3syl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )
25 15 adantr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 0 · 𝐴 ) = 0 )
26 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 · 𝐴 ) = ( 0 · 𝐴 ) )
27 26 eqeq1d ⊢ ( 𝑁 = 0 → ( ( 𝑁 · 𝐴 ) = 0 ↔ ( 0 · 𝐴 ) = 0 ) )
28 25 27 syl5ibrcom ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑁 = 0 → ( 𝑁 · 𝐴 ) = 0 ) )
29 1 2 3 4 odlem2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... 𝑁 ) )
30 29 3com23 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑁 · 𝐴 ) = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... 𝑁 ) )
31 elfznn ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ( 1 ... 𝑁 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
32 nnne0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ≠ 0 )
33 30 31 32 3syl ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑁 · 𝐴 ) = 0 ∧ 𝑁 ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ≠ 0 )
34 33 3expia ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( 𝑁 ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ≠ 0 ) )
35 34 3ad2antl2 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( 𝑁 ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ≠ 0 ) )
36 35 necon2bd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 → ¬ 𝑁 ∈ ℕ ) )
37 simpl3 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 · 𝐴 ) = 0 ) → 𝑁 ∈ ℕ0 )
38 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
39 37 38 sylib ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
40 39 ord ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( ¬ 𝑁 ∈ ℕ → 𝑁 = 0 ) )
41 36 40 syld ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑁 · 𝐴 ) = 0 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 → 𝑁 = 0 ) )
42 41 impancom ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( 𝑁 · 𝐴 ) = 0 → 𝑁 = 0 ) )
43 28 42 impbid ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑁 = 0 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
44 20 24 43 3bitrd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
45 44 ex ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) ) )
46 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
47 46 3ad2ant2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
48 elnn0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
49 47 48 sylib ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
50 18 45 49 mpjaod ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )