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 35052

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 12571	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		3nn0 12528	. . . . . 6 ⊢ 3 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ₀)
5		ssidd 3959	. . . . 5 ⊢ (𝜑 → ℕ ⊆ ℕ)
6	2, 4, 5	reprfi2 35019	. . . 4 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
7		hgt750lemb.a	. . . . 5 ⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
8	7	ssrab3 4035	. . . 4 ⊢ 𝐴 ⊆ (ℕ(repr‘3)𝑁)
9		ssfi 9155	. . . 4 ⊢ (((ℕ(repr‘3)𝑁) ∈ Fin ∧ 𝐴 ⊆ (ℕ(repr‘3)𝑁)) → 𝐴 ∈ Fin)
10	6, 8, 9	sylancl 597	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
11		vmaf 27294	. . . . . 6 ⊢ Λ:ℕ⟶ℝ
12	11	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → Λ:ℕ⟶ℝ)
13		ssidd 3959	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ℕ ⊆ ℕ)
14	1	nnzd 12623	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
15	14	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℤ)
16	3	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 3 ∈ ℕ₀)
17		simpr 489	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ 𝐴)
18	8, 17	sselid 3934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
19	13, 15, 16, 18	reprf 35008	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛:(0..^3)⟶ℕ)
20		c0ex 11206	. . . . . . . . 9 ⊢ 0 ∈ V
21	20	tpid1 4733	. . . . . . . 8 ⊢ 0 ∈ {0, 1, 2}
22		fzo0to3tp 13788	. . . . . . . 8 ⊢ (0..^3) = {0, 1, 2}
23	21, 22	eleqtrri 2861	. . . . . . 7 ⊢ 0 ∈ (0..^3)
24	23	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ∈ (0..^3))
25	19, 24	ffvelcdmd 7080	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℕ)
26	12, 25	ffvelcdmd 7080	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℝ)
27		1eltp012 12317	. . . . . . . . 9 ⊢ 1 ∈ {0, 1, 2}
28	27, 22	eleqtrri 2861	. . . . . . . 8 ⊢ 1 ∈ (0..^3)
29	28	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 1 ∈ (0..^3))
30	19, 29	ffvelcdmd 7080	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℕ)
31	12, 30	ffvelcdmd 7080	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℝ)
32		2ex 12324	. . . . . . . . . 10 ⊢ 2 ∈ V
33	32	tpid3 4738	. . . . . . . . 9 ⊢ 2 ∈ {0, 1, 2}
34	33, 22	eleqtrri 2861	. . . . . . . 8 ⊢ 2 ∈ (0..^3)
35	34	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 2 ∈ (0..^3))
36	19, 35	ffvelcdmd 7080	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℕ)
37	12, 36	ffvelcdmd 7080	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ∈ ℝ)
38	31, 37	remulcld 11245	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
39	26, 38	remulcld 11245	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
40	10, 39	fsumrecl 15792	. 2 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
41	1	nnrpd 13064	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
42	41	relogcld 26799	. . 3 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
43	26, 31	remulcld 11245	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
44	10, 43	fsumrecl 15792	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
45	42, 44	remulcld 11245	. 2 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ∈ ℝ)
46		fzfi 14015	. . . . . . . 8 ⊢ (1...𝑁) ∈ Fin
47		diffi 9157	. . . . . . . 8 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
48	46, 47	ax-mp 5	. . . . . . 7 ⊢ ((1...𝑁) ∖ ℙ) ∈ Fin
49		snfi 9038	. . . . . . 7 ⊢ {2} ∈ Fin
50		unfi 9153	. . . . . . 7 ⊢ ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
51	48, 49, 50	mp2an 704	. . . . . 6 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
52	51	a1i 11	. . . . 5 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
53	11	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
54		difss 4089	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁)
55	54	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁))
56		2nn 12320	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
57	56	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ)
58		hgt750lemb.2	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 𝑁)
59		elfz1b 13628	. . . . . . . . . . . 12 ⊢ (2 ∈ (1...𝑁) ↔ (2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁))
60	59	biimpri 231	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁) → 2 ∈ (1...𝑁))
61	57, 1, 58, 60	syl3anc 1397	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ (1...𝑁))
62	61	snssd 4751	. . . . . . . . 9 ⊢ (𝜑 → {2} ⊆ (1...𝑁))
63	55, 62	unssd 4144	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ (1...𝑁))
64		fz1ssnn 13590	. . . . . . . . 9 ⊢ (1...𝑁) ⊆ ℕ
65	64	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
66	63, 65	sstrd 3946	. . . . . . 7 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
67	66	sselda 3936	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
68	53, 67	ffvelcdmd 7080	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
69	52, 68	fsumrecl 15792	. . . 4 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
70		fzfid 14016	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
71	11	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
72	65	sselda 3936	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
73	71, 72	ffvelcdmd 7080	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
74	70, 73	fsumrecl 15792	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
75	69, 74	remulcld 11245	. . 3 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
76	42, 75	remulcld 11245	. 2 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
77	1	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℕ)
78	77	nnrpd 13064	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℝ⁺)
79		relogcl 26751	. . . . . . 7 ⊢ (𝑁 ∈ ℝ⁺ → (log‘𝑁) ∈ ℝ)
80	78, 79	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℝ)
81	31, 80	remulcld 11245	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (log‘𝑁)) ∈ ℝ)
82	26, 81	remulcld 11245	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) ∈ ℝ)
83		vmage0 27296	. . . . . 6 ⊢ ((𝑛‘0) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘0)))
84	25, 83	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘0)))
85		vmage0 27296	. . . . . . 7 ⊢ ((𝑛‘1) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘1)))
86	30, 85	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘1)))
87	36	nnrpd 13064	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℝ⁺)
88	87	relogcld 26799	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ∈ ℝ)
89		vmalelog 27380	. . . . . . . 8 ⊢ ((𝑛‘2) ∈ ℕ → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
90	36, 89	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
91	13, 15, 16, 18, 35	reprle 35010	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ≤ 𝑁)
92		logleb 26779	. . . . . . . . 9 ⊢ (((𝑛‘2) ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → ((𝑛‘2) ≤ 𝑁 ↔ (log‘(𝑛‘2)) ≤ (log‘𝑁)))
93	92	biimpa 481	. . . . . . . 8 ⊢ ((((𝑛‘2) ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) ∧ (𝑛‘2) ≤ 𝑁) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
94	87, 78, 91, 93	syl21anc 850	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
95	37, 88, 80, 90, 94	letrd 11373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘𝑁))
96	37, 80, 31, 86, 95	lemul2ad 12161	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ≤ ((Λ‘(𝑛‘1)) · (log‘𝑁)))
97	38, 81, 26, 84, 96	lemul2ad 12161	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
98	10, 39, 82, 97	fsumle 15858	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
99	1	nncnd 12255	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
100	1	nnne0d 12292	. . . . . 6 ⊢ (𝜑 → 𝑁 ≠ 0)
101	99, 100	logcld 26746	. . . . 5 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
102	43	recnd 11243	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℂ)
103	10, 101, 102	fsummulc2 15842	. . . 4 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
104	101	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℂ)
105	104, 102	mulcomd 11236	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)))
106	26	recnd 11243	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℂ)
107	31	recnd 11243	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℂ)
108	106, 107, 104	mulassd 11238	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
109	105, 108	eqtrd 2797	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
110	109	sumeq2dv 15760	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
111	103, 110	eqtr2d 2798	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) = ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
112	98, 111	breqtrd 5136	. 2 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
113	1	nnred 12254	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ)
114	1	nnge1d 12290	. . . 4 ⊢ (𝜑 → 1 ≤ 𝑁)
115	113, 114	logge0d 26806	. . 3 ⊢ (𝜑 → 0 ≤ (log‘𝑁))
116		xpfi 9277	. . . . . 6 ⊢ (((((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
117	52, 70, 116	syl2anc 595	. . . . 5 ⊢ (𝜑 → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
118	11	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → Λ:ℕ⟶ℝ)
119	66	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
120		xp1st 8016	. . . . . . . . 9 ⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (1^st ‘𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
121	120	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1^st ‘𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
122	119, 121	sseldd 3937	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1^st ‘𝑢) ∈ ℕ)
123	118, 122	ffvelcdmd 7080	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(1^st ‘𝑢)) ∈ ℝ)
124		xp2nd 8017	. . . . . . . . 9 ⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (2^nd ‘𝑢) ∈ (1...𝑁))
125	124	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2^nd ‘𝑢) ∈ (1...𝑁))
126	64, 125	sselid 3934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2^nd ‘𝑢) ∈ ℕ)
127	118, 126	ffvelcdmd 7080	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(2^nd ‘𝑢)) ∈ ℝ)
128	123, 127	remulcld 11245	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℝ)
129		vmage0 27296	. . . . . . 7 ⊢ ((1^st ‘𝑢) ∈ ℕ → 0 ≤ (Λ‘(1^st ‘𝑢)))
130	122, 129	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(1^st ‘𝑢)))
131		vmage0 27296	. . . . . . 7 ⊢ ((2^nd ‘𝑢) ∈ ℕ → 0 ≤ (Λ‘(2^nd ‘𝑢)))
132	126, 131	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(2^nd ‘𝑢)))
133	123, 127, 130, 132	mulge0d 11797	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
134		ssidd 3959	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ℕ ⊆ ℕ)
135	14	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℤ)
136	3	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 3 ∈ ℕ₀)
137		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴)
138	8, 137	sselid 3934	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
139	134, 135, 136, 138	reprf 35008	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐:(0..^3)⟶ℕ)
140	23	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 0 ∈ (0..^3))
141	139, 140	ffvelcdmd 7080	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℕ)
142	1	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℕ)
143	134, 135, 136, 138, 140	reprle 35010	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ≤ 𝑁)
144		elfz1b 13628	. . . . . . . . . . . . 13 ⊢ ((𝑐‘0) ∈ (1...𝑁) ↔ ((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁))
145	144	biimpri 231	. . . . . . . . . . . 12 ⊢ (((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁) → (𝑐‘0) ∈ (1...𝑁))
146	141, 142, 143, 145	syl3anc 1397	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ (1...𝑁))
147	7	reqabi 3438	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ 𝐴 ↔ (𝑐 ∈ (ℕ(repr‘3)𝑁) ∧ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
148	147	simprbi 502	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
149		hgt750leme.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
150	149	oddprm2 35051	. . . . . . . . . . . . . 14 ⊢ (ℙ ∖ {2}) = (𝑂 ∩ ℙ)
151	150	eleq2i 2854	. . . . . . . . . . . . 13 ⊢ ((𝑐‘0) ∈ (ℙ ∖ {2}) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
152	148, 151	sylnibr 332	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
153	137, 152	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
154	146, 153	jca 520	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
155		eldif 3914	. . . . . . . . . 10 ⊢ ((𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})) ↔ ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
156	154, 155	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})))
157		uncom 4111	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) = ({2} ∪ ((1...𝑁) ∖ ℙ))
158		undif3 4252	. . . . . . . . . . . . 13 ⊢ ({2} ∪ ((1...𝑁) ∖ ℙ)) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
159	157, 158	eqtri 2785	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
160		ssequn1 4138	. . . . . . . . . . . . . 14 ⊢ ({2} ⊆ (1...𝑁) ↔ ({2} ∪ (1...𝑁)) = (1...𝑁))
161	62, 160	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → ({2} ∪ (1...𝑁)) = (1...𝑁))
162	161	difeq1d 4079	. . . . . . . . . . . 12 ⊢ (𝜑 → (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2})) = ((1...𝑁) ∖ (ℙ ∖ {2})))
163	159, 162	eqtrid 2809	. . . . . . . . . . 11 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) = ((1...𝑁) ∖ (ℙ ∖ {2})))
164	163	eleq2d 2848	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))))
165	164	adantr 485	. . . . . . . . 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 7080	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℕ)
169	134, 135, 136, 138, 167	reprle 35010	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ≤ 𝑁)
170		elfz1b 13628	. . . . . . . . . 10 ⊢ ((𝑐‘1) ∈ (1...𝑁) ↔ ((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁))
171	170	biimpri 231	. . . . . . . . 9 ⊢ (((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁) → (𝑐‘1) ∈ (1...𝑁))
172	168, 142, 169, 171	syl3anc 1397	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ (1...𝑁))
173	166, 172	opelxpd 5699	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
174	173	ralrimiva 3156	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
175		fveq1 6880	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
176		fveq1 6880	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → (𝑑‘1) = (𝑐‘1))
177	175, 176	opeq12d 4845	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → ⟨(𝑑‘0), (𝑑‘1)⟩ = ⟨(𝑐‘0), (𝑐‘1)⟩)
178	177	cbvmptv 5214	. . . . . . 7 ⊢ (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐 ∈ 𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩)
179	178	rnmptss 7118	. . . . . 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 15855	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ≤ Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
182		fvex 6894	. . . . . . . 8 ⊢ (𝑛‘0) ∈ V
183		fvex 6894	. . . . . . . 8 ⊢ (𝑛‘1) ∈ V
184	182, 183	op1std 7994	. . . . . . 7 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (1^st ‘𝑢) = (𝑛‘0))
185	184	fveq2d 6885	. . . . . 6 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(1^st ‘𝑢)) = (Λ‘(𝑛‘0)))
186	182, 183	op2ndd 7995	. . . . . . 7 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (2^nd ‘𝑢) = (𝑛‘1))
187	186	fveq2d 6885	. . . . . 6 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(2^nd ‘𝑢)) = (Λ‘(𝑛‘1)))
188	185, 187	oveq12d 7430	. . . . 5 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
189		opex 5444	. . . . . . . 8 ⊢ ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
190	189	rgenw 3082	. . . . . . 7 ⊢ ∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
191	178	fnmpt 6675	. . . . . . 7 ⊢ (∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
192	190, 191	mp1i 14	. . . . . 6 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
193		eqidd 2763	. . . . . 6 ⊢ (𝜑 → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
194	139	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐:(0..^3)⟶ℕ)
195	194	ffnd 6706	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 Fn (0..^3))
196	19	ad4ant13 763	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛:(0..^3)⟶ℕ)
197	196	ffnd 6706	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 Fn (0..^3))
198		simpr 489	. . . . . . . . . . . . . . . 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 7003	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
202	201	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
203	202	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
204		fveq1 6880	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑛 → (𝑐‘0) = (𝑛‘0))
205		fveq1 6880	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑛 → (𝑐‘1) = (𝑛‘1))
206	204, 205	opeq12d 4845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑛 → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
207		opex 5444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V
208	207	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V)
209	178, 206, 17, 208	fvmptd3 7013	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
210	209	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
211	210	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
212	198, 203, 211	3eqtr3d 2805	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
213	182, 183	opth2 5461	. . . . . . . . . . . . . . 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 499	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘0) = (𝑛‘0))
216	215	ad2antrr 738	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘0) = (𝑛‘0))
217		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → 𝑖 = 0)
218	217	fveq2d 6885	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑐‘0))
219	217	fveq2d 6885	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑛‘𝑖) = (𝑛‘0))
220	216, 218, 219	3eqtr4d 2807	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑛‘𝑖))
221	214	simprd 500	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘1) = (𝑛‘1))
222	221	ad2antrr 738	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘1) = (𝑛‘1))
223		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → 𝑖 = 1)
224	223	fveq2d 6885	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑐‘1))
225	223	fveq2d 6885	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑛‘𝑖) = (𝑛‘1))
226	222, 224, 225	3eqtr4d 2807	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑛‘𝑖))
227	215	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) = (𝑛‘0))
228	221	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) = (𝑛‘1))
229	227, 228	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) = ((𝑛‘0) + (𝑛‘1)))
230	229	oveq2d 7428	. . . . . . . . . . . . 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 15758	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗))
233		ssidd 3959	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ℕ ⊆ ℕ)
234	135	ad4antr 744	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℤ)
235	3	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 3 ∈ ℕ₀)
236	138	ad4antr 744	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
237	233, 234, 235, 236	reprsum 35009	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = 𝑁)
238		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑐‘𝑗) = (𝑐‘0))
239		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 1 → (𝑐‘𝑗) = (𝑐‘1))
240		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 2 → (𝑐‘𝑗) = (𝑐‘2))
241	141	nncnd 12255	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℂ)
242	241	ad4antr 744	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) ∈ ℂ)
243	168	nncnd 12255	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℂ)
244	243	ad4antr 744	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) ∈ ℂ)
245	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 2 ∈ (0..^3))
246	139, 245	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℕ)
247	246	nncnd 12255	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℂ)
248	247	ad4antr 744	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) ∈ ℂ)
249	242, 244, 248	3jca 1145	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) ∈ ℂ ∧ (𝑐‘1) ∈ ℂ ∧ (𝑐‘2) ∈ ℂ))
250		1ex 11209	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ V
251	20, 250, 32	3pm3.2i 1357	. . . . . . . . . . . . . . . . 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 12318	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
254	253	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 1)
255		0ne2 12456	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 2
256	255	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 2)
257		1ne2 12457	. . . . . . . . . . . . . . . . 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 15807	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗) = (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)))
260	232, 237, 259	3eqtr3rd 2806	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁)
261	242, 244	addcld 11234	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) ∈ ℂ)
262	99	ad5antr 746	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℂ)
263	261, 248, 262	addrsub 11637	. . . . . . . . . . . . . 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 15758	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗))
266	18	ad4ant13 763	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
267	266	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
268	233, 234, 235, 267	reprsum 35009	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = 𝑁)
269		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑛‘𝑗) = (𝑛‘0))
270		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 1 → (𝑛‘𝑗) = (𝑛‘1))
271		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 2 → (𝑛‘𝑗) = (𝑛‘2))
272	25	nncnd 12255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ)
273	272	adantlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ)
274	273	ad3antrrr 742	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘0) ∈ ℂ)
275	30	nncnd 12255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ)
276	275	adantlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ)
277	276	ad3antrrr 742	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘1) ∈ ℂ)
278	36	nncnd 12255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ)
279	278	adantlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ)
280	279	ad3antrrr 742	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) ∈ ℂ)
281	274, 277, 280	3jca 1145	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) ∈ ℂ ∧ (𝑛‘1) ∈ ℂ ∧ (𝑛‘2) ∈ ℂ))
282	269, 270, 271, 281, 252, 254, 256, 258	sumtp 15807	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗) = (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)))
283	265, 268, 282	3eqtr3rd 2806	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁)
284	274, 277	addcld 11234	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) + (𝑛‘1)) ∈ ℂ)
285	284, 280, 262	addrsub 11637	. . . . . . . . . . . . . 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 2807	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑛‘2))
288		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑖 = 2)
289	288	fveq2d 6885	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑐‘2))
290	288	fveq2d 6885	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘𝑖) = (𝑛‘2))
291	287, 289, 290	3eqtr4d 2807	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑛‘𝑖))
292		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ (0..^3))
293	292, 22	eleqtrdi 2872	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ {0, 1, 2})
294		vex 3458	. . . . . . . . . . . . 13 ⊢ 𝑖 ∈ V
295	294	eltp 4654	. . . . . . . . . . . 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 1458	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑐‘𝑖) = (𝑛‘𝑖))
298	195, 197, 297	eqfnfvd 7028	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 = 𝑛)
299	298	ex 417	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
300	299	anasss 471	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴)) → (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
301	300	ralrimivva 3207	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
302		dff1o6 7273	. . . . . . 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 1397	. . . . 5 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴–1-1-onto→ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
305	180	sselda 3936	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
306	305, 123	syldan 602	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(1^st ‘𝑢)) ∈ ℝ)
307	305, 127	syldan 602	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(2^nd ‘𝑢)) ∈ ℝ)
308	306, 307	remulcld 11245	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℝ)
309	308	recnd 11243	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℂ)
310	188, 10, 304, 209, 309	fsumf1o 15781	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
311	74	recnd 11243	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℂ)
312	68	recnd 11243	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℂ)
313	52, 311, 312	fsummulc1 15843	. . . . 5 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
314	46	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (1...𝑁) ∈ Fin)
315	73	adantrl 728	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑗) ∈ ℝ)
316	315	anassrs 472	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
317	316	recnd 11243	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℂ)
318	314, 312, 317	fsummulc2 15842	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → ((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
319	318	sumeq2dv 15760	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
320		vex 3458	. . . . . . . . 9 ⊢ 𝑗 ∈ V
321	294, 320	op1std 7994	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (1^st ‘𝑢) = 𝑖)
322	321	fveq2d 6885	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(1^st ‘𝑢)) = (Λ‘𝑖))
323	294, 320	op2ndd 7995	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (2^nd ‘𝑢) = 𝑗)
324	323	fveq2d 6885	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(2^nd ‘𝑢)) = (Λ‘𝑗))
325	322, 324	oveq12d 7430	. . . . . 6 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = ((Λ‘𝑖) · (Λ‘𝑗)))
326	68	adantrr 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑖) ∈ ℝ)
327	326, 315	remulcld 11245	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℝ)
328	327	recnd 11243	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℂ)
329	325, 52, 70, 328	fsumxp 15830	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)) = Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
330	313, 319, 329	3eqtrrd 2802	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
331	181, 310, 330	3brtr3d 5141	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ≤ (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
332	44, 75, 42, 115, 331	lemul2ad 12161	. 2 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
333	40, 45, 76, 112, 332	letrd 11373	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 400 ∨ w3o 1101 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 ∀wral 3078 {crab 3415 Vcvv 3454 ∖ cdif 3901 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 {csn 4588 {ctp 4592 ⟨cop 4594 class class class wbr 5108 ↦ cmpt 5191 × cxp 5658 ran crn 5661 Fn wfn 6531 ⟶wf 6532 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7412 1^st c1st 7982 2^nd c2nd 7983 Fincfn 8941 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 ≤ cle 11250 − cmin 11447 ℕcn 12239 2c2 12301 3c3 12302 ℕ₀cn0 12510 ℤcz 12597 ℝ⁺crp 13022 ...cfz 13541 ..^cfzo 13689 Σcsu 15744 ∥ cdvds 16316 ℙcprime 16735 logclog 26730 Λcvma 27267 reprcrepr 35004

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-inf2 9608 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184 ax-addf 11185

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8155 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-oadd 8455 df-er 8692 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9894 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-5 12312 df-6 12313 df-7 12314 df-8 12315 df-9 12316 df-n0 12511 df-z 12598 df-dec 12718 df-uz 12869 df-q 12979 df-rp 13023 df-xneg 13143 df-xadd 13144 df-xmul 13145 df-ioo 13382 df-ioc 13383 df-ico 13384 df-icc 13385 df-fz 13542 df-fzo 13690 df-fl 13832 df-mod 13910 df-seq 14045 df-exp 14105 df-fac 14317 df-bc 14346 df-hash 14374 df-shft 15111 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-limsup 15529 df-clim 15546 df-rlim 15547 df-sum 15745 df-ef 16127 df-sin 16129 df-cos 16130 df-pi 16132 df-dvds 16317 df-gcd 16559 df-prm 16736 df-pc 16903 df-struct 17213 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-mulr 17330 df-starv 17331 df-sca 17332 df-vsca 17333 df-ip 17334 df-tset 17335 df-ple 17336 df-ds 17338 df-unif 17339 df-hom 17340 df-cco 17341 df-rest 17481 df-topn 17482 df-0g 17500 df-gsum 17501 df-topgen 17502 df-pt 17503 df-prds 17506 df-xrs 17562 df-qtop 17567 df-imas 17568 df-xps 17570 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-submnd 18848 df-mulg 19140 df-cntz 19393 df-cmn 19858 df-psmet 21525 df-xmet 21526 df-met 21527 df-bl 21528 df-mopn 21529 df-fbas 21530 df-fg 21531 df-cnfld 21534 df-top 23062 df-topon 23079 df-topsp 23101 df-bases 23114 df-cld 23187 df-ntr 23188 df-cls 23189 df-nei 23266 df-lp 23304 df-perf 23305 df-cn 23395 df-cnp 23396 df-haus 23483 df-tx 23730 df-hmeo 23923 df-fil 24014 df-fm 24106 df-flim 24107 df-flf 24108 df-xms 24488 df-ms 24489 df-tms 24490 df-cncf 25048 df-limc 26036 df-dv 26037 df-log 26732 df-vma 27273 df-repr 35005

This theorem is used by: hgt750leme 35054

W3C validator