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 31500

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 11792	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3		3nn0 11752	. . . . . 6 ⊢ 3 ∈ ℕ₀
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ₀)
5		ssidd 3906	. . . . 5 ⊢ (𝜑 → ℕ ⊆ ℕ)
6	2, 4, 5	reprfi2 31467	. . . 4 ⊢ (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
7		hgt750lemb.a	. . . . 5 ⊢ 𝐴 = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
8	7	ssrab3 3973	. . . 4 ⊢ 𝐴 ⊆ (ℕ(repr‘3)𝑁)
9		ssfi 8574	. . . 4 ⊢ (((ℕ(repr‘3)𝑁) ∈ Fin ∧ 𝐴 ⊆ (ℕ(repr‘3)𝑁)) → 𝐴 ∈ Fin)
10	6, 8, 9	sylancl 586	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
11		vmaf 25366	. . . . . 6 ⊢ Λ:ℕ⟶ℝ
12	11	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → Λ:ℕ⟶ℝ)
13		ssidd 3906	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ℕ ⊆ ℕ)
14	1	nnzd 11924	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
15	14	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℤ)
16	3	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 3 ∈ ℕ₀)
17		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ 𝐴)
18	8, 17	sseldi 3882	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
19	13, 15, 16, 18	reprf 31456	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛:(0..^3)⟶ℕ)
20		c0ex 10470	. . . . . . . . 9 ⊢ 0 ∈ V
21	20	tpid1 4605	. . . . . . . 8 ⊢ 0 ∈ {0, 1, 2}
22		fzo0to3tp 12961	. . . . . . . 8 ⊢ (0..^3) = {0, 1, 2}
23	21, 22	eleqtrri 2880	. . . . . . 7 ⊢ 0 ∈ (0..^3)
24	23	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ∈ (0..^3))
25	19, 24	ffvelrnd 6708	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℕ)
26	12, 25	ffvelrnd 6708	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℝ)
27		1ex 10472	. . . . . . . . . 10 ⊢ 1 ∈ V
28	27	tpid2 4607	. . . . . . . . 9 ⊢ 1 ∈ {0, 1, 2}
29	28, 22	eleqtrri 2880	. . . . . . . 8 ⊢ 1 ∈ (0..^3)
30	29	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 1 ∈ (0..^3))
31	19, 30	ffvelrnd 6708	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℕ)
32	12, 31	ffvelrnd 6708	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℝ)
33		2ex 11551	. . . . . . . . . 10 ⊢ 2 ∈ V
34	33	tpid3 4610	. . . . . . . . 9 ⊢ 2 ∈ {0, 1, 2}
35	34, 22	eleqtrri 2880	. . . . . . . 8 ⊢ 2 ∈ (0..^3)
36	35	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 2 ∈ (0..^3))
37	19, 36	ffvelrnd 6708	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℕ)
38	12, 37	ffvelrnd 6708	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ∈ ℝ)
39	32, 38	remulcld 10506	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
40	26, 39	remulcld 10506	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
41	10, 40	fsumrecl 14912	. 2 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
42	1	nnrpd 12268	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
43	42	relogcld 24875	. . 3 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
44	26, 32	remulcld 10506	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
45	10, 44	fsumrecl 14912	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℝ)
46	43, 45	remulcld 10506	. 2 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ∈ ℝ)
47		fzfi 13178	. . . . . . . 8 ⊢ (1...𝑁) ∈ Fin
48		diffi 8586	. . . . . . . 8 ⊢ ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
49	47, 48	ax-mp 5	. . . . . . 7 ⊢ ((1...𝑁) ∖ ℙ) ∈ Fin
50		snfi 8432	. . . . . . 7 ⊢ {2} ∈ Fin
51		unfi 8621	. . . . . . 7 ⊢ ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
52	49, 50, 51	mp2an 688	. . . . . 6 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
53	52	a1i 11	. . . . 5 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
54	11	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
55		difss 4024	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁)
56	55	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ (1...𝑁))
57		2nn 11547	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
58	57	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ)
59		hgt750lemb.2	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 𝑁)
60		elfz1b 12815	. . . . . . . . . . . 12 ⊢ (2 ∈ (1...𝑁) ↔ (2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁))
61	60	biimpri 229	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁) → 2 ∈ (1...𝑁))
62	58, 1, 59, 61	syl3anc 1362	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ (1...𝑁))
63	62	snssd 4643	. . . . . . . . 9 ⊢ (𝜑 → {2} ⊆ (1...𝑁))
64	56, 63	unssd 4078	. . . . . . . 8 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ (1...𝑁))
65		fz1ssnn 12777	. . . . . . . . 9 ⊢ (1...𝑁) ⊆ ℕ
66	65	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
67	64, 66	sstrd 3894	. . . . . . 7 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
68	67	sselda 3884	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
69	54, 68	ffvelrnd 6708	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
70	53, 69	fsumrecl 14912	. . . 4 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
71		fzfid 13179	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
72	11	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
73	66	sselda 3884	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
74	72, 73	ffvelrnd 6708	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
75	71, 74	fsumrecl 14912	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
76	70, 75	remulcld 10506	. . 3 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
77	43, 76	remulcld 10506	. 2 ⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
78	1	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℕ)
79	78	nnrpd 12268	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ ℝ⁺)
80		relogcl 24828	. . . . . . 7 ⊢ (𝑁 ∈ ℝ⁺ → (log‘𝑁) ∈ ℝ)
81	79, 80	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℝ)
82	32, 81	remulcld 10506	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (log‘𝑁)) ∈ ℝ)
83	26, 82	remulcld 10506	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) ∈ ℝ)
84		vmage0 25368	. . . . . 6 ⊢ ((𝑛‘0) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘0)))
85	25, 84	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘0)))
86		vmage0 25368	. . . . . . 7 ⊢ ((𝑛‘1) ∈ ℕ → 0 ≤ (Λ‘(𝑛‘1)))
87	31, 86	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 0 ≤ (Λ‘(𝑛‘1)))
88	37	nnrpd 12268	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℝ⁺)
89	88	relogcld 24875	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ∈ ℝ)
90		vmalelog 25451	. . . . . . . 8 ⊢ ((𝑛‘2) ∈ ℕ → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
91	37, 90	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘(𝑛‘2)))
92	13, 15, 16, 18, 36	reprle 31458	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ≤ 𝑁)
93		logleb 24855	. . . . . . . . 9 ⊢ (((𝑛‘2) ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → ((𝑛‘2) ≤ 𝑁 ↔ (log‘(𝑛‘2)) ≤ (log‘𝑁)))
94	93	biimpa 477	. . . . . . . 8 ⊢ ((((𝑛‘2) ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) ∧ (𝑛‘2) ≤ 𝑁) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
95	88, 79, 92, 94	syl21anc 834	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘(𝑛‘2)) ≤ (log‘𝑁))
96	38, 89, 81, 91, 95	letrd 10633	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘2)) ≤ (log‘𝑁))
97	38, 81, 32, 87, 96	lemul2ad 11417	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ≤ ((Λ‘(𝑛‘1)) · (log‘𝑁)))
98	39, 82, 26, 85, 97	lemul2ad 11417	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
99	10, 40, 83, 98	fsumle 14975	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
100	1	nncnd 11491	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
101	1	nnne0d 11524	. . . . . 6 ⊢ (𝜑 → 𝑁 ≠ 0)
102	100, 101	logcld 24823	. . . . 5 ⊢ (𝜑 → (log‘𝑁) ∈ ℂ)
103	44	recnd 10504	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ∈ ℂ)
104	10, 102, 103	fsummulc2 14960	. . . 4 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
105	102	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (log‘𝑁) ∈ ℂ)
106	105, 103	mulcomd 10497	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)))
107	26	recnd 10504	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘0)) ∈ ℂ)
108	32	recnd 10504	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (Λ‘(𝑛‘1)) ∈ ℂ)
109	107, 108, 105	mulassd 10499	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) · (log‘𝑁)) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
110	106, 109	eqtrd 2829	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
111	110	sumeq2dv 14881	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((log‘𝑁) · ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))))
112	104, 111	eqtr2d 2830	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (log‘𝑁))) = ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
113	99, 112	breqtrd 4982	. 2 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))))
114	1	nnred 11490	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℝ)
115	1	nnge1d 11522	. . . 4 ⊢ (𝜑 → 1 ≤ 𝑁)
116	114, 115	logge0d 24882	. . 3 ⊢ (𝜑 → 0 ≤ (log‘𝑁))
117		xpfi 8625	. . . . . 6 ⊢ (((((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
118	53, 71, 117	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) ∈ Fin)
119	11	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → Λ:ℕ⟶ℝ)
120	67	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
121		xp1st 7568	. . . . . . . . 9 ⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (1^st ‘𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
122	121	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1^st ‘𝑢) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
123	120, 122	sseldd 3885	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (1^st ‘𝑢) ∈ ℕ)
124	119, 123	ffvelrnd 6708	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(1^st ‘𝑢)) ∈ ℝ)
125		xp2nd 7569	. . . . . . . . 9 ⊢ (𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → (2^nd ‘𝑢) ∈ (1...𝑁))
126	125	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2^nd ‘𝑢) ∈ (1...𝑁))
127	65, 126	sseldi 3882	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (2^nd ‘𝑢) ∈ ℕ)
128	119, 127	ffvelrnd 6708	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → (Λ‘(2^nd ‘𝑢)) ∈ ℝ)
129	124, 128	remulcld 10506	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℝ)
130		vmage0 25368	. . . . . . 7 ⊢ ((1^st ‘𝑢) ∈ ℕ → 0 ≤ (Λ‘(1^st ‘𝑢)))
131	123, 130	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(1^st ‘𝑢)))
132		vmage0 25368	. . . . . . 7 ⊢ ((2^nd ‘𝑢) ∈ ℕ → 0 ≤ (Λ‘(2^nd ‘𝑢)))
133	127, 132	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ (Λ‘(2^nd ‘𝑢)))
134	124, 128, 131, 133	mulge0d 11054	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))) → 0 ≤ ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
135		ssidd 3906	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ℕ ⊆ ℕ)
136	14	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℤ)
137	3	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 3 ∈ ℕ₀)
138		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴)
139	8, 138	sseldi 3882	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
140	135, 136, 137, 139	reprf 31456	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐:(0..^3)⟶ℕ)
141	23	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 0 ∈ (0..^3))
142	140, 141	ffvelrnd 6708	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℕ)
143	1	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℕ)
144	135, 136, 137, 139, 141	reprle 31458	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ≤ 𝑁)
145		elfz1b 12815	. . . . . . . . . . . . 13 ⊢ ((𝑐‘0) ∈ (1...𝑁) ↔ ((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁))
146	145	biimpri 229	. . . . . . . . . . . 12 ⊢ (((𝑐‘0) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘0) ≤ 𝑁) → (𝑐‘0) ∈ (1...𝑁))
147	142, 143, 144, 146	syl3anc 1362	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ (1...𝑁))
148	7	rabeq2i 3427	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ 𝐴 ↔ (𝑐 ∈ (ℕ(repr‘3)𝑁) ∧ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
149	148	simprbi 497	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
150		hgt750leme.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
151	150	oddprm2 31499	. . . . . . . . . . . . . 14 ⊢ (ℙ ∖ {2}) = (𝑂 ∩ ℙ)
152	151	eleq2i 2872	. . . . . . . . . . . . 13 ⊢ ((𝑐‘0) ∈ (ℙ ∖ {2}) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ))
153	149, 152	sylnibr 330	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐴 → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
154	138, 153	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ¬ (𝑐‘0) ∈ (ℙ ∖ {2}))
155	147, 154	jca 512	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
156		eldif 3864	. . . . . . . . . 10 ⊢ ((𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})) ↔ ((𝑐‘0) ∈ (1...𝑁) ∧ ¬ (𝑐‘0) ∈ (ℙ ∖ {2})))
157	155, 156	sylibr 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2})))
158		uncom 4045	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) = ({2} ∪ ((1...𝑁) ∖ ℙ))
159		undif3 4180	. . . . . . . . . . . . 13 ⊢ ({2} ∪ ((1...𝑁) ∖ ℙ)) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
160	158, 159	eqtri 2817	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∖ ℙ) ∪ {2}) = (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2}))
161		ssequn1 4072	. . . . . . . . . . . . . 14 ⊢ ({2} ⊆ (1...𝑁) ↔ ({2} ∪ (1...𝑁)) = (1...𝑁))
162	63, 161	sylib 219	. . . . . . . . . . . . 13 ⊢ (𝜑 → ({2} ∪ (1...𝑁)) = (1...𝑁))
163	162	difeq1d 4014	. . . . . . . . . . . 12 ⊢ (𝜑 → (({2} ∪ (1...𝑁)) ∖ (ℙ ∖ {2})) = ((1...𝑁) ∖ (ℙ ∖ {2})))
164	160, 163	syl5eq 2841	. . . . . . . . . . 11 ⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) = ((1...𝑁) ∖ (ℙ ∖ {2})))
165	164	eleq2d 2866	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))))
166	165	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ↔ (𝑐‘0) ∈ ((1...𝑁) ∖ (ℙ ∖ {2}))))
167	157, 166	mpbird 258	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ (((1...𝑁) ∖ ℙ) ∪ {2}))
168	29	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ (0..^3))
169	140, 168	ffvelrnd 6708	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℕ)
170	135, 136, 137, 139, 168	reprle 31458	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ≤ 𝑁)
171		elfz1b 12815	. . . . . . . . . 10 ⊢ ((𝑐‘1) ∈ (1...𝑁) ↔ ((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁))
172	171	biimpri 229	. . . . . . . . 9 ⊢ (((𝑐‘1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑐‘1) ≤ 𝑁) → (𝑐‘1) ∈ (1...𝑁))
173	169, 143, 170, 172	syl3anc 1362	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ (1...𝑁))
174	167, 173	opelxpd 5473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
175	174	ralrimiva 3147	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
176		fveq1 6529	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
177		fveq1 6529	. . . . . . . . 9 ⊢ (𝑑 = 𝑐 → (𝑑‘1) = (𝑐‘1))
178	176, 177	opeq12d 4712	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → ⟨(𝑑‘0), (𝑑‘1)⟩ = ⟨(𝑐‘0), (𝑐‘1)⟩)
179	178	cbvmptv 5055	. . . . . . 7 ⊢ (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐 ∈ 𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩)
180	179	rnmptss 6740	. . . . . 6 ⊢ (∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)) → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
181	175, 180	syl 17	. . . . 5 ⊢ (𝜑 → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ⊆ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
182	118, 129, 134, 181	fsumless 14972	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ≤ Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
183		fvex 6543	. . . . . . . 8 ⊢ (𝑛‘0) ∈ V
184		fvex 6543	. . . . . . . 8 ⊢ (𝑛‘1) ∈ V
185	183, 184	op1std 7546	. . . . . . 7 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (1^st ‘𝑢) = (𝑛‘0))
186	185	fveq2d 6534	. . . . . 6 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(1^st ‘𝑢)) = (Λ‘(𝑛‘0)))
187	183, 184	op2ndd 7547	. . . . . . 7 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (2^nd ‘𝑢) = (𝑛‘1))
188	187	fveq2d 6534	. . . . . 6 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → (Λ‘(2^nd ‘𝑢)) = (Λ‘(𝑛‘1)))
189	186, 188	oveq12d 7025	. . . . 5 ⊢ (𝑢 = ⟨(𝑛‘0), (𝑛‘1)⟩ → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
190		opex 5241	. . . . . . . 8 ⊢ ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
191	190	rgenw 3115	. . . . . . 7 ⊢ ∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V
192	179	fnmpt 6348	. . . . . . 7 ⊢ (∀𝑐 ∈ 𝐴 ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
193	191, 192	mp1i 13	. . . . . 6 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴)
194		eqidd 2794	. . . . . 6 ⊢ (𝜑 → ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
195	140	ad2antrr 722	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐:(0..^3)⟶ℕ)
196	195	ffnd 6375	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 Fn (0..^3))
197	19	ad4ant13 747	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛:(0..^3)⟶ℕ)
198	197	ffnd 6375	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 Fn (0..^3))
199		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛))
200	179	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = (𝑐 ∈ 𝐴 ↦ ⟨(𝑐‘0), (𝑐‘1)⟩))
201	190	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ⟨(𝑐‘0), (𝑐‘1)⟩ ∈ V)
202	200, 201	fvmpt2d 6638	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
203	202	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
204	203	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ⟨(𝑐‘0), (𝑐‘1)⟩)
205		fveq1 6529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑛 → (𝑐‘0) = (𝑛‘0))
206		fveq1 6529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑛 → (𝑐‘1) = (𝑛‘1))
207	205, 206	opeq12d 4712	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑛 → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
208		opex 5241	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V
209	208	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(𝑛‘0), (𝑛‘1)⟩ ∈ V)
210	179, 207, 17, 209	fvmptd3 6648	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
211	210	adantlr 711	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
212	211	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) = ⟨(𝑛‘0), (𝑛‘1)⟩)
213	199, 204, 212	3eqtr3d 2837	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩)
214	183, 184	opth2 5257	. . . . . . . . . . . . . . 15 ⊢ (⟨(𝑐‘0), (𝑐‘1)⟩ = ⟨(𝑛‘0), (𝑛‘1)⟩ ↔ ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1)))
215	213, 214	sylib 219	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → ((𝑐‘0) = (𝑛‘0) ∧ (𝑐‘1) = (𝑛‘1)))
216	215	simpld 495	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘0) = (𝑛‘0))
217	216	ad2antrr 722	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘0) = (𝑛‘0))
218		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → 𝑖 = 0)
219	218	fveq2d 6534	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑐‘0))
220	218	fveq2d 6534	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑛‘𝑖) = (𝑛‘0))
221	217, 219, 220	3eqtr4d 2839	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 0) → (𝑐‘𝑖) = (𝑛‘𝑖))
222	215	simprd 496	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → (𝑐‘1) = (𝑛‘1))
223	222	ad2antrr 722	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘1) = (𝑛‘1))
224		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → 𝑖 = 1)
225	224	fveq2d 6534	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑐‘1))
226	224	fveq2d 6534	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑛‘𝑖) = (𝑛‘1))
227	223, 225, 226	3eqtr4d 2839	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 1) → (𝑐‘𝑖) = (𝑛‘𝑖))
228	216	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) = (𝑛‘0))
229	222	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) = (𝑛‘1))
230	228, 229	oveq12d 7025	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) = ((𝑛‘0) + (𝑛‘1)))
231	230	oveq2d 7023	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑁 − ((𝑐‘0) + (𝑐‘1))) = (𝑁 − ((𝑛‘0) + (𝑛‘1))))
232	22	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (0..^3) = {0, 1, 2})
233	232	sumeq1d 14879	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗))
234		ssidd 3906	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ℕ ⊆ ℕ)
235	136	ad4antr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℤ)
236	3	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 3 ∈ ℕ₀)
237	139	ad4antr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑐 ∈ (ℕ(repr‘3)𝑁))
238	234, 235, 236, 237	reprsum 31457	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑐‘𝑗) = 𝑁)
239		fveq2 6530	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑐‘𝑗) = (𝑐‘0))
240		fveq2 6530	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 1 → (𝑐‘𝑗) = (𝑐‘1))
241		fveq2 6530	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 2 → (𝑐‘𝑗) = (𝑐‘2))
242	142	nncnd 11491	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘0) ∈ ℂ)
243	242	ad4antr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘0) ∈ ℂ)
244	169	nncnd 11491	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℂ)
245	244	ad4antr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘1) ∈ ℂ)
246	35	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 2 ∈ (0..^3))
247	140, 246	ffvelrnd 6708	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℕ)
248	247	nncnd 11491	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘2) ∈ ℂ)
249	248	ad4antr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) ∈ ℂ)
250	243, 245, 249	3jca 1119	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) ∈ ℂ ∧ (𝑐‘1) ∈ ℂ ∧ (𝑐‘2) ∈ ℂ))
251	20, 27, 33	3pm3.2i 1330	. . . . . . . . . . . . . . . . 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 11545	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
254	253	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 1)
255		0ne2 11681	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 2
256	255	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 0 ≠ 2)
257		1ne2 11682	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 2
258	257	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 1 ≠ 2)
259	239, 240, 241, 250, 252, 254, 256, 258	sumtp 14925	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑐‘𝑗) = (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)))
260	233, 238, 259	3eqtr3rd 2838	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁)
261	243, 245	addcld 10495	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑐‘0) + (𝑐‘1)) ∈ ℂ)
262	100	ad5antr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑁 ∈ ℂ)
263	261, 249, 262	addrsub 10894	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑐‘0) + (𝑐‘1)) + (𝑐‘2)) = 𝑁 ↔ (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1)))))
264	260, 263	mpbid 233	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑁 − ((𝑐‘0) + (𝑐‘1))))
265	232	sumeq1d 14879	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗))
266	18	ad4ant13 747	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
267	266	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
268	234, 235, 236, 267	reprsum 31457	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ (0..^3)(𝑛‘𝑗) = 𝑁)
269		fveq2 6530	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → (𝑛‘𝑗) = (𝑛‘0))
270		fveq2 6530	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 1 → (𝑛‘𝑗) = (𝑛‘1))
271		fveq2 6530	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 2 → (𝑛‘𝑗) = (𝑛‘2))
272	25	nncnd 11491	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ)
273	272	adantlr 711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘0) ∈ ℂ)
274	273	ad3antrrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘0) ∈ ℂ)
275	31	nncnd 11491	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ)
276	275	adantlr 711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘1) ∈ ℂ)
277	276	ad3antrrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘1) ∈ ℂ)
278	37	nncnd 11491	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ)
279	278	adantlr 711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (𝑛‘2) ∈ ℂ)
280	279	ad3antrrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) ∈ ℂ)
281	274, 277, 280	3jca 1119	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) ∈ ℂ ∧ (𝑛‘1) ∈ ℂ ∧ (𝑛‘2) ∈ ℂ))
282	269, 270, 271, 281, 252, 254, 256, 258	sumtp 14925	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → Σ𝑗 ∈ {0, 1, 2} (𝑛‘𝑗) = (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)))
283	265, 268, 282	3eqtr3rd 2838	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁)
284	274, 277	addcld 10495	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((𝑛‘0) + (𝑛‘1)) ∈ ℂ)
285	284, 280, 262	addrsub 10894	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → ((((𝑛‘0) + (𝑛‘1)) + (𝑛‘2)) = 𝑁 ↔ (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1)))))
286	283, 285	mpbid 233	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘2) = (𝑁 − ((𝑛‘0) + (𝑛‘1))))
287	231, 264, 286	3eqtr4d 2839	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘2) = (𝑛‘2))
288		simpr 485	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → 𝑖 = 2)
289	288	fveq2d 6534	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑐‘2))
290	288	fveq2d 6534	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑛‘𝑖) = (𝑛‘2))
291	287, 289, 290	3eqtr4d 2839	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) ∧ 𝑖 = 2) → (𝑐‘𝑖) = (𝑛‘𝑖))
292		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ (0..^3))
293	292, 22	syl6eleq 2891	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → 𝑖 ∈ {0, 1, 2})
294		vex 3435	. . . . . . . . . . . . 13 ⊢ 𝑖 ∈ V
295	294	eltp 4527	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ {0, 1, 2} ↔ (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2))
296	293, 295	sylib 219	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑖 = 0 ∨ 𝑖 = 1 ∨ 𝑖 = 2))
297	221, 227, 291, 296	mpjao3dan 1422	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) ∧ 𝑖 ∈ (0..^3)) → (𝑐‘𝑖) = (𝑛‘𝑖))
298	196, 198, 297	eqfnfvd 6661	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) ∧ ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛)) → 𝑐 = 𝑛)
299	298	ex 413	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑛 ∈ 𝐴) → (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
300	299	anasss 467	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ 𝐴 ∧ 𝑛 ∈ 𝐴)) → (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
301	300	ralrimivva 3156	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛))
302		dff1o6 6888	. . . . . . 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 229	. . . . . 6 ⊢ (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) Fn 𝐴 ∧ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) = ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩) ∧ ∀𝑐 ∈ 𝐴 ∀𝑛 ∈ 𝐴 (((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑐) = ((𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)‘𝑛) → 𝑐 = 𝑛)) → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴–1-1-onto→ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
304	193, 194, 301, 303	syl3anc 1362	. . . . 5 ⊢ (𝜑 → (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩):𝐴–1-1-onto→ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩))
305	181	sselda 3884	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → 𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁)))
306	305, 124	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(1^st ‘𝑢)) ∈ ℝ)
307	305, 128	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → (Λ‘(2^nd ‘𝑢)) ∈ ℝ)
308	306, 307	remulcld 10506	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℝ)
309	308	recnd 10504	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)) → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) ∈ ℂ)
310	189, 10, 304, 210, 309	fsumf1o 14901	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ran (𝑑 ∈ 𝐴 ↦ ⟨(𝑑‘0), (𝑑‘1)⟩)((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))))
311	75	recnd 10504	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℂ)
312	69	recnd 10504	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℂ)
313	53, 311, 312	fsummulc1 14961	. . . . 5 ⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
314	47	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (1...𝑁) ∈ Fin)
315	74	adantrl 712	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑗) ∈ ℝ)
316	315	anassrs 468	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
317	316	recnd 10504	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℂ)
318	314, 312, 317	fsummulc2 14960	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → ((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
319	318	sumeq2dv 14881	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})((Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) = Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)))
320		vex 3435	. . . . . . . . 9 ⊢ 𝑗 ∈ V
321	294, 320	op1std 7546	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (1^st ‘𝑢) = 𝑖)
322	321	fveq2d 6534	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(1^st ‘𝑢)) = (Λ‘𝑖))
323	294, 320	op2ndd 7547	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (2^nd ‘𝑢) = 𝑗)
324	323	fveq2d 6534	. . . . . . 7 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (Λ‘(2^nd ‘𝑢)) = (Λ‘𝑗))
325	322, 324	oveq12d 7025	. . . . . 6 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → ((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = ((Λ‘𝑖) · (Λ‘𝑗)))
326	69	adantrr 713	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → (Λ‘𝑖) ∈ ℝ)
327	326, 315	remulcld 10506	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℝ)
328	327	recnd 10504	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2}) ∧ 𝑗 ∈ (1...𝑁))) → ((Λ‘𝑖) · (Λ‘𝑗)) ∈ ℂ)
329	325, 53, 71, 328	fsumxp 14948	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})Σ𝑗 ∈ (1...𝑁)((Λ‘𝑖) · (Λ‘𝑗)) = Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))))
330	313, 319, 329	3eqtrrd 2834	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ ((((1...𝑁) ∖ ℙ) ∪ {2}) × (1...𝑁))((Λ‘(1^st ‘𝑢)) · (Λ‘(2^nd ‘𝑢))) = (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
331	182, 310, 330	3brtr3d 4987	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1))) ≤ (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))
332	45, 76, 43, 116, 331	lemul2ad 11417	. 2 ⊢ (𝜑 → ((log‘𝑁) · Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · (Λ‘(𝑛‘1)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
333	41, 46, 77, 113, 332	letrd 10633	1 ⊢ (𝜑 → Σ𝑛 ∈ 𝐴 ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ w3o 1077 ∧ w3a 1078 = wceq 1520 ∈ wcel 2079 ≠ wne 2982 ∀wral 3103 {crab 3107 Vcvv 3432 ∖ cdif 3851 ∪ cun 3852 ∩ cin 3853 ⊆ wss 3854 {csn 4466 {ctp 4470 ⟨cop 4472 class class class wbr 4956 ↦ cmpt 5035 × cxp 5433 ran crn 5436 Fn wfn 6212 ⟶wf 6213 –1-1-onto→wf1o 6216 ‘cfv 6217 (class class class)co 7007 1^st c1st 7534 2^nd c2nd 7535 Fincfn 8347 ℂcc 10370 ℝcr 10371 0cc0 10372 1c1 10373 + caddc 10375 · cmul 10377 ≤ cle 10511 − cmin 10706 ℕcn 11475 2c2 11529 3c3 11530 ℕ₀cn0 11734 ℤcz 11818 ℝ⁺crp 12228 ...cfz 12731 ..^cfzo 12872 Σcsu 14864 ∥ cdvds 15428 ℙcprime 15832 logclog 24807 Λcvma 25339 reprcrepr 31452

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-rep 5075 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-inf2 8939 ax-cnex 10428 ax-resscn 10429 ax-1cn 10430 ax-icn 10431 ax-addcl 10432 ax-addrcl 10433 ax-mulcl 10434 ax-mulrcl 10435 ax-mulcom 10436 ax-addass 10437 ax-mulass 10438 ax-distr 10439 ax-i2m1 10440 ax-1ne0 10441 ax-1rid 10442 ax-rnegex 10443 ax-rrecex 10444 ax-cnre 10445 ax-pre-lttri 10446 ax-pre-lttrn 10447 ax-pre-ltadd 10448 ax-pre-mulgt0 10449 ax-pre-sup 10450 ax-addf 10451 ax-mulf 10452

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1079 df-3an 1080 df-tru 1523 df-fal 1533 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-nel 3089 df-ral 3108 df-rex 3109 df-reu 3110 df-rmo 3111 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-pss 3871 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-tp 4471 df-op 4473 df-uni 4740 df-int 4777 df-iun 4821 df-iin 4822 df-br 4957 df-opab 5019 df-mpt 5036 df-tr 5058 df-id 5340 df-eprel 5345 df-po 5354 df-so 5355 df-fr 5394 df-se 5395 df-we 5396 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-pred 6015 df-ord 6061 df-on 6062 df-lim 6063 df-suc 6064 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-isom 6226 df-riota 6968 df-ov 7010 df-oprab 7011 df-mpo 7012 df-of 7258 df-om 7428 df-1st 7536 df-2nd 7537 df-supp 7673 df-wrecs 7789 df-recs 7851 df-rdg 7889 df-1o 7944 df-2o 7945 df-oadd 7948 df-er 8130 df-map 8249 df-pm 8250 df-ixp 8301 df-en 8348 df-dom 8349 df-sdom 8350 df-fin 8351 df-fsupp 8670 df-fi 8711 df-sup 8742 df-inf 8743 df-oi 8810 df-dju 9165 df-card 9203 df-pnf 10512 df-mnf 10513 df-xr 10514 df-ltxr 10515 df-le 10516 df-sub 10708 df-neg 10709 df-div 11135 df-nn 11476 df-2 11537 df-3 11538 df-4 11539 df-5 11540 df-6 11541 df-7 11542 df-8 11543 df-9 11544 df-n0 11735 df-z 11819 df-dec 11937 df-uz 12083 df-q 12187 df-rp 12229 df-xneg 12346 df-xadd 12347 df-xmul 12348 df-ioo 12581 df-ioc 12582 df-ico 12583 df-icc 12584 df-fz 12732 df-fzo 12873 df-fl 13000 df-mod 13076 df-seq 13208 df-exp 13268 df-fac 13472 df-bc 13501 df-hash 13529 df-shft 14248 df-cj 14280 df-re 14281 df-im 14282 df-sqrt 14416 df-abs 14417 df-limsup 14650 df-clim 14667 df-rlim 14668 df-sum 14865 df-ef 15242 df-sin 15244 df-cos 15245 df-pi 15247 df-dvds 15429 df-gcd 15665 df-prm 15833 df-pc 15991 df-struct 16302 df-ndx 16303 df-slot 16304 df-base 16306 df-sets 16307 df-ress 16308 df-plusg 16395 df-mulr 16396 df-starv 16397 df-sca 16398 df-vsca 16399 df-ip 16400 df-tset 16401 df-ple 16402 df-ds 16404 df-unif 16405 df-hom 16406 df-cco 16407 df-rest 16513 df-topn 16514 df-0g 16532 df-gsum 16533 df-topgen 16534 df-pt 16535 df-prds 16538 df-xrs 16592 df-qtop 16597 df-imas 16598 df-xps 16600 df-mre 16674 df-mrc 16675 df-acs 16677 df-mgm 17669 df-sgrp 17711 df-mnd 17722 df-submnd 17763 df-mulg 17970 df-cntz 18176 df-cmn 18623 df-psmet 20207 df-xmet 20208 df-met 20209 df-bl 20210 df-mopn 20211 df-fbas 20212 df-fg 20213 df-cnfld 20216 df-top 21174 df-topon 21191 df-topsp 21213 df-bases 21226 df-cld 21299 df-ntr 21300 df-cls 21301 df-nei 21378 df-lp 21416 df-perf 21417 df-cn 21507 df-cnp 21508 df-haus 21595 df-tx 21842 df-hmeo 22035 df-fil 22126 df-fm 22218 df-flim 22219 df-flf 22220 df-xms 22601 df-ms 22602 df-tms 22603 df-cncf 23157 df-limc 24135 df-dv 24136 df-log 24809 df-vma 25345 df-repr 31453

This theorem is referenced by: hgt750leme 31502

W3C validator