Metamath Proof Explorer

Theorem unitscyglem4

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

Ref Expression
Hypotheses unitscyglem1.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
unitscyglem1.2 ⊢ ↑ = ( .g ‘ 𝐺 )
unitscyglem1.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
unitscyglem1.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
unitscyglem1.5 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑛 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑛 )
unitscyglem4.1 ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
unitscyglem4.2 ⊢ ( 𝜑 → 𝐷 ∥ ( ♯ ‘ 𝐵 ) )
Assertion unitscyglem4 ( 𝜑 → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( 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 unitscyglem4.1 ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
7 unitscyglem4.2 ⊢ ( 𝜑 → 𝐷 ∥ ( ♯ ‘ 𝐵 ) )
8 nfcv ⊢ Ⅎ 𝑦 𝐵
9 nfcv ⊢ Ⅎ 𝑥 𝐵
10 nfv ⊢ Ⅎ 𝑥 ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷
11 nfv ⊢ Ⅎ 𝑦 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷
12 fveqeq2 ⊢ ( 𝑦 = 𝑥 → ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 ) )
13 8 9 10 11 12 cbvrabw ⊢ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 }
14 13 fveq2i ⊢ ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } )
15 14 a1i ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) )
16 7 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → 𝐷 ∥ ( ♯ ‘ 𝐵 ) )
17 16 ex ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ → 𝐷 ∥ ( ♯ ‘ 𝐵 ) ) )
18 17 ancrd ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ → ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) ) )
19 18 imdistani ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( 𝜑 ∧ ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) ) )
20 breq1 ⊢ ( 𝑚 = 𝐷 → ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝐷 ∥ ( ♯ ‘ 𝐵 ) ) )
21 eqeq2 ⊢ ( 𝑚 = 𝐷 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 ) )
22 21 rabbidv ⊢ ( 𝑚 = 𝐷 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } )
23 22 neeq1d ⊢ ( 𝑚 = 𝐷 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ↔ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) )
24 20 23 anbi12d ⊢ ( 𝑚 = 𝐷 → ( ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ) ↔ ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) ) )
25 22 fveq2d ⊢ ( 𝑚 = 𝐷 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) )
26 fveq2 ⊢ ( 𝑚 = 𝐷 → ( ϕ ‘ 𝑚 ) = ( ϕ ‘ 𝐷 ) )
27 25 26 eqeq12d ⊢ ( 𝑚 = 𝐷 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ϕ ‘ 𝑚 ) ↔ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) ) )
28 24 27 imbi12d ⊢ ( 𝑚 = 𝐷 → ( ( ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ϕ ‘ 𝑚 ) ) ↔ ( ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) ) ) )
29 1 2 3 4 5 unitscyglem3 ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ϕ ‘ 𝑚 ) ) )
30 28 29 6 rspcdva ⊢ ( 𝜑 → ( ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) ) )
31 30 imp ⊢ ( ( 𝜑 ∧ ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )
32 19 31 syl ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )
33 15 32 eqtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )
34 id ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ )
35 34 necon1bi ⊢ ( ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ )
36 35 adantl ⊢ ( ( 𝜑 ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ )
37 3 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → 𝐺 ∈ Grp )
38 4 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → 𝐵 ∈ Fin )
39 1 37 38 hashfingrpnn ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
40 1 2 37 38 39 grpods ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ♯ ‘ 𝐵 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
41 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ♯ ‘ 𝐵 ) ) → ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ♯ ‘ 𝐵 ) )
42 41 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) = ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) )
43 42 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) ↑ 𝑥 ) = ( ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 𝑥 ) )
44 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐺 ∈ Grp )
45 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → 𝐺 ∈ Grp )
46 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → 𝑙 ∈ ℤ )
47 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
49 1 47 48 odcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ0 )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ0 )
51 50 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℤ )
52 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → 𝑥 ∈ 𝐵 )
53 46 51 52 3jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → ( 𝑙 ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) )
54 1 2 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑙 ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 𝑥 ) = ( 𝑙 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ↑ 𝑥 ) ) )
55 45 53 54 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → ( ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 𝑥 ) = ( 𝑙 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ↑ 𝑥 ) ) )
56 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
57 1 47 2 56 odid ⊢ ( 𝑥 ∈ 𝐵 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) )
58 52 57 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) )
59 58 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → ( 𝑙 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ↑ 𝑥 ) ) = ( 𝑙 ↑ ( 0g ‘ 𝐺 ) ) )
60 1 2 56 mulgz ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑙 ∈ ℤ ) → ( 𝑙 ↑ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
61 44 60 sylan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → ( 𝑙 ↑ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
62 59 61 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → ( 𝑙 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ↑ 𝑥 ) ) = ( 0g ‘ 𝐺 ) )
63 55 62 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) → ( ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) )
64 63 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ♯ ‘ 𝐵 ) ) → ( ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) )
65 43 64 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) )
66 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ Fin )
67 1 47 oddvds2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) )
68 44 66 48 67 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) )
69 49 nn0zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℤ )
70 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
71 66 70 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
72 71 nn0zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
73 divides ⊢ ( ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) ↔ ∃ 𝑙 ∈ ℤ ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ♯ ‘ 𝐵 ) ) )
74 69 72 73 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) ↔ ∃ 𝑙 ∈ ℤ ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ♯ ‘ 𝐵 ) ) )
75 68 74 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑙 ∈ ℤ ( 𝑙 · ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ♯ ‘ 𝐵 ) )
76 65 75 r19.29a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ♯ ‘ 𝐵 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) )
77 76 rabeqcda ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( ( ♯ ‘ 𝐵 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = 𝐵 )
78 77 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( ♯ ‘ 𝐵 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = 𝐵 )
79 78 fveq2d ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( ♯ ‘ 𝐵 ) ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ 𝐵 ) )
80 40 79 eqtr2d ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
81 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ )
82 nfcv ⊢ Ⅎ 𝑘 ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } )
83 fzfid ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( 1 ... ( ♯ ‘ 𝐵 ) ) ∈ Fin )
84 ssrab2 ⊢ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) )
85 84 a1i ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
86 83 85 ssfid ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∈ Fin )
87 38 adantr ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝐵 ∈ Fin )
88 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ⊆ 𝐵
89 88 a1i ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ⊆ 𝐵 )
90 87 89 ssfid ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∈ Fin )
91 hashcl ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℕ0 )
92 90 91 syl ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℕ0 )
93 92 nn0cnd ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℂ )
94 breq1 ⊢ ( 𝑎 = ( ♯ ‘ 𝐵 ) → ( 𝑎 ∥ ( ♯ ‘ 𝐵 ) ↔ ( ♯ ‘ 𝐵 ) ∥ ( ♯ ‘ 𝐵 ) ) )
95 1zzd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → 1 ∈ ℤ )
96 39 nnzd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
97 39 nnge1d ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → 1 ≤ ( ♯ ‘ 𝐵 ) )
98 39 nnred ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
99 98 leidd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐵 ) )
100 95 96 96 97 99 elfzd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
101 iddvds ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℤ → ( ♯ ‘ 𝐵 ) ∥ ( ♯ ‘ 𝐵 ) )
102 96 101 syl ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∥ ( ♯ ‘ 𝐵 ) )
103 94 100 102 elrabd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
104 eqeq2 ⊢ ( 𝑘 = ( ♯ ‘ 𝐵 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) )
105 104 rabbidv ⊢ ( 𝑘 = ( ♯ ‘ 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } )
106 105 fveq2d ⊢ ( 𝑘 = ( ♯ ‘ 𝐵 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) )
107 81 82 86 93 103 106 fsumsplit1 ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) + Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ) )
108 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ⊆ 𝐵
109 108 a1i ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ⊆ 𝐵 )
110 38 109 ssfid ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ∈ Fin )
111 hashcl ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) ∈ ℕ0 )
112 110 111 syl ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) ∈ ℕ0 )
113 112 nn0red ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) ∈ ℝ )
114 diffi ⊢ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∈ Fin → ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ∈ Fin )
115 86 114 syl ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ∈ Fin )
116 38 adantr ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → 𝐵 ∈ Fin )
117 88 a1i ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ⊆ 𝐵 )
118 116 117 ssfid ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∈ Fin )
119 118 91 syl ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℕ0 )
120 115 119 fsumnn0cl ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℕ0 )
121 120 nn0red ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℝ )
122 39 phicld ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) ∈ ℕ )
123 122 nnred ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) ∈ ℝ )
124 eldifi ⊢ ( 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) → 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
125 breq1 ⊢ ( 𝑎 = 𝑘 → ( 𝑎 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
126 125 elrab ⊢ ( 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ↔ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
127 126 biimpi ⊢ ( 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
128 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 𝑘 ∈ ℤ )
129 elfzle1 ⊢ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑘 )
130 128 129 jca ⊢ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
131 130 adantr ⊢ ( ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
132 127 131 syl ⊢ ( 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
133 124 132 syl ⊢ ( 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
134 133 adantl ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
135 elnnz1 ⊢ ( 𝑘 ∈ ℕ ↔ ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
136 134 135 sylibr ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → 𝑘 ∈ ℕ )
137 phicl ⊢ ( 𝑘 ∈ ℕ → ( ϕ ‘ 𝑘 ) ∈ ℕ )
138 136 137 syl ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → ( ϕ ‘ 𝑘 ) ∈ ℕ )
139 138 nnred ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → ( ϕ ‘ 𝑘 ) ∈ ℝ )
140 115 139 fsumrecl ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) ∈ ℝ )
141 simplll ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝜑 )
142 simplr ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
143 141 142 jca ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) )
144 simpr ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) )
145 143 144 jca ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) )
146 fveqeq2 ⊢ ( 𝑥 = ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 ↔ ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) = 𝐷 ) )
147 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝐺 ∈ Grp )
148 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝐷 ∥ ( ♯ ‘ 𝐵 ) )
149 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝐷 ∈ ℕ )
150 149 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝐷 ∈ ℤ )
151 149 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝐷 ≠ 0 )
152 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝐵 ∈ Fin )
153 152 70 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
154 153 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
155 dvdsval2 ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) → ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℤ ) )
156 150 151 154 155 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℤ ) )
157 148 156 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℤ )
158 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
159 1 2 147 157 158 mulgcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ∈ 𝐵 )
160 153 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℂ )
161 6 nncnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
162 161 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝐷 ∈ ℂ )
163 1 147 152 hashfingrpnn ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
164 163 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ≠ 0 )
165 160 160 162 164 151 divdiv2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ) = ( ( ( ♯ ‘ 𝐵 ) · 𝐷 ) / ( ♯ ‘ 𝐵 ) ) )
166 162 160 164 divcan3d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) · 𝐷 ) / ( ♯ ‘ 𝐵 ) ) = 𝐷 )
167 165 166 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝐷 = ( ( ♯ ‘ 𝐵 ) / ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ) )
168 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) )
169 168 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) = ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ♯ ‘ 𝐵 ) ) )
170 4 70 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
171 170 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
172 6 nnne0d ⊢ ( 𝜑 → 𝐷 ≠ 0 )
173 171 161 172 divcan2d ⊢ ( 𝜑 → ( 𝐷 · ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ) = ( ♯ ‘ 𝐵 ) )
174 173 eqcomd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝐷 · ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ) )
175 174 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ♯ ‘ 𝐵 ) = ( 𝐷 · ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ) )
176 175 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) = ( 𝐷 · ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ) )
177 176 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( 𝐷 · ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ) ) )
178 nndivdvds ⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℕ ) )
179 163 149 178 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( 𝐷 ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℕ ) )
180 148 179 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℕ )
181 180 nnnn0d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℕ0 )
182 181 150 gcdmultipled ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( 𝐷 · ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ) ) = ( ( ♯ ‘ 𝐵 ) / 𝐷 ) )
183 177 182 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐵 ) / 𝐷 ) )
184 169 183 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) = ( ( ♯ ‘ 𝐵 ) / 𝐷 ) )
185 184 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / 𝐷 ) = ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) )
186 185 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ) = ( ( ♯ ‘ 𝐵 ) / ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) ) )
187 167 186 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → 𝐷 = ( ( ♯ ‘ 𝐵 ) / ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) ) )
188 168 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) = ( ( od ‘ 𝐺 ) ‘ 𝑧 ) )
189 1 47 2 odmulg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) · ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) ) )
190 147 158 157 189 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) · ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) ) )
191 188 190 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) = ( ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) · ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) ) )
192 191 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) · ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) ) = ( ♯ ‘ 𝐵 ) )
193 157 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℂ )
194 184 193 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ ℂ )
195 1 47 159 odcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) ∈ ℕ0 )
196 195 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) ∈ ℂ )
197 168 154 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∈ ℤ )
198 168 164 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ≠ 0 )
199 157 197 198 3jca ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ≠ 0 ) )
200 gcd2n0cl ⊢ ( ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ≠ 0 ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ ℕ )
201 199 200 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ ℕ )
202 201 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) ≠ 0 )
203 160 194 196 202 divmuld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) ↔ ( ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) · ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) ) = ( ♯ ‘ 𝐵 ) ) )
204 192 203 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) / ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) gcd ( ( od ‘ 𝐺 ) ‘ 𝑧 ) ) ) = ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) )
205 187 204 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( od ‘ 𝐺 ) ‘ ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ) = 𝐷 )
206 146 159 205 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } )
207 ne0i ⊢ ( ( ( ( ♯ ‘ 𝐵 ) / 𝐷 ) ↑ 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ )
208 206 207 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ )
209 145 208 syl ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ )
210 rabn0 ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) )
211 nfv ⊢ Ⅎ 𝑧 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 )
212 nfv ⊢ Ⅎ 𝑥 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 )
213 fveqeq2 ⊢ ( 𝑥 = 𝑧 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) ) )
214 211 212 213 cbvrexw ⊢ ( ∃ 𝑥 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) )
215 210 214 bitri ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ↔ ∃ 𝑧 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) )
216 215 biimpi ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ → ∃ 𝑧 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) )
217 216 adantl ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) → ∃ 𝑧 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) )
218 209 217 r19.29a ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ )
219 218 ex ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) )
220 219 necon4d ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } = ∅ ) )
221 220 imp ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } = ∅ )
222 221 fveq2d ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) = ( ♯ ‘ ∅ ) )
223 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
224 223 a1i ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ ∅ ) = 0 )
225 222 224 eqtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) = 0 )
226 122 nngt0d ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → 0 < ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) )
227 225 226 eqbrtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) < ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) )
228 eldif ⊢ ( 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ↔ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) )
229 228 biimpi ⊢ ( 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) → ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) )
230 229 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) )
231 breq1 ⊢ ( 𝑎 = 𝑧 → ( 𝑎 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
232 231 elrab ⊢ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ↔ ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
233 232 biimpi ⊢ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
234 233 adantr ⊢ ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
235 velsn ⊢ ( 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ↔ 𝑧 = ( ♯ ‘ 𝐵 ) )
236 235 bicomi ⊢ ( 𝑧 = ( ♯ ‘ 𝐵 ) ↔ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } )
237 236 biimpi ⊢ ( 𝑧 = ( ♯ ‘ 𝐵 ) → 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } )
238 237 necon3bi ⊢ ( ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
239 238 adantl ⊢ ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
240 234 239 jca ⊢ ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) )
241 240 adantl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) ) → ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) )
242 1zzd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 1 ∈ ℤ )
243 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝐵 ∈ Fin )
244 243 70 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
245 244 nn0zd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
246 245 242 zsubcld ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℤ )
247 elfzelz ⊢ ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ ℤ )
248 247 adantr ⊢ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ ℤ )
249 248 adantr ⊢ ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ ℤ )
250 249 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∈ ℤ )
251 elfzle1 ⊢ ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑧 )
252 251 adantr ⊢ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑧 )
253 252 adantr ⊢ ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑧 )
254 253 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 1 ≤ 𝑧 )
255 elfzle2 ⊢ ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
256 255 adantr ⊢ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
257 256 adantr ⊢ ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
258 257 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
259 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
260 259 necomd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐵 ) ≠ 𝑧 )
261 258 260 jca ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑧 ≤ ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐵 ) ≠ 𝑧 ) )
262 250 zred ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∈ ℝ )
263 244 nn0red ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
264 262 263 ltlend ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑧 < ( ♯ ‘ 𝐵 ) ↔ ( 𝑧 ≤ ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐵 ) ≠ 𝑧 ) ) )
265 261 264 mpbird ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 < ( ♯ ‘ 𝐵 ) )
266 250 245 zltlem1d ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑧 < ( ♯ ‘ 𝐵 ) ↔ 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
267 265 266 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
268 242 246 250 254 267 elfzd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
269 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∥ ( ♯ ‘ 𝐵 ) )
270 231 268 269 elrabd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
271 270 ex ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
272 271 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) ) → ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
273 241 272 mpd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
274 273 ex ⊢ ( 𝜑 → ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
275 274 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
276 230 275 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
277 276 ex ⊢ ( 𝜑 → ( 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
278 277 ssrdv ⊢ ( 𝜑 → ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ⊆ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
279 1zzd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 1 ∈ ℤ )
280 170 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℤ )
281 280 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
282 elfzelz ⊢ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 𝑧 ∈ ℤ )
283 282 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ∈ ℤ )
284 elfzle1 ⊢ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 1 ≤ 𝑧 )
285 284 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 1 ≤ 𝑧 )
286 283 zred ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ∈ ℝ )
287 281 zred ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
288 1red ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 1 ∈ ℝ )
289 287 288 resubcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℝ )
290 elfzle2 ⊢ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
291 290 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
292 287 lem1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ≤ ( ♯ ‘ 𝐵 ) )
293 286 289 287 291 292 letrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
294 279 281 283 285 293 elfzd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
295 294 ex ⊢ ( 𝜑 → ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) )
296 295 ssrdv ⊢ ( 𝜑 → ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
297 rabss2 ⊢ ( ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
298 296 297 syl ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
299 298 sseld ⊢ ( 𝜑 → ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
300 299 imp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
301 170 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
302 301 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
303 302 leidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐵 ) )
304 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → 𝑧 = ( ♯ ‘ 𝐵 ) )
305 304 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) = 𝑧 )
306 231 elrab ⊢ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ↔ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
307 306 biimpi ⊢ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
308 307 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
309 291 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
310 309 ex ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
311 310 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
312 308 311 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
313 300 233 248 3syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ ℤ )
314 280 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
315 313 314 zltlem1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝑧 < ( ♯ ‘ 𝐵 ) ↔ 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
316 312 315 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 < ( ♯ ‘ 𝐵 ) )
317 316 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → 𝑧 < ( ♯ ‘ 𝐵 ) )
318 305 317 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐵 ) )
319 302 302 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐵 ) ↔ ¬ ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐵 ) ) )
320 318 319 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ¬ ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐵 ) )
321 303 320 pm2.21dd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
322 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
323 321 322 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
324 300 323 eldifsnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) )
325 324 ex ⊢ ( 𝜑 → ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) )
326 325 ssrdv ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) )
327 278 326 eqssd ⊢ ( 𝜑 → ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) = { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
328 327 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
329 fzfid ⊢ ( 𝜑 → ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∈ Fin )
330 ssrab2 ⊢ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) )
331 330 a1i ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
332 329 331 ssfid ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∈ Fin )
333 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝐵 ∈ Fin )
334 88 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ⊆ 𝐵 )
335 333 334 ssfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∈ Fin )
336 335 91 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℕ0 )
337 336 nn0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℝ )
338 125 elrab ⊢ ( 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ↔ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
339 338 biimpi ⊢ ( 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
340 339 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
341 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 𝑘 ∈ ℤ )
342 elfzle1 ⊢ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 1 ≤ 𝑘 )
343 341 342 jca ⊢ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
344 343 adantr ⊢ ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
345 344 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
346 345 135 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑘 ∈ ℕ )
347 346 ex ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑘 ∈ ℕ ) )
348 347 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑘 ∈ ℕ ) )
349 340 348 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑘 ∈ ℕ )
350 349 phicld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ϕ ‘ 𝑘 ) ∈ ℕ )
351 350 nnred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ϕ ‘ 𝑘 ) ∈ ℝ )
352 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 𝜑 )
353 338 biimpri ⊢ ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
354 353 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
355 354 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
356 352 355 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
357 356 337 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℝ )
358 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
359 356 358 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
360 340 simprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑘 ∥ ( ♯ ‘ 𝐵 ) )
361 360 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 𝑘 ∥ ( ♯ ‘ 𝐵 ) )
362 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
363 361 362 jca ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
364 breq1 ⊢ ( 𝑚 = 𝑘 → ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
365 eqeq2 ⊢ ( 𝑚 = 𝑘 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ) )
366 365 rabbidv ⊢ ( 𝑚 = 𝑘 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
367 366 neeq1d ⊢ ( 𝑚 = 𝑘 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ↔ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
368 364 367 anbi12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ) ↔ ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) ) )
369 366 fveq2d ⊢ ( 𝑚 = 𝑘 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
370 fveq2 ⊢ ( 𝑚 = 𝑘 → ( ϕ ‘ 𝑚 ) = ( ϕ ‘ 𝑘 ) )
371 369 370 eqeq12d ⊢ ( 𝑚 = 𝑘 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ϕ ‘ 𝑚 ) ↔ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) )
372 368 371 imbi12d ⊢ ( 𝑚 = 𝑘 → ( ( ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ϕ ‘ 𝑚 ) ) ↔ ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) ) )
373 29 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ϕ ‘ 𝑚 ) ) )
374 372 373 349 rspcdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) )
375 374 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) )
376 363 375 mpd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) )
377 359 376 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) )
378 357 377 eqled ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) )
379 id ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
380 379 necon1bi ⊢ ( ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } = ∅ )
381 380 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } = ∅ )
382 381 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ♯ ‘ ∅ ) )
383 223 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ ∅ ) = 0 )
384 382 383 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = 0 )
385 346 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 𝑘 ∈ ℕ )
386 385 phicld ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ϕ ‘ 𝑘 ) ∈ ℕ )
387 386 nnnn0d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ϕ ‘ 𝑘 ) ∈ ℕ0 )
388 387 nn0ge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 0 ≤ ( ϕ ‘ 𝑘 ) )
389 384 388 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) )
390 378 389 pm2.61dan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) )
391 390 ex ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) ) )
392 391 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) ) )
393 340 392 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) )
394 332 337 351 393 fsumle ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
395 327 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
396 395 eqcomd ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) )
397 394 396 breqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) )
398 328 397 eqbrtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) )
399 398 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) )
400 113 121 123 140 227 399 ltleaddd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) + Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ) < ( ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) + Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) ) )
401 nfcv ⊢ Ⅎ 𝑘 ( ϕ ‘ ( ♯ ‘ 𝐵 ) )
402 simpll ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝜑 )
403 127 adantl ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
404 402 403 jca ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) )
405 131 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
406 405 adantl ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
407 406 135 sylibr ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ) → 𝑘 ∈ ℕ )
408 407 ex ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑘 ∈ ℕ ) )
409 404 408 mpd ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑘 ∈ ℕ )
410 409 phicld ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ϕ ‘ 𝑘 ) ∈ ℕ )
411 410 nncnd ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ϕ ‘ 𝑘 ) ∈ ℂ )
412 fveq2 ⊢ ( 𝑘 = ( ♯ ‘ 𝐵 ) → ( ϕ ‘ 𝑘 ) = ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) )
413 81 401 86 411 103 412 fsumsplit1 ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = ( ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) + Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) ) )
414 400 413 breqtrrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) + Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ) < Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
415 107 414 eqbrtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) < Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
416 elfzelz ⊢ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 𝑎 ∈ ℤ )
417 elfzle1 ⊢ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑎 )
418 416 417 jca ⊢ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
419 418 adantr ⊢ ( ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
420 419 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
421 elnnz1 ⊢ ( 𝑎 ∈ ℕ ↔ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
422 420 421 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∈ ℕ )
423 422 rabss3d ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
424 simpl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝜑 )
425 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∈ ℕ )
426 424 425 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( 𝜑 ∧ 𝑎 ∈ ℕ ) )
427 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∥ ( ♯ ‘ 𝐵 ) )
428 426 427 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) )
429 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 1 ∈ ℤ )
430 280 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
431 430 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
432 425 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑎 ∈ ℕ )
433 432 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑎 ∈ ℤ )
434 432 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑎 )
435 nnz ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℤ )
436 435 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → 𝑎 ∈ ℤ )
437 1 3 4 hashfingrpnn ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )
438 437 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
439 dvdsle ⊢ ( ( 𝑎 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑎 ∥ ( ♯ ‘ 𝐵 ) → 𝑎 ≤ ( ♯ ‘ 𝐵 ) ) )
440 436 438 439 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( 𝑎 ∥ ( ♯ ‘ 𝐵 ) → 𝑎 ≤ ( ♯ ‘ 𝐵 ) ) )
441 440 imp ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑎 ≤ ( ♯ ‘ 𝐵 ) )
442 429 431 433 434 441 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
443 428 442 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
444 443 rabss3d ⊢ ( 𝜑 → { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
445 423 444 eqssd ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } = { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
446 445 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } = { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
447 446 sumeq1d ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
448 415 447 breqtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) < Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
449 phisum ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ → Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = ( ♯ ‘ 𝐵 ) )
450 39 449 syl ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = ( ♯ ‘ 𝐵 ) )
451 448 450 breqtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) < ( ♯ ‘ 𝐵 ) )
452 80 451 eqbrtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐵 ) )
453 170 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
454 453 nn0red ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
455 454 ltnrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ¬ ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐵 ) )
456 452 455 pm2.21dd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )
457 456 ex ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) ) )
458 457 adantr ⊢ ( ( 𝜑 ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) ) )
459 36 458 mpd ⊢ ( ( 𝜑 ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )
460 33 459 pm2.61dan ⊢ ( 𝜑 → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )