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 47790

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 770	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
2		bgoldbtbnd.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))
3		eluzge3nn 12911	. . . . . . . . 9 ⊢ (𝐷 ∈ (ℤ_≥‘3) → 𝐷 ∈ ℕ)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℕ)
5		iccelpart 47414	. . . . . . . 8 ⊢ (𝐷 ∈ ℕ → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
6	4, 5	syl 17	. . . . . . 7 ⊢ (𝜑 → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
7		bgoldbtbnd.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))
8		fveq1 6880	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘0) = (𝐹‘0))
9		fveq1 6880	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘𝐷) = (𝐹‘𝐷))
10	8, 9	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((𝑓‘0)[,)(𝑓‘𝐷)) = ((𝐹‘0)[,)(𝐹‘𝐷)))
11	10	eleq2d 2821	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) ↔ 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷))))
12		fveq1 6880	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑗) = (𝐹‘𝑗))
13		fveq1 6880	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘(𝑗 + 1)) = (𝐹‘(𝑗 + 1)))
14	12, 13	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) = ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))
15	14	eleq2d 2821	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ 𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
16	15	rexbidv 3165	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
17	11, 16	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → ((𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) ↔ (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
18	17	rspcv 3602	. . . . . . . . 9 ⊢ (𝐹 ∈ (RePart‘𝐷) → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
19	7, 18	syl 17	. . . . . . . 8 ⊢ (𝜑 → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
20		oddz 47612	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℤ)
21	20	zred 12702	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ)
22	21	rexrd 11290	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ^*)
23	22	ad2antrl 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ^*)
24		7re 12338	. . . . . . . . . . . . . . . . 17 ⊢ 7 ∈ ℝ
25		ltle 11328	. . . . . . . . . . . . . . . . 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 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 12868	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ)
33	32	rexrd 11290	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ^*)
34	31, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
35	34	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 ∈ ℝ^*)
36		bgoldbtbnd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)
37	36	rexrd 11290	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ^*)
38	37	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝐷) ∈ ℝ^*)
39		simprrr 781	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < 𝑀)
40		bgoldbtbnd.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))
41	40	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 < (𝐹‘𝐷))
42	23, 35, 38, 39, 41	xrlttrd 13180	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < (𝐹‘𝐷))
43		bgoldbtbnd.0	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘0) = 7)
44	43	oveq1d 7425	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘𝐷)) = (7[,)(𝐹‘𝐷)))
45	44	eleq2d 2821	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
46	45	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
47	24	rexri 11298	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ^*
48		elico1 13410	. . . . . . . . . . . . . 14 ⊢ ((7 ∈ ℝ^* ∧ (𝐹‘𝐷) ∈ ℝ^) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^ ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
49	47, 38, 48	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
50	46, 49	bitrd 279	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
51	23, 30, 42, 50	mpbir3and 1343	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)))
52		fzo0sn0fzo1 13776	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ ℕ → (0..^𝐷) = ({0} ∪ (1..^𝐷)))
53	52	eleq2d 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℕ → (𝑗 ∈ (0..^𝐷) ↔ 𝑗 ∈ ({0} ∪ (1..^𝐷))))
54		elun 4133	. . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
58		velsn 4622	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {0} ↔ 𝑗 = 0)
59		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘𝑗) = (𝐹‘0))
60		fv0p1e1 12368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘(𝑗 + 1)) = (𝐹‘1))
61	59, 60	oveq12d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 0 → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = ((𝐹‘0)[,)(𝐹‘1)))
62		bgoldbtbnd.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹‘1) = ;13)
63	43, 62	oveq12d 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
64	63	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
65	61, 64	sylan9eq 2791	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = (7[,);13))
66	65	eleq2d 2821	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ↔ 𝑛 ∈ (7[,);13)))
67	1	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ Odd )
68		simprrl 780	. . . . . . . . . . . . . . . . . . . . . . . 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 47786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ Odd ∧ 7 < 𝑛 ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOdd )
72	67, 69, 70, 71	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOdd )
73		isgbo 47734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ GoldbachOdd ↔ (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
74	72, 73	sylib 218	. . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
79	78	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
80	58, 79	sylbi 217	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {0} → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
81		bgoldbtbnd.i	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))
82		fzo0ss1 13711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1..^𝐷) ⊆ (0..^𝐷)
83	82	sseli 3959	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1..^𝐷) → 𝑗 ∈ (0..^𝐷))
84		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (𝐹‘𝑖) = (𝐹‘𝑗))
85	84	eleq1d 2820	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → ((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ↔ (𝐹‘𝑗) ∈ (ℙ ∖ {2})))
86		fvoveq1 7433	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (𝐹‘(𝑖 + 1)) = (𝐹‘(𝑗 + 1)))
87	86, 84	oveq12d 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) = ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))
88	87	breq1d 5134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ↔ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4)))
89	87	breq2d 5136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) ↔ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))
90	85, 88, 89	3anbi123d 1438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 → (((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) ↔ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
91	90	rspcv 3602	. . . . . . . . . . . . . . . . . . . 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 47789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ 𝑛 ∈ Odd ) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ (𝑛 − (𝐹‘𝑗)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
97	96	ad2ant2r 747	. . . . . . . . . . . . . . . . . . . . 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 774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝜑)
100		simprl 770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
101		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑗 ∈ (1..^𝐷))
102		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 − (𝐹‘𝑗)) = (𝑛 − (𝐹‘𝑗))
103	31, 94, 95, 2, 7, 81, 43, 62, 40, 36, 102	bgoldbtbndlem3 47788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ Odd ∧ 𝑗 ∈ (1..^𝐷)) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
104	99, 100, 101, 103	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
105		breq2 5128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (4 < 𝑛 ↔ 4 < 𝑚))
106		breq1 5127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (𝑛 < 𝑁 ↔ 𝑚 < 𝑁))
107	105, 106	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → ((4 < 𝑛 ∧ 𝑛 < 𝑁) ↔ (4 < 𝑚 ∧ 𝑚 < 𝑁)))
108		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ GoldbachEven ↔ 𝑚 ∈ GoldbachEven ))
109	107, 108	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑚 → (((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven )))
110	109	cbvralvw 3224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ))
111		breq2 5128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (4 < 𝑚 ↔ 4 < (𝑛 − (𝐹‘𝑗))))
112		breq1 5127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 < 𝑁 ↔ (𝑛 − (𝐹‘𝑗)) < 𝑁))
113	111, 112	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → ((4 < 𝑚 ∧ 𝑚 < 𝑁) ↔ (4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁)))
114		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 ∈ GoldbachEven ↔ (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ))
115	113, 114	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) ↔ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
116	115	rspcv 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
117	110, 116	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
118		pm3.35 802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) ∧ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )
119		isgbe 47732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ↔ ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))))
120		eldifi 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℙ)
121	120	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℙ)
122	121	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℙ)
123	122	ad5antlr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → (𝐹‘𝑗) ∈ ℙ)
124		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑟 ∈ Odd ↔ (𝐹‘𝑗) ∈ Odd ))
125	124	3anbi3d 1444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd )))
126		oveq2 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 + 𝑞) + 𝑟) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
127	126	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
128	125, 127	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 47668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ Odd )
131	130	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ Odd )
132	131	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ Odd )
133	132	ad4antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝐹‘𝑗) ∈ Odd )
134		3simpa 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ))
138	20	zcnd 12703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℂ)
139	138	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℂ)
140		prmz 16699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℤ)
141	140	zcnd 12703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℂ)
142	120, 141	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℂ)
143	142	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℂ)
144	143	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℂ)
145	144	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℂ)
146	139, 145	npcand 11603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
149		oveq1 7417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
150	148, 149	sylan9req 2792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
159	158	reximdva 3154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1116	. . . . . . . . . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ)
179	140	zred 12702	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℝ)
180	120, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℝ)
181	180	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℝ)
182	181	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℝ)
183	178, 182	resubcld 11670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 − (𝐹‘𝑗)) ∈ ℝ)
184		4re 12329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 ∈ ℝ
185		lelttric 11347	. . . . . . . . . . . . . . . . . . . . 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 860	. . . . . . . . . . . . . . . . . . 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 687	. . . . . . . . . . . . . . . . 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 857	. . . . . . . . . . . . . 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 240	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑗 ∈ (0..^𝐷) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
195	194	rexlimdv 3140	. . . . . . . . . . 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 234	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ GoldbachOdd )
204	203	exp32 420	. 2 ⊢ (𝜑 → (𝑛 ∈ Odd → ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd )))
205	204	ralrimiv 3132	1 ⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3052 ∃wrex 3061 ∖ cdif 3928 ∪ cun 3929 {csn 4606 class class class wbr 5124 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 − cmin 11471 ℕcn 12245 2c2 12300 3c3 12301 4c4 12302 7c7 12305 cdc 12713 ℤ_≥cuz 12857 [,)cico 13369 ..^cfzo 13676 ℙcprime 16695 RePartciccp 47394 Even ceven 47605 Odd codd 47606 GoldbachEven cgbe 47726 GoldbachOdd cgbo 47728

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-er 8724 df-map 8847 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-sup 9459 df-inf 9460 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12858 df-rp 13014 df-ico 13373 df-fz 13530 df-fzo 13677 df-seq 14025 df-exp 14085 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-dvds 16278 df-prm 16696 df-iccp 47395 df-even 47607 df-odd 47608 df-gbe 47729 df-gbo 47731

This theorem is referenced by: tgblthelfgott 47796

W3C validator