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 42179
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 2902 . . . . . 6 𝑦𝐵
2 nfcv 2902 . . . . . 6 𝑥𝐵
3 nfv 1911 . . . . . 6 𝑥((od‘𝐺)‘𝑦) = 𝐷
4 nfv 1911 . . . . . 6 𝑦((od‘𝐺)‘𝑥) = 𝐷
5 fveqeq2 6915 . . . . . 6 (𝑦 = 𝑥 → (((od‘𝐺)‘𝑦) = 𝐷 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
61, 2, 3, 4, 5cbvrabw 3470 . . . . 5 {𝑦𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷} = {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}
76fveq2i 6909 . . . 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 5150 . . . . . . . 8 (𝑚 = 𝐷 → (𝑚 ∥ (♯‘𝐵) ↔ 𝐷 ∥ (♯‘𝐵)))
15 eqeq2 2746 . . . . . . . . . 10 (𝑚 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
1615rabbidv 3440 . . . . . . . . 9 (𝑚 = 𝐷 → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
1716neeq1d 2997 . . . . . . . 8 (𝑚 = 𝐷 → ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))
1814, 17anbi12d 632 . . . . . . 7 (𝑚 = 𝐷 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)))
1916fveq2d 6910 . . . . . . . 8 (𝑚 = 𝐷 → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
20 fveq2 6906 . . . . . . . 8 (𝑚 = 𝐷 → (ϕ‘𝑚) = (ϕ‘𝐷))
2119, 20eqeq12d 2750 . . . . . . 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 42178 . . . . . 6 (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)))
29 unitscyglem4.1 . . . . . 6 (𝜑𝐷 ∈ ℕ)
3022, 28, 29rspcdva 3622 . . . . 5 (𝜑 → ((𝐷 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)))
3130imp 406 . . . 4 ((𝜑 ∧ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))
3213, 31syl 17 . . 3 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))
338, 32eqtrd 2774 . 2 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
34 id 22 . . . . 5 ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
3534necon1bi 2966 . . . 4 (¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
3635adantl 481 . . 3 ((𝜑 ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
3725adantr 480 . . . . . . . . 9 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 𝐺 ∈ Grp)
3826adantr 480 . . . . . . . . 9 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 𝐵 ∈ Fin)
3923, 37, 38hashfingrpnn 19002 . . . . . . . . 9 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℕ)
4023, 24, 37, 38, 39grpods 42175 . . . . . . . 8 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥𝐵 ∣ ((♯‘𝐵) 𝑥) = (0g𝐺)}))
41 simpr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵))
4241eqcomd 2740 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (♯‘𝐵) = (𝑙 · ((od‘𝐺)‘𝑥)))
4342oveq1d 7445 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) 𝑥) = ((𝑙 · ((od‘𝐺)‘𝑥)) 𝑥))
4425adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐵) → 𝐺 ∈ Grp)
4544adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → 𝐺 ∈ Grp)
46 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℤ)
47 eqid 2734 . . . . . . . . . . . . . . . . . . . 20 (od‘𝐺) = (od‘𝐺)
48 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝐵) → 𝑥𝐵)
4923, 47, 48odcld 19584 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
5049adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
5150nn0zd 12636 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈ ℤ)
52 simplr 769 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → 𝑥𝐵)
5346, 51, 523jca 1127 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ∈ ℤ ∧ ((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥𝐵))
5423, 24mulgass 19141 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ (𝑙 ∈ ℤ ∧ ((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) 𝑥) = (𝑙 (((od‘𝐺)‘𝑥) 𝑥)))
5545, 53, 54syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) 𝑥) = (𝑙 (((od‘𝐺)‘𝑥) 𝑥)))
56 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (0g𝐺) = (0g𝐺)
5723, 47, 24, 56odid 19570 . . . . . . . . . . . . . . . . . 18 (𝑥𝐵 → (((od‘𝐺)‘𝑥) 𝑥) = (0g𝐺))
5852, 57syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → (((od‘𝐺)‘𝑥) 𝑥) = (0g𝐺))
5958oveq2d 7446 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 (((od‘𝐺)‘𝑥) 𝑥)) = (𝑙 (0g𝐺)))
6023, 24, 56mulgz 19132 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝑙 ∈ ℤ) → (𝑙 (0g𝐺)) = (0g𝐺))
6144, 60sylan 580 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 (0g𝐺)) = (0g𝐺))
6259, 61eqtrd 2774 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 (((od‘𝐺)‘𝑥) 𝑥)) = (0g𝐺))
6355, 62eqtrd 2774 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) 𝑥) = (0g𝐺))
6463adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) 𝑥) = (0g𝐺))
6543, 64eqtrd 2774 . . . . . . . . . . . 12 ((((𝜑𝑥𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) 𝑥) = (0g𝐺))
6626adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐵) → 𝐵 ∈ Fin)
6723, 47oddvds2 19598 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
6844, 66, 48, 67syl3anc 1370 . . . . . . . . . . . . 13 ((𝜑𝑥𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
6949nn0zd 12636 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐵) → ((od‘𝐺)‘𝑥) ∈ ℤ)
70 hashcl 14391 . . . . . . . . . . . . . . . 16 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
7166, 70syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐵) → (♯‘𝐵) ∈ ℕ0)
7271nn0zd 12636 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐵) → (♯‘𝐵) ∈ ℤ)
73 divides 16288 . . . . . . . . . . . . . 14 ((((od‘𝐺)‘𝑥) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → (((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)))
7469, 72, 73syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑥𝐵) → (((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)))
7568, 74mpbid 232 . . . . . . . . . . . 12 ((𝜑𝑥𝐵) → ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵))
7665, 75r19.29a 3159 . . . . . . . . . . 11 ((𝜑𝑥𝐵) → ((♯‘𝐵) 𝑥) = (0g𝐺))
7776rabeqcda 3444 . . . . . . . . . 10 (𝜑 → {𝑥𝐵 ∣ ((♯‘𝐵) 𝑥) = (0g𝐺)} = 𝐵)
7877adantr 480 . . . . . . . . 9 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥𝐵 ∣ ((♯‘𝐵) 𝑥) = (0g𝐺)} = 𝐵)
7978fveq2d 6910 . . . . . . . 8 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥𝐵 ∣ ((♯‘𝐵) 𝑥) = (0g𝐺)}) = (♯‘𝐵))
8040, 79eqtr2d 2775 . . . . . . 7 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) = Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
81 nfv 1911 . . . . . . . . . . 11 𝑘(𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
82 nfcv 2902 . . . . . . . . . . 11 𝑘(♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)})
83 fzfid 14010 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (1...(♯‘𝐵)) ∈ Fin)
84 ssrab2 4089 . . . . . . . . . . . . 13 {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵))
8584a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
8683, 85ssfid 9298 . . . . . . . . . . 11 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin)
8738adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin)
88 ssrab2 4089 . . . . . . . . . . . . . . 15 {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵
8988a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
9087, 89ssfid 9298 . . . . . . . . . . . . 13 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
91 hashcl 14391 . . . . . . . . . . . . 13 ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
9290, 91syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
9392nn0cnd 12586 . . . . . . . . . . 11 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ)
94 breq1 5150 . . . . . . . . . . . 12 (𝑎 = (♯‘𝐵) → (𝑎 ∥ (♯‘𝐵) ↔ (♯‘𝐵) ∥ (♯‘𝐵)))
95 1zzd 12645 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ∈ ℤ)
9639nnzd 12637 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℤ)
9739nnge1d 12311 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ≤ (♯‘𝐵))
9839nnred 12278 . . . . . . . . . . . . . 14 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℝ)
9998leidd 11826 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ≤ (♯‘𝐵))
10095, 96, 96, 97, 99elfzd 13551 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ (1...(♯‘𝐵)))
101 iddvds 16303 . . . . . . . . . . . . 13 ((♯‘𝐵) ∈ ℤ → (♯‘𝐵) ∥ (♯‘𝐵))
10296, 101syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∥ (♯‘𝐵))
10394, 100, 102elrabd 3696 . . . . . . . . . . 11 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
104 eqeq2 2746 . . . . . . . . . . . . 13 (𝑘 = (♯‘𝐵) → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = (♯‘𝐵)))
105104rabbidv 3440 . . . . . . . . . . . 12 (𝑘 = (♯‘𝐵) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)})
106105fveq2d 6910 . . . . . . . . . . 11 (𝑘 = (♯‘𝐵) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}))
10781, 82, 86, 93, 103, 106fsumsplit1 15777 . . . . . . . . . 10 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = ((♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})))
108 ssrab2 4089 . . . . . . . . . . . . . . . 16 {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵
109108a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵)
11038, 109ssfid 9298 . . . . . . . . . . . . . 14 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin)
111 hashcl 14391 . . . . . . . . . . . . . 14 ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℕ0)
112110, 111syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℕ0)
113112nn0red 12585 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℝ)
114 diffi 9213 . . . . . . . . . . . . . . 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 9298 . . . . . . . . . . . . . . 15 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
119118, 91syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
120115, 119fsumnn0cl 15768 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
121120nn0red 12585 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
12239phicld 16805 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (ϕ‘(♯‘𝐵)) ∈ ℕ)
123122nnred 12278 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (ϕ‘(♯‘𝐵)) ∈ ℝ)
124 eldifi 4140 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
125 breq1 5150 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑘 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
126125elrab 3694 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
127126biimpi 216 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
128 elfzelz 13560 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(♯‘𝐵)) → 𝑘 ∈ ℤ)
129 elfzle1 13563 . . . . . . . . . . . . . . . . . . . . 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 12640 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
136134, 135sylibr 234 . . . . . . . . . . . . . . 15 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝑘 ∈ ℕ)
137 phicl 16802 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (ϕ‘𝑘) ∈ ℕ)
138136, 137syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℕ)
139138nnred 12278 . . . . . . . . . . . . 13 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℝ)
140115, 139fsumrecl 15766 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘) ∈ ℝ)
141 simplll 775 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝜑)
142 simplr 769 . . . . . . . . . . . . . . . . . . . . . 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 6915 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (((♯‘𝐵) / 𝐷) 𝑧) → (((od‘𝐺)‘𝑥) = 𝐷 ↔ ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧)) = 𝐷))
14725ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐺 ∈ Grp)
1489ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∥ (♯‘𝐵))
14929ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℕ)
150149nnzd 12637 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℤ)
151149nnne0d 12313 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ≠ 0)
15226ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐵 ∈ Fin)
153152, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
154153nn0zd 12636 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
155 dvdsval2 16289 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ∧ (♯‘𝐵) ∈ ℤ) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℤ))
156150, 151, 154, 155syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℤ))
157148, 156mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℤ)
158 simplr 769 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝑧𝐵)
15923, 24, 147, 157, 158mulgcld 19126 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) 𝑧) ∈ 𝐵)
160153nn0cnd 12586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ)
16129nncnd 12279 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐷 ∈ ℂ)
162161ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℂ)
16323, 147, 152hashfingrpnn 19002 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ)
164163nnne0d 12313 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ≠ 0)
165160, 160, 162, 164, 151divdiv2d 12072 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = (((♯‘𝐵) · 𝐷) / (♯‘𝐵)))
166162, 160, 164divcan3d 12045 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) · 𝐷) / (♯‘𝐵)) = 𝐷)
167165, 166eqtr2d 2775 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)))
168 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = (♯‘𝐵))
169168oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)))
17026, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (♯‘𝐵) ∈ ℕ0)
171170nn0cnd 12586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (♯‘𝐵) ∈ ℂ)
17229nnne0d 12313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐷 ≠ 0)
173171, 161, 172divcan2d 12042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝐷 · ((♯‘𝐵) / 𝐷)) = (♯‘𝐵))
174173eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
175174adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧𝐵) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
176175adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
177176oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷))))
178 nndivdvds 16295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐵) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℕ))
179163, 149, 178syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℕ))
180148, 179mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℕ)
181180nnnn0d 12584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℕ0)
182181, 150gcdmultipled 16567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷))) = ((♯‘𝐵) / 𝐷))
183177, 182eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = ((♯‘𝐵) / 𝐷))
184169, 183eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = ((♯‘𝐵) / 𝐷))
185184eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) = (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)))
186185oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))))
187167, 186eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))))
188168eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((od‘𝐺)‘𝑧))
18923, 47, 24odmulg 19588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐺 ∈ Grp ∧ 𝑧𝐵 ∧ ((♯‘𝐵) / 𝐷) ∈ ℤ) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧))))
190147, 158, 157, 189syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧))))
191188, 190eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧))))
192191eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧))) = (♯‘𝐵))
193157zcnd 12720 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℂ)
194184, 193eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℂ)
19523, 47, 159odcld 19584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧)) ∈ ℕ0)
196195nn0cnd 12586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧)) ∈ ℂ)
197168, 154eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ∈ ℤ)
198168, 164eqnetrd 3005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ≠ 0)
199157, 197, 1983jca 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ≠ 0))
200 gcd2n0cl 16542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((♯‘𝐵) / 𝐷) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ≠ 0) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ)
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ)
202201nnne0d 12313 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ≠ 0)
203160, 194, 196, 202divmuld 12062 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧)) ↔ ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧))) = (♯‘𝐵)))
204192, 203mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧)))
205187, 204eqtr2d 2775 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) 𝑧)) = 𝐷)
206146, 159, 205elrabd 3696 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) 𝑧) ∈ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
207 ne0i 4346 . . . . . . . . . . . . . . . . . . . . 21 ((((♯‘𝐵) / 𝐷) 𝑧) ∈ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
209145, 208syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
210 rabn0 4394 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑥𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵))
211 nfv 1911 . . . . . . . . . . . . . . . . . . . . . . 23 𝑧((od‘𝐺)‘𝑥) = (♯‘𝐵)
212 nfv 1911 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥((od‘𝐺)‘𝑧) = (♯‘𝐵)
213 fveqeq2 6915 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑧 → (((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ((od‘𝐺)‘𝑧) = (♯‘𝐵)))
214211, 212, 213cbvrexw 3304 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ∃𝑧𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
215210, 214bitri 275 . . . . . . . . . . . . . . . . . . . . 21 ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑧𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
216215biimpi 216 . . . . . . . . . . . . . . . . . . . 20 ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ → ∃𝑧𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
217216adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → ∃𝑧𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
218209, 217r19.29a 3159 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
219218ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))
220219necon4d 2961 . . . . . . . . . . . . . . . 16 (𝜑 → ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅))
221220imp 406 . . . . . . . . . . . . . . 15 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅)
222221fveq2d 6910 . . . . . . . . . . . . . 14 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) = (♯‘∅))
223 hash0 14402 . . . . . . . . . . . . . . 15 (♯‘∅) = 0
224223a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘∅) = 0)
225222, 224eqtrd 2774 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) = 0)
226122nngt0d 12312 . . . . . . . . . . . . 13 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 0 < (ϕ‘(♯‘𝐵)))
227225, 226eqbrtrd 5169 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) < (ϕ‘(♯‘𝐵)))
228 eldif 3972 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ↔ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
229228biimpi 216 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
230229adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
231 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑧 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑧 ∥ (♯‘𝐵)))
232231elrab 3694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
233232biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
234233adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
235 velsn 4646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ {(♯‘𝐵)} ↔ 𝑧 = (♯‘𝐵))
236235bicomi 224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (♯‘𝐵) ↔ 𝑧 ∈ {(♯‘𝐵)})
237236biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = (♯‘𝐵) → 𝑧 ∈ {(♯‘𝐵)})
238237necon3bi 2964 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑧 ∈ {(♯‘𝐵)} → 𝑧 ≠ (♯‘𝐵))
239238adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵))
240234, 239jca 511 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)))
241240adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)))
242 1zzd 12645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 1 ∈ ℤ)
24326adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝐵 ∈ Fin)
244243, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℕ0)
245244nn0zd 12636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℤ)
246245, 242zsubcld 12724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → ((♯‘𝐵) − 1) ∈ ℤ)
247 elfzelz 13560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (1...(♯‘𝐵)) → 𝑧 ∈ ℤ)
248247adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ∈ ℤ)
249248adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ ℤ)
250249adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℤ)
251 elfzle1 13563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (1...(♯‘𝐵)) → 1 ≤ 𝑧)
252251adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 1 ≤ 𝑧)
253252adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 1 ≤ 𝑧)
254253adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 1 ≤ 𝑧)
255 elfzle2 13564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 ∈ (1...(♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵))
256255adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵))
257256adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵))
258257adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≤ (♯‘𝐵))
259 simprr 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≠ (♯‘𝐵))
260259necomd 2993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ≠ 𝑧)
261258, 260jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧))
262250zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℝ)
263244nn0red 12585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℝ)
264262, 263ltlend 11403 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧)))
265261, 264mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 < (♯‘𝐵))
266250, 245zltlem1d 12668 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1)))
267265, 266mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≤ ((♯‘𝐵) − 1))
268242, 246, 250, 254, 267elfzd 13551 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ (1...((♯‘𝐵) − 1)))
269 simprlr 780 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∥ (♯‘𝐵))
270231, 268, 269elrabd 3696 . . . . . . . . . . . . . . . . . . . . . . . 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 4000 . . . . . . . . . . . . . . . 16 (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ⊆ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
279 1zzd 12645 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈ ℤ)
280170nn0zd 12636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (♯‘𝐵) ∈ ℤ)
281280adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → (♯‘𝐵) ∈ ℤ)
282 elfzelz 13560 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ∈ ℤ)
283282adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ ℤ)
284 elfzle1 13563 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 1 ≤ 𝑧)
285284adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ≤ 𝑧)
286283zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ ℝ)
287281zred 12719 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → (♯‘𝐵) ∈ ℝ)
288 1red 11259 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈ ℝ)
289287, 288resubcld 11688 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → ((♯‘𝐵) − 1) ∈ ℝ)
290 elfzle2 13564 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ≤ ((♯‘𝐵) − 1))
291290adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ ((♯‘𝐵) − 1))
292287lem1d 12198 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → ((♯‘𝐵) − 1) ≤ (♯‘𝐵))
293286, 289, 287, 291, 292letrd 11415 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ (♯‘𝐵))
294279, 281, 283, 285, 293elfzd 13551 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ (1...(♯‘𝐵)))
295294ex 412 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ∈ (1...(♯‘𝐵))))
296295ssrdv 4000 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...((♯‘𝐵) − 1)) ⊆ (1...(♯‘𝐵)))
297 rabss2 4087 . . . . . . . . . . . . . . . . . . . . . 22 ((1...((♯‘𝐵) − 1)) ⊆ (1...(♯‘𝐵)) → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
298296, 297syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
299298sseld 3993 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}))
300299imp 406 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
301170ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
302301nn0red 12585 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈ ℝ)
303302leidd 11826 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ≤ (♯‘𝐵))
304 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 = (♯‘𝐵))
305304eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) = 𝑧)
306231elrab 3694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12668 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1)))
316312, 315mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 < (♯‘𝐵))
317316adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 < (♯‘𝐵))
318305, 317eqbrtrd 5169 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) < (♯‘𝐵))
319302, 302ltnled 11405 . . . . . . . . . . . . . . . . . . . . . 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 3026 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵))
324300, 323eldifsnd 4791 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}))
325324ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})))
326325ssrdv 4000 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}))
327278, 326eqssd 4012 . . . . . . . . . . . . . . 15 (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) = {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
328327sumeq1d 15732 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
329 fzfid 14010 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...((♯‘𝐵) − 1)) ∈ Fin)
330 ssrab2 4089 . . . . . . . . . . . . . . . . . 18 {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...((♯‘𝐵) − 1))
331330a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...((♯‘𝐵) − 1)))
332329, 331ssfid 9298 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin)
33326adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin)
33488a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
335333, 334ssfid 9298 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
336335, 91syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
337336nn0red 12585 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
338125elrab 3694 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
339338biimpi 216 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
340339adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
341 elfzelz 13560 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (1...((♯‘𝐵) − 1)) → 𝑘 ∈ ℤ)
342 elfzle1 13563 . . . . . . . . . . . . . . . . . . . . . . . . 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 16805 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℕ)
351350nnred 12278 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℝ)
352 simpll 767 . . . . . . . . . . . . . . . . . . . . . . 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 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑘 → (𝑚 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
365 eqeq2 2746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑚 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝑘))
366365rabbidv 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 = 𝑘 → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
367366neeq1d 2997 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑘 → ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
368364, 367anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑘 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)))
369366fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑘 → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
370 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑘 → (ϕ‘𝑚) = (ϕ‘𝑘))
371369, 370eqeq12d 2750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑘 → ((♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚) ↔ (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
372368, 371imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑘 → (((𝑚 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)) ↔ ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))))
37328adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ∀𝑚 ∈ ℕ ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)))
374372, 373, 349rspcdva 3622 . . . . . . . . . . . . . . . . . . . . . . . 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 11361 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
379 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
380379necon1bi 2966 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅)
381380adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅)
382381fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘∅))
383223a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘∅) = 0)
384382, 383eqtrd 2774 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = 0)
385346adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∈ ℕ)
386385phicld 16805 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈ ℕ)
387386nnnn0d 12584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈ ℕ0)
388387nn0ge0d 12587 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 0 ≤ (ϕ‘𝑘))
389384, 388eqbrtrd 5169 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
390378, 389pm2.61dan 813 . . . . . . . . . . . . . . . . . . 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 15831 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
395327sumeq1d 15732 . . . . . . . . . . . . . . . 16 (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
396395eqcomd 2740 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
397394, 396breqtrd 5173 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
398328, 397eqbrtrd 5169 . . . . . . . . . . . . 13 (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
399398adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
400113, 121, 123, 140, 227, 399ltleaddd 11881 . . . . . . . . . . 11 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)))
401 nfcv 2902 . . . . . . . . . . . 12 𝑘(ϕ‘(♯‘𝐵))
402 simpll 767 . . . . . . . . . . . . . . . 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 16805 . . . . . . . . . . . . 13 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℕ)
411410nncnd 12279 . . . . . . . . . . . 12 (((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℂ)
412 fveq2 6906 . . . . . . . . . . . 12 (𝑘 = (♯‘𝐵) → (ϕ‘𝑘) = (ϕ‘(♯‘𝐵)))
41381, 401, 86, 411, 103, 412fsumsplit1 15777 . . . . . . . . . . 11 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)))
414400, 413breqtrrd 5175 . . . . . . . . . 10 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
415107, 414eqbrtrd 5169 . . . . . . . . 9 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
416 elfzelz 13560 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (1...(♯‘𝐵)) → 𝑎 ∈ ℤ)
417 elfzle1 13563 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (1...(♯‘𝐵)) → 1 ≤ 𝑎)
418416, 417jca 511 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (1...(♯‘𝐵)) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
419418adantr 480 . . . . . . . . . . . . . . 15 ((𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵)) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
420419adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵))) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
421 elnnz1 12640 . . . . . . . . . . . . . 14 (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
422420, 421sylibr 234 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ ℕ)
423422rabss3d 4090 . . . . . . . . . . . 12 (𝜑 → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
424 simpl 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝜑)
425 simprl 771 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ ℕ)
426424, 425jca 511 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → (𝜑𝑎 ∈ ℕ))
427 simprr 773 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∥ (♯‘𝐵))
428426, 427jca 511 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → ((𝜑𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)))
429 1zzd 12645 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ∈ ℤ)
430280adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑎 ∈ ℕ) → (♯‘𝐵) ∈ ℤ)
431430adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
432425anassrs 467 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℕ)
433432nnzd 12637 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℤ)
434432nnge1d 12311 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ≤ 𝑎)
435 nnz 12631 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
436435adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎 ∈ ℕ) → 𝑎 ∈ ℤ)
43723, 25, 26hashfingrpnn 19002 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘𝐵) ∈ ℕ)
438437adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎 ∈ ℕ) → (♯‘𝐵) ∈ ℕ)
439 dvdsle 16343 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑎 ∥ (♯‘𝐵) → 𝑎 ≤ (♯‘𝐵)))
440436, 438, 439syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑎 ∈ ℕ) → (𝑎 ∥ (♯‘𝐵) → 𝑎 ≤ (♯‘𝐵)))
441440imp 406 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ≤ (♯‘𝐵))
442429, 431, 433, 434, 441elfzd 13551 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ (1...(♯‘𝐵)))
443428, 442syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ (1...(♯‘𝐵)))
444443rabss3d 4090 . . . . . . . . . . . 12 (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
445423, 444eqssd 4012 . . . . . . . . . . 11 (𝜑 → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
446445adantr 480 . . . . . . . . . 10 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
447446sumeq1d 15732 . . . . . . . . 9 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
448415, 447breqtrd 5173 . . . . . . . 8 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
449 phisum 16823 . . . . . . . . 9 ((♯‘𝐵) ∈ ℕ → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵))
45039, 449syl 17 . . . . . . . 8 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵))
451448, 450breqtrd 5173 . . . . . . 7 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < (♯‘𝐵))
45280, 451eqbrtrd 5169 . . . . . 6 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) < (♯‘𝐵))
453170adantr 480 . . . . . . . 8 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℕ0)
454453nn0red 12585 . . . . . . 7 ((𝜑 ∧ {𝑥𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℝ)
455454ltnrd 11392 . . . . . 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 813 1 (𝜑 → (♯‘{𝑦𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  cdif 3959  wss 3962  c0 4338  {csn 4630   class class class wbr 5147  cfv 6562  (class class class)co 7430  Fincfn 8983  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cle 11293  cmin 11489   / cdiv 11917  cn 12263  0cn0 12523  cz 12610  ...cfz 13543  chash 14365  Σcsu 15718  cdvds 16286   gcd cgcd 16527  ϕcphi 16797  Basecbs 17244  0gc0g 17485  Grpcgrp 18963  .gcmg 19097  odcod 19556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-omul 8509  df-er 8743  df-ec 8745  df-qs 8749  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-acn 9979  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-rp 13032  df-ico 13389  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-dvds 16287  df-gcd 16528  df-phi 16799  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-grp 18966  df-minusg 18967  df-sbg 18968  df-mulg 19098  df-subg 19153  df-eqg 19155  df-od 19560
This theorem is referenced by:  unitscyglem5  42180
  Copyright terms: Public domain W3C validator