Theorem 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	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
	hgt750leme.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	hgt750lemb.2	⊢ ( 𝜑 → 2 ≤ 𝑁 )
	hgt750lemb.a	⊢ 𝐴 = { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) }
Assertion	hgt750lemb	⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) )

Proof

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