bgoldbtbnd - Mathbox for Alexander van der Vekens

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

Theorem bgoldbtbnd 45149

Description: If the binary Goldbach conjecture is valid up to an integer 𝑁, and there is a series ("ladder") of primes with a difference of at most 𝑁 up to an integer 𝑀, then the strong ternary Goldbach conjecture is valid up to 𝑀, see section 1.2.2 in [Helfgott] p. 4 with N = 4 x 10^18, taken from [OeSilva], and M = 8.875 x 10^30. (Contributed by AV, 1-Aug-2020.)

**Hypotheses**
Ref	Expression
bgoldbtbnd.m	⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘;11))
bgoldbtbnd.n	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘;11))
bgoldbtbnd.b	⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))
bgoldbtbnd.d	⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))
bgoldbtbnd.f	⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))
bgoldbtbnd.i	⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))
bgoldbtbnd.0	⊢ (𝜑 → (𝐹‘0) = 7)
bgoldbtbnd.1	⊢ (𝜑 → (𝐹‘1) = ;13)
bgoldbtbnd.l	⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))
bgoldbtbnd.r	⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)

**Assertion**
Ref	Expression
bgoldbtbnd	⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd ))

Distinct variable groups: 𝐷,𝑖 𝑖,𝐹 𝑖,𝑁,𝑛 𝜑,𝑛 Allowed substitution hints: 𝜑(𝑖) 𝐷(𝑛) 𝐹(𝑛) 𝑀(𝑖,𝑛)

