Theorem nnsum4primeseven 40216

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 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑𝑚 (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 40214	. . . 4 ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOdd 𝑁 = (𝑜 + 3)))
2	1	imp 444	. . 3 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) → ∃𝑜 ∈ GoldbachOdd 𝑁 = (𝑜 + 3))
3		simplll 794	. . . . . . 7 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = (𝑜 + 3)) → ∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ))
4		6nn 11066	. . . . . . . . . . . 12 ⊢ 6 ∈ ℕ
5	4	nnzi 11278	. . . . . . . . . . 11 ⊢ 6 ∈ ℤ
6	5	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘9) → 6 ∈ ℤ)
7		3z 11287	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘9) → 3 ∈ ℤ)
9		6p3e9 11047	. . . . . . . . . . . . . 14 ⊢ (6 + 3) = 9
10	9	eqcomi 2619	. . . . . . . . . . . . 13 ⊢ 9 = (6 + 3)
11	10	fveq2i 6106	. . . . . . . . . . . 12 ⊢ (ℤ≥‘9) = (ℤ≥‘(6 + 3))
12	11	eleq2i 2680	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ≥‘9) ↔ 𝑁 ∈ (ℤ≥‘(6 + 3)))
13	12	biimpi 205	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘9) → 𝑁 ∈ (ℤ≥‘(6 + 3)))
14		eluzsub 11593	. . . . . . . . . 10 ⊢ ((6 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(6 + 3))) → (𝑁 − 3) ∈ (ℤ≥‘6))
15	6, 8, 13, 14	syl3anc 1318	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘9) → (𝑁 − 3) ∈ (ℤ≥‘6))
16	15	adantr 480	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (𝑁 − 3) ∈ (ℤ≥‘6))
17	16	ad3antlr 763	. . . . . . 7 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = (𝑜 + 3)) → (𝑁 − 3) ∈ (ℤ≥‘6))
18		3odd 40155	. . . . . . . . . . . . . 14 ⊢ 3 ∈ Odd
19	18	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ≥‘9) → 3 ∈ Odd )
20	19	anim1i 590	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (3 ∈ Odd ∧ 𝑁 ∈ Even ))
21	20	adantl 481	. . . . . . . . . . 11 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) → (3 ∈ Odd ∧ 𝑁 ∈ Even ))
22	21	ancomd 466	. . . . . . . . . 10 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) → (𝑁 ∈ Even ∧ 3 ∈ Odd ))
23	22	adantr 480	. . . . . . . . 9 ⊢ (((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOdd ) → (𝑁 ∈ Even ∧ 3 ∈ Odd ))
24	23	adantr 480	. . . . . . . 8 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = (𝑜 + 3)) → (𝑁 ∈ Even ∧ 3 ∈ Odd ))
25		emoo 40151	. . . . . . . 8 ⊢ ((𝑁 ∈ Even ∧ 3 ∈ Odd ) → (𝑁 − 3) ∈ Odd )
26	24, 25	syl 17	. . . . . . 7 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = (𝑜 + 3)) → (𝑁 − 3) ∈ Odd )
27		nnsum4primesodd 40212	. . . . . . . 8 ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → (((𝑁 − 3) ∈ (ℤ≥‘6) ∧ (𝑁 − 3) ∈ Odd ) → ∃𝑔 ∈ (ℙ ↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)))
28	27	imp 444	. . . . . . 7 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ((𝑁 − 3) ∈ (ℤ≥‘6) ∧ (𝑁 − 3) ∈ Odd )) → ∃𝑔 ∈ (ℙ ↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘))
29	3, 17, 26, 28	syl12anc 1316	. . . . . 6 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = (𝑜 + 3)) → ∃𝑔 ∈ (ℙ ↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘))
30		elmapi 7765	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (ℙ ↑𝑚 (1...3)) → 𝑔:(1...3)⟶ℙ)
31		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 𝑔:(1...3)⟶ℙ)
32		4z 11288	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℤ
33		fzonel 12352	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 4 ∈ (1..^4)
34		fzoval 12340	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 ∈ ℤ → (1..^4) = (1...(4 − 1)))
35	32, 34	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1..^4) = (1...(4 − 1))
36		4cn 10975	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 4 ∈ ℂ
37		ax-1cn 9873	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 1 ∈ ℂ
38		3cn 10972	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 3 ∈ ℂ
39	36, 37, 38	3pm3.2i 1232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (4 ∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ)
40		3p1e4 11030	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (3 + 1) = 4
41		subadd2 10164	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((4 ∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ) → ((4 − 1) = 3 ↔ (3 + 1) = 4))
42	40, 41	mpbiri 247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((4 ∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ) → (4 − 1) = 3)
43	39, 42	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 − 1) = 3
44	43	oveq2i 6560	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...(4 − 1)) = (1...3)
45	35, 44	eqtri 2632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1..^4) = (1...3)
46	45	eqcomi 2619	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1...3) = (1..^4)
47	46	eleq2i 2680	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (4 ∈ (1...3) ↔ 4 ∈ (1..^4))
48	33, 47	mtbir 312	. . . . . . . . . . . . . . . . . . . 20 ⊢ ¬ 4 ∈ (1...3)
49	32, 48	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 ∈ ℤ ∧ ¬ 4 ∈ (1...3))
50	49	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (4 ∈ ℤ ∧ ¬ 4 ∈ (1...3)))
51		3prm 15244	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℙ
52	51	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 3 ∈ ℙ)
53		fsnunf 6356	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔:(1...3)⟶ℙ ∧ (4 ∈ ℤ ∧ ¬ 4 ∈ (1...3)) ∧ 3 ∈ ℙ) → (𝑔 ∪ {⟨4, 3⟩}):((1...3) ∪ {4})⟶ℙ)
54	31, 50, 52, 53	syl3anc 1318	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {⟨4, 3⟩}):((1...3) ∪ {4})⟶ℙ)
55		fzval3 12404	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 ∈ ℤ → (1...4) = (1..^(4 + 1)))
56	32, 55	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...4) = (1..^(4 + 1))
57		1z 11284	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℤ
58		1re 9918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ
59		4re 10974	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 4 ∈ ℝ
60		1lt4 11076	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < 4
61	58, 59, 60	ltleii 10039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≤ 4
62		eluz2 11569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (4 ∈ (ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 4 ∈ ℤ ∧ 1 ≤ 4))
63	57, 32, 61, 62	mpbir3an 1237	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ (ℤ≥‘1)
64		fzosplitsn 12442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 ∈ (ℤ≥‘1) → (1..^(4 + 1)) = ((1..^4) ∪ {4}))
65	63, 64	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (1..^(4 + 1)) = ((1..^4) ∪ {4})
66	45	uneq1i 3725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1..^4) ∪ {4}) = ((1...3) ∪ {4})
67	56, 65, 66	3eqtri 2636	. . . . . . . . . . . . . . . . . 18 ⊢ (1...4) = ((1...3) ∪ {4})
68	67	feq2i 5950	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∪ {⟨4, 3⟩}):(1...4)⟶ℙ ↔ (𝑔 ∪ {⟨4, 3⟩}):((1...3) ∪ {4})⟶ℙ)
69	54, 68	sylibr 223	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {⟨4, 3⟩}):(1...4)⟶ℙ)
70		prmex 15229	. . . . . . . . . . . . . . . . . 18 ⊢ ℙ ∈ V
71		ovex 6577	. . . . . . . . . . . . . . . . . 18 ⊢ (1...4) ∈ V
72	70, 71	pm3.2i 470	. . . . . . . . . . . . . . . . 17 ⊢ (ℙ ∈ V ∧ (1...4) ∈ V)
73		elmapg 7757	. . . . . . . . . . . . . . . . 17 ⊢ ((ℙ ∈ V ∧ (1...4) ∈ V) → ((𝑔 ∪ {⟨4, 3⟩}) ∈ (ℙ ↑𝑚 (1...4)) ↔ (𝑔 ∪ {⟨4, 3⟩}):(1...4)⟶ℙ))
74	72, 73	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩}) ∈ (ℙ ↑𝑚 (1...4)) ↔ (𝑔 ∪ {⟨4, 3⟩}):(1...4)⟶ℙ))
75	69, 74	mpbird 246	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔 ∪ {⟨4, 3⟩}) ∈ (ℙ ↑𝑚 (1...4)))
76	75	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (𝑔 ∪ {⟨4, 3⟩}) ∈ (ℙ ↑𝑚 (1...4)))
77		fveq1 6102	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑔 ∪ {⟨4, 3⟩}) → (𝑓‘𝑘) = ((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
78	77	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = (𝑔 ∪ {⟨4, 3⟩}) ∧ 𝑘 ∈ (1...4)) → (𝑓‘𝑘) = ((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
79	78	sumeq2dv 14281	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∪ {⟨4, 3⟩}) → Σ𝑘 ∈ (1...4)(𝑓‘𝑘) = Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
80	79	eqeq2d 2620	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑔 ∪ {⟨4, 3⟩}) → (𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘) ↔ 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘)))
81	80	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) ∧ 𝑓 = (𝑔 ∪ {⟨4, 3⟩})) → (𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘) ↔ 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘)))
82	63	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 4 ∈ (ℤ≥‘1))
83	67	eleq2i 2680	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...4) ↔ 𝑘 ∈ ((1...3) ∪ {4}))
84		elun 3715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ((1...3) ∪ {4}) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 ∈ {4}))
85		velsn 4141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ {4} ↔ 𝑘 = 4)
86	85	orbi2i 540	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (1...3) ∨ 𝑘 ∈ {4}) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 = 4))
87	83, 84, 86	3bitri 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...4) ↔ (𝑘 ∈ (1...3) ∨ 𝑘 = 4))
88		elfz2 12204	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ (1...3) ↔ ((1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (1 ≤ 𝑘 ∧ 𝑘 ≤ 3)))
89		3re 10971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 3 ∈ ℝ
90	89, 59	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (3 ∈ ℝ ∧ 4 ∈ ℝ)
91		3lt4 11074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 3 < 4
92		ltnle 9996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((3 ∈ ℝ ∧ 4 ∈ ℝ) → (3 < 4 ↔ ¬ 4 ≤ 3))
93	91, 92	mpbii 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((3 ∈ ℝ ∧ 4 ∈ ℝ) → ¬ 4 ≤ 3)
94	90, 93	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ¬ 4 ≤ 3
95		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 = 4 → (𝑘 ≤ 3 ↔ 4 ≤ 3))
96	95	eqcoms 2618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (4 = 𝑘 → (𝑘 ≤ 3 ↔ 4 ≤ 3))
97	94, 96	mtbiri 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (4 = 𝑘 → ¬ 𝑘 ≤ 3)
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ ℤ → (4 = 𝑘 → ¬ 𝑘 ≤ 3))
99	98	necon2ad 2797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ ℤ → (𝑘 ≤ 3 → 4 ≠ 𝑘))
100	99	adantld 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 ∈ ℤ → ((1 ≤ 𝑘 ∧ 𝑘 ≤ 3) → 4 ≠ 𝑘))
101	100	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((1 ≤ 𝑘 ∧ 𝑘 ≤ 3) → 4 ≠ 𝑘))
102	101	imp 444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (1 ≤ 𝑘 ∧ 𝑘 ≤ 3)) → 4 ≠ 𝑘)
103	88, 102	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ (1...3) → 4 ≠ 𝑘)
104	103	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → 4 ≠ 𝑘)
105		fvunsn 6350	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 ≠ 𝑘 → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (𝑔‘𝑘))
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (𝑔‘𝑘))
107		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑔:(1...3)⟶ℙ ∧ 𝑘 ∈ (1...3)) → (𝑔‘𝑘) ∈ ℙ)
108	107	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔‘𝑘) ∈ ℙ)
109		prmz 15227	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔‘𝑘) ∈ ℙ → (𝑔‘𝑘) ∈ ℤ)
110	108, 109	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔‘𝑘) ∈ ℤ)
111	110	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → (𝑔‘𝑘) ∈ ℂ)
112	106, 111	eqeltrd 2688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ (1...3) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ)
113	112	ex 449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (1...3) → (𝑔:(1...3)⟶ℙ → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
114	113	adantld 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...3) → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
115		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 4 → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = ((𝑔 ∪ {⟨4, 3⟩})‘4))
116	32	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:(1...3)⟶ℙ → 4 ∈ ℤ)
117	7	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:(1...3)⟶ℙ → 3 ∈ ℤ)
118		fdm 5964	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔:(1...3)⟶ℙ → dom 𝑔 = (1...3))
119		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (dom 𝑔 = (1...3) → (4 ∈ dom 𝑔 ↔ 4 ∈ (1...3)))
120	48, 119	mtbiri 316	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (dom 𝑔 = (1...3) → ¬ 4 ∈ dom 𝑔)
121	118, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔:(1...3)⟶ℙ → ¬ 4 ∈ dom 𝑔)
122		fsnunfv 6358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((4 ∈ ℤ ∧ 3 ∈ ℤ ∧ ¬ 4 ∈ dom 𝑔) → ((𝑔 ∪ {⟨4, 3⟩})‘4) = 3)
123	116, 117, 121, 122	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:(1...3)⟶ℙ → ((𝑔 ∪ {⟨4, 3⟩})‘4) = 3)
124	123	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘4) = 3)
125	115, 124	sylan9eq 2664	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 = 4 ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ)) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = 3)
126	125, 38	syl6eqel 2696	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 = 4 ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ)) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ)
127	126	ex 449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 4 → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
128	114, 127	jaoi 393	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ (1...3) ∨ 𝑘 = 4) → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
129	128	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑘 ∈ (1...3) ∨ 𝑘 = 4) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
130	87, 129	syl5bi 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (𝑘 ∈ (1...4) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ))
131	130	imp 444	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...4)) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) ∈ ℂ)
132	82, 131, 115	fsumm1 14324	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘) + ((𝑔 ∪ {⟨4, 3⟩})‘4)))
133	132	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘) + ((𝑔 ∪ {⟨4, 3⟩})‘4)))
134	43	eqcomi 2619	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 = (4 − 1)
135	134	oveq2i 6560	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1...3) = (1...(4 − 1))
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → (1...3) = (1...(4 − 1)))
137	103	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → 4 ≠ 𝑘)
138	137, 105	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → ((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (𝑔‘𝑘))
139	138	eqcomd 2616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ 𝑘 ∈ (1...3)) → (𝑔‘𝑘) = ((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
140	136, 139	sumeq12dv 14284	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → Σ𝑘 ∈ (1...3)(𝑔‘𝑘) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
141	140	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) ↔ (𝑁 − 3) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘)))
142	141	biimpa 500	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (𝑁 − 3) = Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
143	142	eqcomd 2616	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘) = (𝑁 − 3))
144	143	oveq1d 6564	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → (Σ𝑘 ∈ (1...(4 − 1))((𝑔 ∪ {⟨4, 3⟩})‘𝑘) + ((𝑔 ∪ {⟨4, 3⟩})‘4)) = ((𝑁 − 3) + ((𝑔 ∪ {⟨4, 3⟩})‘4)))
145	32	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 4 ∈ ℤ)
146	7	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → 3 ∈ ℤ)
147	121	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ¬ 4 ∈ dom 𝑔)
148	145, 146, 147, 122	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑔 ∪ {⟨4, 3⟩})‘4) = 3)
149	148	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + ((𝑔 ∪ {⟨4, 3⟩})‘4)) = ((𝑁 − 3) + 3))
150		eluzelcn 11575	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ≥‘9) → 𝑁 ∈ ℂ)
151	38	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ≥‘9) → 3 ∈ ℂ)
152	150, 151	npcand 10275	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ≥‘9) → ((𝑁 − 3) + 3) = 𝑁)
153	152	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + 3) = 𝑁)
154	149, 153	eqtrd 2644	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) + ((𝑔 ∪ {⟨4, 3⟩})‘4)) = 𝑁)
155	154	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → ((𝑁 − 3) + ((𝑔 ∪ {⟨4, 3⟩})‘4)) = 𝑁)
156	133, 144, 155	3eqtrrd 2649	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → 𝑁 = Σ𝑘 ∈ (1...4)((𝑔 ∪ {⟨4, 3⟩})‘𝑘))
157	76, 81, 156	rspcedvd 3289	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) ∧ (𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘)) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))
158	157	ex 449	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑔:(1...3)⟶ℙ) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
159	158	expcom 450	. . . . . . . . . . 11 ⊢ (𝑔:(1...3)⟶ℙ → (𝑁 ∈ (ℤ≥‘9) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))))
160	30, 159	syl 17	. . . . . . . . . 10 ⊢ (𝑔 ∈ (ℙ ↑𝑚 (1...3)) → (𝑁 ∈ (ℤ≥‘9) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))))
161	160	com12 32	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘9) → (𝑔 ∈ (ℙ ↑𝑚 (1...3)) → ((𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))))
162	161	rexlimdv 3012	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ≥‘9) → (∃𝑔 ∈ (ℙ ↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
163	162	adantr 480	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → (∃𝑔 ∈ (ℙ ↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
164	163	ad3antlr 763	. . . . . 6 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = (𝑜 + 3)) → (∃𝑔 ∈ (ℙ ↑𝑚 (1...3))(𝑁 − 3) = Σ𝑘 ∈ (1...3)(𝑔‘𝑘) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
165	29, 164	mpd 15	. . . . 5 ⊢ ((((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = (𝑜 + 3)) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))
166	165	ex 449	. . . 4 ⊢ (((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) ∧ 𝑜 ∈ GoldbachOdd ) → (𝑁 = (𝑜 + 3) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
167	166	rexlimdva 3013	. . 3 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) → (∃𝑜 ∈ GoldbachOdd 𝑁 = (𝑜 + 3) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))
168	2, 167	mpd 15	. 2 ⊢ ((∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ (𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even )) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))
169	168	ex 449	1 ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑𝑚 (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∪ cun 3538  {csn 4125  ⟨cop 4131   class class class wbr 4583  dom cdm 5038  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↑_𝑚 cmap 7744  ℂcc 9813  ℝcr 9814  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  3c3 10948  4c4 10949  5c5 10950  6c6 10951  9c9 10954  ℤcz 11254  ℤ_≥cuz 11563  ...cfz 12197  ..^cfzo 12334  Σcsu 14264  ℙcprime 15223   Even ceven 40075   Odd codd 40076   GoldbachOdd cgbo 40168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-dvds 14822  df-prm 15224  df-even 40077  df-odd 40078  df-gbo 40171

This theorem is referenced by:  wtgoldbnnsum4prm  40218