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	bilani	$⊢ (φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \to \exists z \in B od (G) (z) = \|B\|$
217	209 216	r19.29a	$⊢ (φ \land \{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset) \to \{x \in B \| od (G) (x) = D\} \neq \emptyset$
218	217	ex	$⊢ φ \to (\{x \in B \| od (G) (x) = \|B\|\} \neq \emptyset \to \{x \in B \| od (G) (x) = D\} \neq \emptyset)$
219	218	necon4d	$⊢ φ \to (\{x \in B \| od (G) (x) = D\} = \emptyset \to \{x \in B \| od (G) (x) = \|B\|\} = \emptyset)$
220	219	imp	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{x \in B \| od (G) (x) = \|B\|\} = \emptyset$
221	220	fveq2d	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| = \|\emptyset\|$
222		hash0	$⊢ \|\emptyset\| = 0$
223	222	a1i	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\emptyset\| = 0$
224	221 223	eqtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| = 0$
225	122	nngt0d	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to 0 < ϕ (\|B\|)$
226	224 225	eqbrtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{x \in B \| od (G) (x) = \|B\|\}\| < ϕ (\|B\|)$
227		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\|\})$
228	227	bilani	$⊢ (φ \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\|\})$
229		breq1	$⊢ a = z \to (a ∥ \|B\| \leftrightarrow z ∥ \|B\|)$
230	229	elrab	$⊢ z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \leftrightarrow (z \in (1 \dots \|B\|) \land z ∥ \|B\|)$
231	230	biimpi	$⊢ z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \to (z \in (1 \dots \|B\|) \land z ∥ \|B\|)$
232	231	adantr	$⊢ (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\}) \to (z \in (1 \dots \|B\|) \land z ∥ \|B\|)$
233		velsn	$⊢ z \in \{\|B\|\} \leftrightarrow z = \|B\|$
234	233	bicomi	$⊢ z = \|B\| \leftrightarrow z \in \{\|B\|\}$
235	234	biimpi	$⊢ z = \|B\| \to z \in \{\|B\|\}$
236	235	necon3bi	$⊢ \neg z \in \{\|B\|\} \to z \neq \|B\|$
237	236	adantl	$⊢ (z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \land \neg z \in \{\|B\|\}) \to z \neq \|B\|$
238	232 237	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\|)$
239	238	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\|)$
240		1zzd	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to 1 \in ℤ$
241	4	adantr	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to B \in Fin$
242	241 70	syl	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| \in ℕ_{0}$
243	242	nn0zd	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| \in ℤ$
244	243 240	zsubcld	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| - 1 \in ℤ$
245		elfzelz	$⊢ z \in (1 \dots \|B\|) \to z \in ℤ$
246	245	adantr	$⊢ (z \in (1 \dots \|B\|) \land z ∥ \|B\|) \to z \in ℤ$
247	246	adantr	$⊢ ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|) \to z \in ℤ$
248	247	adantl	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \in ℤ$
249		elfzle1	$⊢ z \in (1 \dots \|B\|) \to 1 \leq z$
250	249	adantr	$⊢ (z \in (1 \dots \|B\|) \land z ∥ \|B\|) \to 1 \leq z$
251	250	adantr	$⊢ ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|) \to 1 \leq z$
252	251	adantl	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to 1 \leq z$
253		elfzle2	$⊢ z \in (1 \dots \|B\|) \to z \leq \|B\|$
254	253	adantr	$⊢ (z \in (1 \dots \|B\|) \land z ∥ \|B\|) \to z \leq \|B\|$
255	254	adantr	$⊢ ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|) \to z \leq \|B\|$
256	255	adantl	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \leq \|B\|$
257		simprr	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \neq \|B\|$
258	257	necomd	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| \neq z$
259	256 258	jca	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to (z \leq \|B\| \land \|B\| \neq z)$
260	248	zred	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \in ℝ$
261	242	nn0red	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to \|B\| \in ℝ$
262	260 261	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))$
263	259 262	mpbird	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z < \|B\|$
264	248 243	zltlem1d	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to (z < \|B\| \leftrightarrow z \leq \|B\| - 1)$
265	263 264	mpbid	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \leq \|B\| - 1$
266	240 244 248 252 265	elfzd	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z \in (1 \dots \|B\| - 1)$
267		simprlr	$⊢ (φ \land ((z \in (1 \dots \|B\|) \land z ∥ \|B\|) \land z \neq \|B\|)) \to z ∥ \|B\|$
268	229 266 267	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\|\}$
269	268	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\|\})$
270	269	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\|\})$
271	239 270	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\|\}$
272	271	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\|\})$
273	272	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\|\})$
274	228 273	mpd	$⊢ (φ \land z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
275	274	ex	$⊢ φ \to (z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}) \to z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\})$
276	275	ssrdv	$⊢ φ \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\} \subseteq \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
277		1zzd	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to 1 \in ℤ$
278	170	nn0zd	$⊢ φ \to \|B\| \in ℤ$
279	278	adantr	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to \|B\| \in ℤ$
280		elfzelz	$⊢ z \in (1 \dots \|B\| - 1) \to z \in ℤ$
281	280	adantl	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \in ℤ$
282		elfzle1	$⊢ z \in (1 \dots \|B\| - 1) \to 1 \leq z$
283	282	adantl	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to 1 \leq z$
284	281	zred	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \in ℝ$
285	279	zred	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to \|B\| \in ℝ$
286		1red	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to 1 \in ℝ$
287	285 286	resubcld	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to \|B\| - 1 \in ℝ$
288		elfzle2	$⊢ z \in (1 \dots \|B\| - 1) \to z \leq \|B\| - 1$
289	288	adantl	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \leq \|B\| - 1$
290	285	lem1d	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to \|B\| - 1 \leq \|B\|$
291	284 287 285 289 290	letrd	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \leq \|B\|$
292	277 279 281 283 291	elfzd	$⊢ (φ \land z \in (1 \dots \|B\| - 1)) \to z \in (1 \dots \|B\|)$
293	292	ex	$⊢ φ \to (z \in (1 \dots \|B\| - 1) \to z \in (1 \dots \|B\|))$
294	293	ssrdv	$⊢ φ \to (1 \dots \|B\| - 1) \subseteq (1 \dots \|B\|)$
295		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\|\}$
296	294 295	syl	$⊢ φ \to \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \subseteq \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}$
297	296	sseld	$⊢ φ \to (z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \to z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\})$
298	297	imp	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}$
299	170	ad2antrr	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| \in ℕ_{0}$
300	299	nn0red	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| \in ℝ$
301	300	leidd	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| \leq \|B\|$
302		simpr	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to z = \|B\|$
303	302	eqcomd	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| = z$
304	229	elrab	$⊢ z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \leftrightarrow (z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|)$
305	304	bilani	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to (z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|)$
306	289	adantrr	$⊢ (φ \land (z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|)) \to z \leq \|B\| - 1$
307	306	ex	$⊢ φ \to ((z \in (1 \dots \|B\| - 1) \land z ∥ \|B\|) \to z \leq \|B\| - 1)$
308	307	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)$
309	305 308	mpd	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \leq \|B\| - 1$
310	298 231 246	3syl	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \in ℤ$
311	278	adantr	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \|B\| \in ℤ$
312	310 311	zltlem1d	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to (z < \|B\| \leftrightarrow z \leq \|B\| - 1)$
313	309 312	mpbird	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z < \|B\|$
314	313	adantr	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to z < \|B\|$
315	303 314	eqbrtrd	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \|B\| < \|B\|$
316	300 300	ltnled	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to (\|B\| < \|B\| \leftrightarrow \neg \|B\| \leq \|B\|)$
317	315 316	mpbid	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to \neg \|B\| \leq \|B\|$
318	301 317	pm2.21dd	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z = \|B\|) \to z \neq \|B\|$
319		simpr	$⊢ ((φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \land z \neq \|B\|) \to z \neq \|B\|$
320	318 319	pm2.61dane	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \neq \|B\|$
321	298 320	eldifsnd	$⊢ (φ \land z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\})$
322	321	ex	$⊢ φ \to (z \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \to z \in (\{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}))$
323	322	ssrdv	$⊢ φ \to \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \subseteq \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\}$
324	276 323	eqssd	$⊢ φ \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} ∖ \{\|B\|\} = \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
325	324	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\}\|$
326		fzfid	$⊢ φ \to (1 \dots \|B\| - 1) \in Fin$
327		ssrab2	$⊢ \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \subseteq (1 \dots \|B\| - 1)$
328	327	a1i	$⊢ φ \to \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \subseteq (1 \dots \|B\| - 1)$
329	326 328	ssfid	$⊢ φ \to \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \in Fin$
330	4	adantr	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to B \in Fin$
331	88	a1i	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \{x \in B \| od (G) (x) = k\} \subseteq B$
332	330 331	ssfid	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \{x \in B \| od (G) (x) = k\} \in Fin$
333	332 91	syl	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℕ_{0}$
334	333	nn0red	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \|\{x \in B \| od (G) (x) = k\}\| \in ℝ$
335	125	elrab	$⊢ k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\} \leftrightarrow (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)$
336	335	bilani	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)$
337		elfzelz	$⊢ k \in (1 \dots \|B\| - 1) \to k \in ℤ$
338		elfzle1	$⊢ k \in (1 \dots \|B\| - 1) \to 1 \leq k$
339	337 338	jca	$⊢ k \in (1 \dots \|B\| - 1) \to (k \in ℤ \land 1 \leq k)$
340	339	adantr	$⊢ (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|) \to (k \in ℤ \land 1 \leq k)$
341	340	adantl	$⊢ (φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \to (k \in ℤ \land 1 \leq k)$
342	341 135	sylibr	$⊢ (φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \to k \in ℕ$
343	342	ex	$⊢ φ \to ((k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|) \to k \in ℕ)$
344	343	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 ℕ)$
345	336 344	mpd	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to k \in ℕ$
346	345	phicld	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to ϕ (k) \in ℕ$
347	346	nnred	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to ϕ (k) \in ℝ$
348		simpll	$⊢ ((φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \land \{x \in B \| od (G) (x) = k\} \neq \emptyset) \to φ$
349	335	bilanri	$⊢ (φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \to k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}$
350	349	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\|\}$
351	348 350	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\|\})$
352	351 334	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 ℝ$
353		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$
354	351 353	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)$
355	336	simprd	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to k ∥ \|B\|$
356	355	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\|$
357		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$
358	356 357	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)$
359		breq1	$⊢ m = k \to (m ∥ \|B\| \leftrightarrow k ∥ \|B\|)$
360		eqeq2	$⊢ m = k \to (od (G) (x) = m \leftrightarrow od (G) (x) = k)$
361	360	rabbidv	$⊢ m = k \to \{x \in B \| od (G) (x) = m\} = \{x \in B \| od (G) (x) = k\}$
362	361	neeq1d	$⊢ m = k \to (\{x \in B \| od (G) (x) = m\} \neq \emptyset \leftrightarrow \{x \in B \| od (G) (x) = k\} \neq \emptyset)$
363	359 362	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))$
364	361	fveq2d	$⊢ m = k \to \|\{x \in B \| od (G) (x) = m\}\| = \|\{x \in B \| od (G) (x) = k\}\|$
365		fveq2	$⊢ m = k \to ϕ (m) = ϕ (k)$
366	364 365	eqeq12d	$⊢ m = k \to (\|\{x \in B \| od (G) (x) = m\}\| = ϕ (m) \leftrightarrow \|\{x \in B \| od (G) (x) = k\}\| = ϕ (k))$
367	363 366	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)))$
368	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))$
369	367 368 345	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))$
370	369	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))$
371	358 370	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)$
372	354 371	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)$
373	352 372	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)$
374		id	$⊢ \{x \in B \| od (G) (x) = k\} \neq \emptyset \to \{x \in B \| od (G) (x) = k\} \neq \emptyset$
375	374	necon1bi	$⊢ \neg \{x \in B \| od (G) (x) = k\} \neq \emptyset \to \{x \in B \| od (G) (x) = k\} = \emptyset$
376	375	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$
377	376	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\|$
378	222	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$
379	377 378	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$
380	342	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 ℕ$
381	380	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 ℕ$
382	381	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}$
383	382	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)$
384	379 383	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)$
385	373 384	pm2.61dan	$⊢ (φ \land (k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|)) \to \|\{x \in B \| od (G) (x) = k\}\| \leq ϕ (k)$
386	385	ex	$⊢ φ \to ((k \in (1 \dots \|B\| - 1) \land k ∥ \|B\|) \to \|\{x \in B \| od (G) (x) = k\}\| \leq ϕ (k))$
387	386	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))$
388	336 387	mpd	$⊢ (φ \land k \in \{a \in (1 \dots \|B\| - 1) \| a ∥ \|B\|\}) \to \|\{x \in B \| od (G) (x) = k\}\| \leq ϕ (k)$
389	329 334 347 388	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)$
390	324	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)$
391	390	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)$
392	389 391	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)$
393	325 392	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)$
394	393	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)$
395	113 121 123 140 226 394	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)$
396		nfcv	$⊢ \underline{Ⅎ} k ϕ (\|B\|)$
397		simpll	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to φ$
398	126	bilani	$⊢ ((φ \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\|)$
399	397 398	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\|))$
400	131	adantl	$⊢ (φ \land (k \in (1 \dots \|B\|) \land k ∥ \|B\|)) \to (k \in ℤ \land 1 \leq k)$
401	400	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)$
402	401 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 ℕ$
403	402	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 ℕ)$
404	399 403	mpd	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to k \in ℕ$
405	404	phicld	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to ϕ (k) \in ℕ$
406	405	nncnd	$⊢ ((φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \land k \in \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}) \to ϕ (k) \in ℂ$
407		fveq2	$⊢ k = \|B\| \to ϕ (k) = ϕ (\|B\|)$
408	81 396 86 406 103 407	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)$
409	395 408	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)$
410	107 409	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)$
411		elfzelz	$⊢ a \in (1 \dots \|B\|) \to a \in ℤ$
412		elfzle1	$⊢ a \in (1 \dots \|B\|) \to 1 \leq a$
413	411 412	jca	$⊢ a \in (1 \dots \|B\|) \to (a \in ℤ \land 1 \leq a)$
414	413	adantr	$⊢ (a \in (1 \dots \|B\|) \land a ∥ \|B\|) \to (a \in ℤ \land 1 \leq a)$
415	414	adantl	$⊢ (φ \land (a \in (1 \dots \|B\|) \land a ∥ \|B\|)) \to (a \in ℤ \land 1 \leq a)$
416		elnnz1	$⊢ a \in ℕ \leftrightarrow (a \in ℤ \land 1 \leq a)$
417	415 416	sylibr	$⊢ (φ \land (a \in (1 \dots \|B\|) \land a ∥ \|B\|)) \to a \in ℕ$
418	417	rabss3d	$⊢ φ \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} \subseteq \{a \in ℕ \| a ∥ \|B\|\}$
419		simpl	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to φ$
420		simprl	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to a \in ℕ$
421	419 420	jca	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to (φ \land a \in ℕ)$
422		simprr	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to a ∥ \|B\|$
423	421 422	jca	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to ((φ \land a \in ℕ) \land a ∥ \|B\|)$
424		1zzd	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to 1 \in ℤ$
425	278	adantr	$⊢ (φ \land a \in ℕ) \to \|B\| \in ℤ$
426	425	adantr	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to \|B\| \in ℤ$
427	420	anassrs	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to a \in ℕ$
428	427	nnzd	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to a \in ℤ$
429	427	nnge1d	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to 1 \leq a$
430		nnz	$⊢ a \in ℕ \to a \in ℤ$
431	430	adantl	$⊢ (φ \land a \in ℕ) \to a \in ℤ$
432	1 3 4	hashfingrpnn	$⊢ φ \to \|B\| \in ℕ$
433	432	adantr	$⊢ (φ \land a \in ℕ) \to \|B\| \in ℕ$
434		dvdsle	$⊢ (a \in ℤ \land \|B\| \in ℕ) \to (a ∥ \|B\| \to a \leq \|B\|)$
435	431 433 434	syl2anc	$⊢ (φ \land a \in ℕ) \to (a ∥ \|B\| \to a \leq \|B\|)$
436	435	imp	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to a \leq \|B\|$
437	424 426 428 429 436	elfzd	$⊢ ((φ \land a \in ℕ) \land a ∥ \|B\|) \to a \in (1 \dots \|B\|)$
438	423 437	syl	$⊢ (φ \land (a \in ℕ \land a ∥ \|B\|)) \to a \in (1 \dots \|B\|)$
439	438	rabss3d	$⊢ φ \to \{a \in ℕ \| a ∥ \|B\|\} \subseteq \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\}$
440	418 439	eqssd	$⊢ φ \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} = \{a \in ℕ \| a ∥ \|B\|\}$
441	440	adantr	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \{a \in (1 \dots \|B\|) \| a ∥ \|B\|\} = \{a \in ℕ \| a ∥ \|B\|\}$
442	441	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)$
443	410 442	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)$
444		phisum	$⊢ \|B\| \in ℕ \to \sum_{k \in \{a \in ℕ \| a ∥ \|B\|\}} ϕ (k) = \|B\|$
445	39 444	syl	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \sum_{k \in \{a \in ℕ \| a ∥ \|B\|\}} ϕ (k) = \|B\|$
446	443 445	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\|$
447	80 446	eqbrtrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| < \|B\|$
448	170	adantr	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \in ℕ_{0}$
449	448	nn0red	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|B\| \in ℝ$
450	449	ltnrd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \neg \|B\| < \|B\|$
451	447 450	pm2.21dd	$⊢ (φ \land \{x \in B \| od (G) (x) = D\} = \emptyset) \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D)$
452	451	ex	$⊢ φ \to (\{x \in B \| od (G) (x) = D\} = \emptyset \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D))$
453	452	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))$
454	36 453	mpd	$⊢ (φ \land \neg \{x \in B \| od (G) (x) = D\} \neq \emptyset) \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D)$
455	33 454	pm2.61dan	$⊢ φ \to \|\{y \in B \| od (G) (y) = D\}\| = ϕ (D)$

Metamath Proof Explorer

Theorem unitscyglem4

Proof