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

Metamath Proof Explorer

Theorem unitscyglem2

Proof