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 48876

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 783	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
2		bgoldbtbnd.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))
3		eluz3nn 13009	. . . . . . . . 9 ⊢ (𝐷 ∈ (ℤ_≥‘3) → 𝐷 ∈ ℕ)
4	2, 3	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℕ)
5		iccelpart 48484	. . . . . . . 8 ⊢ (𝐷 ∈ ℕ → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
6	4, 5	syl 18	. . . . . . 7 ⊢ (𝜑 → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
7		bgoldbtbnd.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))
8		fveq1 6882	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘0) = (𝐹‘0))
9		fveq1 6882	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘𝐷) = (𝐹‘𝐷))
10	8, 9	oveq12d 7436	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((𝑓‘0)[,)(𝑓‘𝐷)) = ((𝐹‘0)[,)(𝐹‘𝐷)))
11	10	eleq2d 2847	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) ↔ 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷))))
12		fveq1 6882	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑗) = (𝐹‘𝑗))
13		fveq1 6882	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘(𝑗 + 1)) = (𝐹‘(𝑗 + 1)))
14	12, 13	oveq12d 7436	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) = ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))
15	14	eleq2d 2847	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ 𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
16	15	rexbidv 3187	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
17	11, 16	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → ((𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) ↔ (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
18	17	rspcv 3573	. . . . . . . . 9 ⊢ (𝐹 ∈ (RePart‘𝐷) → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
19	7, 18	syl 18	. . . . . . . 8 ⊢ (𝜑 → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
20		oddz 48698	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℤ)
21	20	zred 12796	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ)
22	21	rexrd 11352	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ^*)
23	22	ad2antrl 741	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ^*)
24		7re 12429	. . . . . . . . . . . . . . . . 17 ⊢ 7 ∈ ℝ
25		ltle 11391	. . . . . . . . . . . . . . . . 17 ⊢ ((7 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (7 < 𝑛 → 7 ≤ 𝑛))
26	24, 21, 25	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ Odd → (7 < 𝑛 → 7 ≤ 𝑛))
27	26	com12 33	. . . . . . . . . . . . . . 15 ⊢ (7 < 𝑛 → (𝑛 ∈ Odd → 7 ≤ 𝑛))
28	27	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((7 < 𝑛 ∧ 𝑛 < 𝑀) → (𝑛 ∈ Odd → 7 ≤ 𝑛))
29	28	impcom 413	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → 7 ≤ 𝑛)
30	29	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 7 ≤ 𝑛)
31		bgoldbtbnd.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘;11))
32		eluzelre 12969	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ)
33	32	rexrd 11352	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ^*)
34	31, 33	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
35	34	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 ∈ ℝ^*)
36		bgoldbtbnd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)
37	36	rexrd 11352	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ^*)
38	37	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝐷) ∈ ℝ^*)
39		simprrr 794	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < 𝑀)
40		bgoldbtbnd.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))
41	40	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 < (𝐹‘𝐷))
42	23, 35, 38, 39, 41	xrlttrd 13281	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < (𝐹‘𝐷))
43		bgoldbtbnd.0	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘0) = 7)
44	43	oveq1d 7433	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘𝐷)) = (7[,)(𝐹‘𝐷)))
45	44	eleq2d 2847	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
46	45	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
47	24	rexri 11360	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ^*
48		elico1 13512	. . . . . . . . . . . . . 14 ⊢ ((7 ∈ ℝ^* ∧ (𝐹‘𝐷) ∈ ℝ^) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^ ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
49	47, 38, 48	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
50	46, 49	bitrd 282	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
51	23, 30, 42, 50	mpbir3and 1361	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)))
52		fzo0sn0fzo1 13883	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ ℕ → (0..^𝐷) = ({0} ∪ (1..^𝐷)))
53	52	eleq2d 2847	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℕ → (𝑗 ∈ (0..^𝐷) ↔ 𝑗 ∈ ({0} ∪ (1..^𝐷))))
54		elun 4100	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ({0} ∪ (1..^𝐷)) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)))
55	53, 54	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
56	4, 55	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
57	56	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑗 ∈ (0..^𝐷) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷))))
58		velsn 4600	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {0} ↔ 𝑗 = 0)
59		fveq2 6883	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘𝑗) = (𝐹‘0))
60		fv0p1e1 12457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘(𝑗 + 1)) = (𝐹‘1))
61	59, 60	oveq12d 7436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 0 → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = ((𝐹‘0)[,)(𝐹‘1)))
62		bgoldbtbnd.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹‘1) = ;13)
63	43, 62	oveq12d 7436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
64	63	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
65	61, 64	sylan9eq 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = (7[,);13))
66	65	eleq2d 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ↔ 𝑛 ∈ (7[,);13)))
67	1	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ Odd )
68		simprrl 793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 7 < 𝑛)
69	68	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 7 < 𝑛)
70		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ (7[,);13))
71		bgoldbtbndlem1 48872	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ Odd ∧ 7 < 𝑛 ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOdd )
72	67, 69, 70, 71	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOdd )
73		isgbo 48820	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ GoldbachOdd ↔ (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
74	72, 73	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
75	74	simprd 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
76	75	ex 418	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ (7[,);13) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
77	76	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ (7[,);13) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
78	66, 77	sylbid 243	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
79	78	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
80	58, 79	sylbi 220	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {0} → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
81		bgoldbtbnd.i	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))
82		fzo0ss1 13817	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1..^𝐷) ⊆ (0..^𝐷)
83	82	sseli 3927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1..^𝐷) → 𝑗 ∈ (0..^𝐷))
84		fveq2 6883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (𝐹‘𝑖) = (𝐹‘𝑗))
85	84	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → ((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ↔ (𝐹‘𝑗) ∈ (ℙ ∖ {2})))
86		fvoveq1 7441	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (𝐹‘(𝑖 + 1)) = (𝐹‘(𝑗 + 1)))
87	86, 84	oveq12d 7436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) = ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))
88	87	breq1d 5113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ↔ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4)))
89	87	breq2d 5115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) ↔ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))
90	85, 88, 89	3anbi123d 1464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 → (((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) ↔ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
91	90	rspcv 3573	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) → ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
92	83, 91	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) → ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
93	81, 92	mpan9 516	. . . . . . . . . . . . . . . . . 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 48875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ 𝑛 ∈ Odd ) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ (𝑛 − (𝐹‘𝑗)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
97	96	ad2ant2r 760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ (𝑛 − (𝐹‘𝑗)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
98	97	expcomd 422	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
99		simplll 787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝜑)
100		simprl 783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
101		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑗 ∈ (1..^𝐷))
102		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 − (𝐹‘𝑗)) = (𝑛 − (𝐹‘𝑗))
103	31, 94, 95, 2, 7, 81, 43, 62, 40, 36, 102	bgoldbtbndlem3 48874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ Odd ∧ 𝑗 ∈ (1..^𝐷)) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
104	99, 100, 101, 103	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
105		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (4 < 𝑛 ↔ 4 < 𝑚))
106		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (𝑛 < 𝑁 ↔ 𝑚 < 𝑁))
107	105, 106	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → ((4 < 𝑛 ∧ 𝑛 < 𝑁) ↔ (4 < 𝑚 ∧ 𝑚 < 𝑁)))
108		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ GoldbachEven ↔ 𝑚 ∈ GoldbachEven ))
109	107, 108	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑚 → (((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven )))
110	109	cbvralvw 3241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ))
111		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (4 < 𝑚 ↔ 4 < (𝑛 − (𝐹‘𝑗))))
112		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 < 𝑁 ↔ (𝑛 − (𝐹‘𝑗)) < 𝑁))
113	111, 112	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → ((4 < 𝑚 ∧ 𝑚 < 𝑁) ↔ (4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁)))
114		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 ∈ GoldbachEven ↔ (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ))
115	113, 114	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) ↔ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
116	115	rspcv 3573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
117	110, 116	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
118		pm3.35 815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) ∧ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )
119		isgbe 48818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ↔ ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))))
120		eldifi 4078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℙ)
121	120	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℙ)
122	121	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℙ)
123	122	ad5antlr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → (𝐹‘𝑗) ∈ ℙ)
124		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑟 ∈ Odd ↔ (𝐹‘𝑗) ∈ Odd ))
125	124	3anbi3d 1470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd )))
126		oveq2 7426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 + 𝑞) + 𝑟) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
127	126	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
128	125, 127	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑟 = (𝐹‘𝑗) → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
129	128	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) ∧ 𝑟 = (𝐹‘𝑗)) → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
130		oddprmALTV 48754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ Odd )
131	130	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ Odd )
132	131	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ Odd )
133	132	ad4antlr 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝐹‘𝑗) ∈ Odd )
134		3simpa 1166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ))
135	133, 134	anim12ci 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ (𝐹‘𝑗) ∈ Odd ))
136		df-3an 1105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ (𝐹‘𝑗) ∈ Odd ))
137	135, 136	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ))
138	20	zcnd 12797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℂ)
139	138	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℂ)
140		prmz 16843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℤ)
141	140	zcnd 12797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℂ)
142	120, 141	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℂ)
143	142	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℂ)
144	143	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℂ)
145	144	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℂ)
146	139, 145	npcand 11666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
147	146	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
148	147	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
149		oveq1 7425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
150	148, 149	sylan9req 2817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
151	150	exp31 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
152	151	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) → ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
153	152	3impia 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
154	153	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
155	137, 154	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
156	123, 129, 155	rspcedvd 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
157	156	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
158	157	reximdva 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
159	158	reximdva 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
160	159	exp41 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (𝜑 → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
161	160	com25 100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
162	161	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
163	119, 162	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
164	163	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
165	118, 164	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) ∧ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
166	165	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
167	166	ancoms 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
168	167	com13 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
169	117, 168	syld 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
170	169	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
171	170	3impib 1134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
172	171	com15 102	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
173	95, 172	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
174	173	impl 461	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
175	174	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
176	104, 175	syld 48	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
177	176	expcomd 422	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (4 < (𝑛 − (𝐹‘𝑗)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
178	21	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ)
179	140	zred 12796	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℝ)
180	120, 179	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℝ)
181	180	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℝ)
182	181	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℝ)
183	178, 182	resubcld 11737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 − (𝐹‘𝑗)) ∈ ℝ)
184		4re 12420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 ∈ ℝ
185		lelttric 11410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ ℝ ∧ 4 ∈ ℝ) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 ∨ 4 < (𝑛 − (𝐹‘𝑗))))
186	183, 184, 185	sylancl 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 ∨ 4 < (𝑛 − (𝐹‘𝑗))))
187	98, 177, 186	mpjaod 874	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
188	187	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
189	93, 188	mpdan 700	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
190	189	expcom 419	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1..^𝐷) → (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
191	190	impd 416	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1..^𝐷) → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
192	80, 191	jaoi 871	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)) → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
193	192	com12 33	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
194	57, 193	sylbid 243	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑗 ∈ (0..^𝐷) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
195	194	rexlimdv 3162	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
196	51, 195	embantd 60	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
197	196	ex 418	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ((𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
198	197	com23 87	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
199	19, 198	syld 48	. . . . . . 7 ⊢ (𝜑 → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
200	6, 199	mpd 16	. . . . . 6 ⊢ (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
201	200	imp 412	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
202	1, 201	jca 521	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
203	202, 73	sylibr 237	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ GoldbachOdd )
204	203	exp32 426	. 2 ⊢ (𝜑 → (𝑛 ∈ Odd → ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd )))
205	204	ralrimiv 3154	1 ⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd ))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3077 ∃wrex 3087 ∖ cdif 3896 ∪ cun 3897 {csn 4584 class class class wbr 5103 ‘cfv 6537 (class class class)co 7418 ℂcc 11191 ℝcr 11192 0cc0 11193 1c1 11194 + caddc 11196 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 − cmin 11534 ℕcn 12328 2c2 12390 3c3 12391 4c4 12392 7c7 12395 cdc 12807 ℤ_≥cuz 12958 [,)cico 13471 ..^cfzo 13781 ℙcprime 16839 RePartciccp 48464 Even ceven 48691 Odd codd 48692 GoldbachEven cgbe 48812 GoldbachOdd cgbo 48814

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-sup 9427 df-inf 9428 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-z 12687 df-dec 12808 df-uz 12959 df-rp 13114 df-ico 13475 df-fz 13633 df-fzo 13782 df-seq 14138 df-exp 14198 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-dvds 16416 df-prm 16840 df-iccp 48465 df-even 48693 df-odd 48694 df-gbe 48815 df-gbo 48817

This theorem is used by: tgblthelfgott 48882

W3C validator