hgt750lemb

Description: An upper bound on the contribution of the non-prime terms in the Statement 7.50 of Helfgott p. 69. (Contributed by Thierry Arnoux, 28-Dec-2021)

	Ref	Expression
Hypotheses	hgt750leme.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
	hgt750leme.n	$⊢ φ \to N \in ℕ$
	hgt750lemb.2	$⊢ φ \to 2 \leq N$
	hgt750lemb.a	$⊢ A = \{c \in (ℕ repr (3) N) \| \neg c (0) \in (O \cap ℙ)\}$
Assertion	hgt750lemb	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j)$

Proof

Step	Hyp	Ref	Expression
1		hgt750leme.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
2		hgt750leme.n	$⊢ φ \to N \in ℕ$
3		hgt750lemb.2	$⊢ φ \to 2 \leq N$
4		hgt750lemb.a	$⊢ A = \{c \in (ℕ repr (3) N) \| \neg c (0) \in (O \cap ℙ)\}$
5	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
6		3nn0	$⊢ 3 \in ℕ_{0}$
7	6	a1i	$⊢ φ \to 3 \in ℕ_{0}$
8		ssidd	$⊢ φ \to ℕ \subseteq ℕ$
9	5 7 8	reprfi2	$⊢ φ \to ℕ repr (3) N \in Fin$
10	4	ssrab3	$⊢ A \subseteq ℕ repr (3) N$
11		ssfi	$⊢ (ℕ repr (3) N \in Fin \land A \subseteq ℕ repr (3) N) \to A \in Fin$
12	9 10 11	sylancl	$⊢ φ \to A \in Fin$
13		vmaf	$⊢ Λ : ℕ ⟶ ℝ$
14	13	a1i	$⊢ (φ \land n \in A) \to Λ : ℕ ⟶ ℝ$
15		ssidd	$⊢ (φ \land n \in A) \to ℕ \subseteq ℕ$
16	2	nnzd	$⊢ φ \to N \in ℤ$
17	16	adantr	$⊢ (φ \land n \in A) \to N \in ℤ$
18	6	a1i	$⊢ (φ \land n \in A) \to 3 \in ℕ_{0}$
19		simpr	$⊢ (φ \land n \in A) \to n \in A$
20	10 19	sselid	$⊢ (φ \land n \in A) \to n \in (ℕ repr (3) N)$
21	15 17 18 20	reprf	$⊢ (φ \land n \in A) \to n : (0 ..^3) ⟶ ℕ$
22		c0ex	$⊢ 0 \in V$
23	22	tpid1	$⊢ 0 \in \{0, 1, 2\}$
24		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
25	23 24	eleqtrri	$⊢ 0 \in (0 ..^3)$
26	25	a1i	$⊢ (φ \land n \in A) \to 0 \in (0 ..^3)$
27	21 26	ffvelcdmd	$⊢ (φ \land n \in A) \to n (0) \in ℕ$
28	14 27	ffvelcdmd	$⊢ (φ \land n \in A) \to Λ (n (0)) \in ℝ$
29		1eltp012	$⊢ 1 \in \{0, 1, 2\}$
30	29 24	eleqtrri	$⊢ 1 \in (0 ..^3)$
31	30	a1i	$⊢ (φ \land n \in A) \to 1 \in (0 ..^3)$
32	21 31	ffvelcdmd	$⊢ (φ \land n \in A) \to n (1) \in ℕ$
33	14 32	ffvelcdmd	$⊢ (φ \land n \in A) \to Λ (n (1)) \in ℝ$
34		2ex	$⊢ 2 \in V$
35	34	tpid3	$⊢ 2 \in \{0, 1, 2\}$
36	35 24	eleqtrri	$⊢ 2 \in (0 ..^3)$
37	36	a1i	$⊢ (φ \land n \in A) \to 2 \in (0 ..^3)$
38	21 37	ffvelcdmd	$⊢ (φ \land n \in A) \to n (2) \in ℕ$
39	14 38	ffvelcdmd	$⊢ (φ \land n \in A) \to Λ (n (2)) \in ℝ$
40	33 39	remulcld	$⊢ (φ \land n \in A) \to Λ (n (1)) Λ (n (2)) \in ℝ$
41	28 40	remulcld	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
42	12 41	fsumrecl	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
43	2	nnrpd	$⊢ φ \to N \in ℝ^{+}$
44	43	relogcld	$⊢ φ \to \log N \in ℝ$
45	28 33	remulcld	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) \in ℝ$
46	12 45	fsumrecl	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) \in ℝ$
47	44 46	remulcld	$⊢ φ \to \log N \sum_{n \in A} Λ (n (0)) Λ (n (1)) \in ℝ$
48		fzfi	$⊢ (1 \dots N) \in Fin$
49		diffi	$⊢ (1 \dots N) \in Fin \to (1 \dots N) ∖ ℙ \in Fin$
50	48 49	ax-mp	$⊢ (1 \dots N) ∖ ℙ \in Fin$
51		snfi	$⊢ \{2\} \in Fin$
52		unfi	$⊢ ((1 \dots N) ∖ ℙ \in Fin \land \{2\} \in Fin) \to ((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin$
53	50 51 52	mp2an	$⊢ ((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin$
54	53	a1i	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin$
55	13	a1i	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to Λ : ℕ ⟶ ℝ$
56		difss	$⊢ (1 \dots N) ∖ ℙ \subseteq (1 \dots N)$
57	56	a1i	$⊢ φ \to (1 \dots N) ∖ ℙ \subseteq (1 \dots N)$
58		2nn	$⊢ 2 \in ℕ$
59	58	a1i	$⊢ φ \to 2 \in ℕ$
60		elfz1b	$⊢ 2 \in (1 \dots N) \leftrightarrow (2 \in ℕ \land N \in ℕ \land 2 \leq N)$
61	60	biimpri	$⊢ (2 \in ℕ \land N \in ℕ \land 2 \leq N) \to 2 \in (1 \dots N)$
62	59 2 3 61	syl3anc	$⊢ φ \to 2 \in (1 \dots N)$
63	62	snssd	$⊢ φ \to \{2\} \subseteq (1 \dots N)$
64	57 63	unssd	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} \subseteq (1 \dots N)$
65		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
66	65	a1i	$⊢ φ \to (1 \dots N) \subseteq ℕ$
67	64 66	sstrd	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} \subseteq ℕ$
68	67	sselda	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to i \in ℕ$
69	55 68	ffvelcdmd	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to Λ (i) \in ℝ$
70	54 69	fsumrecl	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \in ℝ$
71		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
72	13	a1i	$⊢ (φ \land j \in (1 \dots N)) \to Λ : ℕ ⟶ ℝ$
73	66	sselda	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℕ$
74	72 73	ffvelcdmd	$⊢ (φ \land j \in (1 \dots N)) \to Λ (j) \in ℝ$
75	71 74	fsumrecl	$⊢ φ \to \sum_{j = 1}^{N} Λ (j) \in ℝ$
76	70 75	remulcld	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \in ℝ$
77	44 76	remulcld	$⊢ φ \to \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \in ℝ$
78	2	adantr	$⊢ (φ \land n \in A) \to N \in ℕ$
79	78	nnrpd	$⊢ (φ \land n \in A) \to N \in ℝ^{+}$
80		relogcl	$⊢ N \in ℝ^{+} \to \log N \in ℝ$
81	79 80	syl	$⊢ (φ \land n \in A) \to \log N \in ℝ$
82	33 81	remulcld	$⊢ (φ \land n \in A) \to Λ (n (1)) \log N \in ℝ$
83	28 82	remulcld	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) \log N \in ℝ$
84		vmage0	$⊢ n (0) \in ℕ \to 0 \leq Λ (n (0))$
85	27 84	syl	$⊢ (φ \land n \in A) \to 0 \leq Λ (n (0))$
86		vmage0	$⊢ n (1) \in ℕ \to 0 \leq Λ (n (1))$
87	32 86	syl	$⊢ (φ \land n \in A) \to 0 \leq Λ (n (1))$
88	38	nnrpd	$⊢ (φ \land n \in A) \to n (2) \in ℝ^{+}$
89	88	relogcld	$⊢ (φ \land n \in A) \to \log n (2) \in ℝ$
90		vmalelog	$⊢ n (2) \in ℕ \to Λ (n (2)) \leq \log n (2)$
91	38 90	syl	$⊢ (φ \land n \in A) \to Λ (n (2)) \leq \log n (2)$
92	15 17 18 20 37	reprle	$⊢ (φ \land n \in A) \to n (2) \leq N$
93		logleb	$⊢ (n (2) \in ℝ^{+} \land N \in ℝ^{+}) \to (n (2) \leq N \leftrightarrow \log n (2) \leq \log N)$
94	93	biimpa	$⊢ ((n (2) \in ℝ^{+} \land N \in ℝ^{+}) \land n (2) \leq N) \to \log n (2) \leq \log N$
95	88 79 92 94	syl21anc	$⊢ (φ \land n \in A) \to \log n (2) \leq \log N$
96	39 89 81 91 95	letrd	$⊢ (φ \land n \in A) \to Λ (n (2)) \leq \log N$
97	39 81 33 87 96	lemul2ad	$⊢ (φ \land n \in A) \to Λ (n (1)) Λ (n (2)) \leq Λ (n (1)) \log N$
98	40 82 28 85 97	lemul2ad	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq Λ (n (0)) Λ (n (1)) \log N$
99	12 41 83 98	fsumle	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq \sum_{n \in A} Λ (n (0)) Λ (n (1)) \log N$
100	2	nncnd	$⊢ φ \to N \in ℂ$
101	2	nnne0d	$⊢ φ \to N \neq 0$
102	100 101	logcld	$⊢ φ \to \log N \in ℂ$
103	45	recnd	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) \in ℂ$
104	12 102 103	fsummulc2	$⊢ φ \to \log N \sum_{n \in A} Λ (n (0)) Λ (n (1)) = \sum_{n \in A} \log N Λ (n (0)) Λ (n (1))$
105	102	adantr	$⊢ (φ \land n \in A) \to \log N \in ℂ$
106	105 103	mulcomd	$⊢ (φ \land n \in A) \to \log N Λ (n (0)) Λ (n (1)) = Λ (n (0)) Λ (n (1)) \log N$
107	28	recnd	$⊢ (φ \land n \in A) \to Λ (n (0)) \in ℂ$
108	33	recnd	$⊢ (φ \land n \in A) \to Λ (n (1)) \in ℂ$
109	107 108 105	mulassd	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) \log N = Λ (n (0)) Λ (n (1)) \log N$
110	106 109	eqtrd	$⊢ (φ \land n \in A) \to \log N Λ (n (0)) Λ (n (1)) = Λ (n (0)) Λ (n (1)) \log N$
111	110	sumeq2dv	$⊢ φ \to \sum_{n \in A} \log N Λ (n (0)) Λ (n (1)) = \sum_{n \in A} Λ (n (0)) Λ (n (1)) \log N$
112	104 111	eqtr2d	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) \log N = \log N \sum_{n \in A} Λ (n (0)) Λ (n (1))$
113	99 112	breqtrd	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq \log N \sum_{n \in A} Λ (n (0)) Λ (n (1))$
114	2	nnred	$⊢ φ \to N \in ℝ$
115	2	nnge1d	$⊢ φ \to 1 \leq N$
116	114 115	logge0d	$⊢ φ \to 0 \leq \log N$
117		xpfi	$⊢ (((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin \land (1 \dots N) \in Fin) \to (((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N) \in Fin$
118	54 71 117	syl2anc	$⊢ φ \to (((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N) \in Fin$
119	13	a1i	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to Λ : ℕ ⟶ ℝ$
120	67	adantr	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to ((1 \dots N) ∖ ℙ) \cup \{2\} \subseteq ℕ$
121		xp1st	$⊢ u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)) \to 1^{st} (u) \in (((1 \dots N) ∖ ℙ) \cup \{2\})$
122	121	adantl	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 1^{st} (u) \in (((1 \dots N) ∖ ℙ) \cup \{2\})$
123	120 122	sseldd	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 1^{st} (u) \in ℕ$
124	119 123	ffvelcdmd	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to Λ (1^{st} (u)) \in ℝ$
125		xp2nd	$⊢ u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)) \to 2^{nd} (u) \in (1 \dots N)$
126	125	adantl	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 2^{nd} (u) \in (1 \dots N)$
127	65 126	sselid	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 2^{nd} (u) \in ℕ$
128	119 127	ffvelcdmd	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to Λ (2^{nd} (u)) \in ℝ$
129	124 128	remulcld	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to Λ (1^{st} (u)) Λ (2^{nd} (u)) \in ℝ$
130		vmage0	$⊢ 1^{st} (u) \in ℕ \to 0 \leq Λ (1^{st} (u))$
131	123 130	syl	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 0 \leq Λ (1^{st} (u))$
132		vmage0	$⊢ 2^{nd} (u) \in ℕ \to 0 \leq Λ (2^{nd} (u))$
133	127 132	syl	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 0 \leq Λ (2^{nd} (u))$
134	124 128 131 133	mulge0d	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 0 \leq Λ (1^{st} (u)) Λ (2^{nd} (u))$
135		ssidd	$⊢ (φ \land c \in A) \to ℕ \subseteq ℕ$
136	16	adantr	$⊢ (φ \land c \in A) \to N \in ℤ$
137	6	a1i	$⊢ (φ \land c \in A) \to 3 \in ℕ_{0}$
138		simpr	$⊢ (φ \land c \in A) \to c \in A$
139	10 138	sselid	$⊢ (φ \land c \in A) \to c \in (ℕ repr (3) N)$
140	135 136 137 139	reprf	$⊢ (φ \land c \in A) \to c : (0 ..^3) ⟶ ℕ$
141	25	a1i	$⊢ (φ \land c \in A) \to 0 \in (0 ..^3)$
142	140 141	ffvelcdmd	$⊢ (φ \land c \in A) \to c (0) \in ℕ$
143	2	adantr	$⊢ (φ \land c \in A) \to N \in ℕ$
144	135 136 137 139 141	reprle	$⊢ (φ \land c \in A) \to c (0) \leq N$
145		elfz1b	$⊢ c (0) \in (1 \dots N) \leftrightarrow (c (0) \in ℕ \land N \in ℕ \land c (0) \leq N)$
146	145	biimpri	$⊢ (c (0) \in ℕ \land N \in ℕ \land c (0) \leq N) \to c (0) \in (1 \dots N)$
147	142 143 144 146	syl3anc	$⊢ (φ \land c \in A) \to c (0) \in (1 \dots N)$
148	4	reqabi	$⊢ c \in A \leftrightarrow (c \in (ℕ repr (3) N) \land \neg c (0) \in (O \cap ℙ))$
149	148	simprbi	$⊢ c \in A \to \neg c (0) \in (O \cap ℙ)$
150	1	oddprm2	$⊢ ℙ ∖ \{2\} = O \cap ℙ$
151	150	eleq2i	$⊢ c (0) \in (ℙ ∖ \{2\}) \leftrightarrow c (0) \in (O \cap ℙ)$
152	149 151	sylnibr	$⊢ c \in A \to \neg c (0) \in (ℙ ∖ \{2\})$
153	138 152	syl	$⊢ (φ \land c \in A) \to \neg c (0) \in (ℙ ∖ \{2\})$
154	147 153	jca	$⊢ (φ \land c \in A) \to (c (0) \in (1 \dots N) \land \neg c (0) \in (ℙ ∖ \{2\}))$
155		eldif	$⊢ c (0) \in ((1 \dots N) ∖ (ℙ ∖ \{2\})) \leftrightarrow (c (0) \in (1 \dots N) \land \neg c (0) \in (ℙ ∖ \{2\}))$
156	154 155	sylibr	$⊢ (φ \land c \in A) \to c (0) \in ((1 \dots N) ∖ (ℙ ∖ \{2\}))$
157		uncom	$⊢ ((1 \dots N) ∖ ℙ) \cup \{2\} = \{2\} \cup ((1 \dots N) ∖ ℙ)$
158		undif3	$⊢ \{2\} \cup ((1 \dots N) ∖ ℙ) = (\{2\} \cup (1 \dots N)) ∖ (ℙ ∖ \{2\})$
159	157 158	eqtri	$⊢ ((1 \dots N) ∖ ℙ) \cup \{2\} = (\{2\} \cup (1 \dots N)) ∖ (ℙ ∖ \{2\})$
160		ssequn1	$⊢ \{2\} \subseteq (1 \dots N) \leftrightarrow \{2\} \cup (1 \dots N) = (1 \dots N)$
161	63 160	sylib	$⊢ φ \to \{2\} \cup (1 \dots N) = (1 \dots N)$
162	161	difeq1d	$⊢ φ \to (\{2\} \cup (1 \dots N)) ∖ (ℙ ∖ \{2\}) = (1 \dots N) ∖ (ℙ ∖ \{2\})$
163	159 162	eqtrid	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} = (1 \dots N) ∖ (ℙ ∖ \{2\})$
164	163	eleq2d	$⊢ φ \to (c (0) \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \leftrightarrow c (0) \in ((1 \dots N) ∖ (ℙ ∖ \{2\})))$
165	164	adantr	$⊢ (φ \land c \in A) \to (c (0) \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \leftrightarrow c (0) \in ((1 \dots N) ∖ (ℙ ∖ \{2\})))$
166	156 165	mpbird	$⊢ (φ \land c \in A) \to c (0) \in (((1 \dots N) ∖ ℙ) \cup \{2\})$
167	30	a1i	$⊢ (φ \land c \in A) \to 1 \in (0 ..^3)$
168	140 167	ffvelcdmd	$⊢ (φ \land c \in A) \to c (1) \in ℕ$
169	135 136 137 139 167	reprle	$⊢ (φ \land c \in A) \to c (1) \leq N$
170		elfz1b	$⊢ c (1) \in (1 \dots N) \leftrightarrow (c (1) \in ℕ \land N \in ℕ \land c (1) \leq N)$
171	170	biimpri	$⊢ (c (1) \in ℕ \land N \in ℕ \land c (1) \leq N) \to c (1) \in (1 \dots N)$
172	168 143 169 171	syl3anc	$⊢ (φ \land c \in A) \to c (1) \in (1 \dots N)$
173	166 172	opelxpd	$⊢ (φ \land c \in A) \to ⟨c (0), c (1)⟩ \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))$
174	173	ralrimiva	$⊢ φ \to \forall c \in A ⟨c (0), c (1)⟩ \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))$
175		fveq1	$⊢ d = c \to d (0) = c (0)$
176		fveq1	$⊢ d = c \to d (1) = c (1)$
177	175 176	opeq12d	$⊢ d = c \to ⟨d (0), d (1)⟩ = ⟨c (0), c (1)⟩$
178	177	cbvmptv	$⊢ (d \in A ⟼ ⟨d (0), d (1)⟩) = (c \in A ⟼ ⟨c (0), c (1)⟩)$
179	178	rnmptss	$⊢ \forall c \in A ⟨c (0), c (1)⟩ \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)) \to ran (d \in A ⟼ ⟨d (0), d (1)⟩) \subseteq (((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)$
180	174 179	syl	$⊢ φ \to ran (d \in A ⟼ ⟨d (0), d (1)⟩) \subseteq (((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)$
181	118 129 134 180	fsumless	$⊢ φ \to \sum_{u \in ran (d \in A ⟼ ⟨d (0), d (1)⟩)} Λ (1^{st} (u)) Λ (2^{nd} (u)) \leq \sum_{u \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)} Λ (1^{st} (u)) Λ (2^{nd} (u))$
182		fvex	$⊢ n (0) \in V$
183		fvex	$⊢ n (1) \in V$
184	182 183	op1std	$⊢ u = ⟨n (0), n (1)⟩ \to 1^{st} (u) = n (0)$
185	184	fveq2d	$⊢ u = ⟨n (0), n (1)⟩ \to Λ (1^{st} (u)) = Λ (n (0))$
186	182 183	op2ndd	$⊢ u = ⟨n (0), n (1)⟩ \to 2^{nd} (u) = n (1)$
187	186	fveq2d	$⊢ u = ⟨n (0), n (1)⟩ \to Λ (2^{nd} (u)) = Λ (n (1))$
188	185 187	oveq12d	$⊢ u = ⟨n (0), n (1)⟩ \to Λ (1^{st} (u)) Λ (2^{nd} (u)) = Λ (n (0)) Λ (n (1))$
189		opex	$⊢ ⟨c (0), c (1)⟩ \in V$
190	189	rgenw	$⊢ \forall c \in A ⟨c (0), c (1)⟩ \in V$
191	178	fnmpt	$⊢ \forall c \in A ⟨c (0), c (1)⟩ \in V \to (d \in A ⟼ ⟨d (0), d (1)⟩) Fn A$
192	190 191	mp1i	$⊢ φ \to (d \in A ⟼ ⟨d (0), d (1)⟩) Fn A$
193		eqidd	$⊢ φ \to ran (d \in A ⟼ ⟨d (0), d (1)⟩) = ran (d \in A ⟼ ⟨d (0), d (1)⟩)$
194	140	ad2antrr	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to c : (0 ..^3) ⟶ ℕ$
195	194	ffnd	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to c Fn (0 ..^3)$
196	21	ad4ant13	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to n : (0 ..^3) ⟶ ℕ$
197	196	ffnd	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to n Fn (0 ..^3)$
198		simpr	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)$
199	178	a1i	$⊢ φ \to (d \in A ⟼ ⟨d (0), d (1)⟩) = (c \in A ⟼ ⟨c (0), c (1)⟩)$
200	189	a1i	$⊢ (φ \land c \in A) \to ⟨c (0), c (1)⟩ \in V$
201	199 200	fvmpt2d	$⊢ (φ \land c \in A) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = ⟨c (0), c (1)⟩$
202	201	adantr	$⊢ ((φ \land c \in A) \land n \in A) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = ⟨c (0), c (1)⟩$
203	202	adantr	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = ⟨c (0), c (1)⟩$
204		fveq1	$⊢ c = n \to c (0) = n (0)$
205		fveq1	$⊢ c = n \to c (1) = n (1)$
206	204 205	opeq12d	$⊢ c = n \to ⟨c (0), c (1)⟩ = ⟨n (0), n (1)⟩$
207		opex	$⊢ ⟨n (0), n (1)⟩ \in V$
208	207	a1i	$⊢ (φ \land n \in A) \to ⟨n (0), n (1)⟩ \in V$
209	178 206 19 208	fvmptd3	$⊢ (φ \land n \in A) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (n) = ⟨n (0), n (1)⟩$
210	209	adantlr	$⊢ ((φ \land c \in A) \land n \in A) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (n) = ⟨n (0), n (1)⟩$
211	210	adantr	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (n) = ⟨n (0), n (1)⟩$
212	198 203 211	3eqtr3d	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to ⟨c (0), c (1)⟩ = ⟨n (0), n (1)⟩$
213	182 183	opth2	$⊢ ⟨c (0), c (1)⟩ = ⟨n (0), n (1)⟩ \leftrightarrow (c (0) = n (0) \land c (1) = n (1))$
214	212 213	sylib	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to (c (0) = n (0) \land c (1) = n (1))$
215	214	simpld	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to c (0) = n (0)$
216	215	ad2antrr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 0) \to c (0) = n (0)$
217		simpr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 0) \to i = 0$
218	217	fveq2d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 0) \to c (i) = c (0)$
219	217	fveq2d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 0) \to n (i) = n (0)$
220	216 218 219	3eqtr4d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 0) \to c (i) = n (i)$
221	214	simprd	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to c (1) = n (1)$
222	221	ad2antrr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 1) \to c (1) = n (1)$
223		simpr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 1) \to i = 1$
224	223	fveq2d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 1) \to c (i) = c (1)$
225	223	fveq2d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 1) \to n (i) = n (1)$
226	222 224 225	3eqtr4d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 1) \to c (i) = n (i)$
227	215	ad2antrr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (0) = n (0)$
228	221	ad2antrr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (1) = n (1)$
229	227 228	oveq12d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (0) + c (1) = n (0) + n (1)$
230	229	oveq2d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to N - (c (0) + c (1)) = N - (n (0) + n (1))$
231	24	a1i	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to (0 ..^3) = \{0, 1, 2\}$
232	231	sumeq1d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to \sum_{j \in (0 ..^3)} c (j) = \sum_{j \in \{0, 1, 2\}} c (j)$
233		ssidd	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to ℕ \subseteq ℕ$
234	136	ad4antr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to N \in ℤ$
235	6	a1i	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to 3 \in ℕ_{0}$
236	139	ad4antr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c \in (ℕ repr (3) N)$
237	233 234 235 236	reprsum	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to \sum_{j \in (0 ..^3)} c (j) = N$
238		fveq2	$⊢ j = 0 \to c (j) = c (0)$
239		fveq2	$⊢ j = 1 \to c (j) = c (1)$
240		fveq2	$⊢ j = 2 \to c (j) = c (2)$
241	142	nncnd	$⊢ (φ \land c \in A) \to c (0) \in ℂ$
242	241	ad4antr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (0) \in ℂ$
243	168	nncnd	$⊢ (φ \land c \in A) \to c (1) \in ℂ$
244	243	ad4antr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (1) \in ℂ$
245	36	a1i	$⊢ (φ \land c \in A) \to 2 \in (0 ..^3)$
246	140 245	ffvelcdmd	$⊢ (φ \land c \in A) \to c (2) \in ℕ$
247	246	nncnd	$⊢ (φ \land c \in A) \to c (2) \in ℂ$
248	247	ad4antr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (2) \in ℂ$
249	242 244 248	3jca	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to (c (0) \in ℂ \land c (1) \in ℂ \land c (2) \in ℂ)$
250		1ex	$⊢ 1 \in V$
251	22 250 34	3pm3.2i	$⊢ (0 \in V \land 1 \in V \land 2 \in V)$
252	251	a1i	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to (0 \in V \land 1 \in V \land 2 \in V)$
253		0ne1	$⊢ 0 \neq 1$
254	253	a1i	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to 0 \neq 1$
255		0ne2	$⊢ 0 \neq 2$
256	255	a1i	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to 0 \neq 2$
257		1ne2	$⊢ 1 \neq 2$
258	257	a1i	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to 1 \neq 2$
259	238 239 240 249 252 254 256 258	sumtp	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to \sum_{j \in \{0, 1, 2\}} c (j) = c (0) + c (1) + c (2)$
260	232 237 259	3eqtr3rd	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (0) + c (1) + c (2) = N$
261	242 244	addcld	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (0) + c (1) \in ℂ$
262	100	ad5antr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to N \in ℂ$
263	261 248 262	addrsub	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to (c (0) + c (1) + c (2) = N \leftrightarrow c (2) = N - (c (0) + c (1)))$
264	260 263	mpbid	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (2) = N - (c (0) + c (1))$
265	231	sumeq1d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to \sum_{j \in (0 ..^3)} n (j) = \sum_{j \in \{0, 1, 2\}} n (j)$
266	20	ad4ant13	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to n \in (ℕ repr (3) N)$
267	266	ad2antrr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to n \in (ℕ repr (3) N)$
268	233 234 235 267	reprsum	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to \sum_{j \in (0 ..^3)} n (j) = N$
269		fveq2	$⊢ j = 0 \to n (j) = n (0)$
270		fveq2	$⊢ j = 1 \to n (j) = n (1)$
271		fveq2	$⊢ j = 2 \to n (j) = n (2)$
272	27	nncnd	$⊢ (φ \land n \in A) \to n (0) \in ℂ$
273	272	adantlr	$⊢ ((φ \land c \in A) \land n \in A) \to n (0) \in ℂ$
274	273	ad3antrrr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to n (0) \in ℂ$
275	32	nncnd	$⊢ (φ \land n \in A) \to n (1) \in ℂ$
276	275	adantlr	$⊢ ((φ \land c \in A) \land n \in A) \to n (1) \in ℂ$
277	276	ad3antrrr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to n (1) \in ℂ$
278	38	nncnd	$⊢ (φ \land n \in A) \to n (2) \in ℂ$
279	278	adantlr	$⊢ ((φ \land c \in A) \land n \in A) \to n (2) \in ℂ$
280	279	ad3antrrr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to n (2) \in ℂ$
281	274 277 280	3jca	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to (n (0) \in ℂ \land n (1) \in ℂ \land n (2) \in ℂ)$
282	269 270 271 281 252 254 256 258	sumtp	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to \sum_{j \in \{0, 1, 2\}} n (j) = n (0) + n (1) + n (2)$
283	265 268 282	3eqtr3rd	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to n (0) + n (1) + n (2) = N$
284	274 277	addcld	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to n (0) + n (1) \in ℂ$
285	284 280 262	addrsub	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to (n (0) + n (1) + n (2) = N \leftrightarrow n (2) = N - (n (0) + n (1)))$
286	283 285	mpbid	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to n (2) = N - (n (0) + n (1))$
287	230 264 286	3eqtr4d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (2) = n (2)$
288		simpr	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to i = 2$
289	288	fveq2d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (i) = c (2)$
290	288	fveq2d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to n (i) = n (2)$
291	287 289 290	3eqtr4d	$⊢ (((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \land i = 2) \to c (i) = n (i)$
292		simpr	$⊢ ((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \to i \in (0 ..^3)$
293	292 24	eleqtrdi	$⊢ ((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \to i \in \{0, 1, 2\}$
294		vex	$⊢ i \in V$
295	294	eltp	$⊢ i \in \{0, 1, 2\} \leftrightarrow (i = 0 \lor i = 1 \lor i = 2)$
296	293 295	sylib	$⊢ ((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \to (i = 0 \lor i = 1 \lor i = 2)$
297	220 226 291 296	mpjao3dan	$⊢ ((((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \land i \in (0 ..^3)) \to c (i) = n (i)$
298	195 197 297	eqfnfvd	$⊢ (((φ \land c \in A) \land n \in A) \land (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n)) \to c = n$
299	298	ex	$⊢ ((φ \land c \in A) \land n \in A) \to ((d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n) \to c = n)$
300	299	anasss	$⊢ (φ \land (c \in A \land n \in A)) \to ((d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n) \to c = n)$
301	300	ralrimivva	$⊢ φ \to \forall c \in A \forall n \in A ((d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n) \to c = n)$
302		dff1o6	$⊢ (d \in A ⟼ ⟨d (0), d (1)⟩) : A \underset{1-1 onto}{⟶} ran (d \in A ⟼ ⟨d (0), d (1)⟩) \leftrightarrow ((d \in A ⟼ ⟨d (0), d (1)⟩) Fn A \land ran (d \in A ⟼ ⟨d (0), d (1)⟩) = ran (d \in A ⟼ ⟨d (0), d (1)⟩) \land \forall c \in A \forall n \in A ((d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n) \to c = n))$
303	302	biimpri	$⊢ ((d \in A ⟼ ⟨d (0), d (1)⟩) Fn A \land ran (d \in A ⟼ ⟨d (0), d (1)⟩) = ran (d \in A ⟼ ⟨d (0), d (1)⟩) \land \forall c \in A \forall n \in A ((d \in A ⟼ ⟨d (0), d (1)⟩) (c) = (d \in A ⟼ ⟨d (0), d (1)⟩) (n) \to c = n)) \to (d \in A ⟼ ⟨d (0), d (1)⟩) : A \underset{1-1 onto}{⟶} ran (d \in A ⟼ ⟨d (0), d (1)⟩)$
304	192 193 301 303	syl3anc	$⊢ φ \to (d \in A ⟼ ⟨d (0), d (1)⟩) : A \underset{1-1 onto}{⟶} ran (d \in A ⟼ ⟨d (0), d (1)⟩)$
305	180	sselda	$⊢ (φ \land u \in ran (d \in A ⟼ ⟨d (0), d (1)⟩)) \to u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))$
306	305 124	syldan	$⊢ (φ \land u \in ran (d \in A ⟼ ⟨d (0), d (1)⟩)) \to Λ (1^{st} (u)) \in ℝ$
307	305 128	syldan	$⊢ (φ \land u \in ran (d \in A ⟼ ⟨d (0), d (1)⟩)) \to Λ (2^{nd} (u)) \in ℝ$
308	306 307	remulcld	$⊢ (φ \land u \in ran (d \in A ⟼ ⟨d (0), d (1)⟩)) \to Λ (1^{st} (u)) Λ (2^{nd} (u)) \in ℝ$
309	308	recnd	$⊢ (φ \land u \in ran (d \in A ⟼ ⟨d (0), d (1)⟩)) \to Λ (1^{st} (u)) Λ (2^{nd} (u)) \in ℂ$
310	188 12 304 209 309	fsumf1o	$⊢ φ \to \sum_{u \in ran (d \in A ⟼ ⟨d (0), d (1)⟩)} Λ (1^{st} (u)) Λ (2^{nd} (u)) = \sum_{n \in A} Λ (n (0)) Λ (n (1))$
311	75	recnd	$⊢ φ \to \sum_{j = 1}^{N} Λ (j) \in ℂ$
312	69	recnd	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to Λ (i) \in ℂ$
313	54 311 312	fsummulc1	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) = \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j)$
314	48	a1i	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to (1 \dots N) \in Fin$
315	74	adantrl	$⊢ (φ \land (i \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \land j \in (1 \dots N))) \to Λ (j) \in ℝ$
316	315	anassrs	$⊢ ((φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \land j \in (1 \dots N)) \to Λ (j) \in ℝ$
317	316	recnd	$⊢ ((φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \land j \in (1 \dots N)) \to Λ (j) \in ℂ$
318	314 312 317	fsummulc2	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to Λ (i) \sum_{j = 1}^{N} Λ (j) = \sum_{j = 1}^{N} Λ (i) Λ (j)$
319	318	sumeq2dv	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) = \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} \sum_{j = 1}^{N} Λ (i) Λ (j)$
320		vex	$⊢ j \in V$
321	294 320	op1std	$⊢ u = ⟨i, j⟩ \to 1^{st} (u) = i$
322	321	fveq2d	$⊢ u = ⟨i, j⟩ \to Λ (1^{st} (u)) = Λ (i)$
323	294 320	op2ndd	$⊢ u = ⟨i, j⟩ \to 2^{nd} (u) = j$
324	323	fveq2d	$⊢ u = ⟨i, j⟩ \to Λ (2^{nd} (u)) = Λ (j)$
325	322 324	oveq12d	$⊢ u = ⟨i, j⟩ \to Λ (1^{st} (u)) Λ (2^{nd} (u)) = Λ (i) Λ (j)$
326	69	adantrr	$⊢ (φ \land (i \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \land j \in (1 \dots N))) \to Λ (i) \in ℝ$
327	326 315	remulcld	$⊢ (φ \land (i \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \land j \in (1 \dots N))) \to Λ (i) Λ (j) \in ℝ$
328	327	recnd	$⊢ (φ \land (i \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \land j \in (1 \dots N))) \to Λ (i) Λ (j) \in ℂ$
329	325 54 71 328	fsumxp	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} \sum_{j = 1}^{N} Λ (i) Λ (j) = \sum_{u \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)} Λ (1^{st} (u)) Λ (2^{nd} (u))$
330	313 319 329	3eqtrrd	$⊢ φ \to \sum_{u \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)} Λ (1^{st} (u)) Λ (2^{nd} (u)) = \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j)$
331	181 310 330	3brtr3d	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) \leq \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j)$
332	46 76 44 116 331	lemul2ad	$⊢ φ \to \log N \sum_{n \in A} Λ (n (0)) Λ (n (1)) \leq \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j)$
333	42 47 77 113 332	letrd	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j)$

Metamath Proof Explorer

Theorem hgt750lemb

Proof