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 30734

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 11351	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		3nn0 11310	. . . . . 6 ⊢ 3 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ₀)
5		ssid 3624	. . . . . 6 ⊢ ℕ ⊆ ℕ
6	5	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ ⊆ ℕ)
7	2, 4, 6	reprfi2 30701	. . . 4 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
8		hgt750lemb.a	. . . . 5 ⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
9	8	ssrab3 3688	. . . 4 ⊢ 𝐴 ⊆ (ℕ(repr‘3)𝑁)
10		ssfi 8180	. . . 4 ⊢ (((ℕ(repr‘3)𝑁) ∈ Fin ∧ 𝐴 ⊆ (ℕ(repr‘3)𝑁)) → 𝐴 ∈ Fin)
11	7, 9, 10	sylancl 694	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
12		vmaf 24845	. . . . . 6 ⊢ Λ:ℕ⟶ℝ
13	12	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → Λ:ℕ⟶ℝ)
14	5	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ℕ ⊆ ℕ)
15	1	nnzd 11481	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
16	15	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℤ)
17	3	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 3 ∈ ℕ₀)
18		simpr 477	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ 𝐴)
19	9, 18	sseldi 3601	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
20	14, 16, 17, 19	reprf 30690	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛:(0..^3)⟶ℕ)
21		c0ex 10034	. . . . . . . . 9 ⊢ 0 ∈ V
22	21	tpid1 4303	. . . . . . . 8 ⊢ 0 ∈ {0, 1, 2}
23		fzo0to3tp 12554	. . . . . . . 8 ⊢ (0..^3) = {0, 1, 2}
24	22, 23	eleqtrri 2700	. . . . . . 7 ⊢ 0 ∈ (0..^3)
25	24	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ∈ (0..^3))
26	20, 25	ffvelrnd 6360	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℕ)
27	13, 26	ffvelrnd 6360	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℝ)
28		1ex 10035	. . . . . . . . . 10 ⊢ 1 ∈ V
29	28	tpid2 4304	. . . . . . . . 9 ⊢ 1 ∈ {0, 1, 2}
30	29, 23	eleqtrri 2700	. . . . . . . 8 ⊢ 1 ∈ (0..^3)
31	30	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 1 ∈ (0..^3))
32	20, 31	ffvelrnd 6360	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℕ)
33	13, 32	ffvelrnd 6360	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℝ)
34		2ex 11092	. . . . . . . . . 10 ⊢ 2 ∈ V
35	34	tpid3 4307	. . . . . . . . 9 ⊢ 2 ∈ {0, 1, 2}
36	35, 23	eleqtrri 2700	. . . . . . . 8 ⊢ 2 ∈ (0..^3)
37	36	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 2 ∈ (0..^3))
38	20, 37	ffvelrnd 6360	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℕ)
39	13, 38	ffvelrnd 6360	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ∈ ℝ)
40	33, 39	remulcld 10070	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
41	27, 40	remulcld 10070	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
42	11, 41	fsumrecl 14465	. 2 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
43	1	nnrpd 11870	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
44	43	relogcld 24369	. . 3 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
45	27, 33	remulcld 10070	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
46	11, 45	fsumrecl 14465	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
47	44, 46	remulcld 10070	. 2 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ∈ ℝ)
48		fzfi 12771	. . . . . . . 8 ⊢ (1...𝑁) ∈ Fin
49		diffi 8192	. . . . . . . 8 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
50	48, 49	ax-mp 5	. . . . . . 7 ⊢ ((1...𝑁) ∖ ℙ) ∈ Fin
51		snfi 8038	. . . . . . 7 ⊢ {2} ∈ Fin
52		unfi 8227	. . . . . . 7 ⊢ ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
53	50, 51, 52	mp2an 708	. . . . . 6 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
54	53	a1i 11	. . . . 5 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
55	12	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
56		difss 3737	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁)
57	56	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁))
58		2nn 11185	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
59	58	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ)
60		hgt750lemb.2	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 𝑁)
61		elfz1b 12409	. . . . . . . . . . . 12 ⊢ (2 ∈ (1...𝑁) ↔ (2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁))
62	61	biimpri 218	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁) → 2 ∈ (1...𝑁))
63	59, 1, 60, 62	syl3anc 1326	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ (1...𝑁))
64	63	snssd 4340	. . . . . . . . 9 ⊢ (𝜑 → {2} ⊆ (1...𝑁))
65	57, 64	unssd 3789	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ (1...𝑁))
66		fz1ssnn 12372	. . . . . . . . 9 ⊢ (1...𝑁) ⊆ ℕ
67	66	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
68	65, 67	sstrd 3613	. . . . . . 7 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
69	68	sselda 3603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
70	55, 69	ffvelrnd 6360	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
71	54, 70	fsumrecl 14465	. . . 4 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
72		fzfid 12772	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
73	12	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
74	67	sselda 3603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
75	73, 74	ffvelrnd 6360	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
76	72, 75	fsumrecl 14465	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
77	71, 76	remulcld 10070	. . 3 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
78	44, 77	remulcld 10070	. 2 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
79	1	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℕ)
80	79	nnrpd 11870	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℝ⁺)
81		relogcl 24322	. . . . . . 7 ⊢ (𝑁 ∈ ℝ⁺ → (log‘𝑁) ∈ ℝ)
82	80, 81	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℝ)
83	33, 82	remulcld 10070	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (log‘𝑁)) ∈ ℝ)
84	27, 83	remulcld 10070	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) ∈ ℝ)
85		vmage0 24847	. . . . . 6 ⊢ ((𝑛‘0) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘0)))
86	26, 85	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘0)))
87		vmage0 24847	. . . . . . 7 ⊢ ((𝑛‘1) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘1)))
88	32, 87	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘1)))
89	38	nnrpd 11870	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℝ⁺)
90	89	relogcld 24369	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ∈ ℝ)
91		vmalelog 24930	. . . . . . . 8 ⊢ ((𝑛‘2) ∈ ℕ → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
92	38, 91	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
93	14, 16, 17, 19, 37	reprle 30692	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ≤ 𝑁)
94		logleb 24349	. . . . . . . . 9 ⊢ (((𝑛‘2) ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → ((𝑛‘2) ≤ 𝑁 ↔ (log‘(𝑛‘2)) ≤ (log‘𝑁)))
95	94	biimpa 501	. . . . . . . 8 ⊢ ((((𝑛‘2) ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) ∧ (𝑛‘2) ≤ 𝑁) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
96	89, 80, 93, 95	syl21anc 1325	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
97	39, 90, 82, 92, 96	letrd 10194	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘𝑁))
98	39, 82, 33, 88, 97	lemul2ad 10964	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ≤ ((Λ‘(𝑛‘1)) · (log‘𝑁)))
99	40, 83, 27, 86, 98	lemul2ad 10964	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
100	11, 41, 84, 99	fsumle 14531	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
101	1	nncnd 11036	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
102	1	nnne0d 11065	. . . . . 6 ⊢ (𝜑 → 𝑁 ≠ 0)
103	101, 102	logcld 24317	. . . . 5 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
104	45	recnd 10068	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℂ)
105	11, 103, 104	fsummulc2 14516	. . . 4 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
106	103	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℂ)
107	106, 104	mulcomd 10061	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)))
108	27	recnd 10068	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℂ)
109	33	recnd 10068	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℂ)
110	108, 109, 106	mulassd 10063	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
111	107, 110	eqtrd 2656	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
112	111	sumeq2dv 14433	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
113	105, 112	eqtr2d 2657	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) = ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
114	100, 113	breqtrd 4679	. 2 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
115	1	nnred 11035	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ)
116	1	nnge1d 11063	. . . 4 ⊢ (𝜑 → 1 ≤ 𝑁)
117	115, 116	logge0d 24376	. . 3 ⊢ (𝜑 → 0 ≤ (log‘𝑁))
118		xpfi 8231	. . . . . 6 ⊢ (((((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
119	54, 72, 118	syl2anc 693	. . . . 5 ⊢ (𝜑 → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
120	12	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → Λ:ℕ⟶ℝ)
121	68	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
122		xp1st 7198	. . . . . . . . 9 ⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (1^st ‘𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
123	122	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1^st ‘𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
124	121, 123	sseldd 3604	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1^st ‘𝑢) ∈ ℕ)
125	120, 124	ffvelrnd 6360	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(1^st ‘𝑢)) ∈ ℝ)
126		xp2nd 7199	. . . . . . . . 9 ⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (2^nd ‘𝑢) ∈ (1...𝑁))
127	126	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2^nd ‘𝑢) ∈ (1...𝑁))
128	66, 127	sseldi 3601	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2^nd ‘𝑢) ∈ ℕ)
129	120, 128	ffvelrnd 6360	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(2^nd ‘𝑢)) ∈ ℝ)
130	125, 129	remulcld 10070	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℝ)
131		vmage0 24847	. . . . . . 7 ⊢ ((1^st ‘𝑢) ∈ ℕ → 0 ≤ (Λ‘(1^st ‘𝑢)))
132	124, 131	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(1^st ‘𝑢)))
133		vmage0 24847	. . . . . . 7 ⊢ ((2^nd ‘𝑢) ∈ ℕ → 0 ≤ (Λ‘(2^nd ‘𝑢)))
134	128, 133	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(2^nd ‘𝑢)))
135	125, 129, 132, 134	mulge0d 10604	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
136	5	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ℕ ⊆ ℕ)
137	15	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℤ)
138	3	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 3 ∈ ℕ₀)
139		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴)
140	9, 139	sseldi 3601	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
141	136, 137, 138, 140	reprf 30690	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐:(0..^3)⟶ℕ)
142	24	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 0 ∈ (0..^3))
143	141, 142	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℕ)
144	1	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℕ)
145	136, 137, 138, 140, 142	reprle 30692	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ≤ 𝑁)
146		elfz1b 12409	. . . . . . . . . . . . 13 ⊢ ((𝑐‘0) ∈ (1...𝑁) ↔ ((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁))
147	146	biimpri 218	. . . . . . . . . . . 12 ⊢ (((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁) → (𝑐‘0) ∈ (1...𝑁))
148	143, 144, 145, 147	syl3anc 1326	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ (1...𝑁))
149	8	rabeq2i 3197	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ 𝐴 ↔ (𝑐 ∈ (ℕ(repr‘3)𝑁) ∧ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
150	149	simprbi 480	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
151		hgt750leme.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
152	151	oddprm2 30733	. . . . . . . . . . . . . 14 ⊢ (ℙ ∖ {2}) = (𝑂 ∩ ℙ)
153	152	eleq2i 2693	. . . . . . . . . . . . 13 ⊢ ((𝑐‘0) ∈ (ℙ ∖ {2}) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
154	150, 153	sylnibr 319	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
155	139, 154	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
156	148, 155	jca 554	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
157		eldif 3584	. . . . . . . . . 10 ⊢ ((𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})) ↔ ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
158	156, 157	sylibr 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})))
159		uncom 3757	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) = ({2} ∪ ((1...𝑁) ∖ ℙ))
160		undif3 3888	. . . . . . . . . . . . 13 ⊢ ({2} ∪ ((1...𝑁) ∖ ℙ)) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
161	159, 160	eqtri 2644	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
162		ssequn1 3783	. . . . . . . . . . . . . 14 ⊢ ({2} ⊆ (1...𝑁) ↔ ({2} ∪ (1...𝑁)) = (1...𝑁))
163	64, 162	sylib 208	. . . . . . . . . . . . 13 ⊢ (𝜑 → ({2} ∪ (1...𝑁)) = (1...𝑁))
164	163	difeq1d 3727	. . . . . . . . . . . 12 ⊢ (𝜑 → (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2})) = ((1...𝑁) ∖ (ℙ ∖ {2})))
165	161, 164	syl5eq 2668	. . . . . . . . . . 11 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) = ((1...𝑁) ∖ (ℙ ∖ {2})))
166	165	eleq2d 2687	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))))
167	166	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))))
168	158, 167	mpbird 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
169	30	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ (0..^3))
170	141, 169	ffvelrnd 6360	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℕ)
171	136, 137, 138, 140, 169	reprle 30692	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ≤ 𝑁)
172		elfz1b 12409	. . . . . . . . . 10 ⊢ ((𝑐‘1) ∈ (1...𝑁) ↔ ((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁))
173	172	biimpri 218	. . . . . . . . 9 ⊢ (((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁) → (𝑐‘1) ∈ (1...𝑁))
174	170, 144, 171, 173	syl3anc 1326	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ (1...𝑁))
175	168, 174	opelxpd 5149	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
176	175	ralrimiva 2966	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
177		fveq1 6190	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
178		fveq1 6190	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → (𝑑‘1) = (𝑐‘1))
179	177, 178	opeq12d 4410	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → ⟨(𝑑‘0), (𝑑‘1)⟩ = ⟨(𝑐‘0), (𝑐‘1)⟩)
180	179	cbvmptv 4750	. . . . . . 7 ⊢ (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐 ∈ 𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩)
181	180	rnmptss 6392	. . . . . 6 ⊢ (∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
182	176, 181	syl 17	. . . . 5 ⊢ (𝜑 → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
183	119, 130, 135, 182	fsumless 14528	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ≤ Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
184		fvex 6201	. . . . . . . 8 ⊢ (𝑛‘0) ∈ V
185		fvex 6201	. . . . . . . 8 ⊢ (𝑛‘1) ∈ V
186	184, 185	op1std 7178	. . . . . . 7 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (1^st ‘𝑢) = (𝑛‘0))
187	186	fveq2d 6195	. . . . . 6 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(1^st ‘𝑢)) = (Λ‘(𝑛‘0)))
188	184, 185	op2ndd 7179	. . . . . . 7 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (2^nd ‘𝑢) = (𝑛‘1))
189	188	fveq2d 6195	. . . . . 6 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(2^nd ‘𝑢)) = (Λ‘(𝑛‘1)))
190	187, 189	oveq12d 6668	. . . . 5 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
191		opex 4932	. . . . . . . 8 ⊢ ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
192	191	rgenw 2924	. . . . . . 7 ⊢ ∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
193	180	fnmpt 6020	. . . . . . 7 ⊢ (∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
194	192, 193	mp1i 13	. . . . . 6 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
195		eqidd 2623	. . . . . 6 ⊢ (𝜑 → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
196	141	ad2antrr 762	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐:(0..^3)⟶ℕ)
197	196	ffnd 6046	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 Fn (0..^3))
198	20	ad4ant13 1292	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛:(0..^3)⟶ℕ)
199	198	ffnd 6046	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 Fn (0..^3))
200		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛))
201	180	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐 ∈ 𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩))
202	191	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V)
203	201, 202	fvmpt2d 6293	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
204	203	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
205	204	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
206	180	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐 ∈ 𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩))
207		fveq1 6190	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑛 → (𝑐‘0) = (𝑛‘0))
208		fveq1 6190	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑛 → (𝑐‘1) = (𝑛‘1))
209	207, 208	opeq12d 4410	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑛 → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
210	209	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐴) ∧ 𝑐 = 𝑛) → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
211		opex 4932	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V
212	211	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V)
213	206, 210, 18, 212	fvmptd 6288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
214	213	adantlr 751	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
215	214	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
216	200, 205, 215	3eqtr3d 2664	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
217	184, 185	opth2 4949	. . . . . . . . . . . . . . 15 ⊢ (⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩ ↔ ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1)))
218	216, 217	sylib 208	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1)))
219	218	simpld 475	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘0) = (𝑛‘0))
220	219	ad2antrr 762	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘0) = (𝑛‘0))
221		simpr 477	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → 𝑖 = 0)
222	221	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑐‘0))
223	221	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑛‘𝑖) = (𝑛‘0))
224	220, 222, 223	3eqtr4d 2666	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑛‘𝑖))
225	218	simprd 479	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘1) = (𝑛‘1))
226	225	ad2antrr 762	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘1) = (𝑛‘1))
227		simpr 477	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → 𝑖 = 1)
228	227	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑐‘1))
229	227	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑛‘𝑖) = (𝑛‘1))
230	226, 228, 229	3eqtr4d 2666	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑛‘𝑖))
231	219	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) = (𝑛‘0))
232	225	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) = (𝑛‘1))
233	231, 232	oveq12d 6668	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) = ((𝑛‘0) + (𝑛‘1)))
234	233	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑁 − ((𝑐‘0) + (𝑐‘1))) = (𝑁 − ((𝑛‘0) + (𝑛‘1))))
235	23	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (0..^3) = {0, 1, 2})
236	235	sumeq1d 14431	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗))
237	5	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ℕ ⊆ ℕ)
238	137	ad4antr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℤ)
239	3	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 3 ∈ ℕ₀)
240	140	ad4antr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
241	237, 238, 239, 240	reprsum 30691	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = 𝑁)
242		fveq2 6191	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑐‘𝑗) = (𝑐‘0))
243		fveq2 6191	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 1 → (𝑐‘𝑗) = (𝑐‘1))
244		fveq2 6191	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 2 → (𝑐‘𝑗) = (𝑐‘2))
245	143	nncnd 11036	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℂ)
246	245	ad4antr 768	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) ∈ ℂ)
247	170	nncnd 11036	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℂ)
248	247	ad4antr 768	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) ∈ ℂ)
249	36	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 2 ∈ (0..^3))
250	141, 249	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℕ)
251	250	nncnd 11036	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℂ)
252	251	ad4antr 768	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) ∈ ℂ)
253	246, 248, 252	3jca 1242	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) ∈ ℂ ∧ (𝑐‘1) ∈ ℂ ∧ (𝑐‘2) ∈ ℂ))
254	21, 28, 34	3pm3.2i 1239	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V)
255	254	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V))
256		0ne1 11088	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
257	256	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 1)
258		0ne2 11239	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 2
259	258	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 2)
260		1ne2 11240	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 2
261	260	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 1 ≠ 2)
262	242, 243, 244, 253, 255, 257, 259, 261	sumtp 14478	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗) = (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)))
263	236, 241, 262	3eqtr3rd 2665	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁)
264	246, 248	addcld 10059	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) ∈ ℂ)
265	101	ad5antr 770	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℂ)
266	264, 252, 265	addrsub 10448	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁 ↔ (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1)))))
267	263, 266	mpbid 222	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1))))
268	235	sumeq1d 14431	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗))
269	19	ad4ant13 1292	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
270	269	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
271	237, 238, 239, 270	reprsum 30691	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = 𝑁)
272		fveq2 6191	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑛‘𝑗) = (𝑛‘0))
273		fveq2 6191	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 1 → (𝑛‘𝑗) = (𝑛‘1))
274		fveq2 6191	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 2 → (𝑛‘𝑗) = (𝑛‘2))
275	26	nncnd 11036	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ)
276	275	adantlr 751	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ)
277	276	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘0) ∈ ℂ)
278	32	nncnd 11036	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ)
279	278	adantlr 751	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ)
280	279	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘1) ∈ ℂ)
281	38	nncnd 11036	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ)
282	281	adantlr 751	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ)
283	282	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) ∈ ℂ)
284	277, 280, 283	3jca 1242	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) ∈ ℂ ∧ (𝑛‘1) ∈ ℂ ∧ (𝑛‘2) ∈ ℂ))
285	272, 273, 274, 284, 255, 257, 259, 261	sumtp 14478	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗) = (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)))
286	268, 271, 285	3eqtr3rd 2665	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁)
287	277, 280	addcld 10059	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) + (𝑛‘1)) ∈ ℂ)
288	287, 283, 265	addrsub 10448	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁 ↔ (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1)))))
289	286, 288	mpbid 222	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1))))
290	234, 267, 289	3eqtr4d 2666	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑛‘2))
291		simpr 477	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑖 = 2)
292	291	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑐‘2))
293	291	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘𝑖) = (𝑛‘2))
294	290, 292, 293	3eqtr4d 2666	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑛‘𝑖))
295		simpr 477	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ (0..^3))
296	295, 23	syl6eleq 2711	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ {0, 1, 2})
297		vex 3203	. . . . . . . . . . . . 13 ⊢ 𝑖 ∈ V
298	297	eltp 4230	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ {0, 1, 2} ↔ (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2))
299	296, 298	sylib 208	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2))
300	224, 230, 294, 299	mpjao3dan 1395	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑐‘𝑖) = (𝑛‘𝑖))
301	197, 199, 300	eqfnfvd 6314	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 = 𝑛)
302	301	ex 450	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
303	302	anasss 679	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴)) → (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
304	303	ralrimivva 2971	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
305		dff1o6 6531	. . . . . . 7 ⊢ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴–1-1-onto→ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ↔ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴 ∧ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ∧ ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛)))
306	305	biimpri 218	. . . . . 6 ⊢ (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴 ∧ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ∧ ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛)) → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴–1-1-onto→ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
307	194, 195, 304, 306	syl3anc 1326	. . . . 5 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴–1-1-onto→ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
308	182	sselda 3603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
309	308, 125	syldan 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(1^st ‘𝑢)) ∈ ℝ)
310	308, 129	syldan 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(2^nd ‘𝑢)) ∈ ℝ)
311	309, 310	remulcld 10070	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℝ)
312	311	recnd 10068	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℂ)
313	190, 11, 307, 213, 312	fsumf1o 14454	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
314	76	recnd 10068	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℂ)
315	70	recnd 10068	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℂ)
316	54, 314, 315	fsummulc1 14517	. . . . 5 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
317	48	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (1...𝑁) ∈ Fin)
318	75	adantrl 752	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑗) ∈ ℝ)
319	318	anassrs 680	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
320	319	recnd 10068	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℂ)
321	317, 315, 320	fsummulc2 14516	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → ((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
322	321	sumeq2dv 14433	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
323		vex 3203	. . . . . . . . 9 ⊢ 𝑗 ∈ V
324	297, 323	op1std 7178	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (1^st ‘𝑢) = 𝑖)
325	324	fveq2d 6195	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(1^st ‘𝑢)) = (Λ‘𝑖))
326	297, 323	op2ndd 7179	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (2^nd ‘𝑢) = 𝑗)
327	326	fveq2d 6195	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(2^nd ‘𝑢)) = (Λ‘𝑗))
328	325, 327	oveq12d 6668	. . . . . 6 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = ((Λ‘𝑖) · (Λ‘𝑗)))
329	70	adantrr 753	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑖) ∈ ℝ)
330	329, 318	remulcld 10070	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℝ)
331	330	recnd 10068	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℂ)
332	328, 54, 72, 331	fsumxp 14503	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)) = Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
333	316, 322, 332	3eqtrrd 2661	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
334	183, 313, 333	3brtr3d 4684	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ≤ (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
335	46, 77, 44, 117, 334	lemul2ad 10964	. 2 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
336	42, 47, 78, 114, 335	letrd 10194	1 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∨ w3o 1036 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 {crab 2916 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 {csn 4177 {ctp 4181 ⟨cop 4183 class class class wbr 4653 ↦ cmpt 4729 × cxp 5112 ran crn 5115 Fn wfn 5883 ⟶wf 5884 –1-1-onto→wf1o 5887 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 2^nd c2nd 7167 Fincfn 7955 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 ≤ cle 10075 − cmin 10266 ℕcn 11020 2c2 11070 3c3 11071 ℕ₀cn0 11292 ℤcz 11377 ℝ⁺crp 11832 ...cfz 12326 ..^cfzo 12465 Σcsu 14416 ∥ cdvds 14983 ℙcprime 15385 logclog 24301 Λcvma 24818 reprcrepr 30686

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-sin 14800 df-cos 14801 df-pi 14803 df-dvds 14984 df-gcd 15217 df-prm 15386 df-pc 15542 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-log 24303 df-vma 24824 df-repr 30687

This theorem is referenced by: hgt750leme 30736

W3C validator