unitscyglem4

	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$
	unitscyglem4.1	$⊢ φ \to D \in ℕ$
	unitscyglem4.2	$⊢ φ \to D ∥ \|B\|$
Assertion	unitscyglem4	$⊢ φ \to \|\{y \in B \| od (G) (y) = 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		unitscyglem4.1	$⊢ φ \to D \in ℕ$
7		unitscyglem4.2	$⊢ φ \to D ∥ \|B\|$
8		nfcv	$⊢ \underline{Ⅎ} y B$
9		nfcv	$⊢ \underline{Ⅎ} x B$
10		nfv	$⊢ Ⅎ x od (G) (y) = D$
11		nfv	$⊢ Ⅎ y od (G) (x) = D$
12		fveqeq2	$⊢ y = x \to (od (G) (y) = D \leftrightarrow od (G) (x) = D)$
13	8 9 10 11 12	cbvrabw	$⊢ \{y \in B \| od (G) (y) = D\} = \{x \in B \| od (G) (x) = D\}$
14	13	fveq2i	$⊢ \|\{y \in B \| od (G) (y) = D\}\| = \|\{x \in B \| od (G) (x) = D\}\|$
15	14	a1i	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to \|\{y \in B \| od (G) (y) = D\}\| = \|\{x \in B \| od (G) (x) = D\}\|$
16	7	adantr	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to D ∥ \|B\|$
17	16	ex	$⊢ φ \to (\{x \in B \| od (G) (x) = D\} \neq \emptyset \to D ∥ \|B\|)$
18	17	ancrd	$⊢ φ \to (\{x \in B \| od (G) (x) = D\} \neq \emptyset \to (D ∥ \|B\| \land \{x \in B \| od (G) (x) = D\} \neq \emptyset))$
19	18	imdistani	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to (φ \land (D ∥ \|B\| \land \{x \in B \| od (G) (x) = D\} \neq \emptyset))$
20		breq1	$⊢ m = D \to (m ∥ \|B\| \leftrightarrow D ∥ \|B\|)$
21		eqeq2	$⊢ m = D \to (od (G) (x) = m \leftrightarrow od (G) (x) = D)$
22	21	rabbidv	$⊢ m = D \to \{x \in B \| od (G) (x) = m\} = \{x \in B \| od (G) (x) = D\}$
23	22	neeq1d	$⊢ m = D \to (\{x \in B \| od (G) (x) = m\} \neq \emptyset \leftrightarrow \{x \in B \| od (G) (x) = D\} \neq \emptyset)$
24	20 23	anbi12d	$⊢ m = D \to ((m ∥ \|B\| \land \{x \in B \| od (G) (x) = m\} \neq \emptyset) \leftrightarrow (D ∥ \|B\| \land \{x \in B \| od (G) (x) = D\} \neq \emptyset))$
25	22	fveq2d	$⊢ m = D \to \|\{x \in B \| od (G) (x) = m\}\| = \|\{x \in B \| od (G) (x) = D\}\|$
26		fveq2	$⊢ m = D \to ϕ (m) = ϕ (D)$
27	25 26	eqeq12d	$⊢ m = D \to (\|\{x \in B \| od (G) (x) = m\}\| = ϕ (m) \leftrightarrow \|\{x \in B \| od (G) (x) = D\}\| = ϕ (D))$
28	24 27	imbi12d	$⊢ m = D \to (((m ∥ \|B\| \land \{x \in B \| od (G) (x) = m\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = m\}\| = ϕ (m)) \leftrightarrow ((D ∥ \|B\| \land \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = D\}\| = ϕ (D)))$
29	1 2 3 4 5	unitscyglem3	$⊢ φ \to \forall m \in ℕ ((m ∥ \|B\| \land \{x \in B \| od (G) (x) = m\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = m\}\| = ϕ (m))$
30	28 29 6	rspcdva	$⊢ φ \to ((D ∥ \|B\| \land \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = D\}\| = ϕ (D))$
31	30	imp	$⊢ (φ \land (D ∥ \|B\| \land \{x \in B \| od (G) (x) = D\} \neq \emptyset)) \to \|\{x \in B \| od (G) (x) = D\}\| = ϕ (D)$
32	19 31	syl	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = D\}\| = ϕ (D)$
33	15 32	eqtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D)$
34		id	$⊢ \{x \in B \| od (G) (x) = D\} \neq \emptyset \to \{x \in B \| od (G) (x) = D\} \neq \emptyset$
35	34	necon1bi	$⊢ \neg \{x \in B \| od (G) (x) = D\} \neq \emptyset \to \{x \in B \| od (G) (x) = D\} = \emptyset$
36	35	adantl	$⊢ (φ \land \neg \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to \{x \in B \| od (G) (x) = D\} = \emptyset$
37	3	adantr	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to G \in Grp$
38	4	adantr	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to B \in Fin$
39	1 37 38	hashfingrpnn	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \in ℕ$
40	1 2 37 38 39	grpods	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| = \|\{x \in B \| \|B\| \underset{˙}{\times} x = 0_{G}\}\|$
41		simpr	$⊢ (((φ \land x \in B) \land l \in ℤ) \land l od (G) (x) = \|B\|) \to l od (G) (x) = \|B\|$
42	41	eqcomd	$⊢ (((φ \land x \in B) \land l \in ℤ) \land l od (G) (x) = \|B\|) \to \|B\| = l od (G) (x)$
43	42	oveq1d	$⊢ (((φ \land x \in B) \land l \in ℤ) \land l od (G) (x) = \|B\|) \to \|B\| \underset{˙}{\times} x = l od (G) (x) \underset{˙}{\times} x$
44	3	adantr	$⊢ (φ \land x \in B) \to G \in Grp$
45	44	adantr	$⊢ ((φ \land x \in B) \land l \in ℤ) \to G \in Grp$
46		simpr	$⊢ ((φ \land x \in B) \land l \in ℤ) \to l \in ℤ$
47		eqid	$⊢ od (G) = od (G)$
48		simpr	$⊢ (φ \land x \in B) \to x \in B$
49	1 47 48	odcld	$⊢ (φ \land x \in B) \to od (G) (x) \in ℕ_{0}$
50	49	adantr	$⊢ ((φ \land x \in B) \land l \in ℤ) \to od (G) (x) \in ℕ_{0}$
51	50	nn0zd	$⊢ ((φ \land x \in B) \land l \in ℤ) \to od (G) (x) \in ℤ$
52		simplr	$⊢ ((φ \land x \in B) \land l \in ℤ) \to x \in B$
53	46 51 52	3jca	$⊢ ((φ \land x \in B) \land l \in ℤ) \to (l \in ℤ \land od (G) (x) \in ℤ \land x \in B)$
54	1 2	mulgass	$⊢ (G \in Grp \land (l \in ℤ \land od (G) (x) \in ℤ \land x \in B)) \to l od (G) (x) \underset{˙}{\times} x = l \underset{˙}{\times} (od (G) (x) \underset{˙}{\times} x)$
55	45 53 54	syl2anc	$⊢ ((φ \land x \in B) \land l \in ℤ) \to l od (G) (x) \underset{˙}{\times} x = l \underset{˙}{\times} (od (G) (x) \underset{˙}{\times} x)$
56		eqid	$⊢ 0_{G} = 0_{G}$
57	1 47 2 56	odid	$⊢ x \in B \to od (G) (x) \underset{˙}{\times} x = 0_{G}$
58	52 57	syl	$⊢ ((φ \land x \in B) \land l \in ℤ) \to od (G) (x) \underset{˙}{\times} x = 0_{G}$
59	58	oveq2d	$⊢ ((φ \land x \in B) \land l \in ℤ) \to l \underset{˙}{\times} (od (G) (x) \underset{˙}{\times} x) = l \underset{˙}{\times} 0_{G}$
60	1 2 56	mulgz	$⊢ (G \in Grp \land l \in ℤ) \to l \underset{˙}{\times} 0_{G} = 0_{G}$
61	44 60	sylan	$⊢ ((φ \land x \in B) \land l \in ℤ) \to l \underset{˙}{\times} 0_{G} = 0_{G}$
62	59 61	eqtrd	$⊢ ((φ \land x \in B) \land l \in ℤ) \to l \underset{˙}{\times} (od (G) (x) \underset{˙}{\times} x) = 0_{G}$
63	55 62	eqtrd	$⊢ ((φ \land x \in B) \land l \in ℤ) \to l od (G) (x) \underset{˙}{\times} x = 0_{G}$
64	63	adantr	$⊢ (((φ \land x \in B) \land l \in ℤ) \land l od (G) (x) = \|B\|) \to l od (G) (x) \underset{˙}{\times} x = 0_{G}$
65	43 64	eqtrd	$⊢ (((φ \land x \in B) \land l \in ℤ) \land l od (G) (x) = \|B\|) \to \|B\| \underset{˙}{\times} x = 0_{G}$
66	4	adantr	$⊢ (φ \land x \in B) \to B \in Fin$
67	1 47	oddvds2	$⊢ (G \in Grp \land B \in Fin \land x \in B) \to od (G) (x) ∥ \|B\|$
68	44 66 48 67	syl3anc	$⊢ (φ \land x \in B) \to od (G) (x) ∥ \|B\|$
69	49	nn0zd	$⊢ (φ \land x \in B) \to od (G) (x) \in ℤ$
70		hashcl	$⊢ B \in Fin \to \|B\| \in ℕ_{0}$
71	66 70	syl	$⊢ (φ \land x \in B) \to \|B\| \in ℕ_{0}$
72	71	nn0zd	$⊢ (φ \land x \in B) \to \|B\| \in ℤ$
73		divides	$⊢ (od (G) (x) \in ℤ \land \|B\| \in ℤ) \to (od (G) (x) ∥ \|B\| \leftrightarrow \exists l \in ℤ l od (G) (x) = \|B\|)$
74	69 72 73	syl2anc	$⊢ (φ \land x \in B) \to (od (G) (x) ∥ \|B\| \leftrightarrow \exists l \in ℤ l od (G) (x) = \|B\|)$
75	68 74	mpbid	$⊢ (φ \land x \in B) \to \exists l \in ℤ l od (G) (x) = \|B\|$
76	65 75	r19.29a	$⊢ (φ \land x \in B) \to \|B\| \underset{˙}{\times} x = 0_{G}$
77	76	rabeqcda	$⊢ φ \to \{x \in B \| \|B\| \underset{˙}{\times} x = 0_{G}\} = B$
78	77	adantr	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{x \in B \| \|B\| \underset{˙}{\times} x = 0_{G}\} = B$
79	78	fveq2d	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| \|B\| \underset{˙}{\times} x = 0_{G}\}\| = \|B\|$
80	40 79	eqtr2d	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| = \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} \|\{x \in B \| od (G) (x) = k\}\|$
81		nfv	$⊢ Ⅎ k (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset)$
82		nfcv	$⊢ \underline{Ⅎ} k \|\{x \in B \| od (G) (x) = \|B\|\}\|$
83		fzfid	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to (1 \dots \|B\|) \in Fin$
84		ssrab2	$⊢ \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \subseteq (1 \dots \|B\|)$
85	84	a1i	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \subseteq (1 \dots \|B\|)$
86	83 85	ssfid	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \in Fin$
87	38	adantr	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to B \in Fin$
88		ssrab2	$⊢ \{x \in B \| od (G) (x) = k\} \subseteq B$
89	88	a1i	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to \{x \in B \| od (G) (x) = k\} \subseteq B$
90	87 89	ssfid	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to \{x \in B \| od (G) (x) = k\} \in Fin$
91		hashcl	$⊢ \{x \in B \| od (G) (x) = k\} \in Fin \to \|\{x \in B \| od (G) (x) = k\}\| \in ℕ_{0}$
92	90 91	syl	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℕ_{0}$
93	92	nn0cnd	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℂ$
94		breq1	$⊢ a = \|B\| \to (a ∥ \|B\| \leftrightarrow \|B\| ∥ \|B\|)$
95		1zzd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to 1 \in ℤ$
96	39	nnzd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \in ℤ$
97	39	nnge1d	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to 1 \leq \|B\|$
98	39	nnred	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \in ℝ$
99	98	leidd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \leq \|B\|$
100	95 96 96 97 99	elfzd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \in (1 \dots \|B\|)$
101		iddvds	$⊢ \|B\| \in ℤ \to \|B\| ∥ \|B\|$
102	96 101	syl	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| ∥ \|B\|$
103	94 100 102	elrabd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}$
104		eqeq2	$⊢ k = \|B\| \to (od (G) (x) = k \leftrightarrow od (G) (x) = \|B\|)$
105	104	rabbidv	$⊢ k = \|B\| \to \{x \in B \| od (G) (x) = k\} = \{x \in B \| od (G) (x) = \|B\|\}$
106	105	fveq2d	$⊢ k = \|B\| \to \|\{x \in B \| od (G) (x) = k\}\| = \|\{x \in B \| od (G) (x) = \|B\|\}\|$
107	81 82 86 93 103 106	fsumsplit1	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| = \|\{x \in B \| od (G) (x) = \|B\|\}\| + \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} \|\{x \in B \| od (G) (x) = k\}\|$
108		ssrab2	$⊢ \{x \in B \| od (G) (x) = \|B\|\} \subseteq B$
109	108	a1i	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{x \in B \| od (G) (x) = \|B\|\} \subseteq B$
110	38 109	ssfid	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{x \in B \| od (G) (x) = \|B\|\} \in Fin$
111		hashcl	$⊢ \{x \in B \| od (G) (x) = \|B\|\} \in Fin \to \|\{x \in B \| od (G) (x) = \|B\|\}\| \in ℕ_{0}$
112	110 111	syl	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| \in ℕ_{0}$
113	112	nn0red	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| \in ℝ$
114		diffi	$⊢ \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \in Fin \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\} \in Fin$
115	86 114	syl	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\} \in Fin$
116	38	adantr	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to B \in Fin$
117	88	a1i	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to \{x \in B \| od (G) (x) = k\} \subseteq B$
118	116 117	ssfid	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to \{x \in B \| od (G) (x) = k\} \in Fin$
119	118 91	syl	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℕ_{0}$
120	115 119	fsumnn0cl	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| \in ℕ_{0}$
121	120	nn0red	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| \in ℝ$
122	39	phicld	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to ϕ (\|B\|) \in ℕ$
123	122	nnred	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to ϕ (\|B\|) \in ℝ$
124		eldifi	$⊢ k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}) \to k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}$
125		breq1	$⊢ a = k \to (a ∥ \|B\| \leftrightarrow k ∥ \|B\|)$
126	125	elrab	$⊢ k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \leftrightarrow (k \in (1 \dots \|B\|) \land k ∥ \|B\|)$
127	126	biimpi	$⊢ k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \to (k \in (1 \dots \|B\|) \land k ∥ \|B\|)$
128		elfzelz	$⊢ k \in (1 \dots \|B\|) \to k \in ℤ$
129		elfzle1	$⊢ k \in (1 \dots \|B\|) \to 1 \leq k$
130	128 129	jca	$⊢ k \in (1 \dots \|B\|) \to (k \in ℤ \land 1 \leq k)$
131	130	adantr	$⊢ (k \in (1 \dots \|B\|) \land k ∥ \|B\|) \to (k \in ℤ \land 1 \leq k)$
132	127 131	syl	$⊢ k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \to (k \in ℤ \land 1 \leq k)$
133	124 132	syl	$⊢ k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}) \to (k \in ℤ \land 1 \leq k)$
134	133	adantl	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to (k \in ℤ \land 1 \leq k)$
135		elnnz1	$⊢ k \in ℕ \leftrightarrow (k \in ℤ \land 1 \leq k)$
136	134 135	sylibr	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to k \in ℕ$
137		phicl	$⊢ k \in ℕ \to ϕ (k) \in ℕ$
138	136 137	syl	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to ϕ (k) \in ℕ$
139	138	nnred	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to ϕ (k) \in ℝ$
140	115 139	fsumrecl	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} ϕ (k) \in ℝ$
141		simplll	$⊢ (((φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \land z \in B) \land od (G) (z) = \|B\|) \to φ$
142		simplr	$⊢ (((φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \land z \in B) \land od (G) (z) = \|B\|) \to z \in B$
143	141 142	jca	$⊢ (((φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \land z \in B) \land od (G) (z) = \|B\|) \to (φ \land z \in B)$
144		simpr	$⊢ (((φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \land z \in B) \land od (G) (z) = \|B\|) \to od (G) (z) = \|B\|$
145	143 144	jca	$⊢ (((φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \land z \in B) \land od (G) (z) = \|B\|) \to ((φ \land z \in B) \land od (G) (z) = \|B\|)$
146		fveqeq2	$⊢ x = (\frac{\|B\|}{D}) \underset{˙}{\times} z \to (od (G) (x) = D \leftrightarrow od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z) = D)$
147	3	ad2antrr	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to G \in Grp$
148	7	ad2antrr	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to D ∥ \|B\|$
149	6	ad2antrr	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to D \in ℕ$
150	149	nnzd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to D \in ℤ$
151	149	nnne0d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to D \neq 0$
152	4	ad2antrr	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to B \in Fin$
153	152 70	syl	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \|B\| \in ℕ_{0}$
154	153	nn0zd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \|B\| \in ℤ$
155		dvdsval2	$⊢ (D \in ℤ \land D \neq 0 \land \|B\| \in ℤ) \to (D ∥ \|B\| \leftrightarrow \frac{\|B\|}{D} \in ℤ)$
156	150 151 154 155	syl3anc	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (D ∥ \|B\| \leftrightarrow \frac{\|B\|}{D} \in ℤ)$
157	148 156	mpbid	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \frac{\|B\|}{D} \in ℤ$
158		simplr	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to z \in B$
159	1 2 147 157 158	mulgcld	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \underset{˙}{\times} z \in B$
160	153	nn0cnd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \|B\| \in ℂ$
161	6	nncnd	$⊢ φ \to D \in ℂ$
162	161	ad2antrr	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to D \in ℂ$
163	1 147 152	hashfingrpnn	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \|B\| \in ℕ$
164	163	nnne0d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \|B\| \neq 0$
165	160 160 162 164 151	divdiv2d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \frac{\|B\|}{\frac{\|B\|}{D}} = \frac{\|B\| D}{\|B\|}$
166	162 160 164	divcan3d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \frac{\|B\| D}{\|B\|} = D$
167	165 166	eqtr2d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to D = \frac{\|B\|}{\frac{\|B\|}{D}}$
168		simpr	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to od (G) (z) = \|B\|$
169	168	oveq2d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \gcd od (G) (z) = (\frac{\|B\|}{D}) \gcd \|B\|$
170	4 70	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
171	170	nn0cnd	$⊢ φ \to \|B\| \in ℂ$
172	6	nnne0d	$⊢ φ \to D \neq 0$
173	171 161 172	divcan2d	$⊢ φ \to D (\frac{\|B\|}{D}) = \|B\|$
174	173	eqcomd	$⊢ φ \to \|B\| = D (\frac{\|B\|}{D})$
175	174	adantr	$⊢ (φ \land z \in B) \to \|B\| = D (\frac{\|B\|}{D})$
176	175	adantr	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \|B\| = D (\frac{\|B\|}{D})$
177	176	oveq2d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \gcd \|B\| = (\frac{\|B\|}{D}) \gcd D (\frac{\|B\|}{D})$
178		nndivdvds	$⊢ (\|B\| \in ℕ \land D \in ℕ) \to (D ∥ \|B\| \leftrightarrow \frac{\|B\|}{D} \in ℕ)$
179	163 149 178	syl2anc	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (D ∥ \|B\| \leftrightarrow \frac{\|B\|}{D} \in ℕ)$
180	148 179	mpbid	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \frac{\|B\|}{D} \in ℕ$
181	180	nnnn0d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \frac{\|B\|}{D} \in ℕ_{0}$
182	181 150	gcdmultipled	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \gcd D (\frac{\|B\|}{D}) = \frac{\|B\|}{D}$
183	177 182	eqtrd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \gcd \|B\| = \frac{\|B\|}{D}$
184	169 183	eqtrd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \gcd od (G) (z) = \frac{\|B\|}{D}$
185	184	eqcomd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \frac{\|B\|}{D} = (\frac{\|B\|}{D}) \gcd od (G) (z)$
186	185	oveq2d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \frac{\|B\|}{\frac{\|B\|}{D}} = \frac{\|B\|}{(\frac{\|B\|}{D}) \gcd od (G) (z)}$
187	167 186	eqtrd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to D = \frac{\|B\|}{(\frac{\|B\|}{D}) \gcd od (G) (z)}$
188	168	eqcomd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \|B\| = od (G) (z)$
189	1 47 2	odmulg	$⊢ (G \in Grp \land z \in B \land \frac{\|B\|}{D} \in ℤ) \to od (G) (z) = ((\frac{\|B\|}{D}) \gcd od (G) (z)) od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z)$
190	147 158 157 189	syl3anc	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to od (G) (z) = ((\frac{\|B\|}{D}) \gcd od (G) (z)) od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z)$
191	188 190	eqtrd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \|B\| = ((\frac{\|B\|}{D}) \gcd od (G) (z)) od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z)$
192	191	eqcomd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to ((\frac{\|B\|}{D}) \gcd od (G) (z)) od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z) = \|B\|$
193	157	zcnd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \frac{\|B\|}{D} \in ℂ$
194	184 193	eqeltrd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \gcd od (G) (z) \in ℂ$
195	1 47 159	odcld	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z) \in ℕ_{0}$
196	195	nn0cnd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z) \in ℂ$
197	168 154	eqeltrd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to od (G) (z) \in ℤ$
198	168 164	eqnetrd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to od (G) (z) \neq 0$
199	157 197 198	3jca	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D} \in ℤ \land od (G) (z) \in ℤ \land od (G) (z) \neq 0)$
200		gcd2n0cl	$⊢ (\frac{\|B\|}{D} \in ℤ \land od (G) (z) \in ℤ \land od (G) (z) \neq 0) \to (\frac{\|B\|}{D}) \gcd od (G) (z) \in ℕ$
201	199 200	syl	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \gcd od (G) (z) \in ℕ$
202	201	nnne0d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \gcd od (G) (z) \neq 0$
203	160 194 196 202	divmuld	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{(\frac{\|B\|}{D}) \gcd od (G) (z)} = od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z) \leftrightarrow ((\frac{\|B\|}{D}) \gcd od (G) (z)) od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z) = \|B\|)$
204	192 203	mpbird	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \frac{\|B\|}{(\frac{\|B\|}{D}) \gcd od (G) (z)} = od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z)$
205	187 204	eqtr2d	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to od (G) ((\frac{\|B\|}{D}) \underset{˙}{\times} z) = D$
206	146 159 205	elrabd	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to (\frac{\|B\|}{D}) \underset{˙}{\times} z \in \{x \in B \| od (G) (x) = D\}$
207		ne0i	$⊢ (\frac{\|B\|}{D}) \underset{˙}{\times} z \in \{x \in B \| od (G) (x) = D\} \to \{x \in B \| od (G) (x) = D\} \neq \emptyset$
208	206 207	syl	$⊢ ((φ \land z \in B) \land od (G) (z) = \|B\|) \to \{x \in B \| od (G) (x) = D\} \neq \emptyset$
209	145 208	syl	$⊢ (((φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \land z \in B) \land od (G) (z) = \|B\|) \to \{x \in B \| od (G) (x) = D\} \neq \emptyset$
210		rabn0	$⊢ \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset \leftrightarrow \exists x \in B od (G) (x) = \|B\|$
211		nfv	$⊢ Ⅎ z od (G) (x) = \|B\|$
212		nfv	$⊢ Ⅎ x od (G) (z) = \|B\|$
213		fveqeq2	$⊢ x = z \to (od (G) (x) = \|B\| \leftrightarrow od (G) (z) = \|B\|)$
214	211 212 213	cbvrexw	$⊢ \exists x \in B od (G) (x) = \|B\| \leftrightarrow \exists z \in B od (G) (z) = \|B\|$
215	210 214	bitri	$⊢ \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset \leftrightarrow \exists z \in B od (G) (z) = \|B\|$
216	215	biimpi	$⊢ \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset \to \exists z \in B od (G) (z) = \|B\|$
217	216	adantl	$⊢ (φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \to \exists z \in B od (G) (z) = \|B\|$
218	209 217	r19.29a	$⊢ (φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \to \{x \in B \| od (G) (x) = D\} \neq \emptyset$
219	218	ex	$⊢ φ \to (\{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset \to \{x \in B \| od (G) (x) = D\} \neq \emptyset)$
220	219	necon4d	$⊢ φ \to (\{x \in B \| od (G) (x) = D\} = \emptyset \to \{x \in B \| od (G) (x) = \|B\|\} = \emptyset)$
221	220	imp	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{x \in B \| od (G) (x) = \|B\|\} = \emptyset$
222	221	fveq2d	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| = \|\emptyset\|$
223		hash0	$⊢ \|\emptyset\| = 0$
224	223	a1i	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\emptyset\| = 0$
225	222 224	eqtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| = 0$
226	122	nngt0d	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to 0 < ϕ (\|B\|)$
227	225 226	eqbrtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| < ϕ (\|B\|)$
228		eldif	$⊢ z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}) \leftrightarrow (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\})$
229	228	biimpi	$⊢ z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}) \to (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\})$
230	229	adantl	$⊢ (φ \land z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\})$
231		breq1	$⊢ a = z \to (a ∥ \|B\| \leftrightarrow z ∥ \|B\|)$
232	231	elrab	$⊢ z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \leftrightarrow (z \in (1 \dots \|B\|) \land z ∥ \|B\|)$
233	232	biimpi	$⊢ z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \to (z \in (1 \dots \|B\|) \land z ∥ \|B\|)$
234	233	adantr	$⊢ (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\}) \to (z \in (1 \dots \|B\|) \land z ∥ \|B\|)$
235		velsn	$⊢ z \in \{\|B\|\} \leftrightarrow z = \|B\|$
236	235	bicomi	$⊢ z = \|B\| \leftrightarrow z \in \{\|B\|\}$
237	236	biimpi	$⊢ z = \|B\| \to z \in \{\|B\|\}$
238	237	necon3bi	$⊢ \neg z \in \{\|B\|\} \to z \neq \|B\|$
239	238	adantl	$⊢ (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\}) \to z \neq \|B\|$
240	234 239	jca	$⊢ (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\}) \to ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)$
241	240	adantl	$⊢ (φ \land (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\})) \to ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)$
242		1zzd	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to 1 \in ℤ$
243	4	adantr	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to B \in Fin$
244	243 70	syl	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| \in ℕ_{0}$
245	244	nn0zd	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| \in ℤ$
246	245 242	zsubcld	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| - 1 \in ℤ$
247		elfzelz	$⊢ z \in (1 \dots \|B\|) \to z \in ℤ$
248	247	adantr	$⊢ (z \in (1 \dots \|B\|) \land z ∥ \|B\|) \to z \in ℤ$
249	248	adantr	$⊢ ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|) \to z \in ℤ$
250	249	adantl	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \in ℤ$
251		elfzle1	$⊢ z \in (1 \dots \|B\|) \to 1 \leq z$
252	251	adantr	$⊢ (z \in (1 \dots \|B\|) \land z ∥ \|B\|) \to 1 \leq z$
253	252	adantr	$⊢ ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|) \to 1 \leq z$
254	253	adantl	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to 1 \leq z$
255		elfzle2	$⊢ z \in (1 \dots \|B\|) \to z \leq \|B\|$
256	255	adantr	$⊢ (z \in (1 \dots \|B\|) \land z ∥ \|B\|) \to z \leq \|B\|$
257	256	adantr	$⊢ ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|) \to z \leq \|B\|$
258	257	adantl	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \leq \|B\|$
259		simprr	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \neq \|B\|$
260	259	necomd	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| \neq z$
261	258 260	jca	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to (z \leq \|B\| \land \|B\| \neq z)$
262	250	zred	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \in ℝ$
263	244	nn0red	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| \in ℝ$
264	262 263	ltlend	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to (z < \|B\| \leftrightarrow (z \leq \|B\| \land \|B\| \neq z))$
265	261 264	mpbird	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z < \|B\|$
266	250 245	zltlem1d	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to (z < \|B\| \leftrightarrow z \leq \|B\| - 1)$
267	265 266	mpbid	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \leq \|B\| - 1$
268	242 246 250 254 267	elfzd	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \in (1 \dots \|B\| - 1)$
269		simprlr	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z ∥ \|B\|$
270	231 268 269	elrabd	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
271	270	ex	$⊢ φ \to (((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\})$
272	271	adantr	$⊢ (φ \land (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\})) \to (((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\})$
273	241 272	mpd	$⊢ (φ \land (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\})) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
274	273	ex	$⊢ φ \to ((z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\}) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\})$
275	274	adantr	$⊢ (φ \land z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to ((z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\}) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\})$
276	230 275	mpd	$⊢ (φ \land z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
277	276	ex	$⊢ φ \to (z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\})$
278	277	ssrdv	$⊢ φ \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\} \subseteq \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
279		1zzd	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to 1 \in ℤ$
280	170	nn0zd	$⊢ φ \to \|B\| \in ℤ$
281	280	adantr	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to \|B\| \in ℤ$
282		elfzelz	$⊢ z \in (1 \dots \|B\| - 1) \to z \in ℤ$
283	282	adantl	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \in ℤ$
284		elfzle1	$⊢ z \in (1 \dots \|B\| - 1) \to 1 \leq z$
285	284	adantl	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to 1 \leq z$
286	283	zred	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \in ℝ$
287	281	zred	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to \|B\| \in ℝ$
288		1red	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to 1 \in ℝ$
289	287 288	resubcld	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to \|B\| - 1 \in ℝ$
290		elfzle2	$⊢ z \in (1 \dots \|B\| - 1) \to z \leq \|B\| - 1$
291	290	adantl	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \leq \|B\| - 1$
292	287	lem1d	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to \|B\| - 1 \leq \|B\|$
293	286 289 287 291 292	letrd	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \leq \|B\|$
294	279 281 283 285 293	elfzd	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \in (1 \dots \|B\|)$
295	294	ex	$⊢ φ \to (z \in (1 \dots \|B\| - 1) \to z \in (1 \dots \|B\|))$
296	295	ssrdv	$⊢ φ \to (1 \dots \|B\| - 1) \subseteq (1 \dots \|B\|)$
297		rabss2	$⊢ (1 \dots \|B\| - 1) \subseteq (1 \dots \|B\|) \to \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \subseteq \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}$
298	296 297	syl	$⊢ φ \to \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \subseteq \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}$
299	298	sseld	$⊢ φ \to (z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \to z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\})$
300	299	imp	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}$
301	170	ad2antrr	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| \in ℕ_{0}$
302	301	nn0red	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| \in ℝ$
303	302	leidd	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| \leq \|B\|$
304		simpr	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to z = \|B\|$
305	304	eqcomd	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| = z$
306	231	elrab	$⊢ z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \leftrightarrow (z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|)$
307	306	biimpi	$⊢ z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \to (z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|)$
308	307	adantl	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to (z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|)$
309	291	adantrr	$⊢ (φ \land (z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|)) \to z \leq \|B\| - 1$
310	309	ex	$⊢ φ \to ((z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|) \to z \leq \|B\| - 1)$
311	310	adantr	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to ((z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|) \to z \leq \|B\| - 1)$
312	308 311	mpd	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \leq \|B\| - 1$
313	300 233 248	3syl	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \in ℤ$
314	280	adantr	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \|B\| \in ℤ$
315	313 314	zltlem1d	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to (z < \|B\| \leftrightarrow z \leq \|B\| - 1)$
316	312 315	mpbird	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z < \|B\|$
317	316	adantr	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to z < \|B\|$
318	305 317	eqbrtrd	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| < \|B\|$
319	302 302	ltnled	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to (\|B\| < \|B\| \leftrightarrow \neg \|B\| \leq \|B\|)$
320	318 319	mpbid	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \neg \|B\| \leq \|B\|$
321	303 320	pm2.21dd	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to z \neq \|B\|$
322		simpr	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z \neq \|B\|) \to z \neq \|B\|$
323	321 322	pm2.61dane	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \neq \|B\|$
324	300 323	eldifsnd	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})$
325	324	ex	$⊢ φ \to (z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \to z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}))$
326	325	ssrdv	$⊢ φ \to \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \subseteq \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}$
327	278 326	eqssd	$⊢ φ \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\} = \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
328	327	sumeq1d	$⊢ φ \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| = \sum_{k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}} \|\{x \in B \| od (G) (x) = k\}\|$
329		fzfid	$⊢ φ \to (1 \dots \|B\| - 1) \in Fin$
330		ssrab2	$⊢ \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \subseteq (1 \dots \|B\| - 1)$
331	330	a1i	$⊢ φ \to \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \subseteq (1 \dots \|B\| - 1)$
332	329 331	ssfid	$⊢ φ \to \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \in Fin$
333	4	adantr	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to B \in Fin$
334	88	a1i	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \{x \in B \| od (G) (x) = k\} \subseteq B$
335	333 334	ssfid	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \{x \in B \| od (G) (x) = k\} \in Fin$
336	335 91	syl	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℕ_{0}$
337	336	nn0red	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℝ$
338	125	elrab	$⊢ k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \leftrightarrow (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)$
339	338	biimpi	$⊢ k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \to (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)$
340	339	adantl	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)$
341		elfzelz	$⊢ k \in (1 \dots \|B\| - 1) \to k \in ℤ$
342		elfzle1	$⊢ k \in (1 \dots \|B\| - 1) \to 1 \leq k$
343	341 342	jca	$⊢ k \in (1 \dots \|B\| - 1) \to (k \in ℤ \land 1 \leq k)$
344	343	adantr	$⊢ (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|) \to (k \in ℤ \land 1 \leq k)$
345	344	adantl	$⊢ (φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \to (k \in ℤ \land 1 \leq k)$
346	345 135	sylibr	$⊢ (φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \to k \in ℕ$
347	346	ex	$⊢ φ \to ((k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|) \to k \in ℕ)$
348	347	adantr	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to ((k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|) \to k \in ℕ)$
349	340 348	mpd	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to k \in ℕ$
350	349	phicld	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to ϕ (k) \in ℕ$
351	350	nnred	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to ϕ (k) \in ℝ$
352		simpll	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to φ$
353	338	biimpri	$⊢ (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|) \to k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
354	353	adantl	$⊢ (φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \to k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
355	354	adantr	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
356	352 355	jca	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\})$
357	356 337	syl	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℝ$
358		simpr	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \{x \in B \| od (G) (x) = k\} \neq \emptyset$
359	356 358	jca	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to ((φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset)$
360	340	simprd	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to k ∥ \|B\|$
361	360	adantr	$⊢ ((φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to k ∥ \|B\|$
362		simpr	$⊢ ((φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \{x \in B \| od (G) (x) = k\} \neq \emptyset$
363	361 362	jca	$⊢ ((φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to (k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset)$
364		breq1	$⊢ m = k \to (m ∥ \|B\| \leftrightarrow k ∥ \|B\|)$
365		eqeq2	$⊢ m = k \to (od (G) (x) = m \leftrightarrow od (G) (x) = k)$
366	365	rabbidv	$⊢ m = k \to \{x \in B \| od (G) (x) = m\} = \{x \in B \| od (G) (x) = k\}$
367	366	neeq1d	$⊢ m = k \to (\{x \in B \| od (G) (x) = m\} \neq \emptyset \leftrightarrow \{x \in B \| od (G) (x) = k\} \neq \emptyset)$
368	364 367	anbi12d	$⊢ m = k \to ((m ∥ \|B\| \land \{x \in B \| od (G) (x) = m\} \neq \emptyset) \leftrightarrow (k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset))$
369	366	fveq2d	$⊢ m = k \to \|\{x \in B \| od (G) (x) = m\}\| = \|\{x \in B \| od (G) (x) = k\}\|$
370		fveq2	$⊢ m = k \to ϕ (m) = ϕ (k)$
371	369 370	eqeq12d	$⊢ m = k \to (\|\{x \in B \| od (G) (x) = m\}\| = ϕ (m) \leftrightarrow \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k))$
372	368 371	imbi12d	$⊢ m = k \to (((m ∥ \|B\| \land \{x \in B \| od (G) (x) = m\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = m\}\| = ϕ (m)) \leftrightarrow ((k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k)))$
373	29	adantr	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \forall m \in ℕ ((m ∥ \|B\| \land \{x \in B \| od (G) (x) = m\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = m\}\| = ϕ (m))$
374	372 373 349	rspcdva	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to ((k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k))$
375	374	adantr	$⊢ ((φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to ((k ∥ \|B\| \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k))$
376	363 375	mpd	$⊢ ((φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k)$
377	359 376	syl	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k)$
378	357 377	eqled	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| \leq ϕ (k)$
379		id	$⊢ \{x \in B \| od (G) (x) = k\} \neq \emptyset \to \{x \in B \| od (G) (x) = k\} \neq \emptyset$
380	379	necon1bi	$⊢ \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset \to \{x \in B \| od (G) (x) = k\} = \emptyset$
381	380	adantl	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \{x \in B \| od (G) (x) = k\} = \emptyset$
382	381	fveq2d	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = \|\emptyset\|$
383	223	a1i	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\emptyset\| = 0$
384	382 383	eqtrd	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| = 0$
385	346	adantr	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to k \in ℕ$
386	385	phicld	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to ϕ (k) \in ℕ$
387	386	nnnn0d	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to ϕ (k) \in ℕ_{0}$
388	387	nn0ge0d	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to 0 \leq ϕ (k)$
389	384 388	eqbrtrd	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to \|\{x \in B \| od (G) (x) = k\}\| \leq ϕ (k)$
390	378 389	pm2.61dan	$⊢ (φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \to \|\{x \in B \| od (G) (x) = k\}\| \leq ϕ (k)$
391	390	ex	$⊢ φ \to ((k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|) \to \|\{x \in B \| od (G) (x) = k\}\| \leq ϕ (k))$
392	391	adantr	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to ((k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|) \to \|\{x \in B \| od (G) (x) = k\}\| \leq ϕ (k))$
393	340 392	mpd	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \|\{x \in B \| od (G) (x) = k\}\| \leq ϕ (k)$
394	332 337 351 393	fsumle	$⊢ φ \to \sum_{k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| \leq \sum_{k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}} ϕ (k)$
395	327	sumeq1d	$⊢ φ \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} ϕ (k) = \sum_{k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}} ϕ (k)$
396	395	eqcomd	$⊢ φ \to \sum_{k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}} ϕ (k) = \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} ϕ (k)$
397	394 396	breqtrd	$⊢ φ \to \sum_{k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| \leq \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} ϕ (k)$
398	328 397	eqbrtrd	$⊢ φ \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| \leq \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} ϕ (k)$
399	398	adantr	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| \leq \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} ϕ (k)$
400	113 121 123 140 227 399	ltleaddd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| + \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| < ϕ (\|B\|) + \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} ϕ (k)$
401		nfcv	$⊢ \underline{Ⅎ} k ϕ (\|B\|)$
402		simpll	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to φ$
403	127	adantl	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to (k \in (1 \dots \|B\|) \land k ∥ \|B\|)$
404	402 403	jca	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to (φ \land (k \in (1 \dots \|B\|) \land k ∥ \|B\|))$
405	131	adantl	$⊢ (φ \land (k \in (1 \dots \|B\|) \land k ∥ \|B\|)) \to (k \in ℤ \land 1 \leq k)$
406	405	adantl	$⊢ (((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \land (φ \land (k \in (1 \dots \|B\|) \land k ∥ \|B\|))) \to (k \in ℤ \land 1 \leq k)$
407	406 135	sylibr	$⊢ (((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \land (φ \land (k \in (1 \dots \|B\|) \land k ∥ \|B\|))) \to k \in ℕ$
408	407	ex	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to ((φ \land (k \in (1 \dots \|B\|) \land k ∥ \|B\|)) \to k \in ℕ)$
409	404 408	mpd	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to k \in ℕ$
410	409	phicld	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to ϕ (k) \in ℕ$
411	410	nncnd	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to ϕ (k) \in ℂ$
412		fveq2	$⊢ k = \|B\| \to ϕ (k) = ϕ (\|B\|)$
413	81 401 86 411 103 412	fsumsplit1	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} ϕ (k) = ϕ (\|B\|) + \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} ϕ (k)$
414	400 413	breqtrrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| + \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| < \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} ϕ (k)$
415	107 414	eqbrtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| < \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} ϕ (k)$
416		elfzelz	$⊢ a \in (1 \dots \|B\|) \to a \in ℤ$
417		elfzle1	$⊢ a \in (1 \dots \|B\|) \to 1 \leq a$
418	416 417	jca	$⊢ a \in (1 \dots \|B\|) \to (a \in ℤ \land 1 \leq a)$
419	418	adantr	$⊢ (a \in (1 \dots \|B\|) \land a ∥ \|B\|) \to (a \in ℤ \land 1 \leq a)$
420	419	adantl	$⊢ (φ \land (a \in (1 \dots \|B\|) \land a ∥ \|B\|)) \to (a \in ℤ \land 1 \leq a)$
421		elnnz1	$⊢ a \in ℕ \leftrightarrow (a \in ℤ \land 1 \leq a)$
422	420 421	sylibr	$⊢ (φ \land (a \in (1 \dots \|B\|) \land a ∥ \|B\|)) \to a \in ℕ$
423	422	rabss3d	$⊢ φ \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \subseteq \{a \in ℕ \| a ∥ \|B\|\}$
424		simpl	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to φ$
425		simprl	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to a \in ℕ$
426	424 425	jca	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to (φ \land a \in ℕ)$
427		simprr	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to a ∥ \|B\|$
428	426 427	jca	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to ((φ \land a \in ℕ) \land a ∥ \|B\|)$
429		1zzd	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to 1 \in ℤ$
430	280	adantr	$⊢ (φ \land a \in ℕ) \to \|B\| \in ℤ$
431	430	adantr	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to \|B\| \in ℤ$
432	425	anassrs	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to a \in ℕ$
433	432	nnzd	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to a \in ℤ$
434	432	nnge1d	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to 1 \leq a$
435		nnz	$⊢ a \in ℕ \to a \in ℤ$
436	435	adantl	$⊢ (φ \land a \in ℕ) \to a \in ℤ$
437	1 3 4	hashfingrpnn	$⊢ φ \to \|B\| \in ℕ$
438	437	adantr	$⊢ (φ \land a \in ℕ) \to \|B\| \in ℕ$
439		dvdsle	$⊢ (a \in ℤ \land \|B\| \in ℕ) \to (a ∥ \|B\| \to a \leq \|B\|)$
440	436 438 439	syl2anc	$⊢ (φ \land a \in ℕ) \to (a ∥ \|B\| \to a \leq \|B\|)$
441	440	imp	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to a \leq \|B\|$
442	429 431 433 434 441	elfzd	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to a \in (1 \dots \|B\|)$
443	428 442	syl	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to a \in (1 \dots \|B\|)$
444	443	rabss3d	$⊢ φ \to \{a \in ℕ \| a ∥ \|B\|\} \subseteq \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}$
445	423 444	eqssd	$⊢ φ \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} = \{a \in ℕ \| a ∥ \|B\|\}$
446	445	adantr	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} = \{a \in ℕ \| a ∥ \|B\|\}$
447	446	sumeq1d	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} ϕ (k) = \sum_{k \in \{a \in ℕ \| a ∥ \|B\|\}} ϕ (k)$
448	415 447	breqtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| < \sum_{k \in \{a \in ℕ \| a ∥ \|B\|\}} ϕ (k)$
449		phisum	$⊢ \|B\| \in ℕ \to \sum_{k \in \{a \in ℕ \| a ∥ \|B\|\}} ϕ (k) = \|B\|$
450	39 449	syl	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in ℕ \| a ∥ \|B\|\}} ϕ (k) = \|B\|$
451	448 450	breqtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}} \|\{x \in B \| od (G) (x) = k\}\| < \|B\|$
452	80 451	eqbrtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| < \|B\|$
453	170	adantr	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \in ℕ_{0}$
454	453	nn0red	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \in ℝ$
455	454	ltnrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \neg \|B\| < \|B\|$
456	452 455	pm2.21dd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D)$
457	456	ex	$⊢ φ \to (\{x \in B \| od (G) (x) = D\} = \emptyset \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D))$
458	457	adantr	$⊢ (φ \land \neg \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to (\{x \in B \| od (G) (x) = D\} = \emptyset \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D))$
459	36 458	mpd	$⊢ (φ \land \neg \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D)$
460	33 459	pm2.61dan	$⊢ φ \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D)$

Metamath Proof Explorer

Theorem unitscyglem4

Proof