hgt750lemb - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hgt750lemb		Structured version Visualization version GIF version

Theorem hgt750lemb 35205

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.)

**Hypotheses**
Ref	Expression
hgt750leme.o	⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
hgt750leme.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
hgt750lemb.2	⊢ (𝜑 → 2 ≤ 𝑁)
hgt750lemb.a	⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}

**Assertion**
Ref	Expression
hgt750lemb	⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))

Distinct variable groups: 𝑧,𝑂 𝐴,𝑐,𝑖,𝑗,𝑛 𝑁,𝑐,𝑖,𝑗,𝑛 𝜑,𝑐,𝑖,𝑗,𝑛 Allowed substitution hints: 𝜑(𝑧) 𝐴(𝑧) 𝑁(𝑧) 𝑂(𝑖, 𝑗, 𝑛, 𝑐)

Proof of Theorem hgt750lemb Dummy variables 𝑑 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hgt750leme.n	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2	1	nnnn0d 12622	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		3nn0 12579	. . . . . 6 ⊢ 3 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ₀)
5		ssidd 3954	. . . . 5 ⊢ (𝜑 → ℕ ⊆ ℕ)
6	2, 4, 5	reprfi2 35172	. . . 4 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
7		hgt750lemb.a	. . . . 5 ⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
8	7	ssrab3 4030	. . . 4 ⊢ 𝐴 ⊆ (ℕ(repr‘3)𝑁)
9		ssfi 9167	. . . 4 ⊢ (((ℕ(repr‘3)𝑁) ∈ Fin ∧ 𝐴 ⊆ (ℕ(repr‘3)𝑁)) → 𝐴 ∈ Fin)
10	6, 8, 9	sylancl 598	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
11		vmaf 27395	. . . . . 6 ⊢ Λ:ℕ⟶ℝ
12	11	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → Λ:ℕ⟶ℝ)
13		ssidd 3954	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ℕ ⊆ ℕ)
14	1	nnzd 12674	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
15	14	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℤ)
16	3	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 3 ∈ ℕ₀)
17		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ 𝐴)
18	8, 17	sselid 3929	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
19	13, 15, 16, 18	reprf 35161	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛:(0..^3)⟶ℕ)
20		c0ex 11257	. . . . . . . . 9 ⊢ 0 ∈ V
21	20	tpid1 4729	. . . . . . . 8 ⊢ 0 ∈ {0, 1, 2}
22		fzo0to3tp 13841	. . . . . . . 8 ⊢ (0..^3) = {0, 1, 2}
23	21, 22	eleqtrri 2859	. . . . . . 7 ⊢ 0 ∈ (0..^3)
24	23	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ∈ (0..^3))
25	19, 24	ffvelcdmd 7074	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℕ)
26	12, 25	ffvelcdmd 7074	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℝ)
27		1eltp012 12368	. . . . . . . . 9 ⊢ 1 ∈ {0, 1, 2}
28	27, 22	eleqtrri 2859	. . . . . . . 8 ⊢ 1 ∈ (0..^3)
29	28	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 1 ∈ (0..^3))
30	19, 29	ffvelcdmd 7074	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℕ)
31	12, 30	ffvelcdmd 7074	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℝ)
32		2ex 12375	. . . . . . . . . 10 ⊢ 2 ∈ V
33	32	tpid3 4734	. . . . . . . . 9 ⊢ 2 ∈ {0, 1, 2}
34	33, 22	eleqtrri 2859	. . . . . . . 8 ⊢ 2 ∈ (0..^3)
35	34	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 2 ∈ (0..^3))
36	19, 35	ffvelcdmd 7074	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℕ)
37	12, 36	ffvelcdmd 7074	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ∈ ℝ)
38	31, 37	remulcld 11296	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
39	26, 38	remulcld 11296	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
40	10, 39	fsumrecl 15853	. 2 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
41	1	nnrpd 13117	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
42	41	relogcld 26900	. . 3 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
43	26, 31	remulcld 11296	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
44	10, 43	fsumrecl 15853	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
45	42, 44	remulcld 11296	. 2 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ∈ ℝ)
46		fzfi 14069	. . . . . . . 8 ⊢ (1...𝑁) ∈ Fin
47		diffi 9169	. . . . . . . 8 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
48	46, 47	ax-mp 5	. . . . . . 7 ⊢ ((1...𝑁) ∖ ℙ) ∈ Fin
49		snfi 9050	. . . . . . 7 ⊢ {2} ∈ Fin
50		unfi 9165	. . . . . . 7 ⊢ ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
51	48, 49, 50	mp2an 705	. . . . . 6 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
52	51	a1i 11	. . . . 5 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
53	11	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
54		difss 4083	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁)
55	54	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁))
56		2nn 12371	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
57	56	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ)
58		hgt750lemb.2	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 𝑁)
59		elfz1b 13681	. . . . . . . . . . . 12 ⊢ (2 ∈ (1...𝑁) ↔ (2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁))
60	59	biimpri 231	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁) → 2 ∈ (1...𝑁))
61	57, 1, 58, 60	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ (1...𝑁))
62	61	snssd 4747	. . . . . . . . 9 ⊢ (𝜑 → {2} ⊆ (1...𝑁))
63	55, 62	unssd 4138	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ (1...𝑁))
64		fz1ssnn 13643	. . . . . . . . 9 ⊢ (1...𝑁) ⊆ ℕ
65	64	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
66	63, 65	sstrd 3941	. . . . . . 7 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
67	66	sselda 3931	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
68	53, 67	ffvelcdmd 7074	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
69	52, 68	fsumrecl 15853	. . . 4 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
70		fzfid 14070	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
71	11	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
72	65	sselda 3931	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
73	71, 72	ffvelcdmd 7074	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
74	70, 73	fsumrecl 15853	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
75	69, 74	remulcld 11296	. . 3 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
76	42, 75	remulcld 11296	. 2 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
77	1	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℕ)
78	77	nnrpd 13117	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℝ⁺)
79		relogcl 26852	. . . . . . 7 ⊢ (𝑁 ∈ ℝ⁺ → (log‘𝑁) ∈ ℝ)
80	78, 79	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℝ)
81	31, 80	remulcld 11296	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (log‘𝑁)) ∈ ℝ)
82	26, 81	remulcld 11296	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) ∈ ℝ)
83		vmage0 27397	. . . . . 6 ⊢ ((𝑛‘0) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘0)))
84	25, 83	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘0)))
85		vmage0 27397	. . . . . . 7 ⊢ ((𝑛‘1) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘1)))
86	30, 85	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘1)))
87	36	nnrpd 13117	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℝ⁺)
88	87	relogcld 26900	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ∈ ℝ)
89		vmalelog 27481	. . . . . . . 8 ⊢ ((𝑛‘2) ∈ ℕ → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
90	36, 89	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
91	13, 15, 16, 18, 35	reprle 35163	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ≤ 𝑁)
92		logleb 26880	. . . . . . . . 9 ⊢ (((𝑛‘2) ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → ((𝑛‘2) ≤ 𝑁 ↔ (log‘(𝑛‘2)) ≤ (log‘𝑁)))
93	92	biimpa 482	. . . . . . . 8 ⊢ ((((𝑛‘2) ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) ∧ (𝑛‘2) ≤ 𝑁) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
94	87, 78, 91, 93	syl21anc 851	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
95	37, 88, 80, 90, 94	letrd 11424	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘𝑁))
96	37, 80, 31, 86, 95	lemul2ad 12212	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ≤ ((Λ‘(𝑛‘1)) · (log‘𝑁)))
97	38, 81, 26, 84, 96	lemul2ad 12212	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
98	10, 39, 82, 97	fsumle 15919	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
99	1	nncnd 12306	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
100	1	nnne0d 12343	. . . . . 6 ⊢ (𝜑 → 𝑁 ≠ 0)
101	99, 100	logcld 26847	. . . . 5 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
102	43	recnd 11294	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℂ)
103	10, 101, 102	fsummulc2 15903	. . . 4 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
104	101	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℂ)
105	104, 102	mulcomd 11287	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)))
106	26	recnd 11294	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℂ)
107	31	recnd 11294	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℂ)
108	106, 107, 104	mulassd 11289	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
109	105, 108	eqtrd 2795	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
110	109	sumeq2dv 15822	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
111	103, 110	eqtr2d 2796	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) = ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
112	98, 111	breqtrd 5131	. 2 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
113	1	nnred 12305	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ)
114	1	nnge1d 12341	. . . 4 ⊢ (𝜑 → 1 ≤ 𝑁)
115	113, 114	logge0d 26907	. . 3 ⊢ (𝜑 → 0 ≤ (log‘𝑁))
116		xpfi 9289	. . . . . 6 ⊢ (((((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
117	52, 70, 116	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
118	11	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → Λ:ℕ⟶ℝ)
119	66	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
120		xp1st 8017	. . . . . . . . 9 ⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (1^st ‘𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
121	120	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1^st ‘𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
122	119, 121	sseldd 3932	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1^st ‘𝑢) ∈ ℕ)
123	118, 122	ffvelcdmd 7074	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(1^st ‘𝑢)) ∈ ℝ)
124		xp2nd 8018	. . . . . . . . 9 ⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (2^nd ‘𝑢) ∈ (1...𝑁))
125	124	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2^nd ‘𝑢) ∈ (1...𝑁))
126	64, 125	sselid 3929	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2^nd ‘𝑢) ∈ ℕ)
127	118, 126	ffvelcdmd 7074	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(2^nd ‘𝑢)) ∈ ℝ)
128	123, 127	remulcld 11296	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℝ)
129		vmage0 27397	. . . . . . 7 ⊢ ((1^st ‘𝑢) ∈ ℕ → 0 ≤ (Λ‘(1^st ‘𝑢)))
130	122, 129	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(1^st ‘𝑢)))
131		vmage0 27397	. . . . . . 7 ⊢ ((2^nd ‘𝑢) ∈ ℕ → 0 ≤ (Λ‘(2^nd ‘𝑢)))
132	126, 131	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(2^nd ‘𝑢)))
133	123, 127, 130, 132	mulge0d 11848	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
134		ssidd 3954	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ℕ ⊆ ℕ)
135	14	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℤ)
136	3	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 3 ∈ ℕ₀)
137		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴)
138	8, 137	sselid 3929	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
139	134, 135, 136, 138	reprf 35161	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐:(0..^3)⟶ℕ)
140	23	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 0 ∈ (0..^3))
141	139, 140	ffvelcdmd 7074	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℕ)
142	1	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℕ)
143	134, 135, 136, 138, 140	reprle 35163	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ≤ 𝑁)
144		elfz1b 13681	. . . . . . . . . . . . 13 ⊢ ((𝑐‘0) ∈ (1...𝑁) ↔ ((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁))
145	144	biimpri 231	. . . . . . . . . . . 12 ⊢ (((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁) → (𝑐‘0) ∈ (1...𝑁))
146	141, 142, 143, 145	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ (1...𝑁))
147	7	reqabi 3434	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ 𝐴 ↔ (𝑐 ∈ (ℕ(repr‘3)𝑁) ∧ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
148	147	simprbi 503	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
149		hgt750leme.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
150	149	oddprm2 35204	. . . . . . . . . . . . . 14 ⊢ (ℙ ∖ {2}) = (𝑂 ∩ ℙ)
151	150	eleq2i 2852	. . . . . . . . . . . . 13 ⊢ ((𝑐‘0) ∈ (ℙ ∖ {2}) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
152	148, 151	sylnibr 332	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
153	137, 152	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
154	146, 153	jca 521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
155		eldif 3909	. . . . . . . . . 10 ⊢ ((𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})) ↔ ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
156	154, 155	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})))
157		uncom 4105	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) = ({2} ∪ ((1...𝑁) ∖ ℙ))
158		undif3 4246	. . . . . . . . . . . . 13 ⊢ ({2} ∪ ((1...𝑁) ∖ ℙ)) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
159	157, 158	eqtri 2783	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
160		ssequn1 4132	. . . . . . . . . . . . . 14 ⊢ ({2} ⊆ (1...𝑁) ↔ ({2} ∪ (1...𝑁)) = (1...𝑁))
161	62, 160	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → ({2} ∪ (1...𝑁)) = (1...𝑁))
162	161	difeq1d 4073	. . . . . . . . . . . 12 ⊢ (𝜑 → (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2})) = ((1...𝑁) ∖ (ℙ ∖ {2})))
163	159, 162	eqtrid 2807	. . . . . . . . . . 11 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) = ((1...𝑁) ∖ (ℙ ∖ {2})))
164	163	eleq2d 2846	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))))
165	164	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))))
166	156, 165	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
167	28	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ (0..^3))
168	139, 167	ffvelcdmd 7074	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℕ)
169	134, 135, 136, 138, 167	reprle 35163	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ≤ 𝑁)
170		elfz1b 13681	. . . . . . . . . 10 ⊢ ((𝑐‘1) ∈ (1...𝑁) ↔ ((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁))
171	170	biimpri 231	. . . . . . . . 9 ⊢ (((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁) → (𝑐‘1) ∈ (1...𝑁))
172	168, 142, 169, 171	syl3anc 1398	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ (1...𝑁))
173	166, 172	opelxpd 5687	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
174	173	ralrimiva 3154	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
175		fveq1 6873	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
176		fveq1 6873	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → (𝑑‘1) = (𝑐‘1))
177	175, 176	opeq12d 4841	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → ⟨(𝑑‘0), (𝑑‘1)⟩ = ⟨(𝑐‘0), (𝑐‘1)⟩)
178	177	cbvmptv 5209	. . . . . . 7 ⊢ (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐 ∈ 𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩)
179	178	rnmptss 7112	. . . . . 6 ⊢ (∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
180	174, 179	syl 18	. . . . 5 ⊢ (𝜑 → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
181	117, 128, 133, 180	fsumless 15916	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ≤ Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
182		fvex 6887	. . . . . . . 8 ⊢ (𝑛‘0) ∈ V
183		fvex 6887	. . . . . . . 8 ⊢ (𝑛‘1) ∈ V
184	182, 183	op1std 7995	. . . . . . 7 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (1^st ‘𝑢) = (𝑛‘0))
185	184	fveq2d 6878	. . . . . 6 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(1^st ‘𝑢)) = (Λ‘(𝑛‘0)))
186	182, 183	op2ndd 7996	. . . . . . 7 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (2^nd ‘𝑢) = (𝑛‘1))
187	186	fveq2d 6878	. . . . . 6 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(2^nd ‘𝑢)) = (Λ‘(𝑛‘1)))
188	185, 187	oveq12d 7427	. . . . 5 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
189		opex 5432	. . . . . . . 8 ⊢ ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
190	189	rgenw 3080	. . . . . . 7 ⊢ ∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
191	178	fnmpt 6668	. . . . . . 7 ⊢ (∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
192	190, 191	mp1i 14	. . . . . 6 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
193		eqidd 2761	. . . . . 6 ⊢ (𝜑 → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
194	139	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐:(0..^3)⟶ℕ)
195	194	ffnd 6699	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 Fn (0..^3))
196	19	ad4ant13 764	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛:(0..^3)⟶ℕ)
197	196	ffnd 6699	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 Fn (0..^3))
198		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛))
199	178	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐 ∈ 𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩))
200	189	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V)
201	199, 200	fvmpt2d 6996	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
202	201	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
203	202	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
204		fveq1 6873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑛 → (𝑐‘0) = (𝑛‘0))
205		fveq1 6873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑛 → (𝑐‘1) = (𝑛‘1))
206	204, 205	opeq12d 4841	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑛 → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
207		opex 5432	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V
208	207	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V)
209	178, 206, 17, 208	fvmptd3 7006	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
210	209	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
211	210	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
212	198, 203, 211	3eqtr3d 2803	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
213	182, 183	opth2 5449	. . . . . . . . . . . . . . 15 ⊢ (⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩ ↔ ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1)))
214	212, 213	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1)))
215	214	simpld 500	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘0) = (𝑛‘0))
216	215	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘0) = (𝑛‘0))
217		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → 𝑖 = 0)
218	217	fveq2d 6878	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑐‘0))
219	217	fveq2d 6878	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑛‘𝑖) = (𝑛‘0))
220	216, 218, 219	3eqtr4d 2805	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑛‘𝑖))
221	214	simprd 501	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘1) = (𝑛‘1))
222	221	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘1) = (𝑛‘1))
223		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → 𝑖 = 1)
224	223	fveq2d 6878	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑐‘1))
225	223	fveq2d 6878	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑛‘𝑖) = (𝑛‘1))
226	222, 224, 225	3eqtr4d 2805	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑛‘𝑖))
227	215	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) = (𝑛‘0))
228	221	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) = (𝑛‘1))
229	227, 228	oveq12d 7427	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) = ((𝑛‘0) + (𝑛‘1)))
230	229	oveq2d 7425	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑁 − ((𝑐‘0) + (𝑐‘1))) = (𝑁 − ((𝑛‘0) + (𝑛‘1))))
231	22	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (0..^3) = {0, 1, 2})
232	231	sumeq1d 15820	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗))
233		ssidd 3954	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ℕ ⊆ ℕ)
234	135	ad4antr 745	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℤ)
235	3	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 3 ∈ ℕ₀)
236	138	ad4antr 745	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
237	233, 234, 235, 236	reprsum 35162	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = 𝑁)
238		fveq2 6874	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑐‘𝑗) = (𝑐‘0))
239		fveq2 6874	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 1 → (𝑐‘𝑗) = (𝑐‘1))
240		fveq2 6874	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 2 → (𝑐‘𝑗) = (𝑐‘2))
241	141	nncnd 12306	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℂ)
242	241	ad4antr 745	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) ∈ ℂ)
243	168	nncnd 12306	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℂ)
244	243	ad4antr 745	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) ∈ ℂ)
245	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 2 ∈ (0..^3))
246	139, 245	ffvelcdmd 7074	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℕ)
247	246	nncnd 12306	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℂ)
248	247	ad4antr 745	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) ∈ ℂ)
249	242, 244, 248	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) ∈ ℂ ∧ (𝑐‘1) ∈ ℂ ∧ (𝑐‘2) ∈ ℂ))
250		1ex 11260	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ V
251	20, 250, 32	3pm3.2i 1358	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V)
252	251	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V))
253		0ne1 12369	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
254	253	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 1)
255		0ne2 12507	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 2
256	255	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 2)
257		1ne2 12508	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 2
258	257	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 1 ≠ 2)
259	238, 239, 240, 249, 252, 254, 256, 258	sumtp 15868	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗) = (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)))
260	232, 237, 259	3eqtr3rd 2804	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁)
261	242, 244	addcld 11285	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) ∈ ℂ)
262	99	ad5antr 747	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℂ)
263	261, 248, 262	addrsub 11688	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁 ↔ (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1)))))
264	260, 263	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1))))
265	231	sumeq1d 15820	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗))
266	18	ad4ant13 764	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
267	266	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
268	233, 234, 235, 267	reprsum 35162	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = 𝑁)
269		fveq2 6874	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑛‘𝑗) = (𝑛‘0))
270		fveq2 6874	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 1 → (𝑛‘𝑗) = (𝑛‘1))
271		fveq2 6874	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 2 → (𝑛‘𝑗) = (𝑛‘2))
272	25	nncnd 12306	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ)
273	272	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ)
274	273	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘0) ∈ ℂ)
275	30	nncnd 12306	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ)
276	275	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ)
277	276	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘1) ∈ ℂ)
278	36	nncnd 12306	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ)
279	278	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ)
280	279	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) ∈ ℂ)
281	274, 277, 280	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) ∈ ℂ ∧ (𝑛‘1) ∈ ℂ ∧ (𝑛‘2) ∈ ℂ))
282	269, 270, 271, 281, 252, 254, 256, 258	sumtp 15868	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗) = (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)))
283	265, 268, 282	3eqtr3rd 2804	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁)
284	274, 277	addcld 11285	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) + (𝑛‘1)) ∈ ℂ)
285	284, 280, 262	addrsub 11688	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁 ↔ (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1)))))
286	283, 285	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1))))
287	230, 264, 286	3eqtr4d 2805	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑛‘2))
288		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑖 = 2)
289	288	fveq2d 6878	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑐‘2))
290	288	fveq2d 6878	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘𝑖) = (𝑛‘2))
291	287, 289, 290	3eqtr4d 2805	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑛‘𝑖))
292		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ (0..^3))
293	292, 22	eleqtrdi 2870	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ {0, 1, 2})
294		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑖 ∈ V
295	294	eltp 4650	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ {0, 1, 2} ↔ (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2))
296	293, 295	sylib 221	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2))
297	220, 226, 291, 296	mpjao3dan 1459	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑐‘𝑖) = (𝑛‘𝑖))
298	195, 197, 297	eqfnfvd 7021	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 = 𝑛)
299	298	ex 418	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
300	299	anasss 472	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴)) → (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
301	300	ralrimivva 3205	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
302		dff1o6 7272	. . . . . . 7 ⊢ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴–1-1-onto→ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ↔ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴 ∧ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ∧ ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛)))
303	302	biimpri 231	. . . . . 6 ⊢ (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴 ∧ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ∧ ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛)) → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴–1-1-onto→ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
304	192, 193, 301, 303	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴–1-1-onto→ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
305	180	sselda 3931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
306	305, 123	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(1^st ‘𝑢)) ∈ ℝ)
307	305, 127	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(2^nd ‘𝑢)) ∈ ℝ)
308	306, 307	remulcld 11296	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℝ)
309	308	recnd 11294	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℂ)
310	188, 10, 304, 209, 309	fsumf1o 15842	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
311	74	recnd 11294	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℂ)
312	68	recnd 11294	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℂ)
313	52, 311, 312	fsummulc1 15904	. . . . 5 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
314	46	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (1...𝑁) ∈ Fin)
315	73	adantrl 729	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑗) ∈ ℝ)
316	315	anassrs 473	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
317	316	recnd 11294	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℂ)
318	314, 312, 317	fsummulc2 15903	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → ((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
319	318	sumeq2dv 15822	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
320		vex 3454	. . . . . . . . 9 ⊢ 𝑗 ∈ V
321	294, 320	op1std 7995	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (1^st ‘𝑢) = 𝑖)
322	321	fveq2d 6878	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(1^st ‘𝑢)) = (Λ‘𝑖))
323	294, 320	op2ndd 7996	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (2^nd ‘𝑢) = 𝑗)
324	323	fveq2d 6878	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(2^nd ‘𝑢)) = (Λ‘𝑗))
325	322, 324	oveq12d 7427	. . . . . 6 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = ((Λ‘𝑖) · (Λ‘𝑗)))
326	68	adantrr 730	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑖) ∈ ℝ)
327	326, 315	remulcld 11296	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℝ)
328	327	recnd 11294	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℂ)
329	325, 52, 70, 328	fsumxp 15891	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)) = Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
330	313, 319, 329	3eqtrrd 2800	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
331	181, 310, 330	3brtr3d 5136	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ≤ (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
332	44, 75, 42, 115, 331	lemul2ad 12212	. 2 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
333	40, 45, 76, 112, 332	letrd 11424	1 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ w3o 1102 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 {crab 3412 Vcvv 3450 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 {csn 4584 {ctp 4588 ⟨cop 4590 class class class wbr 5103 ↦ cmpt 5186 × cxp 5646 ran crn 5649 Fn wfn 6523 ⟶wf 6524 –1-1-onto→wf1o 6527 ‘cfv 6528 (class class class)co 7409 1^st c1st 7983 2^nd c2nd 7984 Fincfn 8952 ℂcc 11155 ℝcr 11156 0cc0 11157 1c1 11158 + caddc 11160 · cmul 11162 ≤ cle 11301 − cmin 11498 ℕcn 12290 2c2 12352 3c3 12353 ℕ₀cn0 12561 ℤcz 12648 ℝ⁺crp 13075 ...cfz 13594 ..^cfzo 13742 Σcsu 15806 ∥ cdvds 16375 ℙcprime 16794 logclog 26831 Λcvma 27368 reprcrepr 35157

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7735 ax-inf2 9620 ax-cnex 11213 ax-resscn 11214 ax-1cn 11215 ax-icn 11216 ax-addcl 11217 ax-addrcl 11218 ax-mulcl 11219 ax-mulrcl 11220 ax-mulcom 11221 ax-addass 11222 ax-mulass 11223 ax-distr 11224 ax-i2m1 11225 ax-1ne0 11226 ax-1rid 11227 ax-rnegex 11228 ax-rrecex 11229 ax-cnre 11230 ax-pre-lttri 11231 ax-pre-lttrn 11232 ax-pre-ltadd 11233 ax-pre-mulgt0 11234 ax-pre-sup 11235 ax-addf 11236

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-se 5602 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6294 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6530 df-fn 6531 df-f 6532 df-f1 6533 df-fo 6534 df-f1o 6535 df-fv 6536 df-isom 6537 df-riota 7366 df-ov 7412 df-oprab 7413 df-mpo 7414 df-of 7677 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8157 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8455 df-2o 8456 df-oadd 8459 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8905 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fsupp 9332 df-fi 9381 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9939 df-card 9977 df-pnf 11302 df-mnf 11303 df-xr 11304 df-ltxr 11305 df-le 11306 df-sub 11500 df-neg 11501 df-div 11929 df-nn 12291 df-2 12360 df-3 12361 df-4 12362 df-5 12363 df-6 12364 df-7 12365 df-8 12366 df-9 12367 df-n0 12562 df-z 12649 df-dec 12770 df-uz 12921 df-q 13031 df-rp 13076 df-xneg 13196 df-xadd 13197 df-xmul 13198 df-ioo 13435 df-ioc 13436 df-ico 13437 df-icc 13438 df-fz 13595 df-fzo 13743 df-fl 13886 df-mod 13964 df-seq 14099 df-exp 14159 df-fac 14371 df-bc 14400 df-hash 14428 df-shft 15173 df-cj 15219 df-re 15220 df-im 15221 df-sqrt 15355 df-abs 15356 df-limsup 15591 df-clim 15608 df-rlim 15609 df-sum 15807 df-ef 16186 df-sin 16188 df-cos 16189 df-pi 16191 df-dvds 16376 df-gcd 16618 df-prm 16795 df-pc 16962 df-struct 17272 df-sets 17289 df-slot 17307 df-ndx 17319 df-base 17335 df-ress 17356 df-plusg 17388 df-mulr 17389 df-starv 17390 df-sca 17391 df-vsca 17392 df-ip 17393 df-tset 17394 df-ple 17395 df-ds 17397 df-unif 17398 df-hom 17399 df-cco 17400 df-rest 17540 df-topn 17541 df-0g 17559 df-gsum 17560 df-topgen 17561 df-pt 17562 df-prds 17565 df-xrs 17621 df-qtop 17626 df-imas 17627 df-xps 17629 df-mre 17703 df-mrc 17704 df-acs 17706 df-mgm 18763 df-sgrp 18855 df-mnd 18871 df-submnd 18926 df-mulg 19225 df-cntz 19478 df-cmn 19943 df-psmet 21617 df-xmet 21618 df-met 21619 df-bl 21620 df-mopn 21621 df-fbas 21622 df-fg 21623 df-cnfld 21626 df-top 23159 df-topon 23176 df-topsp 23198 df-bases 23211 df-cld 23284 df-ntr 23285 df-cls 23286 df-nei 23363 df-lp 23401 df-perf 23402 df-cn 23492 df-cnp 23493 df-haus 23580 df-tx 23828 df-hmeo 24021 df-fil 24112 df-fm 24204 df-flim 24205 df-flf 24206 df-xms 24586 df-ms 24587 df-tms 24588 df-cncf 25146 df-limc 26133 df-dv 26134 df-log 26833 df-vma 27374 df-repr 35158

This theorem is used by: hgt750leme 35207

W3C validator