| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | breq1 5146 | . . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑘 → (𝑎 ∥ 𝐷 ↔ 𝑘 ∥ 𝐷)) | 
| 2 | 1 | elrab 3692 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ↔ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) | 
| 3 | 2 | biimpi 216 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) | 
| 4 | 3 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) | 
| 5 | 4 | simpld 494 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ (1...(𝐷 − 1))) | 
| 6 | 5 | elfzelzd 13565 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℤ) | 
| 7 |  | unitscyglem2.1 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℕ) | 
| 8 | 7 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ) | 
| 9 | 8 | nnzd 12640 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ) | 
| 10 |  | unitscyglem1.4 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ Fin) | 
| 11 |  | hashcl 14395 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) | 
| 12 | 10, 11 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) | 
| 13 | 12 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘𝐵) ∈
ℕ0) | 
| 14 | 13 | nn0zd 12639 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘𝐵) ∈ ℤ) | 
| 15 | 4 | simprd 495 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∥ 𝐷) | 
| 16 |  | unitscyglem2.2 | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵)) | 
| 17 | 16 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∥ (♯‘𝐵)) | 
| 18 | 6, 9, 14, 15, 17 | dvdstrd 16332 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∥ (♯‘𝐵)) | 
| 19 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → 𝜑) | 
| 20 | 2, 5 | sylan2br 595 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → 𝑘 ∈ (1...(𝐷 − 1))) | 
| 21 | 19, 20 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → (𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1)))) | 
| 22 | 2, 15 | sylan2br 595 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → 𝑘 ∥ 𝐷) | 
| 23 | 21, 22 | jca 511 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷)) | 
| 24 |  | fveqeq2 6915 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = ((𝐷 / 𝑘) ↑ 𝐴) → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘)) | 
| 25 |  | unitscyglem1.1 | . . . . . . . . . . . . . . . 16
⊢ 𝐵 = (Base‘𝐺) | 
| 26 |  | unitscyglem1.2 | . . . . . . . . . . . . . . . 16
⊢  ↑ =
(.g‘𝐺) | 
| 27 |  | unitscyglem1.3 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 28 | 27 | ad4antr 732 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐺 ∈ Grp) | 
| 29 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝑙 · 𝑘) = 𝐷) | 
| 30 | 29 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑙 · 𝑘)) | 
| 31 | 30 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = ((𝑙 · 𝑘) / 𝑘)) | 
| 32 |  | simplr 769 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℕ) | 
| 33 | 32 | nncnd 12282 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℂ) | 
| 34 |  | elfzelz 13564 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ∈ ℤ) | 
| 35 | 34 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 𝑘 ∈ ℤ) | 
| 36 | 35 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℤ) | 
| 37 | 36 | zcnd 12723 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℂ) | 
| 38 |  | elfzle1 13567 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑘) | 
| 39 | 38 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 1 ≤ 𝑘) | 
| 40 | 35, 39 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘)) | 
| 41 |  | elnnz1 12643 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤
𝑘)) | 
| 42 | 40, 41 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 𝑘 ∈ ℕ) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → 𝑘 ∈ ℕ) | 
| 44 | 43 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℕ) | 
| 45 | 44 | nnne0d 12316 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ≠ 0) | 
| 46 | 33, 37, 45 | divcan4d 12049 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝑙 · 𝑘) / 𝑘) = 𝑙) | 
| 47 | 31, 46 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = 𝑙) | 
| 48 | 47, 32 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℕ) | 
| 49 | 48 | nnnn0d 12587 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈
ℕ0) | 
| 50 | 49 | nn0zd 12639 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℤ) | 
| 51 |  | unitscyglem2.3 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ 𝐵) | 
| 52 | 51 | ad4antr 732 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐴 ∈ 𝐵) | 
| 53 | 25, 26, 28, 50, 52 | mulgcld 19114 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ 𝐵) | 
| 54 | 7 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → 𝐷 ∈ ℕ) | 
| 55 | 54 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℕ) | 
| 56 | 55 | nncnd 12282 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℂ) | 
| 57 | 56, 37, 45 | divcan1d 12044 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · 𝑘) = 𝐷) | 
| 58 |  | unitscyglem2.4 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((od‘𝐺)‘𝐴) = 𝐷) | 
| 59 | 58 | ad4antr 732 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = 𝐷) | 
| 60 | 59 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((od‘𝐺)‘𝐴)) | 
| 61 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(od‘𝐺) =
(od‘𝐺) | 
| 62 | 25, 61, 26 | odmulg 19574 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ (𝐷 / 𝑘) ∈ ℤ) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)))) | 
| 63 | 28, 52, 50, 62 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)))) | 
| 64 | 60, 63 | eqtrd 2777 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)))) | 
| 65 | 59 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = ((𝐷 / 𝑘) gcd 𝐷)) | 
| 66 | 56, 37, 45 | divcan2d 12045 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝑘 · (𝐷 / 𝑘)) = 𝐷) | 
| 67 | 66 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑘 · (𝐷 / 𝑘))) | 
| 68 | 67 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘)))) | 
| 69 | 49, 36 | gcdmultipled 16571 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘))) = (𝐷 / 𝑘)) | 
| 70 | 68, 69 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = (𝐷 / 𝑘)) | 
| 71 | 65, 70 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = (𝐷 / 𝑘)) | 
| 72 | 71 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)))) | 
| 73 | 64, 72 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)))) | 
| 74 | 57, 73 | eqtr2d 2778 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘)) | 
| 75 | 25, 61, 53 | odcld 19570 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈
ℕ0) | 
| 76 | 75 | nn0cnd 12589 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈ ℂ) | 
| 77 | 50 | zcnd 12723 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℂ) | 
| 78 | 55 | nnne0d 12316 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ≠ 0) | 
| 79 | 56, 37, 78, 45 | divne0d 12059 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ≠ 0) | 
| 80 | 76, 37, 77, 79 | mulcand 11896 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘) ↔ ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘)) | 
| 81 | 74, 80 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘) | 
| 82 | 24, 53, 81 | elrabd 3694 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) | 
| 83 | 82 | ne0d 4342 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) | 
| 84 |  | nndivides 16300 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑘 ∥ 𝐷 ↔ ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷)) | 
| 85 | 43, 54, 84 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → (𝑘 ∥ 𝐷 ↔ ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷)) | 
| 86 | 85 | biimpd 229 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → (𝑘 ∥ 𝐷 → ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷)) | 
| 87 | 86 | syldbl2 842 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷) | 
| 88 | 83, 87 | r19.29a 3162 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) | 
| 89 | 23, 88 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) | 
| 90 | 89 | ex 412 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)) | 
| 91 | 90 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ((𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)) | 
| 92 | 4, 91 | mpd 15 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) | 
| 93 | 18, 92 | jca 511 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)) | 
| 94 | 5, 38 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 1 ≤ 𝑘) | 
| 95 | 6, 94 | jca 511 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘)) | 
| 96 | 95, 41 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℕ) | 
| 97 | 96 | nnred 12281 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℝ) | 
| 98 | 8 | nnred 12281 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℝ) | 
| 99 |  | 1red 11262 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℝ) | 
| 100 | 98, 99 | resubcld 11691 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) ∈ ℝ) | 
| 101 |  | elfzle2 13568 | . . . . . . . . . 10
⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ≤ (𝐷 − 1)) | 
| 102 | 5, 101 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ≤ (𝐷 − 1)) | 
| 103 | 98 | ltm1d 12200 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) < 𝐷) | 
| 104 | 97, 100, 98, 102, 103 | lelttrd 11419 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 < 𝐷) | 
| 105 |  | breq1 5146 | . . . . . . . . . 10
⊢ (𝑐 = 𝑘 → (𝑐 < 𝐷 ↔ 𝑘 < 𝐷)) | 
| 106 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝑘 → (𝑐 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵))) | 
| 107 |  | eqeq2 2749 | . . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑘)) | 
| 108 | 107 | rabbidv 3444 | . . . . . . . . . . . . 13
⊢ (𝑐 = 𝑘 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) | 
| 109 | 108 | neeq1d 3000 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝑘 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)) | 
| 110 | 106, 109 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑐 = 𝑘 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))) | 
| 111 | 108 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝑘 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) | 
| 112 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝑘 → (ϕ‘𝑐) = (ϕ‘𝑘)) | 
| 113 | 111, 112 | eqeq12d 2753 | . . . . . . . . . . 11
⊢ (𝑐 = 𝑘 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))) | 
| 114 | 110, 113 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑐 = 𝑘 → (((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)) ↔ ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))) | 
| 115 | 105, 114 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑐 = 𝑘 → ((𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) ↔ (𝑘 < 𝐷 → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))))) | 
| 116 |  | unitscyglem2.5 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) | 
| 117 | 116 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)))) | 
| 118 | 115, 117,
96 | rspcdva 3623 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 < 𝐷 → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))) | 
| 119 | 104, 118 | mpd 15 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))) | 
| 120 | 93, 119 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)) | 
| 121 | 120 | sumeq2dv 15738 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘)) | 
| 122 | 121 | eqcomd 2743 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) | 
| 123 | 122 | oveq1d 7446 | . . 3
⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))) | 
| 124 |  | elun 4153 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) ↔ (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷})) | 
| 125 | 124 | biimpi 216 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷})) | 
| 126 | 125 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷})) | 
| 127 |  | 1zzd 12648 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℤ) | 
| 128 | 7 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℕ) | 
| 129 | 128 | nnzd 12640 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℤ) | 
| 130 |  | elfzelz 13564 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ∈ ℤ) | 
| 131 | 130 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ∈ ℤ) | 
| 132 | 131 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℤ) | 
| 133 |  | elfzle1 13567 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑎) | 
| 134 | 133 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 1 ≤ 𝑎) | 
| 135 | 134 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ≤ 𝑎) | 
| 136 | 132 | zred 12722 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℝ) | 
| 137 | 128 | nnred 12281 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℝ) | 
| 138 |  | 1red 11262 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℝ) | 
| 139 | 137, 138 | resubcld 11691 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) ∈ ℝ) | 
| 140 |  | elfzle2 13568 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ≤ (𝐷 − 1)) | 
| 141 | 140 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ≤ (𝐷 − 1)) | 
| 142 | 141 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ (𝐷 − 1)) | 
| 143 | 137 | ltm1d 12200 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) < 𝐷) | 
| 144 | 136, 139,
137, 142, 143 | lelttrd 11419 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 < 𝐷) | 
| 145 | 136, 137,
144 | ltled 11409 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ 𝐷) | 
| 146 | 127, 129,
132, 135, 145 | elfzd 13555 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ (1...𝐷)) | 
| 147 | 146 | rabss3d 4081 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 148 | 147 | sseld 3982 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})) | 
| 149 | 148 | imp 406 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 150 |  | elsni 4643 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {𝐷} → 𝑦 = 𝐷) | 
| 151 | 150 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → 𝑦 = 𝐷) | 
| 152 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝑦 = 𝐷) | 
| 153 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝐷 → (𝑎 ∥ 𝐷 ↔ 𝐷 ∥ 𝐷)) | 
| 154 |  | 1zzd 12648 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ∈
ℤ) | 
| 155 | 7 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐷 ∈ ℤ) | 
| 156 | 7 | nnge1d 12314 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ 𝐷) | 
| 157 | 7 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 158 | 157 | leidd 11829 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐷 ≤ 𝐷) | 
| 159 | 154, 155,
155, 156, 158 | elfzd 13555 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐷 ∈ (1...𝐷)) | 
| 160 |  | iddvds 16307 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ ℤ → 𝐷 ∥ 𝐷) | 
| 161 | 155, 160 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐷 ∥ 𝐷) | 
| 162 | 153, 159,
161 | elrabd 3694 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 163 | 162 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 164 | 152, 163 | eqeltrd 2841 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 165 | 164 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑦 = 𝐷 → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})) | 
| 166 | 165 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → (𝑦 = 𝐷 → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})) | 
| 167 | 151, 166 | mpd 15 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 168 | 149, 167 | jaodan 960 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷})) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 169 | 168 | ex 412 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})) | 
| 170 | 169 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) → ((𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})) | 
| 171 | 126, 170 | mpd 15 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 172 | 171 | ex 412 | . . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})) | 
| 173 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝑦 = 𝐷) | 
| 174 |  | eqidd 2738 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 = 𝐷) | 
| 175 | 7 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ ℕ) | 
| 176 |  | elsng 4640 | . . . . . . . . . . . . . . . 16
⊢ (𝐷 ∈ ℕ → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷)) | 
| 177 | 175, 176 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷)) | 
| 178 | 174, 177 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝐷}) | 
| 179 | 173, 178 | eqeltrd 2841 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝑦 ∈ {𝐷}) | 
| 180 | 179 | olcd 875 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷})) | 
| 181 |  | breq1 5146 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑦 → (𝑎 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷)) | 
| 182 | 181 | elrab 3692 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} ↔ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) | 
| 183 | 182 | biimpi 216 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) | 
| 184 | 183 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) | 
| 185 | 184 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) | 
| 186 |  | 1zzd 12648 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ∈ ℤ) | 
| 187 | 155 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ) | 
| 188 | 187, 186 | zsubcld 12727 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝐷 − 1) ∈ ℤ) | 
| 189 |  | elfzelz 13564 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ∈ ℤ) | 
| 190 | 189 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ∈ ℤ) | 
| 191 | 190 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℤ) | 
| 192 |  | elfzle1 13567 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1...𝐷) → 1 ≤ 𝑦) | 
| 193 | 192 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 1 ≤ 𝑦) | 
| 194 | 193 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ≤ 𝑦) | 
| 195 |  | elfzle2 13568 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ≤ 𝐷) | 
| 196 | 195 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ≤ 𝐷) | 
| 197 | 196 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ 𝐷) | 
| 198 |  | neqne 2948 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑦 = 𝐷 → 𝑦 ≠ 𝐷) | 
| 199 | 198 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝑦 ≠ 𝐷) | 
| 200 | 199 | necomd 2996 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝐷 ≠ 𝑦) | 
| 201 | 200 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ≠ 𝑦) | 
| 202 | 197, 201 | jca 511 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦)) | 
| 203 | 191 | zred 12722 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℝ) | 
| 204 | 157 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℝ) | 
| 205 | 203, 204 | ltlend 11406 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦))) | 
| 206 | 202, 205 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 < 𝐷) | 
| 207 | 7 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℕ) | 
| 208 | 207 | nnzd 12640 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ) | 
| 209 | 191, 208 | zltlem1d 12671 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ 𝑦 ≤ (𝐷 − 1))) | 
| 210 | 206, 209 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ (𝐷 − 1)) | 
| 211 | 186, 188,
191, 194, 210 | elfzd 13555 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ (1...(𝐷 − 1))) | 
| 212 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∥ 𝐷) | 
| 213 | 181, 211,
212 | elrabd 3694 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) | 
| 214 | 213 | ex 412 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})) | 
| 215 | 185, 214 | mpd 15 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) | 
| 216 | 215 | orcd 874 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷})) | 
| 217 | 180, 216 | pm2.61dan 813 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷})) | 
| 218 | 217, 124 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) | 
| 219 | 218 | ex 412 | . . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}))) | 
| 220 | 172, 219 | impbid 212 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) ↔ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})) | 
| 221 | 220 | eqrdv 2735 | . . . . . . 7
⊢ (𝜑 → ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 222 | 221 | sumeq1d 15736 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘)) | 
| 223 |  | phisum 16828 | . . . . . . . . 9
⊢ (𝐷 ∈ ℕ →
Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷) | 
| 224 | 7, 223 | syl 17 | . . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷) | 
| 225 |  | eqcom 2744 | . . . . . . . . . . . . . . . . . 18
⊢
(((od‘𝐺)‘𝐴) = 𝐷 ↔ 𝐷 = ((od‘𝐺)‘𝐴)) | 
| 226 | 225 | imbi2i 336 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 → ((od‘𝐺)‘𝐴) = 𝐷) ↔ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴))) | 
| 227 | 58, 226 | mpbi 230 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴)) | 
| 228 | 227 | oveq1d 7446 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷 ↑ 𝑥) = (((od‘𝐺)‘𝐴) ↑ 𝑥)) | 
| 229 | 228 | eqeq1d 2739 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐷 ↑ 𝑥) = (0g‘𝐺) ↔ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺))) | 
| 230 | 229 | rabbidv 3444 | . . . . . . . . . . . . 13
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0g‘𝐺)} = {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) | 
| 231 | 230 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0g‘𝐺)}) = (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)})) | 
| 232 |  | unitscyglem1.5 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛) | 
| 233 | 25, 26, 27, 10, 232, 51 | unitscyglem1 42196 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0g‘𝐺)}) = ((od‘𝐺)‘𝐴)) | 
| 234 | 231, 233 | eqtrd 2777 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0g‘𝐺)}) = ((od‘𝐺)‘𝐴)) | 
| 235 | 234, 58 | eqtr2d 2778 | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0g‘𝐺)})) | 
| 236 | 25, 26, 27, 10, 7 | grpods 42195 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0g‘𝐺)})) | 
| 237 | 235, 236 | eqtr4d 2780 | . . . . . . . . 9
⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) | 
| 238 | 221 | eqcomd 2743 | . . . . . . . . . 10
⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} = ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) | 
| 239 | 238 | sumeq1d 15736 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) | 
| 240 | 237, 239 | eqtrd 2777 | . . . . . . . 8
⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) | 
| 241 | 224, 240 | eqtr2d 2778 | . . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘)) | 
| 242 |  | 1zzd 12648 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℤ) | 
| 243 | 155 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ) | 
| 244 | 181 | elrab 3692 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷)) | 
| 245 | 244 | biimpi 216 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} → (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷)) | 
| 246 | 245 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷)) | 
| 247 | 246 | simpld 494 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℕ) | 
| 248 | 247 | nnzd 12640 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℤ) | 
| 249 | 247 | nnge1d 12314 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ≤ 𝑦) | 
| 250 | 246 | simprd 495 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∥ 𝐷) | 
| 251 | 7 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ) | 
| 252 |  | dvdsle 16347 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷)) | 
| 253 | 248, 251,
252 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷)) | 
| 254 | 250, 253 | mpd 15 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ≤ 𝐷) | 
| 255 | 242, 243,
248, 249, 254 | elfzd 13555 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ (1...𝐷)) | 
| 256 | 181, 255,
250 | elrabd 3694 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 257 | 256 | ex 412 | . . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})) | 
| 258 |  | elfzelz 13564 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (1...𝐷) → 𝑎 ∈ ℤ) | 
| 259 |  | elfzle1 13567 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (1...𝐷) → 1 ≤ 𝑎) | 
| 260 | 258, 259 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (1...𝐷) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎)) | 
| 261 | 260 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎)) | 
| 262 | 261 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷)) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎)) | 
| 263 |  | elnnz1 12643 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤
𝑎)) | 
| 264 | 262, 263 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℕ) | 
| 265 | 264 | rabss3d 4081 | . . . . . . . . . . 11
⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) | 
| 266 | 265 | sseld 3982 | . . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷})) | 
| 267 | 257, 266 | impbid 212 | . . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})) | 
| 268 | 267 | eqrdv 2735 | . . . . . . . 8
⊢ (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) | 
| 269 | 268 | sumeq1d 15736 | . . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘)) | 
| 270 | 241, 269 | eqtr2d 2778 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) | 
| 271 | 222, 270 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) | 
| 272 |  | nfv 1914 | . . . . . 6
⊢
Ⅎ𝑘𝜑 | 
| 273 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑘(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) | 
| 274 |  | fzfid 14014 | . . . . . . 7
⊢ (𝜑 → (1...(𝐷 − 1)) ∈ Fin) | 
| 275 |  | ssrab2 4080 | . . . . . . . 8
⊢ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1)) | 
| 276 | 275 | a1i 11 | . . . . . . 7
⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1))) | 
| 277 | 274, 276 | ssfid 9301 | . . . . . 6
⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∈ Fin) | 
| 278 | 153 | elrab 3692 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ↔ (𝐷 ∈ (1...(𝐷 − 1)) ∧ 𝐷 ∥ 𝐷)) | 
| 279 | 278 | biimpi 216 | . . . . . . . . . . 11
⊢ (𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → (𝐷 ∈ (1...(𝐷 − 1)) ∧ 𝐷 ∥ 𝐷)) | 
| 280 | 279 | simpld 494 | . . . . . . . . . 10
⊢ (𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → 𝐷 ∈ (1...(𝐷 − 1))) | 
| 281 | 280 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ (1...(𝐷 − 1))) | 
| 282 |  | elfzle2 13568 | . . . . . . . . 9
⊢ (𝐷 ∈ (1...(𝐷 − 1)) → 𝐷 ≤ (𝐷 − 1)) | 
| 283 | 281, 282 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ≤ (𝐷 − 1)) | 
| 284 | 157 | ltm1d 12200 | . . . . . . . . . 10
⊢ (𝜑 → (𝐷 − 1) < 𝐷) | 
| 285 |  | 1red 11262 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) | 
| 286 | 157, 285 | resubcld 11691 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐷 − 1) ∈ ℝ) | 
| 287 | 286, 157 | ltnled 11408 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐷 − 1) < 𝐷 ↔ ¬ 𝐷 ≤ (𝐷 − 1))) | 
| 288 | 284, 287 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → ¬ 𝐷 ≤ (𝐷 − 1)) | 
| 289 | 288 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ¬ 𝐷 ≤ (𝐷 − 1)) | 
| 290 | 283, 289 | pm2.21dd 195 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) | 
| 291 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) | 
| 292 | 290, 291 | pm2.61dan 813 | . . . . . 6
⊢ (𝜑 → ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) | 
| 293 | 10 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐵 ∈ Fin) | 
| 294 |  | ssrab2 4080 | . . . . . . . . . 10
⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵 | 
| 295 | 294 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵) | 
| 296 | 293, 295 | ssfid 9301 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin) | 
| 297 |  | hashcl 14395 | . . . . . . . 8
⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈
ℕ0) | 
| 298 | 296, 297 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈
ℕ0) | 
| 299 | 298 | nn0cnd 12589 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ) | 
| 300 |  | eqeq2 2749 | . . . . . . . 8
⊢ (𝑘 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = 𝐷)) | 
| 301 | 300 | rabbidv 3444 | . . . . . . 7
⊢ (𝑘 = 𝐷 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) | 
| 302 | 301 | fveq2d 6910 | . . . . . 6
⊢ (𝑘 = 𝐷 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) | 
| 303 |  | ssrab2 4080 | . . . . . . . . . 10
⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵 | 
| 304 | 303 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵) | 
| 305 | 10, 304 | ssfid 9301 | . . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin) | 
| 306 |  | hashcl 14395 | . . . . . . . 8
⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈
ℕ0) | 
| 307 | 305, 306 | syl 17 | . . . . . . 7
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈
ℕ0) | 
| 308 | 307 | nn0cnd 12589 | . . . . . 6
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℂ) | 
| 309 | 272, 273,
277, 7, 292, 299, 302, 308 | fsumsplitsn 15780 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))) | 
| 310 | 271, 309 | eqtr2d 2778 | . . . 4
⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘)) | 
| 311 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑘(ϕ‘𝐷) | 
| 312 | 120, 299 | eqeltrrd 2842 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (ϕ‘𝑘) ∈ ℂ) | 
| 313 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 𝐷 → (ϕ‘𝑘) = (ϕ‘𝐷)) | 
| 314 | 7 | phicld 16809 | . . . . . 6
⊢ (𝜑 → (ϕ‘𝐷) ∈
ℕ) | 
| 315 | 314 | nncnd 12282 | . . . . 5
⊢ (𝜑 → (ϕ‘𝐷) ∈
ℂ) | 
| 316 | 272, 311,
277, 7, 292, 312, 313, 315 | fsumsplitsn 15780 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷))) | 
| 317 | 310, 316 | eqtrd 2777 | . . 3
⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷))) | 
| 318 | 123, 317 | eqtrd 2777 | . 2
⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷))) | 
| 319 | 277, 312 | fsumcl 15769 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) ∈ ℂ) | 
| 320 | 319, 308,
315 | addcand 11464 | . 2
⊢ (𝜑 → ((Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))) | 
| 321 | 318, 320 | mpbid 232 | 1
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)) |