Proof of Theorem bgoldbtbnd Dummy variables 𝑝 𝑞 𝑟 𝑚 𝑓 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprl 767	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
2		bgoldbtbnd.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))
3		eluzge3nn 12559	. . . . . . . . 9 ⊢ (𝐷 ∈ (ℤ_≥‘3) → 𝐷 ∈ ℕ)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℕ)
5		iccelpart 44773	. . . . . . . 8 ⊢ (𝐷 ∈ ℕ → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
6	4, 5	syl 17	. . . . . . 7 ⊢ (𝜑 → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
7		bgoldbtbnd.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))
8		fveq1 6755	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘0) = (𝐹‘0))
9		fveq1 6755	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘𝐷) = (𝐹‘𝐷))
10	8, 9	oveq12d 7273	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((𝑓‘0)[,)(𝑓‘𝐷)) = ((𝐹‘0)[,)(𝐹‘𝐷)))
11	10	eleq2d 2824	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) ↔ 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷))))
12		fveq1 6755	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑗) = (𝐹‘𝑗))
13		fveq1 6755	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘(𝑗 + 1)) = (𝐹‘(𝑗 + 1)))
14	12, 13	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) = ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))
15	14	eleq2d 2824	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ 𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
16	15	rexbidv 3225	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
17	11, 16	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → ((𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) ↔ (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
18	17	rspcv 3547	. . . . . . . . 9 ⊢ (𝐹 ∈ (RePart‘𝐷) → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
19	7, 18	syl 17	. . . . . . . 8 ⊢ (𝜑 → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
20		oddz 44971	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℤ)
21	20	zred 12355	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ)
22	21	rexrd 10956	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ^*)
23	22	ad2antrl 724	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ^*)
24		7re 11996	. . . . . . . . . . . . . . . . 17 ⊢ 7 ∈ ℝ
25		ltle 10994	. . . . . . . . . . . . . . . . 17 ⊢ ((7 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (7 < 𝑛 → 7 ≤ 𝑛))
26	24, 21, 25	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ Odd → (7 < 𝑛 → 7 ≤ 𝑛))
27	26	com12 32	. . . . . . . . . . . . . . 15 ⊢ (7 < 𝑛 → (𝑛 ∈ Odd → 7 ≤ 𝑛))
28	27	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((7 < 𝑛 ∧ 𝑛 < 𝑀) → (𝑛 ∈ Odd → 7 ≤ 𝑛))
29	28	impcom 407	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → 7 ≤ 𝑛)
30	29	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 7 ≤ 𝑛)
31		bgoldbtbnd.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘;11))
32		eluzelre 12522	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ)
33	32	rexrd 10956	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ^*)
34	31, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
35	34	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 ∈ ℝ^*)
36		bgoldbtbnd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)
37	36	rexrd 10956	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ^*)
38	37	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝐷) ∈ ℝ^*)
39		simprrr 778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < 𝑀)
40		bgoldbtbnd.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))
41	40	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 < (𝐹‘𝐷))
42	23, 35, 38, 39, 41	xrlttrd 12822	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < (𝐹‘𝐷))
43		bgoldbtbnd.0	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘0) = 7)
44	43	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘𝐷)) = (7[,)(𝐹‘𝐷)))
45	44	eleq2d 2824	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
46	45	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
47	24	rexri 10964	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ^*
48		elico1 13051	. . . . . . . . . . . . . 14 ⊢ ((7 ∈ ℝ^* ∧ (𝐹‘𝐷) ∈ ℝ^) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^ ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
49	47, 38, 48	sylancr 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
50	46, 49	bitrd 278	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
51	23, 30, 42, 50	mpbir3and 1340	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)))
52		fzo0sn0fzo1 13404	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ ℕ → (0..^𝐷) = ({0} ∪ (1..^𝐷)))
53	52	eleq2d 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℕ → (𝑗 ∈ (0..^𝐷) ↔ 𝑗 ∈ ({0} ∪ (1..^𝐷))))
54		elun 4079	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ({0} ∪ (1..^𝐷)) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)))
55	53, 54	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
56	4, 55	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
57	56	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
58		velsn 4574	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {0} ↔ 𝑗 = 0)
59		fveq2 6756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘𝑗) = (𝐹‘0))
60		fv0p1e1 12026	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘(𝑗 + 1)) = (𝐹‘1))
61	59, 60	oveq12d 7273	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 0 → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = ((𝐹‘0)[,)(𝐹‘1)))
62		bgoldbtbnd.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹‘1) = ;13)
63	43, 62	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
64	63	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
65	61, 64	sylan9eq 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = (7[,);13))
66	65	eleq2d 2824	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ↔ 𝑛 ∈ (7[,);13)))
67	1	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ Odd )
68		simprrl 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 7 < 𝑛)
69	68	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 7 < 𝑛)
70		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ (7[,);13))
71		bgoldbtbndlem1 45145	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ Odd ∧ 7 < 𝑛 ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOdd )
72	67, 69, 70, 71	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOdd )
73		isgbo 45093	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ GoldbachOdd ↔ (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
74	72, 73	sylib 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
75	74	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
76	75	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ (7[,);13) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
77	76	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ (7[,);13) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
78	66, 77	sylbid 239	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
79	78	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
80	58, 79	sylbi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {0} → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
81		bgoldbtbnd.i	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))
82		fzo0ss1 13345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1..^𝐷) ⊆ (0..^𝐷)
83	82	sseli 3913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1..^𝐷) → 𝑗 ∈ (0..^𝐷))
84		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (𝐹‘𝑖) = (𝐹‘𝑗))
85	84	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → ((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ↔ (𝐹‘𝑗) ∈ (ℙ ∖ {2})))
86		fvoveq1 7278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (𝐹‘(𝑖 + 1)) = (𝐹‘(𝑗 + 1)))
87	86, 84	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) = ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))
88	87	breq1d 5080	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ↔ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4)))
89	87	breq2d 5082	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) ↔ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))
90	85, 88, 89	3anbi123d 1434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 → (((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) ↔ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
91	90	rspcv 3547	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) → ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
92	83, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) → ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
93	81, 92	mpan9 506	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) → ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))
94		bgoldbtbnd.n	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘;11))
95		bgoldbtbnd.b	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))
96	31, 94, 95, 2, 7, 81, 43, 62, 40, 36	bgoldbtbndlem4 45148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ 𝑛 ∈ Odd ) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ (𝑛 − (𝐹‘𝑗)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
97	96	ad2ant2r 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ (𝑛 − (𝐹‘𝑗)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
98	97	expcomd 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
99		simplll 771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝜑)
100		simprl 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
101		simpllr 772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑗 ∈ (1..^𝐷))
102		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 − (𝐹‘𝑗)) = (𝑛 − (𝐹‘𝑗))
103	31, 94, 95, 2, 7, 81, 43, 62, 40, 36, 102	bgoldbtbndlem3 45147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ Odd ∧ 𝑗 ∈ (1..^𝐷)) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
104	99, 100, 101, 103	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
105		breq2 5074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (4 < 𝑛 ↔ 4 < 𝑚))
106		breq1 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (𝑛 < 𝑁 ↔ 𝑚 < 𝑁))
107	105, 106	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → ((4 < 𝑛 ∧ 𝑛 < 𝑁) ↔ (4 < 𝑚 ∧ 𝑚 < 𝑁)))
108		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ GoldbachEven ↔ 𝑚 ∈ GoldbachEven ))
109	107, 108	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑚 → (((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven )))
110	109	cbvralvw 3372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ))
111		breq2 5074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (4 < 𝑚 ↔ 4 < (𝑛 − (𝐹‘𝑗))))
112		breq1 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 < 𝑁 ↔ (𝑛 − (𝐹‘𝑗)) < 𝑁))
113	111, 112	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → ((4 < 𝑚 ∧ 𝑚 < 𝑁) ↔ (4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁)))
114		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 ∈ GoldbachEven ↔ (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ))
115	113, 114	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) ↔ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
116	115	rspcv 3547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
117	110, 116	syl5bi 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
118		pm3.35 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) ∧ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )
119		isgbe 45091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ↔ ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))))
120		eldifi 4057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℙ)
121	120	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℙ)
122	121	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℙ)
123	122	ad5antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → (𝐹‘𝑗) ∈ ℙ)
124		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑟 ∈ Odd ↔ (𝐹‘𝑗) ∈ Odd ))
125	124	3anbi3d 1440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd )))
126		oveq2 7263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 + 𝑞) + 𝑟) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
127	126	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
128	125, 127	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑟 = (𝐹‘𝑗) → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
129	128	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) ∧ 𝑟 = (𝐹‘𝑗)) → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
130		oddprmALTV 45027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ Odd )
131	130	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ Odd )
132	131	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ Odd )
133	132	ad4antlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝐹‘𝑗) ∈ Odd )
134		3simpa 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ))
135	133, 134	anim12ci 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ (𝐹‘𝑗) ∈ Odd ))
136		df-3an 1087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ (𝐹‘𝑗) ∈ Odd ))
137	135, 136	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ))
138	20	zcnd 12356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℂ)
139	138	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℂ)
140		prmz 16308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℤ)
141	140	zcnd 12356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℂ)
142	120, 141	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℂ)
143	142	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℂ)
144	143	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℂ)
145	144	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℂ)
146	139, 145	npcand 11266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
147	146	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
148	147	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
149		oveq1 7262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
150	148, 149	sylan9req 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
151	150	exp31 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
152	151	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) → ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
153	152	3impia 1115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
154	153	impcom 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
155	137, 154	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
156	123, 129, 155	rspcedvd 3555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
157	156	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
158	157	reximdva 3202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
159	158	reximdva 3202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
160	159	exp41 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (𝜑 → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
161	160	com25 99	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
162	161	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
163	119, 162	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
164	163	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
165	118, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) ∧ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
166	165	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
167	166	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
168	167	com13 88	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
169	117, 168	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
170	169	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
171	170	3impib 1114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
172	171	com15 101	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
173	95, 172	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
174	173	impl 455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
175	174	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
176	104, 175	syld 47	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
177	176	expcomd 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (4 < (𝑛 − (𝐹‘𝑗)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
178	21	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ)
179	140	zred 12355	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℝ)
180	120, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℝ)
181	180	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℝ)
182	181	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℝ)
183	178, 182	resubcld 11333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 − (𝐹‘𝑗)) ∈ ℝ)
184		4re 11987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 ∈ ℝ
185		lelttric 11012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ ℝ ∧ 4 ∈ ℝ) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 ∨ 4 < (𝑛 − (𝐹‘𝑗))))
186	183, 184, 185	sylancl 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 ∨ 4 < (𝑛 − (𝐹‘𝑗))))
187	98, 177, 186	mpjaod 856	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
188	187	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
189	93, 188	mpdan 683	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
190	189	expcom 413	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1..^𝐷) → (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
191	190	impd 410	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1..^𝐷) → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
192	80, 191	jaoi 853	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)) → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
193	192	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
194	57, 193	sylbid 239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑗 ∈ (0..^𝐷) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
195	194	rexlimdv 3211	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
196	51, 195	embantd 59	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
197	196	ex 412	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ((𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
198	197	com23 86	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
199	19, 198	syld 47	. . . . . . 7 ⊢ (𝜑 → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
200	6, 199	mpd 15	. . . . . 6 ⊢ (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
201	200	imp 406	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
202	1, 201	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
203	202, 73	sylibr 233	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ GoldbachOdd )
204	203	exp32 420	. 2 ⊢ (𝜑 → (𝑛 ∈ Odd → ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd )))
205	204	ralrimiv 3106	1 ⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∀wral 3063 ∃wrex 3064 ∖ cdif 3880 ∪ cun 3881 {csn 4558 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 ℕcn 11903 2c2 11958 3c3 11959 4c4 11960 7c7 11963 cdc 12366 ℤ_≥cuz 12511 [,)cico 13010 ..^cfzo 13311 ℙcprime 16304 RePartciccp 44753 Even ceven 44964 Odd codd 44965 GoldbachEven cgbe 45085 GoldbachOdd cgbo 45087

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-rp 12660 df-ico 13014 df-fz 13169 df-fzo 13312 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-dvds 15892 df-prm 16305 df-iccp 44754 df-even 44966 df-odd 44967 df-gbe 45088 df-gbo 45090

This theorem is referenced by: tgblthelfgott 45155

W3C validator