Metamath Proof Explorer

Theorem fimgmcyclem

Description: Lemma for fimgmcyc . (Contributed by SN, 7-Jul-2025)

Ref Expression
Hypothesis fimgmcyclem.s ⊢ ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
Assertion fimgmcyclem ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fimgmcyclem.s ⊢ ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
2 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
3 rexcom ⊢ ( ∃ 𝑟 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) ↔ ∃ 𝑝 ∈ ℕ ∃ 𝑟 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) )
4 eqcom ⊢ ( ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ↔ ( 𝑝 · 𝐴 ) = ( 𝑟 · 𝐴 ) )
5 4 anbi2i ⊢ ( ( 𝑝 < 𝑟 ∧ ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) ↔ ( 𝑝 < 𝑟 ∧ ( 𝑝 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) )
6 5 2rexbii ⊢ ( ∃ 𝑝 ∈ ℕ ∃ 𝑟 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) ↔ ∃ 𝑝 ∈ ℕ ∃ 𝑟 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑝 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) )
7 3 6 sylbb ⊢ ( ∃ 𝑟 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) → ∃ 𝑝 ∈ ℕ ∃ 𝑟 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑝 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) )
8 breq2 ⊢ ( 𝑜 = 𝑟 → ( 𝑝 < 𝑜 ↔ 𝑝 < 𝑟 ) )
9 oveq1 ⊢ ( 𝑜 = 𝑟 → ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) )
10 9 eqeq1d ⊢ ( 𝑜 = 𝑟 → ( ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) ↔ ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) )
11 8 10 anbi12d ⊢ ( 𝑜 = 𝑟 → ( ( 𝑝 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) ↔ ( 𝑝 < 𝑟 ∧ ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) ) )
12 11 rexbidv ⊢ ( 𝑜 = 𝑟 → ( ∃ 𝑝 ∈ ℕ ( 𝑝 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) ↔ ∃ 𝑝 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) ) )
13 12 cbvrexvw ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑝 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) ↔ ∃ 𝑟 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑟 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) )
14 breq1 ⊢ ( 𝑜 = 𝑝 → ( 𝑜 < 𝑟 ↔ 𝑝 < 𝑟 ) )
15 oveq1 ⊢ ( 𝑜 = 𝑝 → ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) )
16 15 eqeq1d ⊢ ( 𝑜 = 𝑝 → ( ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) ↔ ( 𝑝 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) )
17 14 16 anbi12d ⊢ ( 𝑜 = 𝑝 → ( ( 𝑜 < 𝑟 ∧ ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) ↔ ( 𝑝 < 𝑟 ∧ ( 𝑝 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) ) )
18 17 rexbidv ⊢ ( 𝑜 = 𝑝 → ( ∃ 𝑟 ∈ ℕ ( 𝑜 < 𝑟 ∧ ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) ↔ ∃ 𝑟 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑝 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) ) )
19 18 cbvrexvw ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑟 ∈ ℕ ( 𝑜 < 𝑟 ∧ ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) ↔ ∃ 𝑝 ∈ ℕ ∃ 𝑟 ∈ ℕ ( 𝑝 < 𝑟 ∧ ( 𝑝 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) )
20 7 13 19 3imtr4i ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑝 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) → ∃ 𝑜 ∈ ℕ ∃ 𝑟 ∈ ℕ ( 𝑜 < 𝑟 ∧ ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) )
21 breq1 ⊢ ( 𝑞 = 𝑝 → ( 𝑞 < 𝑜 ↔ 𝑝 < 𝑜 ) )
22 oveq1 ⊢ ( 𝑞 = 𝑝 → ( 𝑞 · 𝐴 ) = ( 𝑝 · 𝐴 ) )
23 22 eqeq2d ⊢ ( 𝑞 = 𝑝 → ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ↔ ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) )
24 21 23 anbi12d ⊢ ( 𝑞 = 𝑝 → ( ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( 𝑝 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) ) )
25 24 cbvrexvw ⊢ ( ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ∃ 𝑝 ∈ ℕ ( 𝑝 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) )
26 25 rexbii ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ∃ 𝑜 ∈ ℕ ∃ 𝑝 ∈ ℕ ( 𝑝 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑝 · 𝐴 ) ) )
27 breq2 ⊢ ( 𝑞 = 𝑟 → ( 𝑜 < 𝑞 ↔ 𝑜 < 𝑟 ) )
28 oveq1 ⊢ ( 𝑞 = 𝑟 → ( 𝑞 · 𝐴 ) = ( 𝑟 · 𝐴 ) )
29 28 eqeq2d ⊢ ( 𝑞 = 𝑟 → ( ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ↔ ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) )
30 27 29 anbi12d ⊢ ( 𝑞 = 𝑟 → ( ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( 𝑜 < 𝑟 ∧ ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) ) )
31 30 cbvrexvw ⊢ ( ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ∃ 𝑟 ∈ ℕ ( 𝑜 < 𝑟 ∧ ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) )
32 31 rexbii ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ∃ 𝑜 ∈ ℕ ∃ 𝑟 ∈ ℕ ( 𝑜 < 𝑟 ∧ ( 𝑜 · 𝐴 ) = ( 𝑟 · 𝐴 ) ) )
33 20 26 32 3imtr4i ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
34 33 adantl ⊢ ( ( 𝜑 ∧ ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )
35 simpl ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → 𝑜 ∈ ℕ )
36 35 nnred ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → 𝑜 ∈ ℝ )
37 simpr ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → 𝑞 ∈ ℕ )
38 37 nnred ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → 𝑞 ∈ ℝ )
39 36 38 lttri2d ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( 𝑜 ≠ 𝑞 ↔ ( 𝑜 < 𝑞 ∨ 𝑞 < 𝑜 ) ) )
40 39 anbi1d ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( ( 𝑜 < 𝑞 ∨ 𝑞 < 𝑜 ) ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
41 andir ⊢ ( ( ( 𝑜 < 𝑞 ∨ 𝑞 < 𝑜 ) ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
42 40 41 bitrdi ⊢ ( ( 𝑜 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) ) )
43 42 2rexbiia ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
44 r19.43 ⊢ ( ∃ 𝑞 ∈ ℕ ( ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) ↔ ( ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
45 44 rexbii ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) ↔ ∃ 𝑜 ∈ ℕ ( ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
46 r19.43 ⊢ ( ∃ 𝑜 ∈ ℕ ( ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) ↔ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
47 43 45 46 3bitri ⊢ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 ≠ 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ↔ ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
48 1 47 sylib ⊢ ( 𝜑 → ( ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ∨ ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑞 < 𝑜 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) ) )
49 2 34 48 mpjaodan ⊢ ( 𝜑 → ∃ 𝑜 ∈ ℕ ∃ 𝑞 ∈ ℕ ( 𝑜 < 𝑞 ∧ ( 𝑜 · 𝐴 ) = ( 𝑞 · 𝐴 ) ) )