Metamath Proof Explorer

Theorem unitscyglem2

Description: Lemma for unitscyg . (Contributed by metakunt, 13-Jul-2025)

Ref Expression
Hypotheses unitscyglem1.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
unitscyglem1.2 ⊢ ↑ = ( .g ‘ 𝐺 )
unitscyglem1.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
unitscyglem1.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
unitscyglem1.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
unitscyglem2.1 ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
unitscyglem2.2 ⊢ ( 𝜑 → 𝐷 ∥ ( ♯ ‘ 𝐵 ) )
unitscyglem2.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
unitscyglem2.4 ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = 𝐷 )
unitscyglem2.5 ⊢ ( 𝜑 → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝐷 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
Assertion unitscyglem2 ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 unitscyglem1.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 unitscyglem1.2 ⊢ ↑ = ( .g ‘ 𝐺 )
3 unitscyglem1.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
4 unitscyglem1.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
5 unitscyglem1.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
6 unitscyglem2.1 ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
7 unitscyglem2.2 ⊢ ( 𝜑 → 𝐷 ∥ ( ♯ ‘ 𝐵 ) )
8 unitscyglem2.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
9 unitscyglem2.4 ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = 𝐷 )
10 unitscyglem2.5 ⊢ ( 𝜑 → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝐷 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
11 breq1 ⊢ ( 𝑎 = 𝑘 → ( 𝑎 ∥ 𝐷 ↔ 𝑘 ∥ 𝐷 ) )
12 11 elrab ⊢ ( 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ↔ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) )
13 12 bilani ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) )
14 13 simpld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) )
15 14 elfzelzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑘 ∈ ℤ )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝐷 ∈ ℕ )
17 16 nnzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝐷 ∈ ℤ )
18 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
19 4 18 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
21 20 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
22 13 simprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑘 ∥ 𝐷 )
23 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝐷 ∥ ( ♯ ‘ 𝐵 ) )
24 15 17 21 22 23 dvdstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑘 ∥ ( ♯ ‘ 𝐵 ) )
25 simpl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) ) → 𝜑 )
26 12 14 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) ) → 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) )
27 25 26 jca ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) ) → ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) )
28 12 22 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) ) → 𝑘 ∥ 𝐷 )
29 27 28 jca ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) ) → ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) )
30 fveqeq2 ⊢ ( 𝑥 = ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ↔ ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) = 𝑘 ) )
31 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐺 ∈ Grp )
32 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( 𝑙 · 𝑘 ) = 𝐷 )
33 32 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐷 = ( 𝑙 · 𝑘 ) )
34 33 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( 𝐷 / 𝑘 ) = ( ( 𝑙 · 𝑘 ) / 𝑘 ) )
35 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝑙 ∈ ℕ )
36 35 nncnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝑙 ∈ ℂ )
37 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) → 𝑘 ∈ ℤ )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) → 𝑘 ∈ ℤ )
39 38 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝑘 ∈ ℤ )
40 39 zcnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝑘 ∈ ℂ )
41 elfzle1 ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) → 1 ≤ 𝑘 )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) → 1 ≤ 𝑘 )
43 38 42 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
44 elnnz1 ⊢ ( 𝑘 ∈ ℕ ↔ ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
45 43 44 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) → 𝑘 ∈ ℕ )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) → 𝑘 ∈ ℕ )
47 46 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝑘 ∈ ℕ )
48 47 nnne0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝑘 ≠ 0 )
49 36 40 48 divcan4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝑙 · 𝑘 ) / 𝑘 ) = 𝑙 )
50 34 49 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( 𝐷 / 𝑘 ) = 𝑙 )
51 50 35 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( 𝐷 / 𝑘 ) ∈ ℕ )
52 51 nnnn0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( 𝐷 / 𝑘 ) ∈ ℕ0 )
53 52 nn0zd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( 𝐷 / 𝑘 ) ∈ ℤ )
54 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐴 ∈ 𝐵 )
55 1 2 31 53 54 mulgcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ∈ 𝐵 )
56 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) → 𝐷 ∈ ℕ )
57 56 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐷 ∈ ℕ )
58 57 nncnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐷 ∈ ℂ )
59 58 40 48 divcan1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝐷 / 𝑘 ) · 𝑘 ) = 𝐷 )
60 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = 𝐷 )
61 60 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐷 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )
62 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
63 1 62 2 odmulg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ ( 𝐷 / 𝑘 ) ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( ( ( 𝐷 / 𝑘 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ) )
64 31 54 53 63 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( ( ( 𝐷 / 𝑘 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ) )
65 61 64 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐷 = ( ( ( 𝐷 / 𝑘 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ) )
66 60 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝐷 / 𝑘 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( 𝐷 / 𝑘 ) gcd 𝐷 ) )
67 58 40 48 divcan2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( 𝑘 · ( 𝐷 / 𝑘 ) ) = 𝐷 )
68 67 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐷 = ( 𝑘 · ( 𝐷 / 𝑘 ) ) )
69 68 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝐷 / 𝑘 ) gcd 𝐷 ) = ( ( 𝐷 / 𝑘 ) gcd ( 𝑘 · ( 𝐷 / 𝑘 ) ) ) )
70 52 39 gcdmultipled ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝐷 / 𝑘 ) gcd ( 𝑘 · ( 𝐷 / 𝑘 ) ) ) = ( 𝐷 / 𝑘 ) )
71 69 70 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝐷 / 𝑘 ) gcd 𝐷 ) = ( 𝐷 / 𝑘 ) )
72 66 71 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝐷 / 𝑘 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) = ( 𝐷 / 𝑘 ) )
73 72 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( ( 𝐷 / 𝑘 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ) = ( ( 𝐷 / 𝑘 ) · ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ) )
74 65 73 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐷 = ( ( 𝐷 / 𝑘 ) · ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ) )
75 59 74 eqtr2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝐷 / 𝑘 ) · ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ) = ( ( 𝐷 / 𝑘 ) · 𝑘 ) )
76 1 62 55 odcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ∈ ℕ0 )
77 76 nn0cnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ∈ ℂ )
78 53 zcnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( 𝐷 / 𝑘 ) ∈ ℂ )
79 57 nnne0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → 𝐷 ≠ 0 )
80 58 40 79 48 divne0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( 𝐷 / 𝑘 ) ≠ 0 )
81 77 40 78 80 mulcand ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( ( 𝐷 / 𝑘 ) · ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) ) = ( ( 𝐷 / 𝑘 ) · 𝑘 ) ↔ ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) = 𝑘 ) )
82 75 81 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( od ‘ 𝐺 ) ‘ ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ) = 𝑘 )
83 30 55 82 elrabd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → ( ( 𝐷 / 𝑘 ) ↑ 𝐴 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
84 83 ne0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) ∧ 𝑙 ∈ ℕ ) ∧ ( 𝑙 · 𝑘 ) = 𝐷 ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
85 nndivides ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑘 ∥ 𝐷 ↔ ∃ 𝑙 ∈ ℕ ( 𝑙 · 𝑘 ) = 𝐷 ) )
86 46 56 85 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) → ( 𝑘 ∥ 𝐷 ↔ ∃ 𝑙 ∈ ℕ ( 𝑙 · 𝑘 ) = 𝐷 ) )
87 86 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) → ( 𝑘 ∥ 𝐷 → ∃ 𝑙 ∈ ℕ ( 𝑙 · 𝑘 ) = 𝐷 ) )
88 87 syldbl2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) → ∃ 𝑙 ∈ ℕ ( 𝑙 · 𝑘 ) = 𝐷 )
89 84 88 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ) ∧ 𝑘 ∥ 𝐷 ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
90 29 89 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
91 90 ex ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑘 ∥ 𝐷 ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
93 13 92 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
94 24 93 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
95 14 41 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 1 ≤ 𝑘 )
96 15 95 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
97 96 44 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑘 ∈ ℕ )
98 97 nnred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑘 ∈ ℝ )
99 16 nnred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝐷 ∈ ℝ )
100 1red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 1 ∈ ℝ )
101 99 100 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( 𝐷 − 1 ) ∈ ℝ )
102 elfzle2 ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐷 − 1 ) ) → 𝑘 ≤ ( 𝐷 − 1 ) )
103 14 102 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑘 ≤ ( 𝐷 − 1 ) )
104 99 ltm1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( 𝐷 − 1 ) < 𝐷 )
105 98 101 99 103 104 lelttrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑘 < 𝐷 )
106 breq1 ⊢ ( 𝑐 = 𝑘 → ( 𝑐 < 𝐷 ↔ 𝑘 < 𝐷 ) )
107 breq1 ⊢ ( 𝑐 = 𝑘 → ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
108 eqeq2 ⊢ ( 𝑐 = 𝑘 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ) )
109 108 rabbidv ⊢ ( 𝑐 = 𝑘 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
110 109 neeq1d ⊢ ( 𝑐 = 𝑘 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ↔ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
111 107 110 anbi12d ⊢ ( 𝑐 = 𝑘 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) ↔ ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) ) )
112 109 fveq2d ⊢ ( 𝑐 = 𝑘 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
113 fveq2 ⊢ ( 𝑐 = 𝑘 → ( ϕ ‘ 𝑐 ) = ( ϕ ‘ 𝑘 ) )
114 112 113 eqeq12d ⊢ ( 𝑐 = 𝑘 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ↔ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) )
115 111 114 imbi12d ⊢ ( 𝑐 = 𝑘 → ( ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ↔ ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) ) )
116 106 115 imbi12d ⊢ ( 𝑐 = 𝑘 → ( ( 𝑐 < 𝐷 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) ↔ ( 𝑘 < 𝐷 → ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) ) ) )
117 10 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ∀ 𝑐 ∈ ℕ ( 𝑐 < 𝐷 → ( ( 𝑐 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑐 } ) = ( ϕ ‘ 𝑐 ) ) ) )
118 116 117 97 rspcdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( 𝑘 < 𝐷 → ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) ) )
119 105 118 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) )
120 94 119 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) )
121 120 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) )
122 121 eqcomd ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
123 122 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) + ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ) = ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) + ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ) )
124 elun ⊢ ( 𝑦 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ↔ ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∨ 𝑦 ∈ { 𝐷 } ) )
125 124 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ) → ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∨ 𝑦 ∈ { 𝐷 } ) )
126 1zzd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 1 ∈ ℤ )
127 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝐷 ∈ ℕ )
128 127 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝐷 ∈ ℤ )
129 elfzelz ⊢ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) → 𝑎 ∈ ℤ )
130 129 adantr ⊢ ( ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) → 𝑎 ∈ ℤ )
131 130 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝑎 ∈ ℤ )
132 elfzle1 ⊢ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) → 1 ≤ 𝑎 )
133 132 adantr ⊢ ( ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) → 1 ≤ 𝑎 )
134 133 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 1 ≤ 𝑎 )
135 131 zred ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝑎 ∈ ℝ )
136 127 nnred ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝐷 ∈ ℝ )
137 1red ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 1 ∈ ℝ )
138 136 137 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → ( 𝐷 − 1 ) ∈ ℝ )
139 elfzle2 ⊢ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) → 𝑎 ≤ ( 𝐷 − 1 ) )
140 139 adantr ⊢ ( ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) → 𝑎 ≤ ( 𝐷 − 1 ) )
141 140 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝑎 ≤ ( 𝐷 − 1 ) )
142 136 ltm1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → ( 𝐷 − 1 ) < 𝐷 )
143 135 138 136 141 142 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝑎 < 𝐷 )
144 135 136 143 ltled ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝑎 ≤ 𝐷 )
145 126 128 131 134 144 elfzd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝑎 ∈ ( 1 ... 𝐷 ) )
146 145 rabss3d ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ⊆ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
147 146 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) )
148 147 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
149 elsni ⊢ ( 𝑦 ∈ { 𝐷 } → 𝑦 = 𝐷 )
150 149 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝐷 } ) → 𝑦 = 𝐷 )
151 simpr ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐷 ) → 𝑦 = 𝐷 )
152 breq1 ⊢ ( 𝑎 = 𝐷 → ( 𝑎 ∥ 𝐷 ↔ 𝐷 ∥ 𝐷 ) )
153 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
154 6 nnzd ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
155 6 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐷 )
156 6 nnred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
157 156 leidd ⊢ ( 𝜑 → 𝐷 ≤ 𝐷 )
158 153 154 154 155 157 elfzd ⊢ ( 𝜑 → 𝐷 ∈ ( 1 ... 𝐷 ) )
159 iddvds ⊢ ( 𝐷 ∈ ℤ → 𝐷 ∥ 𝐷 )
160 154 159 syl ⊢ ( 𝜑 → 𝐷 ∥ 𝐷 )
161 152 158 160 elrabd ⊢ ( 𝜑 → 𝐷 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
162 161 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐷 ) → 𝐷 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
163 151 162 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐷 ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
164 163 ex ⊢ ( 𝜑 → ( 𝑦 = 𝐷 → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) )
165 164 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝐷 } ) → ( 𝑦 = 𝐷 → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) )
166 150 165 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝐷 } ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
167 148 166 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∨ 𝑦 ∈ { 𝐷 } ) ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
168 167 ex ⊢ ( 𝜑 → ( ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∨ 𝑦 ∈ { 𝐷 } ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ) → ( ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∨ 𝑦 ∈ { 𝐷 } ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) )
170 125 169 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
171 170 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) )
172 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ 𝑦 = 𝐷 ) → 𝑦 = 𝐷 )
173 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ 𝑦 = 𝐷 ) → 𝐷 = 𝐷 )
174 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ 𝑦 = 𝐷 ) → 𝐷 ∈ ℕ )
175 elsng ⊢ ( 𝐷 ∈ ℕ → ( 𝐷 ∈ { 𝐷 } ↔ 𝐷 = 𝐷 ) )
176 174 175 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ 𝑦 = 𝐷 ) → ( 𝐷 ∈ { 𝐷 } ↔ 𝐷 = 𝐷 ) )
177 173 176 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ 𝑦 = 𝐷 ) → 𝐷 ∈ { 𝐷 } )
178 172 177 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ 𝑦 = 𝐷 ) → 𝑦 ∈ { 𝐷 } )
179 178 olcd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ 𝑦 = 𝐷 ) → ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∨ 𝑦 ∈ { 𝐷 } ) )
180 breq1 ⊢ ( 𝑎 = 𝑦 → ( 𝑎 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷 ) )
181 180 elrab ⊢ ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ↔ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) )
182 181 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) → ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) )
183 182 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) → ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) )
184 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 1 ∈ ℤ )
185 154 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝐷 ∈ ℤ )
186 185 184 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → ( 𝐷 − 1 ) ∈ ℤ )
187 elfzelz ⊢ ( 𝑦 ∈ ( 1 ... 𝐷 ) → 𝑦 ∈ ℤ )
188 187 adantr ⊢ ( ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) → 𝑦 ∈ ℤ )
189 188 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝑦 ∈ ℤ )
190 elfzle1 ⊢ ( 𝑦 ∈ ( 1 ... 𝐷 ) → 1 ≤ 𝑦 )
191 190 adantr ⊢ ( ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) → 1 ≤ 𝑦 )
192 191 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 1 ≤ 𝑦 )
193 elfzle2 ⊢ ( 𝑦 ∈ ( 1 ... 𝐷 ) → 𝑦 ≤ 𝐷 )
194 193 adantr ⊢ ( ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) → 𝑦 ≤ 𝐷 )
195 194 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝑦 ≤ 𝐷 )
196 neqne ⊢ ( ¬ 𝑦 = 𝐷 → 𝑦 ≠ 𝐷 )
197 196 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) → 𝑦 ≠ 𝐷 )
198 197 necomd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) → 𝐷 ≠ 𝑦 )
199 198 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝐷 ≠ 𝑦 )
200 195 199 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → ( 𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦 ) )
201 189 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝑦 ∈ ℝ )
202 156 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝐷 ∈ ℝ )
203 201 202 ltlend ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → ( 𝑦 < 𝐷 ↔ ( 𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦 ) ) )
204 200 203 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝑦 < 𝐷 )
205 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝐷 ∈ ℕ )
206 205 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝐷 ∈ ℤ )
207 189 206 zltlem1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → ( 𝑦 < 𝐷 ↔ 𝑦 ≤ ( 𝐷 − 1 ) ) )
208 204 207 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝑦 ≤ ( 𝐷 − 1 ) )
209 184 186 189 192 208 elfzd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝑦 ∈ ( 1 ... ( 𝐷 − 1 ) ) )
210 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝑦 ∥ 𝐷 )
211 180 209 210 elrabd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) ∧ ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } )
212 211 ex ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) → ( ( 𝑦 ∈ ( 1 ... 𝐷 ) ∧ 𝑦 ∥ 𝐷 ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) )
213 183 212 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } )
214 213 orcd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) ∧ ¬ 𝑦 = 𝐷 ) → ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∨ 𝑦 ∈ { 𝐷 } ) )
215 179 214 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) → ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∨ 𝑦 ∈ { 𝐷 } ) )
216 215 124 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) → 𝑦 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) )
217 216 ex ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } → 𝑦 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ) )
218 171 217 impbid ⊢ ( 𝜑 → ( 𝑦 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ↔ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) )
219 218 eqrdv ⊢ ( 𝜑 → ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) = { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
220 219 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) )
221 phisum ⊢ ( 𝐷 ∈ ℕ → Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) = 𝐷 )
222 6 221 syl ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) = 𝐷 )
223 eqcom ⊢ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = 𝐷 ↔ 𝐷 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )
224 223 imbi2i ⊢ ( ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = 𝐷 ) ↔ ( 𝜑 → 𝐷 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) )
225 9 224 mpbi ⊢ ( 𝜑 → 𝐷 = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )
226 225 oveq1d ⊢ ( 𝜑 → ( 𝐷 ↑ 𝑥 ) = ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) )
227 226 eqeq1d ⊢ ( 𝜑 → ( ( 𝐷 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) ↔ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
228 227 rabbidv ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( 𝐷 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
229 228 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝐷 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
230 1 2 3 4 5 8 unitscyglem1 ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )
231 229 230 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝐷 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )
232 231 9 eqtr2d ⊢ ( 𝜑 → 𝐷 = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝐷 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
233 1 2 3 4 6 grpods ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝐷 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
234 232 233 eqtr4d ⊢ ( 𝜑 → 𝐷 = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
235 219 eqcomd ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } = ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) )
236 235 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
237 234 236 eqtrd ⊢ ( 𝜑 → 𝐷 = Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
238 222 237 eqtr2d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) )
239 1zzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 1 ∈ ℤ )
240 154 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 𝐷 ∈ ℤ )
241 180 elrab ⊢ ( 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷 ) )
242 241 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → ( 𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷 ) )
243 242 simpld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 𝑦 ∈ ℕ )
244 243 nnzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 𝑦 ∈ ℤ )
245 243 nnge1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 1 ≤ 𝑦 )
246 242 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 𝑦 ∥ 𝐷 )
247 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 𝐷 ∈ ℕ )
248 dvdsle ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷 ) )
249 244 247 248 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → ( 𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷 ) )
250 246 249 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 𝑦 ≤ 𝐷 )
251 239 240 244 245 250 elfzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 𝑦 ∈ ( 1 ... 𝐷 ) )
252 180 251 246 elrabd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
253 252 ex ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } → 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) )
254 elfzelz ⊢ ( 𝑎 ∈ ( 1 ... 𝐷 ) → 𝑎 ∈ ℤ )
255 elfzle1 ⊢ ( 𝑎 ∈ ( 1 ... 𝐷 ) → 1 ≤ 𝑎 )
256 254 255 jca ⊢ ( 𝑎 ∈ ( 1 ... 𝐷 ) → ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
257 256 adantr ⊢ ( ( 𝑎 ∈ ( 1 ... 𝐷 ) ∧ 𝑎 ∥ 𝐷 ) → ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
258 257 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... 𝐷 ) ∧ 𝑎 ∥ 𝐷 ) ) → ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
259 elnnz1 ⊢ ( 𝑎 ∈ ℕ ↔ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
260 258 259 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... 𝐷 ) ∧ 𝑎 ∥ 𝐷 ) ) → 𝑎 ∈ ℕ )
261 260 rabss3d ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ⊆ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } )
262 261 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } → 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ) )
263 253 262 impbid ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ↔ 𝑦 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ) )
264 263 eqrdv ⊢ ( 𝜑 → { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } = { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } )
265 264 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) )
266 238 265 eqtr2d ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... 𝐷 ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
267 220 266 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
268 nfv ⊢ Ⅎ 𝑘 𝜑
269 nfcv ⊢ Ⅎ 𝑘 ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } )
270 fzfid ⊢ ( 𝜑 → ( 1 ... ( 𝐷 − 1 ) ) ∈ Fin )
271 ssrab2 ⊢ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ⊆ ( 1 ... ( 𝐷 − 1 ) )
272 271 a1i ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ⊆ ( 1 ... ( 𝐷 − 1 ) ) )
273 270 272 ssfid ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∈ Fin )
274 152 elrab ⊢ ( 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ↔ ( 𝐷 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝐷 ∥ 𝐷 ) )
275 274 biimpi ⊢ ( 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } → ( 𝐷 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∧ 𝐷 ∥ 𝐷 ) )
276 275 simpld ⊢ ( 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } → 𝐷 ∈ ( 1 ... ( 𝐷 − 1 ) ) )
277 276 adantl ⊢ ( ( 𝜑 ∧ 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝐷 ∈ ( 1 ... ( 𝐷 − 1 ) ) )
278 elfzle2 ⊢ ( 𝐷 ∈ ( 1 ... ( 𝐷 − 1 ) ) → 𝐷 ≤ ( 𝐷 − 1 ) )
279 277 278 syl ⊢ ( ( 𝜑 ∧ 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝐷 ≤ ( 𝐷 − 1 ) )
280 156 ltm1d ⊢ ( 𝜑 → ( 𝐷 − 1 ) < 𝐷 )
281 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
282 156 281 resubcld ⊢ ( 𝜑 → ( 𝐷 − 1 ) ∈ ℝ )
283 282 156 ltnled ⊢ ( 𝜑 → ( ( 𝐷 − 1 ) < 𝐷 ↔ ¬ 𝐷 ≤ ( 𝐷 − 1 ) ) )
284 280 283 mpbid ⊢ ( 𝜑 → ¬ 𝐷 ≤ ( 𝐷 − 1 ) )
285 284 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ¬ 𝐷 ≤ ( 𝐷 − 1 ) )
286 279 285 pm2.21dd ⊢ ( ( 𝜑 ∧ 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ¬ 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } )
287 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ¬ 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } )
288 286 287 pm2.61dan ⊢ ( 𝜑 → ¬ 𝐷 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } )
289 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → 𝐵 ∈ Fin )
290 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ⊆ 𝐵
291 290 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ⊆ 𝐵 )
292 289 291 ssfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∈ Fin )
293 hashcl ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℕ0 )
294 292 293 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℕ0 )
295 294 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℂ )
296 eqeq2 ⊢ ( 𝑘 = 𝐷 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 ) )
297 296 rabbidv ⊢ ( 𝑘 = 𝐷 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } )
298 297 fveq2d ⊢ ( 𝑘 = 𝐷 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) )
299 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ⊆ 𝐵
300 299 a1i ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ⊆ 𝐵 )
301 4 300 ssfid ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ∈ Fin )
302 hashcl ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ∈ ℕ0 )
303 301 302 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ∈ ℕ0 )
304 303 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ∈ ℂ )
305 268 269 273 6 288 295 298 304 fsumsplitsn ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) + ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ) )
306 267 305 eqtr2d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) + ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ) = Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ϕ ‘ 𝑘 ) )
307 nfcv ⊢ Ⅎ 𝑘 ( ϕ ‘ 𝐷 )
308 120 295 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ) → ( ϕ ‘ 𝑘 ) ∈ ℂ )
309 fveq2 ⊢ ( 𝑘 = 𝐷 → ( ϕ ‘ 𝑘 ) = ( ϕ ‘ 𝐷 ) )
310 6 phicld ⊢ ( 𝜑 → ( ϕ ‘ 𝐷 ) ∈ ℕ )
311 310 nncnd ⊢ ( 𝜑 → ( ϕ ‘ 𝐷 ) ∈ ℂ )
312 268 307 273 6 288 308 309 311 fsumsplitsn ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ∪ { 𝐷 } ) ( ϕ ‘ 𝑘 ) = ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) + ( ϕ ‘ 𝐷 ) ) )
313 306 312 eqtrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) + ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ) = ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) + ( ϕ ‘ 𝐷 ) ) )
314 123 313 eqtrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) + ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ) = ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) + ( ϕ ‘ 𝐷 ) ) )
315 273 308 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) ∈ ℂ )
316 315 304 311 addcand ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) + ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) ) = ( Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( 𝐷 − 1 ) ) ∣ 𝑎 ∥ 𝐷 } ( ϕ ‘ 𝑘 ) + ( ϕ ‘ 𝐷 ) ) ↔ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) ) )
317 314 316 mpbid ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )