nnsum4primeseven - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > nnsum4primeseven		Structured version Visualization version GIF version

Theorem nnsum4primeseven 46468

Description: If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of 4 primes. (Contributed by AV, 25-Jul-2020.)

**Assertion**
Ref	Expression
nnsum4primeseven	⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))

Distinct variable group: 𝑓,𝑁,𝑘,𝑚

Proof of Theorem nnsum4primeseven Dummy variables 𝑜 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evengpop3 46466	. . . 4 ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3)))
2	1	imp 408	. . 3 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3))
3		simplll 774	. . . . . 6 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → ∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ))
4		6nn 12301	. . . . . . . . . . 11 ⊢ 6 ∈ ℕ
5	4	nnzi 12586	. . . . . . . . . 10 ⊢ 6 ∈ ℤ
6	5	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘9) → 6 ∈ ℤ)
7		3z 12595	. . . . . . . . . 10 ⊢ 3 ∈ ℤ
8	7	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘9) → 3 ∈ ℤ)
9		6p3e9 12372	. . . . . . . . . . . . 13 ⊢ (6 + 3) = 9
10	9	eqcomi 2742	. . . . . . . . . . . 12 ⊢ 9 = (6 + 3)
11	10	fveq2i 6895	. . . . . . . . . . 11 ⊢ (ℤ_≥‘9) = (ℤ_≥‘(6 + 3))
12	11	eleq2i 2826	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘9) ↔ 𝑁 ∈ (ℤ_≥‘(6 + 3)))
13	12	biimpi 215	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘9) → 𝑁 ∈ (ℤ_≥‘(6 + 3)))
14		eluzsub 12852	. . . . . . . . 9 ⊢ ((6 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑁 ∈ (ℤ_≥‘(6 + 3))) → (𝑁 − 3) ∈ (ℤ_≥‘6))
15	6, 8, 13, 14	syl3anc 1372	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘9) → (𝑁 − 3) ∈ (ℤ_≥‘6))
16	15	adantr 482	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even ) → (𝑁 − 3) ∈ (ℤ_≥‘6))
17	16	ad3antlr 730	. . . . . 6 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → (𝑁 − 3) ∈ (ℤ_≥‘6))
18		3odd 46376	. . . . . . . . . . . . 13 ⊢ 3 ∈ Odd
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘9) → 3 ∈ Odd )
20	19	anim1i 616	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even ) → (3 ∈ Odd ∧ 𝑁 ∈ Even ))
21	20	adantl 483	. . . . . . . . . 10 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) → (3 ∈ Odd ∧ 𝑁 ∈ Even ))
22	21	ancomd 463	. . . . . . . . 9 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) → (𝑁 ∈ Even ∧ 3 ∈ Odd ))
23	22	adantr 482	. . . . . . . 8 ⊢ (((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) → (𝑁 ∈ Even ∧ 3 ∈ Odd ))
24	23	adantr 482	. . . . . . 7 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → (𝑁 ∈ Even ∧ 3 ∈ Odd ))
25		emoo 46372	. . . . . . 7 ⊢ ((𝑁 ∈ Even ∧ 3 ∈ Odd ) → (𝑁 − 3) ∈ Odd )
26	24, 25	syl 17	. . . . . 6 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → (𝑁 − 3) ∈ Odd )
27		nnsum4primesodd 46464	. . . . . . 7 ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → (((𝑁 − 3) ∈ (ℤ_≥‘6) ∧ (𝑁 − 3) ∈ Odd ) → ∃𝑔 ∈ (ℙ ↑_m (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)))
28	27	imp 408	. . . . . 6 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ ((𝑁 − 3) ∈ (ℤ_≥‘6) ∧ (𝑁 − 3) ∈ Odd )) → ∃𝑔 ∈ (ℙ ↑_m (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘))
29	3, 17, 26, 28	syl12anc 836	. . . . 5 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → ∃𝑔 ∈ (ℙ ↑_m (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘))
30		simpr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 𝑔:(1...3)⟶ℙ)
31		4z 12596	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℤ
32		fzonel 13646	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 4 ∈ (1..^4)
33		fzoval 13633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ∈ ℤ → (1..^4) = (1...(4 − 1)))
34	31, 33	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1..^4) = (1...(4 − 1))
35		4cn 12297	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 4 ∈ ℂ
36		ax-1cn 11168	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℂ
37		3cn 12293	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℂ
38	35, 36, 37	3pm3.2i 1340	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 ∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ)
39		3p1e4 12357	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (3 + 1) = 4
40		subadd2 11464	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((4 ∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ) → ((4 − 1) = 3 ↔ (3 + 1) = 4))
41	39, 40	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((4 ∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ) → (4 − 1) = 3)
42	38, 41	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 − 1) = 3
43	42	oveq2i 7420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1...(4 − 1)) = (1...3)
44	34, 43	eqtri 2761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1..^4) = (1...3)
45	44	eqcomi 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...3) = (1..^4)
46	45	eleq2i 2826	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 ∈ (1...3) ↔ 4 ∈ (1..^4))
47	32, 46	mtbir 323	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 4 ∈ (1...3)
48	31, 47	pm3.2i 472	. . . . . . . . . . . . . . . . 17 ⊢ (4 ∈ ℤ ∧ ¬ 4 ∈ (1...3))
49	48	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (4 ∈ ℤ ∧ ¬ 4 ∈ (1...3)))
50		3prm 16631	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℙ
51	50	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 3 ∈ ℙ)
52		fsnunf 7183	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔:(1...3)⟶ℙ ∧ (4 ∈ ℤ ∧ ¬ 4 ∈ (1...3)) ∧ 3 ∈ ℙ) → (𝑔 ∪ {⟨4, 3⟩}):((1...3) ∪ {4})⟶ℙ)
53	30, 49, 51, 52	syl3anc 1372	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {⟨4, 3⟩}):((1...3) ∪ {4})⟶ℙ)
54		fzval3 13701	. . . . . . . . . . . . . . . . . 18 ⊢ (4 ∈ ℤ → (1...4) = (1..^(4 + 1)))
55	31, 54	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (1...4) = (1..^(4 + 1))
56		1z 12592	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℤ
57		1re 11214	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℝ
58		4re 12296	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℝ
59		1lt4 12388	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 4
60	57, 58, 59	ltleii 11337	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ≤ 4
61		eluz2 12828	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 ∈ (ℤ_≥‘1) ↔ (1 ∈ ℤ ∧ 4 ∈ ℤ ∧ 1 ≤ 4))
62	56, 31, 60, 61	mpbir3an 1342	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ (ℤ_≥‘1)
63		fzosplitsn 13740	. . . . . . . . . . . . . . . . . 18 ⊢ (4 ∈ (ℤ_≥‘1) → (1..^(4 + 1)) = ((1..^4) ∪ {4}))
64	62, 63	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (1..^(4 + 1)) = ((1..^4) ∪ {4})
65	44	uneq1i 4160	. . . . . . . . . . . . . . . . 17 ⊢ ((1..^4) ∪ {4}) = ((1...3) ∪ {4})
66	55, 64, 65	3eqtri 2765	. . . . . . . . . . . . . . . 16 ⊢ (1...4) = ((1...3) ∪ {4})
67	66	feq2i 6710	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∪ {⟨4, 3⟩}):(1...4)⟶ℙ ↔ (𝑔 ∪ {⟨4, 3⟩}):((1...3) ∪ {4})⟶ℙ)
68	53, 67	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {⟨4, 3⟩}):(1...4)⟶ℙ)
69		prmex 16614	. . . . . . . . . . . . . . . 16 ⊢ ℙ ∈ V
70		ovex 7442	. . . . . . . . . . . . . . . 16 ⊢ (1...4) ∈ V
71	69, 70	pm3.2i 472	. . . . . . . . . . . . . . 15 ⊢ (ℙ ∈ V ∧ (1...4) ∈ V)
72		elmapg 8833	. . . . . . . . . . . . . . 15 ⊢ ((ℙ ∈ V ∧ (1...4) ∈ V) → ((𝑔 ∪ {⟨4, 3⟩}) ∈ (ℙ ↑_m (1...4)) ↔ (𝑔 ∪ {⟨4, 3⟩}):(1...4)⟶ℙ))
73	71, 72	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩}) ∈ (ℙ ↑_m (1...4)) ↔ (𝑔 ∪ {⟨4, 3⟩}):(1...4)⟶ℙ))
74	68, 73	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {⟨4, 3⟩}) ∈ (ℙ ↑_m (1...4)))
75	74	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (𝑔 ∪ {⟨4, 3⟩}) ∈ (ℙ ↑_m (1...4)))
76		fveq1 6891	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨4, 3⟩}) → (𝑓‘𝑘) = ((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
77	76	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (𝑔 ∪ {⟨4, 3⟩}) ∧ 𝑘 ∈ (1...4)) → (𝑓‘𝑘) = ((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
78	77	sumeq2dv 15649	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑔 ∪ {⟨4, 3⟩}) → Σ𝑘 ∈ (1...4)(𝑓‘𝑘) = Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
79	78	eqeq2d 2744	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑔 ∪ {⟨4, 3⟩}) → (𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘) ↔ 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘)))
80	79	adantl 483	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) ∧ 𝑓 = (𝑔 ∪ {⟨4, 3⟩})) → (𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘) ↔ 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘)))
81	62	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 4 ∈ (ℤ_≥‘1))
82	66	eleq2i 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...4) ↔ 𝑘 ∈ ((1...3) ∪ {4}))
83		elun 4149	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ((1...3) ∪ {4}) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 ∈ {4}))
84		velsn 4645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ {4} ↔ 𝑘 = 4)
85	84	orbi2i 912	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ (1...3) ∨ 𝑘 ∈ {4}) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 = 4))
86	82, 83, 85	3bitri 297	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (1...4) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 = 4))
87		elfz2 13491	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (1...3) ↔ ((1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (1 ≤ 𝑘 ∧ 𝑘 ≤ 3)))
88		3re 12292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 3 ∈ ℝ
89	88, 58	pm3.2i 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (3 ∈ ℝ ∧ 4 ∈ ℝ)
90		3lt4 12386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 3 < 4
91		ltnle 11293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((3 ∈ ℝ ∧ 4 ∈ ℝ) → (3 < 4 ↔ ¬ 4 ≤ 3))
92	90, 91	mpbii 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((3 ∈ ℝ ∧ 4 ∈ ℝ) → ¬ 4 ≤ 3)
93	89, 92	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ¬ 4 ≤ 3
94		breq1 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 4 → (𝑘 ≤ 3 ↔ 4 ≤ 3))
95	94	eqcoms 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (4 = 𝑘 → (𝑘 ≤ 3 ↔ 4 ≤ 3))
96	93, 95	mtbiri 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (4 = 𝑘 → ¬ 𝑘 ≤ 3)
97	96	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 ∈ ℤ → (4 = 𝑘 → ¬ 𝑘 ≤ 3))
98	97	necon2ad 2956	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ ℤ → (𝑘 ≤ 3 → 4 ≠ 𝑘))
99	98	adantld 492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ℤ → ((1 ≤ 𝑘 ∧ 𝑘 ≤ 3) → 4 ≠ 𝑘))
100	99	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((1 ≤ 𝑘 ∧ 𝑘 ≤ 3) → 4 ≠ 𝑘))
101	100	imp 408	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (1 ≤ 𝑘 ∧ 𝑘 ≤ 3)) → 4 ≠ 𝑘)
102	87, 101	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (1...3) → 4 ≠ 𝑘)
103	102	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → 4 ≠ 𝑘)
104		fvunsn 7177	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (4 ≠ 𝑘 → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (𝑔‘𝑘))
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (𝑔‘𝑘))
106		ffvelcdm 7084	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:(1...3)⟶ℙ ∧ 𝑘 ∈ (1...3)) → (𝑔‘𝑘) ∈ ℙ)
107	106	ancoms 460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔‘𝑘) ∈ ℙ)
108		prmz 16612	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔‘𝑘) ∈ ℙ → (𝑔‘𝑘) ∈ ℤ)
109	107, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔‘𝑘) ∈ ℤ)
110	109	zcnd 12667	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔‘𝑘) ∈ ℂ)
111	105, 110	eqeltrd 2834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ)
112	111	ex 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...3) → (𝑔:(1...3)⟶ℙ → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
113	112	adantld 492	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...3) → ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
114		fveq2 6892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 4 → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = ((𝑔 ∪ {⟨4, 3⟩})‘4))
115	31	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔:(1...3)⟶ℙ → 4 ∈ ℤ)
116	7	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔:(1...3)⟶ℙ → 3 ∈ ℤ)
117		fdm 6727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:(1...3)⟶ℙ → dom 𝑔 = (1...3))
118		eleq2 2823	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (dom 𝑔 = (1...3) → (4 ∈ dom 𝑔 ↔ 4 ∈ (1...3)))
119	47, 118	mtbiri 327	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (dom 𝑔 = (1...3) → ¬ 4 ∈ dom 𝑔)
120	117, 119	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔:(1...3)⟶ℙ → ¬ 4 ∈ dom 𝑔)
121		fsnunfv 7185	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((4 ∈ ℤ ∧ 3 ∈ ℤ ∧ ¬ 4 ∈ dom 𝑔) → ((𝑔 ∪ {⟨4, 3⟩})‘4) = 3)
122	115, 116, 120, 121	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔:(1...3)⟶ℙ → ((𝑔 ∪ {⟨4, 3⟩})‘4) = 3)
123	122	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘4) = 3)
124	114, 123	sylan9eq 2793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 = 4 ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ)) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = 3)
125	124, 37	eqeltrdi 2842	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 = 4 ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ)) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ)
126	125	ex 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 4 → ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
127	113, 126	jaoi 856	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ (1...3) ∨ 𝑘 = 4) → ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
128	127	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑘 ∈ (1...3) ∨ 𝑘 = 4) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
129	86, 128	biimtrid 241	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑘 ∈ (1...4) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
130	129	imp 408	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...4)) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ)
131	81, 130, 114	fsumm1 15697	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘) + ((𝑔 ∪ {⟨4, 3⟩})‘4)))
132	131	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘) + ((𝑔 ∪ {⟨4, 3⟩})‘4)))
133	42	eqcomi 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ 3 = (4 − 1)
134	133	oveq2i 7420	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...3) = (1...(4 − 1))
135	134	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (1...3) = (1...(4 − 1)))
136	102	adantl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → 4 ≠ 𝑘)
137	136, 104	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (𝑔‘𝑘))
138	137	eqcomd 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → (𝑔‘𝑘) = ((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
139	135, 138	sumeq12dv 15652	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → Σ𝑘 ∈ (1...3)(𝑔‘𝑘) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
140	139	eqeq2d 2744	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) ↔ (𝑁 − 3) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘)))
141	140	biimpa 478	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (𝑁 − 3) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
142	141	eqcomd 2739	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (𝑁 − 3))
143	142	oveq1d 7424	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘) + ((𝑔 ∪ {⟨4, 3⟩})‘4)) = ((𝑁 − 3) + ((𝑔 ∪ {⟨4, 3⟩})‘4)))
144	31	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 4 ∈ ℤ)
145	7	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 3 ∈ ℤ)
146	120	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ¬ 4 ∈ dom 𝑔)
147	144, 145, 146, 121	syl3anc 1372	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘4) = 3)
148	147	oveq2d 7425	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + ((𝑔 ∪ {⟨4, 3⟩})‘4)) = ((𝑁 − 3) + 3))
149		eluzelcn 12834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘9) → 𝑁 ∈ ℂ)
150	37	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘9) → 3 ∈ ℂ)
151	149, 150	npcand 11575	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘9) → ((𝑁 − 3) + 3) = 𝑁)
152	151	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + 3) = 𝑁)
153	148, 152	eqtrd 2773	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + ((𝑔 ∪ {⟨4, 3⟩})‘4)) = 𝑁)
154	153	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → ((𝑁 − 3) + ((𝑔 ∪ {⟨4, 3⟩})‘4)) = 𝑁)
155	132, 143, 154	3eqtrrd 2778	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
156	75, 80, 155	rspcedvd 3615	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))
157	156	ex 414	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
158	157	expcom 415	. . . . . . . . 9 ⊢ (𝑔:(1...3)⟶ℙ → (𝑁 ∈ (ℤ_≥‘9) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))))
159		elmapi 8843	. . . . . . . . 9 ⊢ (𝑔 ∈ (ℙ ↑_m (1...3)) → 𝑔:(1...3)⟶ℙ)
160	158, 159	syl11 33	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘9) → (𝑔 ∈ (ℙ ↑_m (1...3)) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))))
161	160	rexlimdv 3154	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘9) → (∃𝑔 ∈ (ℙ ↑_m (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
162	161	adantr 482	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even ) → (∃𝑔 ∈ (ℙ ↑_m (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
163	162	ad3antlr 730	. . . . 5 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → (∃𝑔 ∈ (ℙ ↑_m (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
164	29, 163	mpd 15	. . . 4 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOddW ) ∧ 𝑁 = (𝑜 + 3)) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))
165	164	rexlimdva2 3158	. . 3 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) → (∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
166	2, 165	mpd 15	. 2 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ (𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even )) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))
167	166	ex 414	1 ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ∪ cun 3947 {csn 4629 ⟨cop 4635 class class class wbr 5149 dom cdm 5677 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 ↑_m cmap 8820 ℂcc 11108 ℝcr 11109 1c1 11111 + caddc 11113 < clt 11248 ≤ cle 11249 − cmin 11444 3c3 12268 4c4 12269 5c5 12270 6c6 12271 9c9 12274 ℤcz 12558 ℤ_≥cuz 12822 ...cfz 13484 ..^cfzo 13627 Σcsu 15632 ℙcprime 16608 Even ceven 46292 Odd codd 46293 GoldbachOddW cgbow 46414

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-inf2 9636 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-pre-sup 11188

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-2o 8467 df-er 8703 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9437 df-oi 9505 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-7 12280 df-8 12281 df-9 12282 df-n0 12473 df-z 12559 df-uz 12823 df-rp 12975 df-fz 13485 df-fzo 13628 df-seq 13967 df-exp 14028 df-hash 14291 df-cj 15046 df-re 15047 df-im 15048 df-sqrt 15182 df-abs 15183 df-clim 15432 df-sum 15633 df-dvds 16198 df-prm 16609 df-even 46294 df-odd 46295 df-gbow 46417

This theorem is referenced by: wtgoldbnnsum4prm 46470

W3C validator