unitscyglem2

	Ref	Expression
Hypotheses	unitscyglem1.1	$⊢ B = {Base}_{G}$
	unitscyglem1.2	$⊢ \underset{˙}{\times} = \cdot_{G}$
	unitscyglem1.3	$⊢ φ \to G \in Grp$
	unitscyglem1.4	$⊢ φ \to B \in Fin$
	unitscyglem1.5	$⊢ φ \to \forall n \in ℕ \|\{x \in B \| n \underset{˙}{\times} x = 0_{G}\}\| \leq n$
	unitscyglem2.1	$⊢ φ \to D \in ℕ$
	unitscyglem2.2	$⊢ φ \to D ∥ \|B\|$
	unitscyglem2.3	$⊢ φ \to A \in B$
	unitscyglem2.4	$⊢ φ \to od (G) (A) = D$
	unitscyglem2.5	$⊢ φ \to \forall c \in ℕ (c < D \to ((c ∥ \|B\| \land \{x \in B \| od (G) (x) = c\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = c\}\| = ϕ (c)))$
Assertion	unitscyglem2	$⊢ φ \to \|\{x \in B \| od (G) (x) = D\}\| = ϕ (D)$

Proof

Step	Hyp	Ref	Expression
1		unitscyglem1.1	$⊢ B = {Base}_{G}$
2		unitscyglem1.2	$⊢ \underset{˙}{\times} = \cdot_{G}$
3		unitscyglem1.3	$⊢ φ \to G \in Grp$
4		unitscyglem1.4	$⊢ φ \to B \in Fin$
5		unitscyglem1.5	$⊢ φ \to \forall n \in ℕ \|\{x \in B \| n \underset{˙}{\times} x = 0_{G}\}\| \leq n$
6		unitscyglem2.1	$⊢ φ \to D \in ℕ$
7		unitscyglem2.2	$⊢ φ \to D ∥ \|B\|$
8		unitscyglem2.3	$⊢ φ \to A \in B$
9		unitscyglem2.4	$⊢ φ \to od (G) (A) = D$
10		unitscyglem2.5	$⊢ φ \to \forall c \in ℕ (c < D \to ((c ∥ \|B\| \land \{x \in B \| od (G) (x) = c\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = c\}\| = ϕ (c)))$
11		breq1	$⊢ a = k \to (a ∥ D \leftrightarrow k ∥ D)$
12	11	elrab	$⊢ k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \leftrightarrow (k \in (1 \dots D - 1) \land k ∥ D)$
13	12	bilani	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to (k \in (1 \dots D - 1) \land k ∥ D)$
14	13	simpld	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to k \in (1 \dots D - 1)$
15	14	elfzelzd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to k \in ℤ$
16	6	adantr	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to D \in ℕ$
17	16	nnzd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to D \in ℤ$
18		hashcl	$⊢ B \in Fin \to \|B\| \in ℕ_{0}$
19	4 18	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
20	19	adantr	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \|B\| \in ℕ_{0}$
21	20	nn0zd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \|B\| \in ℤ$
22	13	simprd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to k ∥ D$
23	7	adantr	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to D ∥ \|B\|$
24	15 17 21 22 23	dvdstrd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to k ∥ \|B\|$
25		simpl	$⊢ (φ \land (k \in (1 \dots D - 1) \land k ∥ D)) \to φ$
26	12 14	sylan2br	$⊢ (φ \land (k \in (1 \dots D - 1) \land k ∥ D)) \to k \in (1 \dots D - 1)$
27	25 26	jca	$⊢ (φ \land (k \in (1 \dots D - 1) \land k ∥ D)) \to (φ \land k \in (1 \dots D - 1))$
28	12 22	sylan2br	$⊢ (φ \land (k \in (1 \dots D - 1) \land k ∥ D)) \to k ∥ D$
29	27 28	jca	$⊢ (φ \land (k \in (1 \dots D - 1) \land k ∥ D)) \to ((φ \land k \in (1 \dots D - 1)) \land k ∥ D)$
30		fveqeq2	$⊢ x = (\frac{D}{k}) \underset{˙}{\times} A \to (od (G) (x) = k \leftrightarrow od (G) ((\frac{D}{k}) \underset{˙}{\times} A) = k)$
31	3	ad4antr	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to G \in Grp$
32		simpr	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to l k = D$
33	32	eqcomd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to D = l k$
34	33	oveq1d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to \frac{D}{k} = \frac{l k}{k}$
35		simplr	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to l \in ℕ$
36	35	nncnd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to l \in ℂ$
37		elfzelz	$⊢ k \in (1 \dots D - 1) \to k \in ℤ$
38	37	adantl	$⊢ (φ \land k \in (1 \dots D - 1)) \to k \in ℤ$
39	38	ad3antrrr	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to k \in ℤ$
40	39	zcnd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to k \in ℂ$
41		elfzle1	$⊢ k \in (1 \dots D - 1) \to 1 \leq k$
42	41	adantl	$⊢ (φ \land k \in (1 \dots D - 1)) \to 1 \leq k$
43	38 42	jca	$⊢ (φ \land k \in (1 \dots D - 1)) \to (k \in ℤ \land 1 \leq k)$
44		elnnz1	$⊢ k \in ℕ \leftrightarrow (k \in ℤ \land 1 \leq k)$
45	43 44	sylibr	$⊢ (φ \land k \in (1 \dots D - 1)) \to k \in ℕ$
46	45	adantr	$⊢ ((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \to k \in ℕ$
47	46	ad2antrr	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to k \in ℕ$
48	47	nnne0d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to k \neq 0$
49	36 40 48	divcan4d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to \frac{l k}{k} = l$
50	34 49	eqtrd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to \frac{D}{k} = l$
51	50 35	eqeltrd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to \frac{D}{k} \in ℕ$
52	51	nnnn0d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to \frac{D}{k} \in ℕ_{0}$
53	52	nn0zd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to \frac{D}{k} \in ℤ$
54	8	ad4antr	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to A \in B$
55	1 2 31 53 54	mulgcld	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to (\frac{D}{k}) \underset{˙}{\times} A \in B$
56	6	ad2antrr	$⊢ ((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \to D \in ℕ$
57	56	ad2antrr	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to D \in ℕ$
58	57	nncnd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to D \in ℂ$
59	58 40 48	divcan1d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to (\frac{D}{k}) k = D$
60	9	ad4antr	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to od (G) (A) = D$
61	60	eqcomd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to D = od (G) (A)$
62		eqid	$⊢ od (G) = od (G)$
63	1 62 2	odmulg	$⊢ (G \in Grp \land A \in B \land \frac{D}{k} \in ℤ) \to od (G) (A) = ((\frac{D}{k}) \gcd od (G) (A)) od (G) ((\frac{D}{k}) \underset{˙}{\times} A)$
64	31 54 53 63	syl3anc	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to od (G) (A) = ((\frac{D}{k}) \gcd od (G) (A)) od (G) ((\frac{D}{k}) \underset{˙}{\times} A)$
65	61 64	eqtrd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to D = ((\frac{D}{k}) \gcd od (G) (A)) od (G) ((\frac{D}{k}) \underset{˙}{\times} A)$
66	60	oveq2d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to (\frac{D}{k}) \gcd od (G) (A) = (\frac{D}{k}) \gcd D$
67	58 40 48	divcan2d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to k (\frac{D}{k}) = D$
68	67	eqcomd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to D = k (\frac{D}{k})$
69	68	oveq2d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to (\frac{D}{k}) \gcd D = (\frac{D}{k}) \gcd k (\frac{D}{k})$
70	52 39	gcdmultipled	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to (\frac{D}{k}) \gcd k (\frac{D}{k}) = \frac{D}{k}$
71	69 70	eqtrd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to (\frac{D}{k}) \gcd D = \frac{D}{k}$
72	66 71	eqtrd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to (\frac{D}{k}) \gcd od (G) (A) = \frac{D}{k}$
73	72	oveq1d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to ((\frac{D}{k}) \gcd od (G) (A)) od (G) ((\frac{D}{k}) \underset{˙}{\times} A) = (\frac{D}{k}) od (G) ((\frac{D}{k}) \underset{˙}{\times} A)$
74	65 73	eqtrd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to D = (\frac{D}{k}) od (G) ((\frac{D}{k}) \underset{˙}{\times} A)$
75	59 74	eqtr2d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to (\frac{D}{k}) od (G) ((\frac{D}{k}) \underset{˙}{\times} A) = (\frac{D}{k}) k$
76	1 62 55	odcld	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to od (G) ((\frac{D}{k}) \underset{˙}{\times} A) \in ℕ_{0}$
77	76	nn0cnd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to od (G) ((\frac{D}{k}) \underset{˙}{\times} A) \in ℂ$
78	53	zcnd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to \frac{D}{k} \in ℂ$
79	57	nnne0d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to D \neq 0$
80	58 40 79 48	divne0d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to \frac{D}{k} \neq 0$
81	77 40 78 80	mulcand	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to ((\frac{D}{k}) od (G) ((\frac{D}{k}) \underset{˙}{\times} A) = (\frac{D}{k}) k \leftrightarrow od (G) ((\frac{D}{k}) \underset{˙}{\times} A) = k)$
82	75 81	mpbid	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to od (G) ((\frac{D}{k}) \underset{˙}{\times} A) = k$
83	30 55 82	elrabd	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to (\frac{D}{k}) \underset{˙}{\times} A \in \{x \in B \| od (G) (x) = k\}$
84	83	ne0d	$⊢ ((((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \land l \in ℕ) \land l k = D) \to \{x \in B \| od (G) (x) = k\} \neq \emptyset$
85		nndivides	$⊢ (k \in ℕ \land D \in ℕ) \to (k ∥ D \leftrightarrow \exists l \in ℕ l k = D)$
86	46 56 85	syl2anc	$⊢ ((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \to (k ∥ D \leftrightarrow \exists l \in ℕ l k = D)$
87	86	biimpd	$⊢ ((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \to (k ∥ D \to \exists l \in ℕ l k = D)$
88	87	syldbl2	$⊢ ((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \to \exists l \in ℕ l k = D$
89	84 88	r19.29a	$⊢ ((φ \land k \in (1 \dots D - 1)) \land k ∥ D) \to \{x \in B \| od (G) (x) = k\} \neq \emptyset$
90	29 89	syl	$⊢ (φ \land (k \in (1 \dots D - 1) \land k ∥ D)) \to \{x \in B \| od (G) (x) = k\} \neq \emptyset$
91	90	ex	$⊢ φ \to ((k \in (1 \dots D - 1) \land k ∥ D) \to \{x \in B \| od (G) (x) = k\} \neq \emptyset)$
92	91	adantr	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to ((k \in (1 \dots D - 1) \land k ∥ D) \to \{x \in B \| od (G) (x) = k\} \neq \emptyset)$
93	13 92	mpd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \{x \in B \| od (G) (x) = k\} \neq \emptyset$
94	24 93	jca	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to (k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset)$
95	14 41	syl	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to 1 \leq k$
96	15 95	jca	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to (k \in ℤ \land 1 \leq k)$
97	96 44	sylibr	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to k \in ℕ$
98	97	nnred	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to k \in ℝ$
99	16	nnred	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to D \in ℝ$
100		1red	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to 1 \in ℝ$
101	99 100	resubcld	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to D - 1 \in ℝ$
102		elfzle2	$⊢ k \in (1 \dots D - 1) \to k \leq D - 1$
103	14 102	syl	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to k \leq D - 1$
104	99	ltm1d	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to D - 1 < D$
105	98 101 99 103 104	lelttrd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to k < D$
106		breq1	$⊢ c = k \to (c < D \leftrightarrow k < D)$
107		breq1	$⊢ c = k \to (c ∥ \|B\| \leftrightarrow k ∥ \|B\|)$
108		eqeq2	$⊢ c = k \to (od (G) (x) = c \leftrightarrow od (G) (x) = k)$
109	108	rabbidv	$⊢ c = k \to \{x \in B \| od (G) (x) = c\} = \{x \in B \| od (G) (x) = k\}$
110	109	neeq1d	$⊢ c = k \to (\{x \in B \| od (G) (x) = c\} \neq \emptyset \leftrightarrow \{x \in B \| od (G) (x) = k\} \neq \emptyset)$
111	107 110	anbi12d	$⊢ c = k \to ((c ∥ \|B\| \land \{x \in B \| od (G) (x) = c\} \neq \emptyset) \leftrightarrow (k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset))$
112	109	fveq2d	$⊢ c = k \to \|\{x \in B \| od (G) (x) = c\}\| = \|\{x \in B \| od (G) (x) = k\}\|$
113		fveq2	$⊢ c = k \to ϕ (c) = ϕ (k)$
114	112 113	eqeq12d	$⊢ c = k \to (\|\{x \in B \| od (G) (x) = c\}\| = ϕ (c) \leftrightarrow \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k))$
115	111 114	imbi12d	$⊢ c = k \to (((c ∥ \|B\| \land \{x \in B \| od (G) (x) = c\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = c\}\| = ϕ (c)) \leftrightarrow ((k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k)))$
116	106 115	imbi12d	$⊢ c = k \to ((c < D \to ((c ∥ \|B\| \land \{x \in B \| od (G) (x) = c\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = c\}\| = ϕ (c))) \leftrightarrow (k < D \to ((k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k))))$
117	10	adantr	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \forall c \in ℕ (c < D \to ((c ∥ \|B\| \land \{x \in B \| od (G) (x) = c\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = c\}\| = ϕ (c)))$
118	116 117 97	rspcdva	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to (k < D \to ((k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k)))$
119	105 118	mpd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to ((k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k))$
120	94 119	mpd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k)$
121	120	sumeq2dv	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} \|\{x \in B \| od (G) (x) = k\}\| = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k)$
122	121	eqcomd	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k) = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} \|\{x \in B \| od (G) (x) = k\}\|$
123	122	oveq1d	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k) + \|\{x \in B \| od (G) (x) = D\}\| = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} \|\{x \in B \| od (G) (x) = k\}\| + \|\{x \in B \| od (G) (x) = D\}\|$
124		elun	$⊢ y \in (\{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}) \leftrightarrow (y \in \{a \in (1 \dots D - 1) \| a ∥ D\} \lor y \in \{D\})$
125	124	bilani	$⊢ (φ \land y \in (\{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\})) \to (y \in \{a \in (1 \dots D - 1) \| a ∥ D\} \lor y \in \{D\})$
126		1zzd	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to 1 \in ℤ$
127	6	adantr	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to D \in ℕ$
128	127	nnzd	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to D \in ℤ$
129		elfzelz	$⊢ a \in (1 \dots D - 1) \to a \in ℤ$
130	129	adantr	$⊢ (a \in (1 \dots D - 1) \land a ∥ D) \to a \in ℤ$
131	130	adantl	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to a \in ℤ$
132		elfzle1	$⊢ a \in (1 \dots D - 1) \to 1 \leq a$
133	132	adantr	$⊢ (a \in (1 \dots D - 1) \land a ∥ D) \to 1 \leq a$
134	133	adantl	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to 1 \leq a$
135	131	zred	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to a \in ℝ$
136	127	nnred	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to D \in ℝ$
137		1red	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to 1 \in ℝ$
138	136 137	resubcld	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to D - 1 \in ℝ$
139		elfzle2	$⊢ a \in (1 \dots D - 1) \to a \leq D - 1$
140	139	adantr	$⊢ (a \in (1 \dots D - 1) \land a ∥ D) \to a \leq D - 1$
141	140	adantl	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to a \leq D - 1$
142	136	ltm1d	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to D - 1 < D$
143	135 138 136 141 142	lelttrd	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to a < D$
144	135 136 143	ltled	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to a \leq D$
145	126 128 131 134 144	elfzd	$⊢ (φ \land (a \in (1 \dots D - 1) \land a ∥ D)) \to a \in (1 \dots D)$
146	145	rabss3d	$⊢ φ \to \{a \in (1 \dots D - 1) \| a ∥ D\} \subseteq \{a \in (1 \dots D) \| a ∥ D\}$
147	146	sseld	$⊢ φ \to (y \in \{a \in (1 \dots D - 1) \| a ∥ D\} \to y \in \{a \in (1 \dots D) \| a ∥ D\})$
148	147	imp	$⊢ (φ \land y \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to y \in \{a \in (1 \dots D) \| a ∥ D\}$
149		elsni	$⊢ y \in \{D\} \to y = D$
150	149	adantl	$⊢ (φ \land y \in \{D\}) \to y = D$
151		simpr	$⊢ (φ \land y = D) \to y = D$
152		breq1	$⊢ a = D \to (a ∥ D \leftrightarrow D ∥ D)$
153		1zzd	$⊢ φ \to 1 \in ℤ$
154	6	nnzd	$⊢ φ \to D \in ℤ$
155	6	nnge1d	$⊢ φ \to 1 \leq D$
156	6	nnred	$⊢ φ \to D \in ℝ$
157	156	leidd	$⊢ φ \to D \leq D$
158	153 154 154 155 157	elfzd	$⊢ φ \to D \in (1 \dots D)$
159		iddvds	$⊢ D \in ℤ \to D ∥ D$
160	154 159	syl	$⊢ φ \to D ∥ D$
161	152 158 160	elrabd	$⊢ φ \to D \in \{a \in (1 \dots D) \| a ∥ D\}$
162	161	adantr	$⊢ (φ \land y = D) \to D \in \{a \in (1 \dots D) \| a ∥ D\}$
163	151 162	eqeltrd	$⊢ (φ \land y = D) \to y \in \{a \in (1 \dots D) \| a ∥ D\}$
164	163	ex	$⊢ φ \to (y = D \to y \in \{a \in (1 \dots D) \| a ∥ D\})$
165	164	adantr	$⊢ (φ \land y \in \{D\}) \to (y = D \to y \in \{a \in (1 \dots D) \| a ∥ D\})$
166	150 165	mpd	$⊢ (φ \land y \in \{D\}) \to y \in \{a \in (1 \dots D) \| a ∥ D\}$
167	148 166	jaodan	$⊢ (φ \land (y \in \{a \in (1 \dots D - 1) \| a ∥ D\} \lor y \in \{D\})) \to y \in \{a \in (1 \dots D) \| a ∥ D\}$
168	167	ex	$⊢ φ \to ((y \in \{a \in (1 \dots D - 1) \| a ∥ D\} \lor y \in \{D\}) \to y \in \{a \in (1 \dots D) \| a ∥ D\})$
169	168	adantr	$⊢ (φ \land y \in (\{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\})) \to ((y \in \{a \in (1 \dots D - 1) \| a ∥ D\} \lor y \in \{D\}) \to y \in \{a \in (1 \dots D) \| a ∥ D\})$
170	125 169	mpd	$⊢ (φ \land y \in (\{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\})) \to y \in \{a \in (1 \dots D) \| a ∥ D\}$
171	170	ex	$⊢ φ \to (y \in (\{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}) \to y \in \{a \in (1 \dots D) \| a ∥ D\})$
172		simpr	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land y = D) \to y = D$
173		eqidd	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land y = D) \to D = D$
174	6	ad2antrr	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land y = D) \to D \in ℕ$
175		elsng	$⊢ D \in ℕ \to (D \in \{D\} \leftrightarrow D = D)$
176	174 175	syl	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land y = D) \to (D \in \{D\} \leftrightarrow D = D)$
177	173 176	mpbird	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land y = D) \to D \in \{D\}$
178	172 177	eqeltrd	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land y = D) \to y \in \{D\}$
179	178	olcd	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land y = D) \to (y \in \{a \in (1 \dots D - 1) \| a ∥ D\} \lor y \in \{D\})$
180		breq1	$⊢ a = y \to (a ∥ D \leftrightarrow y ∥ D)$
181	180	elrab	$⊢ y \in \{a \in (1 \dots D) \| a ∥ D\} \leftrightarrow (y \in (1 \dots D) \land y ∥ D)$
182	181	bilani	$⊢ (φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \to (y \in (1 \dots D) \land y ∥ D)$
183	182	adantr	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \to (y \in (1 \dots D) \land y ∥ D)$
184		1zzd	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to 1 \in ℤ$
185	154	ad3antrrr	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to D \in ℤ$
186	185 184	zsubcld	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to D - 1 \in ℤ$
187		elfzelz	$⊢ y \in (1 \dots D) \to y \in ℤ$
188	187	adantr	$⊢ (y \in (1 \dots D) \land y ∥ D) \to y \in ℤ$
189	188	adantl	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to y \in ℤ$
190		elfzle1	$⊢ y \in (1 \dots D) \to 1 \leq y$
191	190	adantr	$⊢ (y \in (1 \dots D) \land y ∥ D) \to 1 \leq y$
192	191	adantl	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to 1 \leq y$
193		elfzle2	$⊢ y \in (1 \dots D) \to y \leq D$
194	193	adantr	$⊢ (y \in (1 \dots D) \land y ∥ D) \to y \leq D$
195	194	adantl	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to y \leq D$
196		neqne	$⊢ \neg y = D \to y \neq D$
197	196	adantl	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \to y \neq D$
198	197	necomd	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \to D \neq y$
199	198	adantr	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to D \neq y$
200	195 199	jca	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to (y \leq D \land D \neq y)$
201	189	zred	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to y \in ℝ$
202	156	ad3antrrr	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to D \in ℝ$
203	201 202	ltlend	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to (y < D \leftrightarrow (y \leq D \land D \neq y))$
204	200 203	mpbird	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to y < D$
205	6	ad3antrrr	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to D \in ℕ$
206	205	nnzd	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to D \in ℤ$
207	189 206	zltlem1d	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to (y < D \leftrightarrow y \leq D - 1)$
208	204 207	mpbid	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to y \leq D - 1$
209	184 186 189 192 208	elfzd	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to y \in (1 \dots D - 1)$
210		simprr	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to y ∥ D$
211	180 209 210	elrabd	$⊢ (((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \land (y \in (1 \dots D) \land y ∥ D)) \to y \in \{a \in (1 \dots D - 1) \| a ∥ D\}$
212	211	ex	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \to ((y \in (1 \dots D) \land y ∥ D) \to y \in \{a \in (1 \dots D - 1) \| a ∥ D\})$
213	183 212	mpd	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \to y \in \{a \in (1 \dots D - 1) \| a ∥ D\}$
214	213	orcd	$⊢ ((φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \land \neg y = D) \to (y \in \{a \in (1 \dots D - 1) \| a ∥ D\} \lor y \in \{D\})$
215	179 214	pm2.61dan	$⊢ (φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \to (y \in \{a \in (1 \dots D - 1) \| a ∥ D\} \lor y \in \{D\})$
216	215 124	sylibr	$⊢ (φ \land y \in \{a \in (1 \dots D) \| a ∥ D\}) \to y \in (\{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\})$
217	216	ex	$⊢ φ \to (y \in \{a \in (1 \dots D) \| a ∥ D\} \to y \in (\{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}))$
218	171 217	impbid	$⊢ φ \to (y \in (\{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}) \leftrightarrow y \in \{a \in (1 \dots D) \| a ∥ D\})$
219	218	eqrdv	$⊢ φ \to \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\} = \{a \in (1 \dots D) \| a ∥ D\}$
220	219	sumeq1d	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} ϕ (k) = \sum_{k \in \{a \in (1 \dots D) \| a ∥ D\}} ϕ (k)$
221		phisum	$⊢ D \in ℕ \to \sum_{k \in \{a \in ℕ \| a ∥ D\}} ϕ (k) = D$
222	6 221	syl	$⊢ φ \to \sum_{k \in \{a \in ℕ \| a ∥ D\}} ϕ (k) = D$
223		eqcom	$⊢ od (G) (A) = D \leftrightarrow D = od (G) (A)$
224	223	imbi2i	$⊢ (φ \to od (G) (A) = D) \leftrightarrow (φ \to D = od (G) (A))$
225	9 224	mpbi	$⊢ φ \to D = od (G) (A)$
226	225	oveq1d	$⊢ φ \to D \underset{˙}{\times} x = od (G) (A) \underset{˙}{\times} x$
227	226	eqeq1d	$⊢ φ \to (D \underset{˙}{\times} x = 0_{G} \leftrightarrow od (G) (A) \underset{˙}{\times} x = 0_{G})$
228	227	rabbidv	$⊢ φ \to \{x \in B \| D \underset{˙}{\times} x = 0_{G}\} = \{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}$
229	228	fveq2d	$⊢ φ \to \|\{x \in B \| D \underset{˙}{\times} x = 0_{G}\}\| = \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\|$
230	1 2 3 4 5 8	unitscyglem1	$⊢ φ \to \|\{x \in B \| od (G) (A) \underset{˙}{\times} x = 0_{G}\}\| = od (G) (A)$
231	229 230	eqtrd	$⊢ φ \to \|\{x \in B \| D \underset{˙}{\times} x = 0_{G}\}\| = od (G) (A)$
232	231 9	eqtr2d	$⊢ φ \to D = \|\{x \in B \| D \underset{˙}{\times} x = 0_{G}\}\|$
233	1 2 3 4 6	grpods	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D) \| a ∥ D\}} \|\{x \in B \| od (G) (x) = k\}\| = \|\{x \in B \| D \underset{˙}{\times} x = 0_{G}\}\|$
234	232 233	eqtr4d	$⊢ φ \to D = \sum_{k \in \{a \in (1 \dots D) \| a ∥ D\}} \|\{x \in B \| od (G) (x) = k\}\|$
235	219	eqcomd	$⊢ φ \to \{a \in (1 \dots D) \| a ∥ D\} = \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}$
236	235	sumeq1d	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D) \| a ∥ D\}} \|\{x \in B \| od (G) (x) = k\}\| = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} \|\{x \in B \| od (G) (x) = k\}\|$
237	234 236	eqtrd	$⊢ φ \to D = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} \|\{x \in B \| od (G) (x) = k\}\|$
238	222 237	eqtr2d	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} \|\{x \in B \| od (G) (x) = k\}\| = \sum_{k \in \{a \in ℕ \| a ∥ D\}} ϕ (k)$
239		1zzd	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to 1 \in ℤ$
240	154	adantr	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to D \in ℤ$
241	180	elrab	$⊢ y \in \{a \in ℕ \| a ∥ D\} \leftrightarrow (y \in ℕ \land y ∥ D)$
242	241	bilani	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to (y \in ℕ \land y ∥ D)$
243	242	simpld	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to y \in ℕ$
244	243	nnzd	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to y \in ℤ$
245	243	nnge1d	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to 1 \leq y$
246	242	simprd	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to y ∥ D$
247	6	adantr	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to D \in ℕ$
248		dvdsle	$⊢ (y \in ℤ \land D \in ℕ) \to (y ∥ D \to y \leq D)$
249	244 247 248	syl2anc	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to (y ∥ D \to y \leq D)$
250	246 249	mpd	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to y \leq D$
251	239 240 244 245 250	elfzd	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to y \in (1 \dots D)$
252	180 251 246	elrabd	$⊢ (φ \land y \in \{a \in ℕ \| a ∥ D\}) \to y \in \{a \in (1 \dots D) \| a ∥ D\}$
253	252	ex	$⊢ φ \to (y \in \{a \in ℕ \| a ∥ D\} \to y \in \{a \in (1 \dots D) \| a ∥ D\})$
254		elfzelz	$⊢ a \in (1 \dots D) \to a \in ℤ$
255		elfzle1	$⊢ a \in (1 \dots D) \to 1 \leq a$
256	254 255	jca	$⊢ a \in (1 \dots D) \to (a \in ℤ \land 1 \leq a)$
257	256	adantr	$⊢ (a \in (1 \dots D) \land a ∥ D) \to (a \in ℤ \land 1 \leq a)$
258	257	adantl	$⊢ (φ \land (a \in (1 \dots D) \land a ∥ D)) \to (a \in ℤ \land 1 \leq a)$
259		elnnz1	$⊢ a \in ℕ \leftrightarrow (a \in ℤ \land 1 \leq a)$
260	258 259	sylibr	$⊢ (φ \land (a \in (1 \dots D) \land a ∥ D)) \to a \in ℕ$
261	260	rabss3d	$⊢ φ \to \{a \in (1 \dots D) \| a ∥ D\} \subseteq \{a \in ℕ \| a ∥ D\}$
262	261	sseld	$⊢ φ \to (y \in \{a \in (1 \dots D) \| a ∥ D\} \to y \in \{a \in ℕ \| a ∥ D\})$
263	253 262	impbid	$⊢ φ \to (y \in \{a \in ℕ \| a ∥ D\} \leftrightarrow y \in \{a \in (1 \dots D) \| a ∥ D\})$
264	263	eqrdv	$⊢ φ \to \{a \in ℕ \| a ∥ D\} = \{a \in (1 \dots D) \| a ∥ D\}$
265	264	sumeq1d	$⊢ φ \to \sum_{k \in \{a \in ℕ \| a ∥ D\}} ϕ (k) = \sum_{k \in \{a \in (1 \dots D) \| a ∥ D\}} ϕ (k)$
266	238 265	eqtr2d	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D) \| a ∥ D\}} ϕ (k) = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} \|\{x \in B \| od (G) (x) = k\}\|$
267	220 266	eqtrd	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} ϕ (k) = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} \|\{x \in B \| od (G) (x) = k\}\|$
268		nfv	$⊢ Ⅎ k φ$
269		nfcv	$⊢ \underline{Ⅎ} k \|\{x \in B \| od (G) (x) = D\}\|$
270		fzfid	$⊢ φ \to (1 \dots D - 1) \in Fin$
271		ssrab2	$⊢ \{a \in (1 \dots D - 1) \| a ∥ D\} \subseteq (1 \dots D - 1)$
272	271	a1i	$⊢ φ \to \{a \in (1 \dots D - 1) \| a ∥ D\} \subseteq (1 \dots D - 1)$
273	270 272	ssfid	$⊢ φ \to \{a \in (1 \dots D - 1) \| a ∥ D\} \in Fin$
274	152	elrab	$⊢ D \in \{a \in (1 \dots D - 1) \| a ∥ D\} \leftrightarrow (D \in (1 \dots D - 1) \land D ∥ D)$
275	274	biimpi	$⊢ D \in \{a \in (1 \dots D - 1) \| a ∥ D\} \to (D \in (1 \dots D - 1) \land D ∥ D)$
276	275	simpld	$⊢ D \in \{a \in (1 \dots D - 1) \| a ∥ D\} \to D \in (1 \dots D - 1)$
277	276	adantl	$⊢ (φ \land D \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to D \in (1 \dots D - 1)$
278		elfzle2	$⊢ D \in (1 \dots D - 1) \to D \leq D - 1$
279	277 278	syl	$⊢ (φ \land D \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to D \leq D - 1$
280	156	ltm1d	$⊢ φ \to D - 1 < D$
281		1red	$⊢ φ \to 1 \in ℝ$
282	156 281	resubcld	$⊢ φ \to D - 1 \in ℝ$
283	282 156	ltnled	$⊢ φ \to (D - 1 < D \leftrightarrow \neg D \leq D - 1)$
284	280 283	mpbid	$⊢ φ \to \neg D \leq D - 1$
285	284	adantr	$⊢ (φ \land D \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \neg D \leq D - 1$
286	279 285	pm2.21dd	$⊢ (φ \land D \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \neg D \in \{a \in (1 \dots D - 1) \| a ∥ D\}$
287		simpr	$⊢ (φ \land \neg D \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \neg D \in \{a \in (1 \dots D - 1) \| a ∥ D\}$
288	286 287	pm2.61dan	$⊢ φ \to \neg D \in \{a \in (1 \dots D - 1) \| a ∥ D\}$
289	4	adantr	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to B \in Fin$
290		ssrab2	$⊢ \{x \in B \| od (G) (x) = k\} \subseteq B$
291	290	a1i	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \{x \in B \| od (G) (x) = k\} \subseteq B$
292	289 291	ssfid	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \{x \in B \| od (G) (x) = k\} \in Fin$
293		hashcl	$⊢ \{x \in B \| od (G) (x) = k\} \in Fin \to \|\{x \in B \| od (G) (x) = k\}\| \in ℕ_{0}$
294	292 293	syl	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℕ_{0}$
295	294	nn0cnd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℂ$
296		eqeq2	$⊢ k = D \to (od (G) (x) = k \leftrightarrow od (G) (x) = D)$
297	296	rabbidv	$⊢ k = D \to \{x \in B \| od (G) (x) = k\} = \{x \in B \| od (G) (x) = D\}$
298	297	fveq2d	$⊢ k = D \to \|\{x \in B \| od (G) (x) = k\}\| = \|\{x \in B \| od (G) (x) = D\}\|$
299		ssrab2	$⊢ \{x \in B \| od (G) (x) = D\} \subseteq B$
300	299	a1i	$⊢ φ \to \{x \in B \| od (G) (x) = D\} \subseteq B$
301	4 300	ssfid	$⊢ φ \to \{x \in B \| od (G) (x) = D\} \in Fin$
302		hashcl	$⊢ \{x \in B \| od (G) (x) = D\} \in Fin \to \|\{x \in B \| od (G) (x) = D\}\| \in ℕ_{0}$
303	301 302	syl	$⊢ φ \to \|\{x \in B \| od (G) (x) = D\}\| \in ℕ_{0}$
304	303	nn0cnd	$⊢ φ \to \|\{x \in B \| od (G) (x) = D\}\| \in ℂ$
305	268 269 273 6 288 295 298 304	fsumsplitsn	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} \|\{x \in B \| od (G) (x) = k\}\| = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} \|\{x \in B \| od (G) (x) = k\}\| + \|\{x \in B \| od (G) (x) = D\}\|$
306	267 305	eqtr2d	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} \|\{x \in B \| od (G) (x) = k\}\| + \|\{x \in B \| od (G) (x) = D\}\| = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} ϕ (k)$
307		nfcv	$⊢ \underline{Ⅎ} k ϕ (D)$
308	120 295	eqeltrrd	$⊢ (φ \land k \in \{a \in (1 \dots D - 1) \| a ∥ D\}) \to ϕ (k) \in ℂ$
309		fveq2	$⊢ k = D \to ϕ (k) = ϕ (D)$
310	6	phicld	$⊢ φ \to ϕ (D) \in ℕ$
311	310	nncnd	$⊢ φ \to ϕ (D) \in ℂ$
312	268 307 273 6 288 308 309 311	fsumsplitsn	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\} \cup \{D\}} ϕ (k) = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k) + ϕ (D)$
313	306 312	eqtrd	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} \|\{x \in B \| od (G) (x) = k\}\| + \|\{x \in B \| od (G) (x) = D\}\| = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k) + ϕ (D)$
314	123 313	eqtrd	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k) + \|\{x \in B \| od (G) (x) = D\}\| = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k) + ϕ (D)$
315	273 308	fsumcl	$⊢ φ \to \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k) \in ℂ$
316	315 304 311	addcand	$⊢ φ \to (\sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k) + \|\{x \in B \| od (G) (x) = D\}\| = \sum_{k \in \{a \in (1 \dots D - 1) \| a ∥ D\}} ϕ (k) + ϕ (D) \leftrightarrow \|\{x \in B \| od (G) (x) = D\}\| = ϕ (D))$
317	314 316	mpbid	$⊢ φ \to \|\{x \in B \| od (G) (x) = D\}\| = ϕ (D)$

Metamath Proof Explorer

Theorem unitscyglem2

Proof