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 bilani ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) → ∃ 𝑧 ∈ 𝐵 ( ( od ‘ 𝐺 ) ‘ 𝑧 ) = ( ♯ ‘ 𝐵 ) )
217 209 216 r19.29a ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ )
218 217 ex ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ≠ ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) )
219 218 necon4d ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } = ∅ ) )
220 219 imp ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } = ∅ )
221 220 fveq2d ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) = ( ♯ ‘ ∅ ) )
222 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
223 222 a1i ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ ∅ ) = 0 )
224 221 223 eqtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) = 0 )
225 122 nngt0d ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → 0 < ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) )
226 224 225 eqbrtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) < ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) )
227 eldif ⊢ ( 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ↔ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) )
228 227 bilani ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) )
229 breq1 ⊢ ( 𝑎 = 𝑧 → ( 𝑎 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
230 229 elrab ⊢ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ↔ ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
231 230 biimpi ⊢ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
232 231 adantr ⊢ ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
233 velsn ⊢ ( 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ↔ 𝑧 = ( ♯ ‘ 𝐵 ) )
234 233 bicomi ⊢ ( 𝑧 = ( ♯ ‘ 𝐵 ) ↔ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } )
235 234 biimpi ⊢ ( 𝑧 = ( ♯ ‘ 𝐵 ) → 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } )
236 235 necon3bi ⊢ ( ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
237 236 adantl ⊢ ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
238 232 237 jca ⊢ ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) )
239 238 adantl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) ) → ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) )
240 1zzd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 1 ∈ ℤ )
241 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝐵 ∈ Fin )
242 241 70 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
243 242 nn0zd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
244 243 240 zsubcld ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℤ )
245 elfzelz ⊢ ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ ℤ )
246 245 adantr ⊢ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ ℤ )
247 246 adantr ⊢ ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ ℤ )
248 247 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∈ ℤ )
249 elfzle1 ⊢ ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑧 )
250 249 adantr ⊢ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑧 )
251 250 adantr ⊢ ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑧 )
252 251 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 1 ≤ 𝑧 )
253 elfzle2 ⊢ ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
254 253 adantr ⊢ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
255 254 adantr ⊢ ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
256 255 adantl ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
257 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
258 257 necomd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐵 ) ≠ 𝑧 )
259 256 258 jca ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑧 ≤ ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐵 ) ≠ 𝑧 ) )
260 248 zred ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∈ ℝ )
261 242 nn0red ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
262 260 261 ltlend ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑧 < ( ♯ ‘ 𝐵 ) ↔ ( 𝑧 ≤ ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐵 ) ≠ 𝑧 ) ) )
263 259 262 mpbird ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 < ( ♯ ‘ 𝐵 ) )
264 248 243 zltlem1d ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑧 < ( ♯ ‘ 𝐵 ) ↔ 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
265 263 264 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
266 240 244 248 252 265 elfzd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
267 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∥ ( ♯ ‘ 𝐵 ) )
268 229 266 267 elrabd ⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
269 268 ex ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
270 269 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) ) → ( ( ( 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
271 239 270 mpd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
272 271 ex ⊢ ( 𝜑 → ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
273 272 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → ( ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∧ ¬ 𝑧 ∈ { ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
274 228 273 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
275 274 ex ⊢ ( 𝜑 → ( 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
276 275 ssrdv ⊢ ( 𝜑 → ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ⊆ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
277 1zzd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 1 ∈ ℤ )
278 170 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℤ )
279 278 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
280 elfzelz ⊢ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 𝑧 ∈ ℤ )
281 280 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ∈ ℤ )
282 elfzle1 ⊢ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 1 ≤ 𝑧 )
283 282 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 1 ≤ 𝑧 )
284 281 zred ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ∈ ℝ )
285 279 zred ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
286 1red ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 1 ∈ ℝ )
287 285 286 resubcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℝ )
288 elfzle2 ⊢ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
289 288 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
290 285 lem1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → ( ( ♯ ‘ 𝐵 ) − 1 ) ≤ ( ♯ ‘ 𝐵 ) )
291 284 287 285 289 290 letrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ≤ ( ♯ ‘ 𝐵 ) )
292 277 279 281 283 291 elfzd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ) → 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
293 292 ex ⊢ ( 𝜑 → ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 𝑧 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) )
294 293 ssrdv ⊢ ( 𝜑 → ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
295 rabss2 ⊢ ( ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
296 294 295 syl ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
297 296 sseld ⊢ ( 𝜑 → ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
298 297 imp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
299 170 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
300 299 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
301 300 leidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐵 ) )
302 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → 𝑧 = ( ♯ ‘ 𝐵 ) )
303 302 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) = 𝑧 )
304 229 elrab ⊢ ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ↔ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
305 304 bilani ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) )
306 289 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
307 306 ex ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
308 307 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑧 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑧 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
309 305 308 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) )
310 298 231 246 3syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ ℤ )
311 278 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
312 310 311 zltlem1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝑧 < ( ♯ ‘ 𝐵 ) ↔ 𝑧 ≤ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
313 309 312 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 < ( ♯ ‘ 𝐵 ) )
314 313 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → 𝑧 < ( ♯ ‘ 𝐵 ) )
315 303 314 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐵 ) )
316 300 300 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐵 ) ↔ ¬ ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐵 ) ) )
317 315 316 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → ¬ ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐵 ) )
318 301 317 pm2.21dd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 = ( ♯ ‘ 𝐵 ) ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
319 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ 𝑧 ≠ ( ♯ ‘ 𝐵 ) ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
320 318 319 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ≠ ( ♯ ‘ 𝐵 ) )
321 298 320 eldifsnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) )
322 321 ex ⊢ ( 𝜑 → ( 𝑧 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } → 𝑧 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ) )
323 322 ssrdv ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) )
324 276 323 eqssd ⊢ ( 𝜑 → ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) = { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
325 324 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
326 fzfid ⊢ ( 𝜑 → ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∈ Fin )
327 ssrab2 ⊢ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) )
328 327 a1i ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
329 326 328 ssfid ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∈ Fin )
330 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝐵 ∈ Fin )
331 88 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ⊆ 𝐵 )
332 330 331 ssfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∈ Fin )
333 332 91 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℕ0 )
334 333 nn0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℝ )
335 125 elrab ⊢ ( 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ↔ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
336 335 bilani ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
337 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 𝑘 ∈ ℤ )
338 elfzle1 ⊢ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → 1 ≤ 𝑘 )
339 337 338 jca ⊢ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
340 339 adantr ⊢ ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
341 340 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
342 341 135 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑘 ∈ ℕ )
343 342 ex ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑘 ∈ ℕ ) )
344 343 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑘 ∈ ℕ ) )
345 336 344 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑘 ∈ ℕ )
346 345 phicld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ϕ ‘ 𝑘 ) ∈ ℕ )
347 346 nnred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ϕ ‘ 𝑘 ) ∈ ℝ )
348 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 𝜑 )
349 335 bilanri ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
350 349 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
351 348 350 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) )
352 351 334 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∈ ℝ )
353 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
354 351 353 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
355 336 simprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑘 ∥ ( ♯ ‘ 𝐵 ) )
356 355 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 𝑘 ∥ ( ♯ ‘ 𝐵 ) )
357 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
358 356 357 jca ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
359 breq1 ⊢ ( 𝑚 = 𝑘 → ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
360 eqeq2 ⊢ ( 𝑚 = 𝑘 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ) )
361 360 rabbidv ⊢ ( 𝑚 = 𝑘 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
362 361 neeq1d ⊢ ( 𝑚 = 𝑘 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ↔ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) )
363 359 362 anbi12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ) ↔ ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) ) )
364 361 fveq2d ⊢ ( 𝑚 = 𝑘 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
365 fveq2 ⊢ ( 𝑚 = 𝑘 → ( ϕ ‘ 𝑚 ) = ( ϕ ‘ 𝑘 ) )
366 364 365 eqeq12d ⊢ ( 𝑚 = 𝑘 → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ϕ ‘ 𝑚 ) ↔ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) )
367 363 366 imbi12d ⊢ ( 𝑚 = 𝑘 → ( ( ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ϕ ‘ 𝑚 ) ) ↔ ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) ) )
368 29 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ∀ 𝑚 ∈ ℕ ( ( 𝑚 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑚 } ) = ( ϕ ‘ 𝑚 ) ) )
369 367 368 345 rspcdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) )
370 369 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ( 𝑘 ∥ ( ♯ ‘ 𝐵 ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) ) )
371 358 370 mpd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) )
372 354 371 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ϕ ‘ 𝑘 ) )
373 352 372 eqled ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) )
374 id ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ )
375 374 necon1bi ⊢ ( ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } = ∅ )
376 375 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } = ∅ )
377 376 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ♯ ‘ ∅ ) )
378 222 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ ∅ ) = 0 )
379 377 378 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = 0 )
380 342 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 𝑘 ∈ ℕ )
381 380 phicld ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ϕ ‘ 𝑘 ) ∈ ℕ )
382 381 nnnn0d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ϕ ‘ 𝑘 ) ∈ ℕ0 )
383 382 nn0ge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → 0 ≤ ( ϕ ‘ 𝑘 ) )
384 379 383 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) )
385 373 384 pm2.61dan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) )
386 385 ex ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) ) )
387 386 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝑘 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) ) )
388 336 387 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ ( ϕ ‘ 𝑘 ) )
389 329 334 347 388 fsumle ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
390 324 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
391 390 eqcomd ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) )
392 389 391 breqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) )
393 325 392 eqbrtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) )
394 393 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ≤ Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) )
395 113 121 123 140 226 394 ltleaddd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) + Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ) < ( ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) + Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) ) )
396 nfcv ⊢ Ⅎ 𝑘 ( ϕ ‘ ( ♯ ‘ 𝐵 ) )
397 simpll ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝜑 )
398 126 bilani ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) )
399 397 398 jca ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) )
400 131 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
401 400 adantl ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘 ) )
402 401 135 sylibr ⊢ ( ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) ∧ ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) ) → 𝑘 ∈ ℕ )
403 402 ex ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ( 𝜑 ∧ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑘 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑘 ∈ ℕ ) )
404 399 403 mpd ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → 𝑘 ∈ ℕ )
405 404 phicld ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ϕ ‘ 𝑘 ) ∈ ℕ )
406 405 nncnd ⊢ ( ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) ∧ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ) → ( ϕ ‘ 𝑘 ) ∈ ℂ )
407 fveq2 ⊢ ( 𝑘 = ( ♯ ‘ 𝐵 ) → ( ϕ ‘ 𝑘 ) = ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) )
408 81 396 86 406 103 407 fsumsplit1 ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = ( ( ϕ ‘ ( ♯ ‘ 𝐵 ) ) + Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ϕ ‘ 𝑘 ) ) )
409 395 408 breqtrrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) } ) + Σ 𝑘 ∈ ( { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ∖ { ( ♯ ‘ 𝐵 ) } ) ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ) < Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
410 107 409 eqbrtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) < Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
411 elfzelz ⊢ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 𝑎 ∈ ℤ )
412 elfzle1 ⊢ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑎 )
413 411 412 jca ⊢ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
414 413 adantr ⊢ ( ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
415 414 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
416 elnnz1 ⊢ ( 𝑎 ∈ ℕ ↔ ( 𝑎 ∈ ℤ ∧ 1 ≤ 𝑎 ) )
417 415 416 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∈ ℕ )
418 417 rabss3d ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
419 simpl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝜑 )
420 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∈ ℕ )
421 419 420 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( 𝜑 ∧ 𝑎 ∈ ℕ ) )
422 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∥ ( ♯ ‘ 𝐵 ) )
423 421 422 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) )
424 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 1 ∈ ℤ )
425 278 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
426 425 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
427 420 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑎 ∈ ℕ )
428 427 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑎 ∈ ℤ )
429 427 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 1 ≤ 𝑎 )
430 nnz ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℤ )
431 430 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → 𝑎 ∈ ℤ )
432 1 3 4 hashfingrpnn ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )
433 432 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
434 dvdsle ⊢ ( ( 𝑎 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑎 ∥ ( ♯ ‘ 𝐵 ) → 𝑎 ≤ ( ♯ ‘ 𝐵 ) ) )
435 431 433 434 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) → ( 𝑎 ∥ ( ♯ ‘ 𝐵 ) → 𝑎 ≤ ( ♯ ‘ 𝐵 ) ) )
436 435 imp ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑎 ≤ ( ♯ ‘ 𝐵 ) )
437 424 426 428 429 436 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℕ ) ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
438 423 437 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) ) → 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
439 438 rabss3d ⊢ ( 𝜑 → { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ⊆ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
440 418 439 eqssd ⊢ ( 𝜑 → { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } = { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
441 440 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } = { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } )
442 441 sumeq1d ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
443 410 442 breqtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) < Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) )
444 phisum ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ → Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = ( ♯ ‘ 𝐵 ) )
445 39 444 syl ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ℕ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ϕ ‘ 𝑘 ) = ( ♯ ‘ 𝐵 ) )
446 443 445 breqtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → Σ 𝑘 ∈ { 𝑎 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) < ( ♯ ‘ 𝐵 ) )
447 80 446 eqbrtrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐵 ) )
448 170 adantr ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
449 448 nn0red ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
450 449 ltnrd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ¬ ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐵 ) )
451 447 450 pm2.21dd ⊢ ( ( 𝜑 ∧ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ ) → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )
452 451 ex ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) ) )
453 452 adantr ⊢ ( ( 𝜑 ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } = ∅ → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) ) )
454 36 453 mpd ⊢ ( ( 𝜑 ∧ ¬ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝐷 } ≠ ∅ ) → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )
455 33 454 pm2.61dan ⊢ ( 𝜑 → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )