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	ffvelrnd	$⊢ (φ \land n \in A) \to n (0) \in ℕ$
28	14 27	ffvelrnd	$⊢ (φ \land n \in A) \to Λ (n (0)) \in ℝ$
29		1ex	$⊢ 1 \in V$
30	29	tpid2	$⊢ 1 \in \{0, 1, 2\}$
31	30 24	eleqtrri	$⊢ 1 \in (0 ..^3)$
32	31	a1i	$⊢ (φ \land n \in A) \to 1 \in (0 ..^3)$
33	21 32	ffvelrnd	$⊢ (φ \land n \in A) \to n (1) \in ℕ$
34	14 33	ffvelrnd	$⊢ (φ \land n \in A) \to Λ (n (1)) \in ℝ$
35		2ex	$⊢ 2 \in V$
36	35	tpid3	$⊢ 2 \in \{0, 1, 2\}$
37	36 24	eleqtrri	$⊢ 2 \in (0 ..^3)$
38	37	a1i	$⊢ (φ \land n \in A) \to 2 \in (0 ..^3)$
39	21 38	ffvelrnd	$⊢ (φ \land n \in A) \to n (2) \in ℕ$
40	14 39	ffvelrnd	$⊢ (φ \land n \in A) \to Λ (n (2)) \in ℝ$
41	34 40	remulcld	$⊢ (φ \land n \in A) \to Λ (n (1)) Λ (n (2)) \in ℝ$
42	28 41	remulcld	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
43	12 42	fsumrecl	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
44	2	nnrpd	$⊢ φ \to N \in ℝ^{+}$
45	44	relogcld	$⊢ φ \to \log N \in ℝ$
46	28 34	remulcld	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) \in ℝ$
47	12 46	fsumrecl	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) \in ℝ$
48	45 47	remulcld	$⊢ φ \to \log N \sum_{n \in A} Λ (n (0)) Λ (n (1)) \in ℝ$
49		fzfi	$⊢ (1 \dots N) \in Fin$
50		diffi	$⊢ (1 \dots N) \in Fin \to (1 \dots N) ∖ ℙ \in Fin$
51	49 50	ax-mp	$⊢ (1 \dots N) ∖ ℙ \in Fin$
52		snfi	$⊢ \{2\} \in Fin$
53		unfi	$⊢ ((1 \dots N) ∖ ℙ \in Fin \land \{2\} \in Fin) \to ((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin$
54	51 52 53	mp2an	$⊢ ((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin$
55	54	a1i	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin$
56	13	a1i	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to Λ : ℕ ⟶ ℝ$
57		difss	$⊢ (1 \dots N) ∖ ℙ \subseteq (1 \dots N)$
58	57	a1i	$⊢ φ \to (1 \dots N) ∖ ℙ \subseteq (1 \dots N)$
59		2nn	$⊢ 2 \in ℕ$
60	59	a1i	$⊢ φ \to 2 \in ℕ$
61		elfz1b	$⊢ 2 \in (1 \dots N) \leftrightarrow (2 \in ℕ \land N \in ℕ \land 2 \leq N)$
62	61	biimpri	$⊢ (2 \in ℕ \land N \in ℕ \land 2 \leq N) \to 2 \in (1 \dots N)$
63	60 2 3 62	syl3anc	$⊢ φ \to 2 \in (1 \dots N)$
64	63	snssd	$⊢ φ \to \{2\} \subseteq (1 \dots N)$
65	58 64	unssd	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} \subseteq (1 \dots N)$
66		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
67	66	a1i	$⊢ φ \to (1 \dots N) \subseteq ℕ$
68	65 67	sstrd	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} \subseteq ℕ$
69	68	sselda	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to i \in ℕ$
70	56 69	ffvelrnd	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to Λ (i) \in ℝ$
71	55 70	fsumrecl	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \in ℝ$
72		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
73	13	a1i	$⊢ (φ \land j \in (1 \dots N)) \to Λ : ℕ ⟶ ℝ$
74	67	sselda	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℕ$
75	73 74	ffvelrnd	$⊢ (φ \land j \in (1 \dots N)) \to Λ (j) \in ℝ$
76	72 75	fsumrecl	$⊢ φ \to \sum_{j = 1}^{N} Λ (j) \in ℝ$
77	71 76	remulcld	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \in ℝ$
78	45 77	remulcld	$⊢ φ \to \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \in ℝ$
79	2	adantr	$⊢ (φ \land n \in A) \to N \in ℕ$
80	79	nnrpd	$⊢ (φ \land n \in A) \to N \in ℝ^{+}$
81		relogcl	$⊢ N \in ℝ^{+} \to \log N \in ℝ$
82	80 81	syl	$⊢ (φ \land n \in A) \to \log N \in ℝ$
83	34 82	remulcld	$⊢ (φ \land n \in A) \to Λ (n (1)) \log N \in ℝ$
84	28 83	remulcld	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) \log N \in ℝ$
85		vmage0	$⊢ n (0) \in ℕ \to 0 \leq Λ (n (0))$
86	27 85	syl	$⊢ (φ \land n \in A) \to 0 \leq Λ (n (0))$
87		vmage0	$⊢ n (1) \in ℕ \to 0 \leq Λ (n (1))$
88	33 87	syl	$⊢ (φ \land n \in A) \to 0 \leq Λ (n (1))$
89	39	nnrpd	$⊢ (φ \land n \in A) \to n (2) \in ℝ^{+}$
90	89	relogcld	$⊢ (φ \land n \in A) \to \log n (2) \in ℝ$
91		vmalelog	$⊢ n (2) \in ℕ \to Λ (n (2)) \leq \log n (2)$
92	39 91	syl	$⊢ (φ \land n \in A) \to Λ (n (2)) \leq \log n (2)$
93	15 17 18 20 38	reprle	$⊢ (φ \land n \in A) \to n (2) \leq N$
94		logleb	$⊢ (n (2) \in ℝ^{+} \land N \in ℝ^{+}) \to (n (2) \leq N \leftrightarrow \log n (2) \leq \log N)$
95	94	biimpa	$⊢ ((n (2) \in ℝ^{+} \land N \in ℝ^{+}) \land n (2) \leq N) \to \log n (2) \leq \log N$
96	89 80 93 95	syl21anc	$⊢ (φ \land n \in A) \to \log n (2) \leq \log N$
97	40 90 82 92 96	letrd	$⊢ (φ \land n \in A) \to Λ (n (2)) \leq \log N$
98	40 82 34 88 97	lemul2ad	$⊢ (φ \land n \in A) \to Λ (n (1)) Λ (n (2)) \leq Λ (n (1)) \log N$
99	41 83 28 86 98	lemul2ad	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq Λ (n (0)) Λ (n (1)) \log N$
100	12 42 84 99	fsumle	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq \sum_{n \in A} Λ (n (0)) Λ (n (1)) \log N$
101	2	nncnd	$⊢ φ \to N \in ℂ$
102	2	nnne0d	$⊢ φ \to N \neq 0$
103	101 102	logcld	$⊢ φ \to \log N \in ℂ$
104	46	recnd	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) \in ℂ$
105	12 103 104	fsummulc2	$⊢ φ \to \log N \sum_{n \in A} Λ (n (0)) Λ (n (1)) = \sum_{n \in A} \log N Λ (n (0)) Λ (n (1))$
106	103	adantr	$⊢ (φ \land n \in A) \to \log N \in ℂ$
107	106 104	mulcomd	$⊢ (φ \land n \in A) \to \log N Λ (n (0)) Λ (n (1)) = Λ (n (0)) Λ (n (1)) \log N$
108	28	recnd	$⊢ (φ \land n \in A) \to Λ (n (0)) \in ℂ$
109	34	recnd	$⊢ (φ \land n \in A) \to Λ (n (1)) \in ℂ$
110	108 109 106	mulassd	$⊢ (φ \land n \in A) \to Λ (n (0)) Λ (n (1)) \log N = Λ (n (0)) Λ (n (1)) \log N$
111	107 110	eqtrd	$⊢ (φ \land n \in A) \to \log N Λ (n (0)) Λ (n (1)) = Λ (n (0)) Λ (n (1)) \log N$
112	111	sumeq2dv	$⊢ φ \to \sum_{n \in A} \log N Λ (n (0)) Λ (n (1)) = \sum_{n \in A} Λ (n (0)) Λ (n (1)) \log N$
113	105 112	eqtr2d	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) \log N = \log N \sum_{n \in A} Λ (n (0)) Λ (n (1))$
114	100 113	breqtrd	$⊢ φ \to \sum_{n \in A} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq \log N \sum_{n \in A} Λ (n (0)) Λ (n (1))$
115	2	nnred	$⊢ φ \to N \in ℝ$
116	2	nnge1d	$⊢ φ \to 1 \leq N$
117	115 116	logge0d	$⊢ φ \to 0 \leq \log N$
118		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$
119	55 72 118	syl2anc	$⊢ φ \to (((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N) \in Fin$
120	13	a1i	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to Λ : ℕ ⟶ ℝ$
121	68	adantr	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to ((1 \dots N) ∖ ℙ) \cup \{2\} \subseteq ℕ$
122		xp1st	$⊢ u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)) \to 1^{st} (u) \in (((1 \dots N) ∖ ℙ) \cup \{2\})$
123	122	adantl	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 1^{st} (u) \in (((1 \dots N) ∖ ℙ) \cup \{2\})$
124	121 123	sseldd	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 1^{st} (u) \in ℕ$
125	120 124	ffvelrnd	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to Λ (1^{st} (u)) \in ℝ$
126		xp2nd	$⊢ u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)) \to 2^{nd} (u) \in (1 \dots N)$
127	126	adantl	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 2^{nd} (u) \in (1 \dots N)$
128	66 127	sselid	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 2^{nd} (u) \in ℕ$
129	120 128	ffvelrnd	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to Λ (2^{nd} (u)) \in ℝ$
130	125 129	remulcld	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to Λ (1^{st} (u)) Λ (2^{nd} (u)) \in ℝ$
131		vmage0	$⊢ 1^{st} (u) \in ℕ \to 0 \leq Λ (1^{st} (u))$
132	124 131	syl	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 0 \leq Λ (1^{st} (u))$
133		vmage0	$⊢ 2^{nd} (u) \in ℕ \to 0 \leq Λ (2^{nd} (u))$
134	128 133	syl	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 0 \leq Λ (2^{nd} (u))$
135	125 129 132 134	mulge0d	$⊢ (φ \land u \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))) \to 0 \leq Λ (1^{st} (u)) Λ (2^{nd} (u))$
136		ssidd	$⊢ (φ \land c \in A) \to ℕ \subseteq ℕ$
137	16	adantr	$⊢ (φ \land c \in A) \to N \in ℤ$
138	6	a1i	$⊢ (φ \land c \in A) \to 3 \in ℕ_{0}$
139		simpr	$⊢ (φ \land c \in A) \to c \in A$
140	10 139	sselid	$⊢ (φ \land c \in A) \to c \in (ℕ repr (3) N)$
141	136 137 138 140	reprf	$⊢ (φ \land c \in A) \to c : (0 ..^3) ⟶ ℕ$
142	25	a1i	$⊢ (φ \land c \in A) \to 0 \in (0 ..^3)$
143	141 142	ffvelrnd	$⊢ (φ \land c \in A) \to c (0) \in ℕ$
144	2	adantr	$⊢ (φ \land c \in A) \to N \in ℕ$
145	136 137 138 140 142	reprle	$⊢ (φ \land c \in A) \to c (0) \leq N$
146		elfz1b	$⊢ c (0) \in (1 \dots N) \leftrightarrow (c (0) \in ℕ \land N \in ℕ \land c (0) \leq N)$
147	146	biimpri	$⊢ (c (0) \in ℕ \land N \in ℕ \land c (0) \leq N) \to c (0) \in (1 \dots N)$
148	143 144 145 147	syl3anc	$⊢ (φ \land c \in A) \to c (0) \in (1 \dots N)$
149	4	rabeq2i	$⊢ c \in A \leftrightarrow (c \in (ℕ repr (3) N) \land \neg c (0) \in (O \cap ℙ))$
150	149	simprbi	$⊢ c \in A \to \neg c (0) \in (O \cap ℙ)$
151	1	oddprm2	$⊢ ℙ ∖ \{2\} = O \cap ℙ$
152	151	eleq2i	$⊢ c (0) \in (ℙ ∖ \{2\}) \leftrightarrow c (0) \in (O \cap ℙ)$
153	150 152	sylnibr	$⊢ c \in A \to \neg c (0) \in (ℙ ∖ \{2\})$
154	139 153	syl	$⊢ (φ \land c \in A) \to \neg c (0) \in (ℙ ∖ \{2\})$
155	148 154	jca	$⊢ (φ \land c \in A) \to (c (0) \in (1 \dots N) \land \neg c (0) \in (ℙ ∖ \{2\}))$
156		eldif	$⊢ c (0) \in ((1 \dots N) ∖ (ℙ ∖ \{2\})) \leftrightarrow (c (0) \in (1 \dots N) \land \neg c (0) \in (ℙ ∖ \{2\}))$
157	155 156	sylibr	$⊢ (φ \land c \in A) \to c (0) \in ((1 \dots N) ∖ (ℙ ∖ \{2\}))$
158		uncom	$⊢ ((1 \dots N) ∖ ℙ) \cup \{2\} = \{2\} \cup ((1 \dots N) ∖ ℙ)$
159		undif3	$⊢ \{2\} \cup ((1 \dots N) ∖ ℙ) = (\{2\} \cup (1 \dots N)) ∖ (ℙ ∖ \{2\})$
160	158 159	eqtri	$⊢ ((1 \dots N) ∖ ℙ) \cup \{2\} = (\{2\} \cup (1 \dots N)) ∖ (ℙ ∖ \{2\})$
161		ssequn1	$⊢ \{2\} \subseteq (1 \dots N) \leftrightarrow \{2\} \cup (1 \dots N) = (1 \dots N)$
162	64 161	sylib	$⊢ φ \to \{2\} \cup (1 \dots N) = (1 \dots N)$
163	162	difeq1d	$⊢ φ \to (\{2\} \cup (1 \dots N)) ∖ (ℙ ∖ \{2\}) = (1 \dots N) ∖ (ℙ ∖ \{2\})$
164	160 163	syl5eq	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} = (1 \dots N) ∖ (ℙ ∖ \{2\})$
165	164	eleq2d	$⊢ φ \to (c (0) \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \leftrightarrow c (0) \in ((1 \dots N) ∖ (ℙ ∖ \{2\})))$
166	165	adantr	$⊢ (φ \land c \in A) \to (c (0) \in (((1 \dots N) ∖ ℙ) \cup \{2\}) \leftrightarrow c (0) \in ((1 \dots N) ∖ (ℙ ∖ \{2\})))$
167	157 166	mpbird	$⊢ (φ \land c \in A) \to c (0) \in (((1 \dots N) ∖ ℙ) \cup \{2\})$
168	31	a1i	$⊢ (φ \land c \in A) \to 1 \in (0 ..^3)$
169	141 168	ffvelrnd	$⊢ (φ \land c \in A) \to c (1) \in ℕ$
170	136 137 138 140 168	reprle	$⊢ (φ \land c \in A) \to c (1) \leq N$
171		elfz1b	$⊢ c (1) \in (1 \dots N) \leftrightarrow (c (1) \in ℕ \land N \in ℕ \land c (1) \leq N)$
172	171	biimpri	$⊢ (c (1) \in ℕ \land N \in ℕ \land c (1) \leq N) \to c (1) \in (1 \dots N)$
173	169 144 170 172	syl3anc	$⊢ (φ \land c \in A) \to c (1) \in (1 \dots N)$
174	167 173	opelxpd	$⊢ (φ \land c \in A) \to ⟨c (0), c (1)⟩ \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))$
175	174	ralrimiva	$⊢ φ \to \forall c \in A ⟨c (0), c (1)⟩ \in ((((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N))$
176		fveq1	$⊢ d = c \to d (0) = c (0)$
177		fveq1	$⊢ d = c \to d (1) = c (1)$
178	176 177	opeq12d	$⊢ d = c \to ⟨d (0), d (1)⟩ = ⟨c (0), c (1)⟩$
179	178	cbvmptv	$⊢ (d \in A ⟼ ⟨d (0), d (1)⟩) = (c \in A ⟼ ⟨c (0), c (1)⟩)$
180	179	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)$
181	175 180	syl	$⊢ φ \to ran (d \in A ⟼ ⟨d (0), d (1)⟩) \subseteq (((1 \dots N) ∖ ℙ) \cup \{2\}) \times (1 \dots N)$
182	119 130 135 181	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))$
183		fvex	$⊢ n (0) \in V$
184		fvex	$⊢ n (1) \in V$
185	183 184	op1std	$⊢ u = ⟨n (0), n (1)⟩ \to 1^{st} (u) = n (0)$
186	185	fveq2d	$⊢ u = ⟨n (0), n (1)⟩ \to Λ (1^{st} (u)) = Λ (n (0))$
187	183 184	op2ndd	$⊢ u = ⟨n (0), n (1)⟩ \to 2^{nd} (u) = n (1)$
188	187	fveq2d	$⊢ u = ⟨n (0), n (1)⟩ \to Λ (2^{nd} (u)) = Λ (n (1))$
189	186 188	oveq12d	$⊢ u = ⟨n (0), n (1)⟩ \to Λ (1^{st} (u)) Λ (2^{nd} (u)) = Λ (n (0)) Λ (n (1))$
190		opex	$⊢ ⟨c (0), c (1)⟩ \in V$
191	190	rgenw	$⊢ \forall c \in A ⟨c (0), c (1)⟩ \in V$
192	179	fnmpt	$⊢ \forall c \in A ⟨c (0), c (1)⟩ \in V \to (d \in A ⟼ ⟨d (0), d (1)⟩) Fn A$
193	191 192	mp1i	$⊢ φ \to (d \in A ⟼ ⟨d (0), d (1)⟩) Fn A$
194		eqidd	$⊢ φ \to ran (d \in A ⟼ ⟨d (0), d (1)⟩) = ran (d \in A ⟼ ⟨d (0), d (1)⟩)$
195	141	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) ⟶ ℕ$
196	195	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)$
197	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) ⟶ ℕ$
198	197	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)$
199		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)$
200	179	a1i	$⊢ φ \to (d \in A ⟼ ⟨d (0), d (1)⟩) = (c \in A ⟼ ⟨c (0), c (1)⟩)$
201	190	a1i	$⊢ (φ \land c \in A) \to ⟨c (0), c (1)⟩ \in V$
202	200 201	fvmpt2d	$⊢ (φ \land c \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) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (c) = ⟨c (0), c (1)⟩$
204	203	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)⟩$
205		fveq1	$⊢ c = n \to c (0) = n (0)$
206		fveq1	$⊢ c = n \to c (1) = n (1)$
207	205 206	opeq12d	$⊢ c = n \to ⟨c (0), c (1)⟩ = ⟨n (0), n (1)⟩$
208		opex	$⊢ ⟨n (0), n (1)⟩ \in V$
209	208	a1i	$⊢ (φ \land n \in A) \to ⟨n (0), n (1)⟩ \in V$
210	179 207 19 209	fvmptd3	$⊢ (φ \land n \in A) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (n) = ⟨n (0), n (1)⟩$
211	210	adantlr	$⊢ ((φ \land c \in A) \land n \in A) \to (d \in A ⟼ ⟨d (0), d (1)⟩) (n) = ⟨n (0), n (1)⟩$
212	211	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)⟩$
213	199 204 212	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)⟩$
214	183 184	opth2	$⊢ ⟨c (0), c (1)⟩ = ⟨n (0), n (1)⟩ \leftrightarrow (c (0) = n (0) \land c (1) = n (1))$
215	213 214	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))$
216	215	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)$
217	216	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)$
218		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$
219	218	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)$
220	218	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)$
221	217 219 220	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)$
222	215	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)$
223	222	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)$
224		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$
225	224	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)$
226	224	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)$
227	223 225 226	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)$
228	216	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)$
229	222	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)$
230	228 229	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)$
231	230	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))$
232	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\}$
233	232	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)$
234		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 ℕ$
235	137	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 ℤ$
236	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}$
237	140	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)$
238	234 235 236 237	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$
239		fveq2	$⊢ j = 0 \to c (j) = c (0)$
240		fveq2	$⊢ j = 1 \to c (j) = c (1)$
241		fveq2	$⊢ j = 2 \to c (j) = c (2)$
242	143	nncnd	$⊢ (φ \land c \in A) \to c (0) \in ℂ$
243	242	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 ℂ$
244	169	nncnd	$⊢ (φ \land c \in A) \to c (1) \in ℂ$
245	244	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 ℂ$
246	37	a1i	$⊢ (φ \land c \in A) \to 2 \in (0 ..^3)$
247	141 246	ffvelrnd	$⊢ (φ \land c \in A) \to c (2) \in ℕ$
248	247	nncnd	$⊢ (φ \land c \in A) \to c (2) \in ℂ$
249	248	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 ℂ$
250	243 245 249	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 ℂ)$
251	22 29 35	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	239 240 241 250 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	233 238 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	243 245	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	101	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 249 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	232	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	234 235 236 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	33	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	39	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	231 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	221 227 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	196 198 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	193 194 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	181	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 125	syldan	$⊢ (φ \land u \in ran (d \in A ⟼ ⟨d (0), d (1)⟩)) \to Λ (1^{st} (u)) \in ℝ$
307	305 129	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	189 12 304 210 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	76	recnd	$⊢ φ \to \sum_{j = 1}^{N} Λ (j) \in ℂ$
312	70	recnd	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to Λ (i) \in ℂ$
313	55 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	49	a1i	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to (1 \dots N) \in Fin$
315	75	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	70	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 55 72 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	182 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	47 77 45 117 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	43 48 78 114 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