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 45261

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 768	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
2		bgoldbtbnd.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))
3		eluzge3nn 12630	. . . . . . . . 9 ⊢ (𝐷 ∈ (ℤ_≥‘3) → 𝐷 ∈ ℕ)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℕ)
5		iccelpart 44885	. . . . . . . 8 ⊢ (𝐷 ∈ ℕ → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
6	4, 5	syl 17	. . . . . . 7 ⊢ (𝜑 → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
7		bgoldbtbnd.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))
8		fveq1 6773	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘0) = (𝐹‘0))
9		fveq1 6773	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘𝐷) = (𝐹‘𝐷))
10	8, 9	oveq12d 7293	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((𝑓‘0)[,)(𝑓‘𝐷)) = ((𝐹‘0)[,)(𝐹‘𝐷)))
11	10	eleq2d 2824	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) ↔ 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷))))
12		fveq1 6773	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑗) = (𝐹‘𝑗))
13		fveq1 6773	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘(𝑗 + 1)) = (𝐹‘(𝑗 + 1)))
14	12, 13	oveq12d 7293	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) = ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))
15	14	eleq2d 2824	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ 𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
16	15	rexbidv 3226	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
17	11, 16	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → ((𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) ↔ (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
18	17	rspcv 3557	. . . . . . . . 9 ⊢ (𝐹 ∈ (RePart‘𝐷) → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
19	7, 18	syl 17	. . . . . . . 8 ⊢ (𝜑 → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
20		oddz 45083	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℤ)
21	20	zred 12426	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ)
22	21	rexrd 11025	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ^*)
23	22	ad2antrl 725	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ^*)
24		7re 12066	. . . . . . . . . . . . . . . . 17 ⊢ 7 ∈ ℝ
25		ltle 11063	. . . . . . . . . . . . . . . . 17 ⊢ ((7 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (7 < 𝑛 → 7 ≤ 𝑛))
26	24, 21, 25	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ Odd → (7 < 𝑛 → 7 ≤ 𝑛))
27	26	com12 32	. . . . . . . . . . . . . . 15 ⊢ (7 < 𝑛 → (𝑛 ∈ Odd → 7 ≤ 𝑛))
28	27	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((7 < 𝑛 ∧ 𝑛 < 𝑀) → (𝑛 ∈ Odd → 7 ≤ 𝑛))
29	28	impcom 408	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → 7 ≤ 𝑛)
30	29	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 7 ≤ 𝑛)
31		bgoldbtbnd.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘;11))
32		eluzelre 12593	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ)
33	32	rexrd 11025	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ^*)
34	31, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
35	34	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 ∈ ℝ^*)
36		bgoldbtbnd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)
37	36	rexrd 11025	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ^*)
38	37	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝐷) ∈ ℝ^*)
39		simprrr 779	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < 𝑀)
40		bgoldbtbnd.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))
41	40	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 < (𝐹‘𝐷))
42	23, 35, 38, 39, 41	xrlttrd 12893	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < (𝐹‘𝐷))
43		bgoldbtbnd.0	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘0) = 7)
44	43	oveq1d 7290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘𝐷)) = (7[,)(𝐹‘𝐷)))
45	44	eleq2d 2824	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
46	45	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
47	24	rexri 11033	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ^*
48		elico1 13122	. . . . . . . . . . . . . 14 ⊢ ((7 ∈ ℝ^* ∧ (𝐹‘𝐷) ∈ ℝ^) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^ ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
49	47, 38, 48	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
50	46, 49	bitrd 278	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
51	23, 30, 42, 50	mpbir3and 1341	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)))
52		fzo0sn0fzo1 13476	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ ℕ → (0..^𝐷) = ({0} ∪ (1..^𝐷)))
53	52	eleq2d 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℕ → (𝑗 ∈ (0..^𝐷) ↔ 𝑗 ∈ ({0} ∪ (1..^𝐷))))
54		elun 4083	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ({0} ∪ (1..^𝐷)) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)))
55	53, 54	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
56	4, 55	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
57	56	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
58		velsn 4577	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {0} ↔ 𝑗 = 0)
59		fveq2 6774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘𝑗) = (𝐹‘0))
60		fv0p1e1 12096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘(𝑗 + 1)) = (𝐹‘1))
61	59, 60	oveq12d 7293	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 0 → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = ((𝐹‘0)[,)(𝐹‘1)))
62		bgoldbtbnd.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹‘1) = ;13)
63	43, 62	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
64	63	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
65	61, 64	sylan9eq 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = (7[,);13))
66	65	eleq2d 2824	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ↔ 𝑛 ∈ (7[,);13)))
67	1	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ Odd )
68		simprrl 778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 7 < 𝑛)
69	68	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 7 < 𝑛)
70		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ (7[,);13))
71		bgoldbtbndlem1 45257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ Odd ∧ 7 < 𝑛 ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOdd )
72	67, 69, 70, 71	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOdd )
73		isgbo 45205	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ GoldbachOdd ↔ (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
74	72, 73	sylib 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
75	74	simprd 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
76	75	ex 413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ (7[,);13) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
77	76	adantl 482	. . . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . . 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 13417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1..^𝐷) ⊆ (0..^𝐷)
83	82	sseli 3917	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1..^𝐷) → 𝑗 ∈ (0..^𝐷))
84		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (𝐹‘𝑖) = (𝐹‘𝑗))
85	84	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → ((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ↔ (𝐹‘𝑗) ∈ (ℙ ∖ {2})))
86		fvoveq1 7298	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (𝐹‘(𝑖 + 1)) = (𝐹‘(𝑗 + 1)))
87	86, 84	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) = ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))
88	87	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ↔ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4)))
89	87	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) ↔ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))
90	85, 88, 89	3anbi123d 1435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 → (((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) ↔ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
91	90	rspcv 3557	. . . . . . . . . . . . . . . . . . . 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 507	. . . . . . . . . . . . . . . . . 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 45260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ 𝑛 ∈ Odd ) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ (𝑛 − (𝐹‘𝑗)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
97	96	ad2ant2r 744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ (𝑛 − (𝐹‘𝑗)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
98	97	expcomd 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
99		simplll 772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝜑)
100		simprl 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
101		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . 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 45259	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ Odd ∧ 𝑗 ∈ (1..^𝐷)) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
104	99, 100, 101, 103	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
105		breq2 5078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (4 < 𝑛 ↔ 4 < 𝑚))
106		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (𝑛 < 𝑁 ↔ 𝑚 < 𝑁))
107	105, 106	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → ((4 < 𝑛 ∧ 𝑛 < 𝑁) ↔ (4 < 𝑚 ∧ 𝑚 < 𝑁)))
108		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ GoldbachEven ↔ 𝑚 ∈ GoldbachEven ))
109	107, 108	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑚 → (((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven )))
110	109	cbvralvw 3383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ))
111		breq2 5078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (4 < 𝑚 ↔ 4 < (𝑛 − (𝐹‘𝑗))))
112		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 < 𝑁 ↔ (𝑛 − (𝐹‘𝑗)) < 𝑁))
113	111, 112	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → ((4 < 𝑚 ∧ 𝑚 < 𝑁) ↔ (4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁)))
114		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 ∈ GoldbachEven ↔ (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ))
115	113, 114	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) ↔ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
116	115	rspcv 3557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
117	110, 116	syl5bi 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
118		pm3.35 800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) ∧ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )
119		isgbe 45203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ↔ ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))))
120		eldifi 4061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℙ)
121	120	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℙ)
122	121	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℙ)
123	122	ad5antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → (𝐹‘𝑗) ∈ ℙ)
124		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑟 ∈ Odd ↔ (𝐹‘𝑗) ∈ Odd ))
125	124	3anbi3d 1441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd )))
126		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 + 𝑞) + 𝑟) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
127	126	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
128	125, 127	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑟 = (𝐹‘𝑗) → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
129	128	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) ∧ 𝑟 = (𝐹‘𝑗)) → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
130		oddprmALTV 45139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ Odd )
131	130	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ Odd )
132	131	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ Odd )
133	132	ad4antlr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝐹‘𝑗) ∈ Odd )
134		3simpa 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ))
135	133, 134	anim12ci 614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ (𝐹‘𝑗) ∈ Odd ))
136		df-3an 1088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℂ)
139	138	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℂ)
140		prmz 16380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℤ)
141	140	zcnd 12427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℂ)
142	120, 141	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℂ)
143	142	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℂ)
144	143	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℂ)
145	144	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℂ)
146	139, 145	npcand 11336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
147	146	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
148	147	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
149		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
150	148, 149	sylan9req 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
151	150	exp31 420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
154	153	impcom 408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
155	137, 154	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
156	123, 129, 155	rspcedvd 3563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
157	156	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
158	157	reximdva 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
159	158	reximdva 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
160	159	exp41 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
167	166	ancoms 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1115	. . . . . . . . . . . . . . . . . . . . . . . . . 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 456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
175	174	imp 407	. . . . . . . . . . . . . . . . . . . . . 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 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (4 < (𝑛 − (𝐹‘𝑗)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
178	21	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ)
179	140	zred 12426	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℝ)
180	120, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℝ)
181	180	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℝ)
182	181	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℝ)
183	178, 182	resubcld 11403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 − (𝐹‘𝑗)) ∈ ℝ)
184		4re 12057	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 ∈ ℝ
185		lelttric 11082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ ℝ ∧ 4 ∈ ℝ) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 ∨ 4 < (𝑛 − (𝐹‘𝑗))))
186	183, 184, 185	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 ∨ 4 < (𝑛 − (𝐹‘𝑗))))
187	98, 177, 186	mpjaod 857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
188	187	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
189	93, 188	mpdan 684	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
190	189	expcom 414	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1..^𝐷) → (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
191	190	impd 411	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1..^𝐷) → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
192	80, 191	jaoi 854	. . . . . . . . . . . . . 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 3212	. . . . . . . . . . 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 413	. . . . . . . . 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 407	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
202	1, 201	jca 512	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
203	202, 73	sylibr 233	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ GoldbachOdd )
204	203	exp32 421	. 2 ⊢ (𝜑 → (𝑛 ∈ Odd → ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd )))
205	204	ralrimiv 3102	1 ⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 ∖ cdif 3884 ∪ cun 3885 {csn 4561 class class class wbr 5074 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 − cmin 11205 ℕcn 11973 2c2 12028 3c3 12029 4c4 12030 7c7 12033 cdc 12437 ℤ_≥cuz 12582 [,)cico 13081 ..^cfzo 13382 ℙcprime 16376 RePartciccp 44865 Even ceven 45076 Odd codd 45077 GoldbachEven cgbe 45197 GoldbachOdd cgbo 45199

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-er 8498 df-map 8617 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-inf 9202 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-rp 12731 df-ico 13085 df-fz 13240 df-fzo 13383 df-seq 13722 df-exp 13783 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-dvds 15964 df-prm 16377 df-iccp 44866 df-even 45078 df-odd 45079 df-gbe 45200 df-gbo 45202

This theorem is referenced by: tgblthelfgott 45267

W3C validator