Metamath Proof Explorer

Theorem fimgmcyc

Description: Version of odcl2 for finite magmas: the multiples of an element A e. B are eventually periodic. (Contributed by SN, 3-Jul-2025)

Ref Expression
Hypotheses fimgmcyc.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
fimgmcyc.m ⊢ · = ( .g ‘ 𝑀 )
fimgmcyc.s ⊢ ( 𝜑 → 𝑀 ∈ Mgm )
fimgmcyc.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
fimgmcyc.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion fimgmcyc ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑜 · 𝐴 ) = ( ( 𝑜 + 𝑝 ) · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fimgmcyc.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 fimgmcyc.m ⊢ · = ( .g ‘ 𝑀 )
3 fimgmcyc.s ⊢ ( 𝜑 → 𝑀 ∈ Mgm )
4 fimgmcyc.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
5 fimgmcyc.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
6 domnsym ⊢ ( ℕ ≼ 𝐵 → ¬ 𝐵 ≺ ℕ )
7 fisdomnn ⊢ ( 𝐵 ∈ Fin → 𝐵 ≺ ℕ )
8 4 7 syl ⊢ ( 𝜑 → 𝐵 ≺ ℕ )
9 6 8 nsyl3 ⊢ ( 𝜑 → ¬ ℕ ≼ 𝐵 )
10 1 fvexi ⊢ 𝐵 ∈ V
11 10 f1dom ⊢ ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) : ℕ –1-1→ 𝐵 → ℕ ≼ 𝐵 )
12 9 11 nsyl ⊢ ( 𝜑 → ¬ ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) : ℕ –1-1→ 𝐵 )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 ∈ Mgm )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ 𝐵 )
16 1 2 mulgnncl ⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑛 ∈ ℕ ∧ 𝐴 ∈ 𝐵 ) → ( 𝑛 · 𝐴 ) ∈ 𝐵 )
17 13 14 15 16 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · 𝐴 ) ∈ 𝐵 )
18 17 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) : ℕ ⟶ 𝐵 )
19 dff13 ⊢ ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) : ℕ –1-1→ 𝐵 ↔ ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) : ℕ ⟶ 𝐵 ∧ ∀ 𝑜 ∈ ℕ ∀ 𝑞 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑜 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑞 ) → 𝑜 = 𝑞 ) ) )
20 19 baib ⊢ ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) : ℕ ⟶ 𝐵 → ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) : ℕ –1-1→ 𝐵 ↔ ∀ 𝑜 ∈ ℕ ∀ 𝑞 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑜 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑞 ) → 𝑜 = 𝑞 ) ) )
21 18 20 syl ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) : ℕ –1-1→ 𝐵 ↔ ∀ 𝑜 ∈ ℕ ∀ 𝑞 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑜 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑞 ) → 𝑜 = 𝑞 ) ) )
22 12 21 mtbid ⊢ ( 𝜑 → ¬ ∀ 𝑜 ∈ ℕ ∀ 𝑞 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑜 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑞 ) → 𝑜 = 𝑞 ) )
23 oveq1 ⊢ ( 𝑛 = 𝑜 → ( 𝑛 · 𝐴 ) = ( 𝑜 · 𝐴 ) )
24 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) )
25 ovex ⊢ ( 𝑜 · 𝐴 ) ∈ V
26 23 24 25 fvmpt ⊢ ( 𝑜 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑜 ) = ( 𝑜 · 𝐴 ) )
27 oveq1 ⊢ ( 𝑛 = 𝑞 → ( 𝑛 · 𝐴 ) = ( 𝑞 · 𝐴 ) )
28 ovex ⊢ ( 𝑞 · 𝐴 ) ∈ V
29 27 24 28 fvmpt ⊢ ( 𝑞 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑞 ) = ( 𝑞 · 𝐴 ) )
30 26 29 eqeqan12d ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑜 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑞 ) ↔ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
31 30 imbi1d ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑜 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑞 ) → 𝑜 = 𝑞 ) ↔ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) ) )
32 31 ralbidva ⊢ ( 𝑜 ∈ ℕ → ( ∀ 𝑞 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑜 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑞 ) → 𝑜 = 𝑞 ) ↔ ∀ 𝑞 ∈ ℕ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) ) )
33 32 ralbiia ⊢ ( ∀ 𝑜 ∈ ℕ ∀ 𝑞 ∈ ℕ ( ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑜 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 · 𝐴 ) ) ‘ 𝑞 ) → 𝑜 = 𝑞 ) ↔ ∀ 𝑜 ∈ ℕ ∀ 𝑞 ∈ ℕ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) )
34 22 33 sylnib ⊢ ( 𝜑 → ¬ ∀ 𝑜 ∈ ℕ ∀ 𝑞 ∈ ℕ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) )
35 df-ne ⊢ ( 𝑜 ≠ 𝑞 ↔ ¬ 𝑜 = 𝑞 )
36 35 anbi1i ⊢ ( ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( ¬ 𝑜 = 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
37 ancom ⊢ ( ( ¬ 𝑜 = 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ∧ ¬ 𝑜 = 𝑞 ) )
38 annim ⊢ ( ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ∧ ¬ 𝑜 = 𝑞 ) ↔ ¬ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) )
39 36 37 38 3bitri ⊢ ( ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ¬ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) )
40 39 2rexbii ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ¬ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) )
41 rexnal2 ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ¬ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) ↔ ¬ ∀ 𝑜 ∈ ℕ ∀ 𝑞 ∈ ℕ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) )
42 40 41 bitri ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ¬ ∀ 𝑜 ∈ ℕ ∀ 𝑞 ∈ ℕ ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) → 𝑜 = 𝑞 ) )
43 34 42 sylibr ⊢ ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
44 43 fimgmcyclem ⊢ ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
45 nnz ⊢ ( 𝑜 ∈ ℕ → 𝑜 ∈ ℤ )
46 eluzp1 ⊢ ( 𝑜 ∈ ℤ → ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ↔ ( 𝑞 ∈ ℤ ∧ 𝑜 < 𝑞 ) ) )
47 45 46 syl ⊢ ( 𝑜 ∈ ℕ → ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ↔ ( 𝑞 ∈ ℤ ∧ 𝑜 < 𝑞 ) ) )
48 idd ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) → ( 𝑞 ∈ ℤ → 𝑞 ∈ ℤ ) )
49 nnz ⊢ ( 𝑞 ∈ ℕ → 𝑞 ∈ ℤ )
50 49 a1i ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) → ( 𝑞 ∈ ℕ → 𝑞 ∈ ℤ ) )
51 0red ⊢ ( ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) ∧ 𝑞 ∈ ℤ ) → 0 ∈ ℝ )
52 nnre ⊢ ( 𝑜 ∈ ℕ → 𝑜 ∈ ℝ )
53 52 ad2antrr ⊢ ( ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) ∧ 𝑞 ∈ ℤ ) → 𝑜 ∈ ℝ )
54 zre ⊢ ( 𝑞 ∈ ℤ → 𝑞 ∈ ℝ )
55 54 adantl ⊢ ( ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) ∧ 𝑞 ∈ ℤ ) → 𝑞 ∈ ℝ )
56 nngt0 ⊢ ( 𝑜 ∈ ℕ → 0 < 𝑜 )
57 56 ad2antrr ⊢ ( ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) ∧ 𝑞 ∈ ℤ ) → 0 < 𝑜 )
58 simplr ⊢ ( ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) ∧ 𝑞 ∈ ℤ ) → 𝑜 < 𝑞 )
59 51 53 55 57 58 lttrd ⊢ ( ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) ∧ 𝑞 ∈ ℤ ) → 0 < 𝑞 )
60 elnnz ⊢ ( 𝑞 ∈ ℕ ↔ ( 𝑞 ∈ ℤ ∧ 0 < 𝑞 ) )
61 60 rbaibr ⊢ ( 0 < 𝑞 → ( 𝑞 ∈ ℤ ↔ 𝑞 ∈ ℕ ) )
62 59 61 syl ⊢ ( ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) ∧ 𝑞 ∈ ℤ ) → ( 𝑞 ∈ ℤ ↔ 𝑞 ∈ ℕ ) )
63 62 ex ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) → ( 𝑞 ∈ ℤ → ( 𝑞 ∈ ℤ ↔ 𝑞 ∈ ℕ ) ) )
64 48 50 63 pm5.21ndd ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑜 < 𝑞 ) → ( 𝑞 ∈ ℤ ↔ 𝑞 ∈ ℕ ) )
65 64 ex ⊢ ( 𝑜 ∈ ℕ → ( 𝑜 < 𝑞 → ( 𝑞 ∈ ℤ ↔ 𝑞 ∈ ℕ ) ) )
66 65 pm5.32rd ⊢ ( 𝑜 ∈ ℕ → ( ( 𝑞 ∈ ℤ ∧ 𝑜 < 𝑞 ) ↔ ( 𝑞 ∈ ℕ ∧ 𝑜 < 𝑞 ) ) )
67 47 66 bitrd ⊢ ( 𝑜 ∈ ℕ → ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ↔ ( 𝑞 ∈ ℕ ∧ 𝑜 < 𝑞 ) ) )
68 67 anbi1d ⊢ ( 𝑜 ∈ ℕ → ( ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( ( 𝑞 ∈ ℕ ∧ 𝑜 < 𝑞 ) ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
69 anass ⊢ ( ( ( 𝑞 ∈ ℕ ∧ 𝑜 < 𝑞 ) ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( 𝑞 ∈ ℕ ∧ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
70 68 69 bitrdi ⊢ ( 𝑜 ∈ ℕ → ( ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( 𝑞 ∈ ℕ ∧ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) ) )
71 70 exbidv ⊢ ( 𝑜 ∈ ℕ → ( ∃ 𝑞 ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ∃ 𝑞 ( 𝑞 ∈ ℕ ∧ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) ) )
72 df-rex ⊢ ( ∃ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ↔ ∃ 𝑞 ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
73 df-rex ⊢ ( ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ∃ 𝑞 ( 𝑞 ∈ ℕ ∧ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
74 71 72 73 3bitr4g ⊢ ( 𝑜 ∈ ℕ → ( ∃ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ↔ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
75 74 rexbiia ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ↔ ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
76 44 75 sylibr ⊢ ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) )
77 simplr ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → 𝑜 ∈ ℕ )
78 77 peano2nnd ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → ( 𝑜 + 1 ) ∈ ℕ )
79 78 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → ( 𝑜 + 1 ) ∈ ℤ )
80 simpr ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → 𝑝 ∈ ℕ )
81 77 80 nnaddcld ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → ( 𝑜 + 𝑝 ) ∈ ℕ )
82 81 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → ( 𝑜 + 𝑝 ) ∈ ℤ )
83 1red ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → 1 ∈ ℝ )
84 80 nnred ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → 𝑝 ∈ ℝ )
85 77 nnred ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → 𝑜 ∈ ℝ )
86 80 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → 1 ≤ 𝑝 )
87 83 84 85 86 leadd2dd ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → ( 𝑜 + 1 ) ≤ ( 𝑜 + 𝑝 ) )
88 eluz2 ⊢ ( ( 𝑜 + 𝑝 ) ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ↔ ( ( 𝑜 + 1 ) ∈ ℤ ∧ ( 𝑜 + 𝑝 ) ∈ ℤ ∧ ( 𝑜 + 1 ) ≤ ( 𝑜 + 𝑝 ) ) )
89 79 82 87 88 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑝 ∈ ℕ ) → ( 𝑜 + 𝑝 ) ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) )
90 simpr ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) → 𝑜 ∈ ℕ )
91 90 nnzd ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) → 𝑜 ∈ ℤ )
92 eluzp1l ⊢ ( ( 𝑜 ∈ ℤ ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) → 𝑜 < 𝑞 )
93 91 92 sylan ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) → 𝑜 < 𝑞 )
94 simplr ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) → 𝑜 ∈ ℕ )
95 peano2nn ⊢ ( 𝑜 ∈ ℕ → ( 𝑜 + 1 ) ∈ ℕ )
96 95 adantl ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) → ( 𝑜 + 1 ) ∈ ℕ )
97 eluznn ⊢ ( ( ( 𝑜 + 1 ) ∈ ℕ ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) → 𝑞 ∈ ℕ )
98 96 97 sylan ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) → 𝑞 ∈ ℕ )
99 nnsub ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( 𝑜 < 𝑞 ↔ ( 𝑞 − 𝑜 ) ∈ ℕ ) )
100 94 98 99 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) → ( 𝑜 < 𝑞 ↔ ( 𝑞 − 𝑜 ) ∈ ℕ ) )
101 93 100 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) → ( 𝑞 − 𝑜 ) ∈ ℕ )
102 eluzelcn ⊢ ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) → 𝑞 ∈ ℂ )
103 102 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) ∧ 𝑝 = ( 𝑞 − 𝑜 ) ) → 𝑞 ∈ ℂ )
104 nncn ⊢ ( 𝑜 ∈ ℕ → 𝑜 ∈ ℂ )
105 104 adantl ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) → 𝑜 ∈ ℂ )
106 105 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) ∧ 𝑝 = ( 𝑞 − 𝑜 ) ) → 𝑜 ∈ ℂ )
107 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) ∧ 𝑝 = ( 𝑞 − 𝑜 ) ) → 𝑝 = ( 𝑞 − 𝑜 ) )
108 103 106 107 rsubrotld ⊢ ( ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) ∧ 𝑝 = ( 𝑞 − 𝑜 ) ) → 𝑞 = ( 𝑜 + 𝑝 ) )
109 101 108 rspcedeq2vd ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ) → ∃ 𝑝 ∈ ℕ 𝑞 = ( 𝑜 + 𝑝 ) )
110 oveq1 ⊢ ( 𝑞 = ( 𝑜 + 𝑝 ) → ( 𝑞 · 𝐴 ) = ( ( 𝑜 + 𝑝 ) · 𝐴 ) )
111 110 eqeq2d ⊢ ( 𝑞 = ( 𝑜 + 𝑝 ) → ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ↔ ( 𝑜 · 𝐴 ) = ( ( 𝑜 + 𝑝 ) · 𝐴 ) ) )
112 111 adantl ⊢ ( ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) ∧ 𝑞 = ( 𝑜 + 𝑝 ) ) → ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ↔ ( 𝑜 · 𝐴 ) = ( ( 𝑜 + 𝑝 ) · 𝐴 ) ) )
113 89 109 112 rexxfrd ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ℕ ) → ( ∃ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ↔ ∃ 𝑝 ∈ ℕ ( 𝑜 · 𝐴 ) = ( ( 𝑜 + 𝑝 ) · 𝐴 ) ) )
114 113 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑜 + 1 ) ) ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ↔ ∃ 𝑜 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑜 · 𝐴 ) = ( ( 𝑜 + 𝑝 ) · 𝐴 ) ) )
115 76 114 mpbid ⊢ ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑜 · 𝐴 ) = ( ( 𝑜 + 𝑝 ) · 𝐴 ) )