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 40225

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 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOddALTV ))

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 790	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
2		bgoldbtbnd.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))
3		eluzge3nn 11606	. . . . . . . . 9 ⊢ (𝐷 ∈ (ℤ_≥‘3) → 𝐷 ∈ ℕ)
4	2, 3	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℕ)
5		iccelpart 39971	. . . . . . . 8 ⊢ (𝐷 ∈ ℕ → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
6	4, 5	syl 17	. . . . . . 7 ⊢ (𝜑 → ∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))))
7		bgoldbtbnd.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))
8		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘0) = (𝐹‘0))
9		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (𝑓‘𝐷) = (𝐹‘𝐷))
10	8, 9	oveq12d 6567	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((𝑓‘0)[,)(𝑓‘𝐷)) = ((𝐹‘0)[,)(𝐹‘𝐷)))
11	10	eleq2d 2673	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) ↔ 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷))))
12		fveq1 6102	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑗) = (𝐹‘𝑗))
13		fveq1 6102	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓‘(𝑗 + 1)) = (𝐹‘(𝑗 + 1)))
14	12, 13	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) = ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))
15	14	eleq2d 2673	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ 𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
16	15	rexbidv 3034	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))))
17	11, 16	imbi12d 333	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → ((𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) ↔ (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
18	17	rspcv 3278	. . . . . . . . 9 ⊢ (𝐹 ∈ (RePart‘𝐷) → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
19	7, 18	syl 17	. . . . . . . 8 ⊢ (𝜑 → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))))))
20		oddz 40082	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℤ)
21	20	zred 11358	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ)
22	21	rexrd 9968	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℝ^*)
23	22	ad2antrl 760	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ^*)
24		7re 10980	. . . . . . . . . . . . . . . . 17 ⊢ 7 ∈ ℝ
25		ltle 10005	. . . . . . . . . . . . . . . . 17 ⊢ ((7 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (7 < 𝑛 → 7 ≤ 𝑛))
26	24, 21, 25	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ Odd → (7 < 𝑛 → 7 ≤ 𝑛))
27	26	com12 32	. . . . . . . . . . . . . . 15 ⊢ (7 < 𝑛 → (𝑛 ∈ Odd → 7 ≤ 𝑛))
28	27	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((7 < 𝑛 ∧ 𝑛 < 𝑀) → (𝑛 ∈ Odd → 7 ≤ 𝑛))
29	28	impcom 445	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → 7 ≤ 𝑛)
30	29	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 7 ≤ 𝑛)
31		bgoldbtbnd.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘;11))
32		eluzelre 11574	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ)
33	32	rexrd 9968	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘;11) → 𝑀 ∈ ℝ^*)
34	31, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ^*)
35	34	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 ∈ ℝ^*)
36		bgoldbtbnd.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)
37	36	rexrd 9968	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ^*)
38	37	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝐷) ∈ ℝ^*)
39		simprrr 801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < 𝑀)
40		bgoldbtbnd.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))
41	40	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑀 < (𝐹‘𝐷))
42	23, 35, 38, 39, 41	xrlttrd 11866	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 < (𝐹‘𝐷))
43		bgoldbtbnd.0	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘0) = 7)
44	43	oveq1d 6564	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘𝐷)) = (7[,)(𝐹‘𝐷)))
45	44	eleq2d 2673	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
46	45	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ 𝑛 ∈ (7[,)(𝐹‘𝐷))))
47	24	rexri 9976	. . . . . . . . . . . . . 14 ⊢ 7 ∈ ℝ^*
48		elico1 12089	. . . . . . . . . . . . . 14 ⊢ ((7 ∈ ℝ^* ∧ (𝐹‘𝐷) ∈ ℝ^) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^ ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
49	47, 38, 48	sylancr 694	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ (7[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
50	46, 49	bitrd 267	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) ↔ (𝑛 ∈ ℝ^* ∧ 7 ≤ 𝑛 ∧ 𝑛 < (𝐹‘𝐷))))
51	23, 30, 42, 50	mpbir3and 1238	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)))
52		fzo0sn0fzo1 12424	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ ℕ → (0..^𝐷) = ({0} ∪ (1..^𝐷)))
53	52	eleq2d 2673	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℕ → (𝑗 ∈ (0..^𝐷) ↔ 𝑗 ∈ ({0} ∪ (1..^𝐷))))
54		elun 3715	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ({0} ∪ (1..^𝐷)) ↔ (𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)))
55	53, 54	syl6bb 275	. . . . . . . . . . . . . . 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 4141	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ {0} ↔ 𝑗 = 0)
59		fveq2 6103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘𝑗) = (𝐹‘0))
60		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → (𝑗 + 1) = (0 + 1))
61		0p1e1 11009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 + 1) = 1
62	60, 61	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → (𝑗 + 1) = 1)
63	62	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 0 → (𝐹‘(𝑗 + 1)) = (𝐹‘1))
64	59, 63	oveq12d 6567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 0 → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = ((𝐹‘0)[,)(𝐹‘1)))
65		bgoldbtbnd.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹‘1) = ;13)
66	43, 65	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
67	66	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝐹‘0)[,)(𝐹‘1)) = (7[,);13))
68	64, 67	sylan9eq 2664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) = (7[,);13))
69	68	eleq2d 2673	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ↔ 𝑛 ∈ (7[,);13)))
70	1	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ Odd )
71		simprrl 800	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 7 < 𝑛)
72	71	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 7 < 𝑛)
73		simpr 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ (7[,);13))
74		bgoldbtbndlem1 40221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ Odd ∧ 7 < 𝑛 ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOddALTV )
75	70, 72, 73, 74	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → 𝑛 ∈ GoldbachOddALTV )
76		isgboa 40175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ GoldbachOddALTV ↔ (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
77	75, 76	sylib 207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
78	77	simprd 478	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑛 ∈ (7[,);13)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
79	78	ex 449	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ (7[,);13) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
80	79	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ (7[,);13) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
81	69, 80	sylbid 229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 = 0 ∧ (𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
82	81	ex 449	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 0 → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
83	58, 82	sylbi 206	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {0} → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
84		bgoldbtbnd.i	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))
85		fzo0ss1 12367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1..^𝐷) ⊆ (0..^𝐷)
86	85	sseli 3564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1..^𝐷) → 𝑗 ∈ (0..^𝐷))
87		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (𝐹‘𝑖) = (𝐹‘𝑗))
88	87	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → ((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ↔ (𝐹‘𝑗) ∈ (ℙ ∖ {2})))
89		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
90	89	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (𝐹‘(𝑖 + 1)) = (𝐹‘(𝑗 + 1)))
91	90, 87	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) = ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))
92	91	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ↔ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4)))
93	91	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 𝑗 → (4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) ↔ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))
94	88, 92, 93	3anbi123d 1391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 → (((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) ↔ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
95	94	rspcv 3278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) → ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
96	86, 95	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (1..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) → ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))))
97	84, 96	mpan9 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) → ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))
98		bgoldbtbnd.n	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘;11))
99		bgoldbtbnd.b	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))
100	31, 98, 99, 2, 7, 84, 43, 65, 40, 36	bgoldbtbndlem4 40224	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ 𝑛 ∈ Odd ) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ (𝑛 − (𝐹‘𝑗)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
101	100	ad2ant2r 779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ (𝑛 − (𝐹‘𝑗)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
102	101	expcomd 453	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
103		simplll 794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝜑)
104		simprl 790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ Odd )
105		simpllr 795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑗 ∈ (1..^𝐷))
106		eqid 2610	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 − (𝐹‘𝑗)) = (𝑛 − (𝐹‘𝑗))
107	31, 98, 99, 2, 7, 84, 43, 65, 40, 36, 106	bgoldbtbndlem3 40223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ Odd ∧ 𝑗 ∈ (1..^𝐷)) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
108	103, 104, 105, 107	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗)))))
109		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (4 < 𝑛 ↔ 4 < 𝑚))
110		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑛 = 𝑚 → (𝑛 < 𝑁 ↔ 𝑚 < 𝑁))
111	109, 110	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → ((4 < 𝑛 ∧ 𝑛 < 𝑁) ↔ (4 < 𝑚 ∧ 𝑚 < 𝑁)))
112		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ GoldbachEven ↔ 𝑚 ∈ GoldbachEven ))
113	111, 112	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 𝑚 → (((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven )))
114	113	cbvralv 3147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ))
115		breq2 4587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (4 < 𝑚 ↔ 4 < (𝑛 − (𝐹‘𝑗))))
116		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 < 𝑁 ↔ (𝑛 − (𝐹‘𝑗)) < 𝑁))
117	115, 116	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → ((4 < 𝑚 ∧ 𝑚 < 𝑁) ↔ (4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁)))
118		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (𝑚 ∈ GoldbachEven ↔ (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ))
119	117, 118	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 = (𝑛 − (𝐹‘𝑗)) → (((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) ↔ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
120	119	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑚 ∈ Even ((4 < 𝑚 ∧ 𝑚 < 𝑁) → 𝑚 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
121	114, 120	syl5bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )))
122		pm3.35 609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) ∧ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )
123		isgbe 40173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ↔ ((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))))
124		eldifi 3694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℙ)
125	124	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℙ)
126	125	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℙ)
127	126	ad5antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → (𝐹‘𝑗) ∈ ℙ)
128		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑟 ∈ Odd ↔ (𝐹‘𝑗) ∈ Odd ))
129	128	3anbi3d 1397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd )))
130		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑟 = (𝐹‘𝑗) → ((𝑝 + 𝑞) + 𝑟) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
131	130	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑟 = (𝐹‘𝑗) → (𝑛 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
132	129, 131	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑟 = (𝐹‘𝑗) → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
133	132	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) ∧ 𝑟 = (𝐹‘𝑗)) → (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
134		oddprmALTV 40136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ Odd )
135	134	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ Odd )
136	135	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ Odd )
137	136	ad4antlr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝐹‘𝑗) ∈ Odd )
138		3simpa 1051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ))
139	137, 138	anim12ci 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ (𝐹‘𝑗) ∈ Odd ))
140		df-3an 1033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ↔ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ (𝐹‘𝑗) ∈ Odd ))
141	139, 140	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ))
142	20	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (𝑛 ∈ Odd → 𝑛 ∈ ℂ)
143	142	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℂ)
144		prmz 15227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℤ)
145	144	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℂ)
146	124, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℂ)
147	146	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℂ)
148	147	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → (𝐹‘𝑗) ∈ ℂ)
149	148	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℂ)
150	143, 149	npcand 10275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
151	150	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
152	151	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = 𝑛)
153		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → ((𝑛 − (𝐹‘𝑗)) + (𝐹‘𝑗)) = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
154	152, 153	sylan9req 2665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
155	154	exp31 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
156	155	com23 84	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) → ((𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))))
157	156	3impia 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
158	157	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗)))
159	141, 158	jca 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝐹‘𝑗) ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + (𝐹‘𝑗))))
160	127, 133, 159	rspcedvd 3289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
161	160	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
162	161	reximdva 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
163	162	reximdva 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ 𝜑) ∧ (𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
164	163	exp41 636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (𝜑 → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
165	164	com25 97	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞)) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
166	165	imp 444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ (𝑛 − (𝐹‘𝑗)) = (𝑝 + 𝑞))) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
167	123, 166	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
168	167	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
169	122, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) ∧ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven )) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
170	169	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
171	170	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → ((𝑛 − (𝐹‘𝑗)) ∈ Even → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
172	171	com13 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (((4 < (𝑛 − (𝐹‘𝑗)) ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁) → (𝑛 − (𝐹‘𝑗)) ∈ GoldbachEven ) → (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
173	121, 172	syld 46	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
174	173	com23 84	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 − (𝐹‘𝑗)) ∈ Even → (((𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))))
175	174	3impib 1254	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
176	175	com15 99	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ) → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))))
177	99, 176	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝑗 ∈ (1..^𝐷) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
178	177	impl 648	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
179	178	imp 444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (((𝑛 − (𝐹‘𝑗)) ∈ Even ∧ (𝑛 − (𝐹‘𝑗)) < 𝑁 ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
180	108, 179	syld 46	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) ∧ 4 < (𝑛 − (𝐹‘𝑗))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
181	180	expcomd 453	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (4 < (𝑛 − (𝐹‘𝑗)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
182	21	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ ℝ)
183	144	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑗) ∈ ℙ → (𝐹‘𝑗) ∈ ℝ)
184	124, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) → (𝐹‘𝑗) ∈ ℝ)
185	184	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗))) → (𝐹‘𝑗) ∈ ℝ)
186	185	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝐹‘𝑗) ∈ ℝ)
187	182, 186	resubcld 10337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 − (𝐹‘𝑗)) ∈ ℝ)
188		4re 10974	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 4 ∈ ℝ
189		lelttric 10023	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 − (𝐹‘𝑗)) ∈ ℝ ∧ 4 ∈ ℝ) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 ∨ 4 < (𝑛 − (𝐹‘𝑗))))
190	187, 188, 189	sylancl 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 − (𝐹‘𝑗)) ≤ 4 ∨ 4 < (𝑛 − (𝐹‘𝑗))))
191	102, 181, 190	mpjaod 395	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
192	191	ex 449	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) ∧ ((𝐹‘𝑗) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑗 + 1)) − (𝐹‘𝑗)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
193	97, 192	mpdan 699	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1..^𝐷)) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
194	193	expcom 450	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (1..^𝐷) → (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))))
195	194	impd 446	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (1..^𝐷) → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
196	83, 195	jaoi 393	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)) → ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
197	196	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑗 ∈ {0} ∨ 𝑗 ∈ (1..^𝐷)) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
198	57, 197	sylbid 229	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑗 ∈ (0..^𝐷) → (𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
199	198	rexlimdv 3012	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
200	51, 199	embantd 57	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ((𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
201	200	ex 449	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ((𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
202	201	com23 84	. . . . . . . 8 ⊢ (𝜑 → ((𝑛 ∈ ((𝐹‘0)[,)(𝐹‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝐹‘𝑗)[,)(𝐹‘(𝑗 + 1)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
203	19, 202	syld 46	. . . . . . 7 ⊢ (𝜑 → (∀𝑓 ∈ (RePart‘𝐷)(𝑛 ∈ ((𝑓‘0)[,)(𝑓‘𝐷)) → ∃𝑗 ∈ (0..^𝐷)𝑛 ∈ ((𝑓‘𝑗)[,)(𝑓‘(𝑗 + 1)))) → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))))
204	6, 203	mpd 15	. . . . . 6 ⊢ (𝜑 → ((𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
205	204	imp 444	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟)))
206	1, 205	jca 553	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → (𝑛 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑛 = ((𝑝 + 𝑞) + 𝑟))))
207	206, 76	sylibr 223	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ Odd ∧ (7 < 𝑛 ∧ 𝑛 < 𝑀))) → 𝑛 ∈ GoldbachOddALTV )
208	207	exp32 629	. 2 ⊢ (𝜑 → (𝑛 ∈ Odd → ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOddALTV )))
209	208	ralrimiv 2948	1 ⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOddALTV ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 ∖ cdif 3537 ∪ cun 3538 {csn 4125 class class class wbr 4583 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 2c2 10947 3c3 10948 4c4 10949 7c7 10952 cdc 11369 ℤ_≥cuz 11563 [,)cico 12048 ..^cfzo 12334 ℙcprime 15223 RePartciccp 39951 Even ceven 40075 Odd codd 40076 GoldbachEven cgbe 40167 GoldbachOddALTV cgboa 40169

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

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

This theorem is referenced by: tgblthelfgott 40229 tgblthelfgottOLD 40236

W3C validator