Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  unitscyglem4 Structured version   Visualization version   GIF version
Theorem unitscyglem4 42159
Description: Lemma for unitscyg (Contributed by metakunt, 14-Jul-2025.)
Hypotheses
Ref Expression
unitscyglem1.1 𝐵 = (Base‘𝐺)
unitscyglem1.2 ↑ = (.g‘𝐺)
unitscyglem1.3 (𝜑 → 𝐺 ∈ Grp)
unitscyglem1.4 (𝜑 → 𝐵 ∈ Fin)
unitscyglem1.5 (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)
unitscyglem4.1 (𝜑 → 𝐷 ∈ ℕ)
unitscyglem4.2 (𝜑 → 𝐷 ∥ (♯‘𝐵))
Assertion
Ref Expression
unitscyglem4 (𝜑 → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
Distinct variable groups:   𝑥, ↑ ,𝑛   𝑥,𝐵,𝑛   𝑦,𝐵,𝑥   𝑥,𝐷,𝑦   𝑥,𝐺,𝑛   𝑦,𝐺   𝜑,𝑥,𝑛
Allowed substitution hints:   𝜑(𝑦)   𝐷(𝑛)   ↑ (𝑦)
Proof of Theorem unitscyglem4
Dummy variables 𝑙 𝑎 𝑘 𝑚 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfcv 2891 . . . . . 6 Ⅎ𝑦𝐵
2 nfcv 2891 . . . . . 6 Ⅎ𝑥𝐵
3 nfv 1914 . . . . . 6 Ⅎ𝑥((od‘𝐺)‘𝑦) = 𝐷
4 nfv 1914 . . . . . 6 Ⅎ𝑦((od‘𝐺)‘𝑥) = 𝐷
5 fveqeq2 6849 . . . . . 6 (𝑦 = 𝑥 → (((od‘𝐺)‘𝑦) = 𝐷 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
61, 2, 3, 4, 5cbvrabw 3438 . . . . 5 {𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}
76fveq2i 6843 . . . 4 (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
87a1i 11 . . 3 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
9 unitscyglem4.2 . . . . . . . 8 (𝜑 → 𝐷 ∥ (♯‘𝐵))
109adantr 480 . . . . . . 7 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → 𝐷 ∥ (♯‘𝐵))
1110ex 412 . . . . . 6 (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → 𝐷 ∥ (♯‘𝐵)))
1211ancrd 551 . . . . 5 (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)))
1312imdistani 568 . . . 4 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (𝜑 ∧ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)))
14 breq1 5105 . . . . . . . 8 (𝑚 = 𝐷 → (𝑚 ∥ (♯‘𝐵) ↔ 𝐷 ∥ (♯‘𝐵)))
15 eqeq2 2741 . . . . . . . . . 10 (𝑚 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
1615rabbidv 3410 . . . . . . . . 9 (𝑚 = 𝐷 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
1716neeq1d 2984 . . . . . . . 8 (𝑚 = 𝐷 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))
1814, 17anbi12d 632 . . . . . . 7 (𝑚 = 𝐷 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)))
1916fveq2d 6844 . . . . . . . 8 (𝑚 = 𝐷 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
20 fveq2 6840 . . . . . . . 8 (𝑚 = 𝐷 → (ϕ‘𝑚) = (ϕ‘𝐷))
2119, 20eqeq12d 2745 . . . . . . 7 (𝑚 = 𝐷 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)))
2218, 21imbi12d 344 . . . . . 6 (𝑚 = 𝐷 → (((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)) ↔ ((𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))))
23 unitscyglem1.1 . . . . . . 7 𝐵 = (Base‘𝐺)
24 unitscyglem1.2 . . . . . . 7 ↑ = (.g‘𝐺)
25 unitscyglem1.3 . . . . . . 7 (𝜑 → 𝐺 ∈ Grp)
26 unitscyglem1.4 . . . . . . 7 (𝜑 → 𝐵 ∈ Fin)
27 unitscyglem1.5 . . . . . . 7 (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)
2823, 24, 25, 26, 27unitscyglem3 42158 . . . . . 6 (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)))
29 unitscyglem4.1 . . . . . 6 (𝜑 → 𝐷 ∈ ℕ)
3022, 28, 29rspcdva 3586 . . . . 5 (𝜑 → ((𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)))
3130imp 406 . . . 4 ((𝜑 ∧ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))
3213, 31syl 17 . . 3 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))
338, 32eqtrd 2764 . 2 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
34 id 22 . . . . 5 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
3534necon1bi 2953 . . . 4 (¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
3635adantl 481 . . 3 ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
3725adantr 480 . . . . . . . . 9 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 𝐺 ∈ Grp)
3826adantr 480 . . . . . . . . 9 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 𝐵 ∈ Fin)
3923, 37, 38hashfingrpnn 18880 . . . . . . . . 9 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℕ)
4023, 24, 37, 38, 39grpods 42155 . . . . . . . 8 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)}))
41 simpr 484 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵))
4241eqcomd 2735 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (♯‘𝐵) = (𝑙 · ((od‘𝐺)‘𝑥)))
4342oveq1d 7384 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) ↑ 𝑥) = ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥))
4425adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐺 ∈ Grp)
4544adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝐺 ∈ Grp)
46 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℤ)
47 eqid 2729 . . . . . . . . . . . . . . . . . . . 20 (od‘𝐺) = (od‘𝐺)
48 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
4923, 47, 48odcld 19458 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
5049adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
5150nn0zd 12531 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈ ℤ)
52 simplr 768 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝑥 ∈ 𝐵)
5346, 51, 523jca 1128 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ∈ ℤ ∧ ((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥 ∈ 𝐵))
5423, 24mulgass 19019 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ (𝑙 ∈ ℤ ∧ ((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)))
5545, 53, 54syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)))
56 eqid 2729 . . . . . . . . . . . . . . . . . . 19 (0g‘𝐺) = (0g‘𝐺)
5723, 47, 24, 56odid 19444 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ 𝐵 → (((od‘𝐺)‘𝑥) ↑ 𝑥) = (0g‘𝐺))
5852, 57syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (((od‘𝐺)‘𝑥) ↑ 𝑥) = (0g‘𝐺))
5958oveq2d 7385 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)) = (𝑙 ↑ (0g‘𝐺)))
6023, 24, 56mulgz 19010 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (0g‘𝐺)) = (0g‘𝐺))
6144, 60sylan 580 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (0g‘𝐺)) = (0g‘𝐺))
6259, 61eqtrd 2764 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)) = (0g‘𝐺))
6355, 62eqtrd 2764 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (0g‘𝐺))
6463adantr 480 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (0g‘𝐺))
6543, 64eqtrd 2764 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺))
6626adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐵 ∈ Fin)
6723, 47oddvds2 19472 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
6844, 66, 48, 67syl3anc 1373 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
6949nn0zd 12531 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℤ)
70 hashcl 14297 . . . . . . . . . . . . . . . 16 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
7166, 70syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℕ0)
7271nn0zd 12531 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℤ)
73 divides 16200 . . . . . . . . . . . . . 14 ((((od‘𝐺)‘𝑥) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → (((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)))
7469, 72, 73syl2anc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)))
7568, 74mpbid 232 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵))
7665, 75r19.29a 3141 . . . . . . . . . . 11 ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺))
7776rabeqcda 3414 . . . . . . . . . 10 (𝜑 → {𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)} = 𝐵)
7877adantr 480 . . . . . . . . 9 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)} = 𝐵)
7978fveq2d 6844 . . . . . . . 8 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)}) = (♯‘𝐵))
8040, 79eqtr2d 2765 . . . . . . 7 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) = Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
81 nfv 1914 . . . . . . . . . . 11 Ⅎ𝑘(𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
82 nfcv 2891 . . . . . . . . . . 11 Ⅎ𝑘(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)})
83 fzfid 13914 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (1...(♯‘𝐵)) ∈ Fin)
84 ssrab2 4039 . . . . . . . . . . . . 13 {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵))
8584a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
8683, 85ssfid 9188 . . . . . . . . . . 11 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin)
8738adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin)
88 ssrab2 4039 . . . . . . . . . . . . . . 15 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵
8988a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
9087, 89ssfid 9188 . . . . . . . . . . . . 13 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
91 hashcl 14297 . . . . . . . . . . . . 13 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
9290, 91syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
9392nn0cnd 12481 . . . . . . . . . . 11 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ)
94 breq1 5105 . . . . . . . . . . . 12 (𝑎 = (♯‘𝐵) → (𝑎 ∥ (♯‘𝐵) ↔ (♯‘𝐵) ∥ (♯‘𝐵)))
95 1zzd 12540 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ∈ ℤ)
9639nnzd 12532 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℤ)
9739nnge1d 12210 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ≤ (♯‘𝐵))
9839nnred 12177 . . . . . . . . . . . . . 14 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℝ)
9998leidd 11720 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ≤ (♯‘𝐵))
10095, 96, 96, 97, 99elfzd 13452 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ (1...(♯‘𝐵)))
101 iddvds 16215 . . . . . . . . . . . . 13 ((♯‘𝐵) ∈ ℤ → (♯‘𝐵) ∥ (♯‘𝐵))
10296, 101syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∥ (♯‘𝐵))
10394, 100, 102elrabd 3658 . . . . . . . . . . 11 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
104 eqeq2 2741 . . . . . . . . . . . . 13 (𝑘 = (♯‘𝐵) → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = (♯‘𝐵)))
105104rabbidv 3410 . . . . . . . . . . . 12 (𝑘 = (♯‘𝐵) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)})
106105fveq2d 6844 . . . . . . . . . . 11 (𝑘 = (♯‘𝐵) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}))
10781, 82, 86, 93, 103, 106fsumsplit1 15687 . . . . . . . . . 10 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})))
108 ssrab2 4039 . . . . . . . . . . . . . . . 16 {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵
109108a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵)
11038, 109ssfid 9188 . . . . . . . . . . . . . 14 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin)
111 hashcl 14297 . . . . . . . . . . . . . 14 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℕ0)
112110, 111syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℕ0)
113112nn0red 12480 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℝ)
114 diffi 9116 . . . . . . . . . . . . . . 15 ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ∈ Fin)
11586, 114syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ∈ Fin)
11638adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝐵 ∈ Fin)
11788a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
118116, 117ssfid 9188 . . . . . . . . . . . . . . 15 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
119118, 91syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
120115, 119fsumnn0cl 15678 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
121120nn0red 12480 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
12239phicld 16718 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (ϕ‘(♯‘𝐵)) ∈ ℕ)
123122nnred 12177 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (ϕ‘(♯‘𝐵)) ∈ ℝ)
124 eldifi 4090 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
125 breq1 5105 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑘 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
126125elrab 3656 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
127126biimpi 216 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
128 elfzelz 13461 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(♯‘𝐵)) → 𝑘 ∈ ℤ)
129 elfzle1 13464 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(♯‘𝐵)) → 1 ≤ 𝑘)
130128, 129jca 511 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (1...(♯‘𝐵)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
131130adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
132127, 131syl 17 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
133124, 132syl 17 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
134133adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
135 elnnz1 12535 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
136134, 135sylibr 234 . . . . . . . . . . . . . . 15 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝑘 ∈ ℕ)
137 phicl 16715 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (ϕ‘𝑘) ∈ ℕ)
138136, 137syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℕ)
139138nnred 12177 . . . . . . . . . . . . 13 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℝ)
140115, 139fsumrecl 15676 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘) ∈ ℝ)
141 simplll 774 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝜑)
142 simplr 768 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝑧 ∈ 𝐵)
143141, 142jca 511 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝜑 ∧ 𝑧 ∈ 𝐵))
144 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = (♯‘𝐵))
145143, 144jca 511 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)))
146 fveqeq2 6849 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (((♯‘𝐵) / 𝐷) ↑ 𝑧) → (((od‘𝐺)‘𝑥) = 𝐷 ↔ ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) = 𝐷))
14725ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐺 ∈ Grp)
1489ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∥ (♯‘𝐵))
14929ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℕ)
150149nnzd 12532 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℤ)
151149nnne0d 12212 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ≠ 0)
15226ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐵 ∈ Fin)
153152, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
154153nn0zd 12531 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
155 dvdsval2 16201 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ∧ (♯‘𝐵) ∈ ℤ) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℤ))
156150, 151, 154, 155syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℤ))
157148, 156mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℤ)
158 simplr 768 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝑧 ∈ 𝐵)
15923, 24, 147, 157, 158mulgcld 19004 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ 𝐵)
160153nn0cnd 12481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ)
16129nncnd 12178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 𝐷 ∈ ℂ)
162161ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℂ)
16323, 147, 152hashfingrpnn 18880 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ)
164163nnne0d 12212 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ≠ 0)
165160, 160, 162, 164, 151divdiv2d 11966 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = (((♯‘𝐵) · 𝐷) / (♯‘𝐵)))
166162, 160, 164divcan3d 11939 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) · 𝐷) / (♯‘𝐵)) = 𝐷)
167165, 166eqtr2d 2765 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)))
168 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = (♯‘𝐵))
169168oveq2d 7385 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)))
17026, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (♯‘𝐵) ∈ ℕ0)
171170nn0cnd 12481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (♯‘𝐵) ∈ ℂ)
17229nnne0d 12212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 𝐷 ≠ 0)
173171, 161, 172divcan2d 11936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝐷 · ((♯‘𝐵) / 𝐷)) = (♯‘𝐵))
174173eqcomd 2735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
175174adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ 𝑧 ∈ 𝐵) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
176175adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
177176oveq2d 7385 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷))))
178 nndivdvds 16207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐵) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℕ))
179163, 149, 178syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℕ))
180148, 179mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℕ)
181180nnnn0d 12479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℕ0)
182181, 150gcdmultipled 16480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷))) = ((♯‘𝐵) / 𝐷))
183177, 182eqtrd 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = ((♯‘𝐵) / 𝐷))
184169, 183eqtrd 2764 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = ((♯‘𝐵) / 𝐷))
185184eqcomd 2735 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) = (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)))
186185oveq2d 7385 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))))
187167, 186eqtrd 2764 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))))
188168eqcomd 2735 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((od‘𝐺)‘𝑧))
18923, 47, 24odmulg 19462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ ((♯‘𝐵) / 𝐷) ∈ ℤ) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))))
190147, 158, 157, 189syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))))
191188, 190eqtrd 2764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))))
192191eqcomd 2735 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))) = (♯‘𝐵))
193157zcnd 12615 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℂ)
194184, 193eqeltrd 2828 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℂ)
19523, 47, 159odcld 19458 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ∈ ℕ0)
196195nn0cnd 12481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ∈ ℂ)
197168, 154eqeltrd 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ∈ ℤ)
198168, 164eqnetrd 2992 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ≠ 0)
199157, 197, 1983jca 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ≠ 0))
200 gcd2n0cl 16455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((♯‘𝐵) / 𝐷) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ≠ 0) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ)
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ)
202201nnne0d 12212 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ≠ 0)
203160, 194, 196, 202divmuld 11956 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ↔ ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))) = (♯‘𝐵)))
204192, 203mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)))
205187, 204eqtr2d 2765 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) = 𝐷)
206146, 159, 205elrabd 3658 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
207 ne0i 4300 . . . . . . . . . . . . . . . . . . . . 21 ((((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
209145, 208syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
210 rabn0 4348 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵))
211 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . 23 Ⅎ𝑧((od‘𝐺)‘𝑥) = (♯‘𝐵)
212 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . 23 Ⅎ𝑥((od‘𝐺)‘𝑧) = (♯‘𝐵)
213 fveqeq2 6849 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ((od‘𝐺)‘𝑧) = (♯‘𝐵)))
214211, 212, 213cbvrexw 3279 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
215210, 214bitri 275 . . . . . . . . . . . . . . . . . . . . 21 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
216215biimpi 216 . . . . . . . . . . . . . . . . . . . 20 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ → ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
217216adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
218209, 217r19.29a 3141 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
219218ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))
220219necon4d 2949 . . . . . . . . . . . . . . . 16 (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅))
221220imp 406 . . . . . . . . . . . . . . 15 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅)
222221fveq2d 6844 . . . . . . . . . . . . . 14 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) = (♯‘∅))
223 hash0 14308 . . . . . . . . . . . . . . 15 (♯‘∅) = 0
224223a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘∅) = 0)
225222, 224eqtrd 2764 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) = 0)
226122nngt0d 12211 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 0 < (ϕ‘(♯‘𝐵)))
227225, 226eqbrtrd 5124 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) < (ϕ‘(♯‘𝐵)))
228 eldif 3921 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ↔ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
229228biimpi 216 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
230229adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
231 breq1 5105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑧 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑧 ∥ (♯‘𝐵)))
232231elrab 3656 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
233232biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
234233adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
235 velsn 4601 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ {(♯‘𝐵)} ↔ 𝑧 = (♯‘𝐵))
236235bicomi 224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (♯‘𝐵) ↔ 𝑧 ∈ {(♯‘𝐵)})
237236biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (♯‘𝐵) → 𝑧 ∈ {(♯‘𝐵)})
238237necon3bi 2951 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ 𝑧 ∈ {(♯‘𝐵)} → 𝑧 ≠ (♯‘𝐵))
239238adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵))
240234, 239jca 511 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)))
241240adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)))
242 1zzd 12540 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 1 ∈ ℤ)
24326adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝐵 ∈ Fin)
244243, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℕ0)
245244nn0zd 12531 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℤ)
246245, 242zsubcld 12619 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → ((♯‘𝐵) − 1) ∈ ℤ)
247 elfzelz 13461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (1...(♯‘𝐵)) → 𝑧 ∈ ℤ)
248247adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ∈ ℤ)
249248adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ ℤ)
250249adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℤ)
251 elfzle1 13464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (1...(♯‘𝐵)) → 1 ≤ 𝑧)
252251adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 1 ≤ 𝑧)
253252adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 1 ≤ 𝑧)
254253adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 1 ≤ 𝑧)
255 elfzle2 13465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 ∈ (1...(♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵))
256255adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵))
257256adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵))
258257adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≤ (♯‘𝐵))
259 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≠ (♯‘𝐵))
260259necomd 2980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ≠ 𝑧)
261258, 260jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧))
262250zred 12614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℝ)
263244nn0red 12480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℝ)
264262, 263ltlend 11295 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧)))
265261, 264mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 < (♯‘𝐵))
266250, 245zltlem1d 12563 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1)))
267265, 266mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≤ ((♯‘𝐵) − 1))
268242, 246, 250, 254, 267elfzd 13452 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ (1...((♯‘𝐵) − 1)))
269 simprlr 779 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∥ (♯‘𝐵))
270231, 268, 269elrabd 3658 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
271270ex 412 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
272271adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
273241, 272mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
274273ex 412 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
275274adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
276230, 275mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
277276ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
278277ssrdv 3949 . . . . . . . . . . . . . . . 16 (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ⊆ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
279 1zzd 12540 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈ ℤ)
280170nn0zd 12531 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (♯‘𝐵) ∈ ℤ)
281280adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → (♯‘𝐵) ∈ ℤ)
282 elfzelz 13461 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ∈ ℤ)
283282adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ ℤ)
284 elfzle1 13464 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 1 ≤ 𝑧)
285284adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ≤ 𝑧)
286283zred 12614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ ℝ)
287281zred 12614 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → (♯‘𝐵) ∈ ℝ)
288 1red 11151 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈ ℝ)
289287, 288resubcld 11582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → ((♯‘𝐵) − 1) ∈ ℝ)
290 elfzle2 13465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ≤ ((♯‘𝐵) − 1))
291290adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ ((♯‘𝐵) − 1))
292287lem1d 12092 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → ((♯‘𝐵) − 1) ≤ (♯‘𝐵))
293286, 289, 287, 291, 292letrd 11307 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ (♯‘𝐵))
294279, 281, 283, 285, 293elfzd 13452 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ (1...(♯‘𝐵)))
295294ex 412 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ∈ (1...(♯‘𝐵))))
296295ssrdv 3949 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...((♯‘𝐵) − 1)) ⊆ (1...(♯‘𝐵)))
297 rabss2 4037 . . . . . . . . . . . . . . . . . . . . . 22 ((1...((♯‘𝐵) − 1)) ⊆ (1...(♯‘𝐵)) → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
298296, 297syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
299298sseld 3942 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}))
300299imp 406 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
301170ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
302301nn0red 12480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈ ℝ)
303302leidd 11720 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ≤ (♯‘𝐵))
304 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 = (♯‘𝐵))
305304eqcomd 2735 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) = 𝑧)
306231elrab 3656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)))
307306biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)))
308307adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)))
309291adantrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵))) → 𝑧 ≤ ((♯‘𝐵) − 1))
310309ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ≤ ((♯‘𝐵) − 1)))
311310adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ≤ ((♯‘𝐵) − 1)))
312308, 311mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ≤ ((♯‘𝐵) − 1))
313300, 233, 2483syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ ℤ)
314280adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘𝐵) ∈ ℤ)
315313, 314zltlem1d 12563 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1)))
316312, 315mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 < (♯‘𝐵))
317316adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 < (♯‘𝐵))
318305, 317eqbrtrd 5124 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) < (♯‘𝐵))
319302, 302ltnled 11297 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → ((♯‘𝐵) < (♯‘𝐵) ↔ ¬ (♯‘𝐵) ≤ (♯‘𝐵)))
320318, 319mpbid 232 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → ¬ (♯‘𝐵) ≤ (♯‘𝐵))
321303, 320pm2.21dd 195 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 ≠ (♯‘𝐵))
322 simpr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ≠ (♯‘𝐵))
323321, 322pm2.61dane 3012 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵))
324300, 323eldifsnd 4747 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}))
325324ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})))
326325ssrdv 3949 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}))
327278, 326eqssd 3961 . . . . . . . . . . . . . . 15 (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) = {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
328327sumeq1d 15642 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
329 fzfid 13914 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...((♯‘𝐵) − 1)) ∈ Fin)
330 ssrab2 4039 . . . . . . . . . . . . . . . . . 18 {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...((♯‘𝐵) − 1))
331330a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...((♯‘𝐵) − 1)))
332329, 331ssfid 9188 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin)
33326adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin)
33488a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
335333, 334ssfid 9188 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
336335, 91syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
337336nn0red 12480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
338125elrab 3656 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
339338biimpi 216 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
340339adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
341 elfzelz 13461 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (1...((♯‘𝐵) − 1)) → 𝑘 ∈ ℤ)
342 elfzle1 13464 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (1...((♯‘𝐵) − 1)) → 1 ≤ 𝑘)
343341, 342jca 511 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (1...((♯‘𝐵) − 1)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
344343adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
345344adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
346345, 135sylibr 234 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → 𝑘 ∈ ℕ)
347346ex 412 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → 𝑘 ∈ ℕ))
348347adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → 𝑘 ∈ ℕ))
349340, 348mpd 15 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑘 ∈ ℕ)
350349phicld 16718 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℕ)
351350nnred 12177 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℝ)
352 simpll 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝜑)
353338biimpri 228 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
354353adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
355354adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
356352, 355jca 511 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
357356, 337syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
358 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
359356, 358jca 511 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
360340simprd 495 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑘 ∥ (♯‘𝐵))
361360adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∥ (♯‘𝐵))
362 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
363361, 362jca 511 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
364 breq1 5105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑘 → (𝑚 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
365 eqeq2 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑚 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝑘))
366365rabbidv 3410 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 = 𝑘 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
367366neeq1d 2984 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑘 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
368364, 367anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑘 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)))
369366fveq2d 6844 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑘 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
370 fveq2 6840 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑘 → (ϕ‘𝑚) = (ϕ‘𝑘))
371369, 370eqeq12d 2745 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑘 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
372368, 371imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘 → (((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)) ↔ ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))))
37328adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ∀𝑚 ∈ ℕ ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)))
374372, 373, 349rspcdva 3586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
375374adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
376363, 375mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))
377359, 376syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))
378357, 377eqled 11253 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
379 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
380379necon1bi 2953 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅)
381380adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅)
382381fveq2d 6844 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘∅))
383223a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘∅) = 0)
384382, 383eqtrd 2764 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = 0)
385346adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∈ ℕ)
386385phicld 16718 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈ ℕ)
387386nnnn0d 12479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈ ℕ0)
388387nn0ge0d 12482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 0 ≤ (ϕ‘𝑘))
389384, 388eqbrtrd 5124 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
390378, 389pm2.61dan 812 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
391390ex 412 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘)))
392391adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘)))
393340, 392mpd 15 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
394332, 337, 351, 393fsumle 15741 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
395327sumeq1d 15642 . . . . . . . . . . . . . . . 16 (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
396395eqcomd 2735 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
397394, 396breqtrd 5128 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
398328, 397eqbrtrd 5124 . . . . . . . . . . . . 13 (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
399398adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
400113, 121, 123, 140, 227, 399ltleaddd 11775 . . . . . . . . . . 11 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)))
401 nfcv 2891 . . . . . . . . . . . 12 Ⅎ𝑘(ϕ‘(♯‘𝐵))
402 simpll 766 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝜑)
403127adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
404402, 403jca 511 . . . . . . . . . . . . . . 15 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))))
405131adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
406405adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ (𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
407406, 135sylibr 234 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ (𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))) → 𝑘 ∈ ℕ)
408407ex 412 . . . . . . . . . . . . . . 15 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))) → 𝑘 ∈ ℕ))
409404, 408mpd 15 . . . . . . . . . . . . . 14 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑘 ∈ ℕ)
410409phicld 16718 . . . . . . . . . . . . 13 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℕ)
411410nncnd 12178 . . . . . . . . . . . 12 (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℂ)
412 fveq2 6840 . . . . . . . . . . . 12 (𝑘 = (♯‘𝐵) → (ϕ‘𝑘) = (ϕ‘(♯‘𝐵)))
41381, 401, 86, 411, 103, 412fsumsplit1 15687 . . . . . . . . . . 11 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)))
414400, 413breqtrrd 5130 . . . . . . . . . 10 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
415107, 414eqbrtrd 5124 . . . . . . . . 9 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
416 elfzelz 13461 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (1...(♯‘𝐵)) → 𝑎 ∈ ℤ)
417 elfzle1 13464 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (1...(♯‘𝐵)) → 1 ≤ 𝑎)
418416, 417jca 511 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (1...(♯‘𝐵)) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
419418adantr 480 . . . . . . . . . . . . . . 15 ((𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵)) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
420419adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵))) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
421 elnnz1 12535 . . . . . . . . . . . . . 14 (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
422420, 421sylibr 234 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ ℕ)
423422rabss3d 4040 . . . . . . . . . . . 12 (𝜑 → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
424 simpl 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝜑)
425 simprl 770 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ ℕ)
426424, 425jca 511 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → (𝜑 ∧ 𝑎 ∈ ℕ))
427 simprr 772 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∥ (♯‘𝐵))
428426, 427jca 511 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → ((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)))
429 1zzd 12540 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ∈ ℤ)
430280adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑎 ∈ ℕ) → (♯‘𝐵) ∈ ℤ)
431430adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
432425anassrs 467 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℕ)
433432nnzd 12532 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℤ)
434432nnge1d 12210 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ≤ 𝑎)
435 nnz 12526 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
436435adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑎 ∈ ℕ) → 𝑎 ∈ ℤ)
43723, 25, 26hashfingrpnn 18880 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘𝐵) ∈ ℕ)
438437adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑎 ∈ ℕ) → (♯‘𝐵) ∈ ℕ)
439 dvdsle 16256 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑎 ∥ (♯‘𝐵) → 𝑎 ≤ (♯‘𝐵)))
440436, 438, 439syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑎 ∈ ℕ) → (𝑎 ∥ (♯‘𝐵) → 𝑎 ≤ (♯‘𝐵)))
441440imp 406 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ≤ (♯‘𝐵))
442429, 431, 433, 434, 441elfzd 13452 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ (1...(♯‘𝐵)))
443428, 442syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ (1...(♯‘𝐵)))
444443rabss3d 4040 . . . . . . . . . . . 12 (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
445423, 444eqssd 3961 . . . . . . . . . . 11 (𝜑 → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
446445adantr 480 . . . . . . . . . 10 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
447446sumeq1d 15642 . . . . . . . . 9 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
448415, 447breqtrd 5128 . . . . . . . 8 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
449 phisum 16737 . . . . . . . . 9 ((♯‘𝐵) ∈ ℕ → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵))
45039, 449syl 17 . . . . . . . 8 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵))
451448, 450breqtrd 5128 . . . . . . 7 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < (♯‘𝐵))
45280, 451eqbrtrd 5124 . . . . . 6 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) < (♯‘𝐵))
453170adantr 480 . . . . . . . 8 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℕ0)
454453nn0red 12480 . . . . . . 7 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℝ)
455454ltnrd 11284 . . . . . 6 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ¬ (♯‘𝐵) < (♯‘𝐵))
456452, 455pm2.21dd 195 . . . . 5 ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
457456ex 412 . . . 4 (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)))
458457adantr 480 . . 3 ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)))
45936, 458mpd 15 . 2 ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
46033, 459pm2.61dan 812 1 (𝜑 → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3402   ∖ cdif 3908   ⊆ wss 3911  ∅c0 4292  {csn 4585   class class class wbr 5102  ‘cfv 6499  (class class class)co 7369  Fincfn 8895  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045   + caddc 11047   · cmul 11049   < clt 11184   ≤ cle 11185   − cmin 11381   / cdiv 11811  ℕcn 12162  ℕ0cn0 12418  ℤcz 12505  ...cfz 13444  ♯chash 14271  Σcsu 15628   ∥ cdvds 16198   gcd cgcd 16440  ϕcphi 16710  Basecbs 17155  0gc0g 17378  Grpcgrp 18841  .gcmg 18975  odcod 19430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-inf2 9570  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-disj 5070  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-oadd 8415  df-omul 8416  df-er 8648  df-ec 8650  df-qs 8654  df-map 8778  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-sup 9369  df-inf 9370  df-oi 9439  df-card 9868  df-acn 9871  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-n0 12419  df-xnn0 12492  df-z 12506  df-uz 12770  df-rp 12928  df-ico 13288  df-fz 13445  df-fzo 13592  df-fl 13730  df-mod 13808  df-seq 13943  df-exp 14003  df-hash 14272  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-clim 15430  df-sum 15629  df-dvds 16199  df-gcd 16441  df-phi 16712  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-0g 17380  df-mgm 18543  df-sgrp 18622  df-mnd 18638  df-grp 18844  df-minusg 18845  df-sbg 18846  df-mulg 18976  df-subg 19031  df-eqg 19033  df-od 19434
This theorem is referenced by:  unitscyglem5  42160
  Copyright terms: Public domain W3C validator