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