Theorem prmgaplem7 17142

Description: Lemma for prmgap 17144. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.)

Hypotheses

Ref	Expression
prmgaplem7.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
prmgaplem7.f	⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ))
prmgaplem7.i	⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))

Assertion

Ref	Expression
prmgaplem7	⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))

Distinct variable groups:   𝐹,𝑝,𝑞,𝑧   𝑖,𝐹   𝑁,𝑝,𝑞,𝑧   𝑖,𝑁   𝜑,𝑝,𝑞,𝑧

Allowed substitution hint:   𝜑(𝑖)

Proof of Theorem prmgaplem7

Dummy variables 𝑟 𝑠 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmgaplem7.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ))
2		elmapi 8855	. . . 4 ⊢ (𝐹 ∈ (ℕ ↑m ℕ) → 𝐹:ℕ⟶ℕ)
3	1, 2	syl 18	. . 3 ⊢ (𝜑 → 𝐹:ℕ⟶ℕ)
4		prmgaplem7.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
5	3, 4	ffvelcdmd 7087	. 2 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℕ)
6		elnnuz 12920	. . . . . . 7 ⊢ ((𝐹‘𝑁) ∈ ℕ ↔ (𝐹‘𝑁) ∈ (ℤ≥‘1))
7	6	bilani 510	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ (ℤ≥‘1))
8		2z 12644	. . . . . . 7 ⊢ 2 ∈ ℤ
9	8	eluzaddi 12911	. . . . . 6 ⊢ ((𝐹‘𝑁) ∈ (ℤ≥‘1) → ((𝐹‘𝑁) + 2) ∈ (ℤ≥‘(1 + 2)))
10	7, 9	syl 18	. . . . 5 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 2) ∈ (ℤ≥‘(1 + 2)))
11		1p2e3 12401	. . . . . . 7 ⊢ (1 + 2) = 3
12	11	eqcomi 2775	. . . . . 6 ⊢ 3 = (1 + 2)
13	12	fveq2i 6891	. . . . 5 ⊢ (ℤ≥‘3) = (ℤ≥‘(1 + 2))
14	10, 13	eleqtrrdi 2877	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 2) ∈ (ℤ≥‘3))
15		prmgaplem5 17140	. . . 4 ⊢ (((𝐹‘𝑁) + 2) ∈ (ℤ≥‘3) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ))
16	14, 15	syl 18	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ))
17	4	anim1ci 628	. . . . 5 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ))
18		nnaddcl 12274	. . . . 5 ⊢ (((𝐹‘𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹‘𝑁) + 𝑁) ∈ ℕ)
19	17, 18	syl 18	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 𝑁) ∈ ℕ)
20		prmgaplem6 17141	. . . 4 ⊢ (((𝐹‘𝑁) + 𝑁) ∈ ℕ → ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
21	19, 20	syl 18	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
22		reeanv 3240	. . . 4 ⊢ (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) ↔ (∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)))
23		simprll 791	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → 𝑝 < ((𝐹‘𝑁) + 2))
24		simprrl 793	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ((𝐹‘𝑁) + 𝑁) < 𝑞)
25		nnz 12630	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑁) ∈ ℕ → (𝐹‘𝑁) ∈ ℤ)
26	25	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℤ)
27	8	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 2 ∈ ℤ)
28	26, 27	zaddcld 12722	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 2) ∈ ℤ)
29	28	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝐹‘𝑁) + 2) ∈ ℤ)
30	29	anim1ci 628	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹‘𝑁) + 2) ∈ ℤ))
31		fzospliti 13739	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹‘𝑁) + 2) ∈ ℤ) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)))
32	30, 31	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)))
33	32	ex 418	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞))))
34		neleq1 3073	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑧 → (𝑟 ∉ ℙ ↔ 𝑧 ∉ ℙ))
35	34	rspcv 3580	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → (∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ → 𝑧 ∉ ℙ))
36	35	adantld 496	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) → 𝑧 ∉ ℙ))
37	36	adantrd 497	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
38	37	a1d 26	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
39	19	nnzd 12635	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 𝑁) ∈ ℤ)
40	39	peano2zd 12721	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ)
41	40	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ)
42	41	anim1ci 628	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ))
43		fzospliti 13739	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)))
44	42, 43	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)))
45	44	ex 418	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞))))
46		prmgaplem7.i	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))
47	4	nnzd 12635	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∈ ℤ)
48		fzshftral 13662	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐹‘𝑁) ∈ ℤ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖)))
49	8, 47, 25, 48	mp3an3an 1496	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖)))
50		2cnd 12337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 2 ∈ ℂ)
51		nncn 12259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘𝑁) ∈ ℕ → (𝐹‘𝑁) ∈ ℂ)
52		addcom 11414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((2 ∈ ℂ ∧ (𝐹‘𝑁) ∈ ℂ) → (2 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 2))
53	50, 51, 52	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (2 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 2))
54	4	nncnd 12267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑁 ∈ ℂ)
55		addcom 11414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℂ ∧ (𝐹‘𝑁) ∈ ℂ) → (𝑁 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 𝑁))
56	54, 51, 55	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑁 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 𝑁))
57	53, 56	oveq12d 7441	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁))) = (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)))
58		ovex 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 − (𝐹‘𝑁)) ∈ V
59		sbcbr2g 5174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ([(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖)))
60	58, 59	mp1i 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ([(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖)))
61		csbov12g 7469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) = (⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) gcd ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖))
62	58, 61	mp1i 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) = (⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) gcd ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖))
63		csbov2g 7471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) = ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖))
64	58, 63	mp1i 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) = ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖))
65		csbvarg 4402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖 = (𝑗 − (𝐹‘𝑁)))
66	65	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖) = ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))))
67	58, 66	mp1i 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖) = ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))))
68	64, 67	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) = ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))))
69	58, 65	mp1i 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖 = (𝑗 − (𝐹‘𝑁)))
70	68, 69	oveq12d 7441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) gcd ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖) = (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))))
71	62, 70	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) = (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))))
72	71	breq2d 5126	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (1 < ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁)))))
73	60, 72	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ([(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁)))))
74	57, 73	raleqbidv 3341	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁)))))
75		fzval3 13782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐹‘𝑁) + 𝑁) ∈ ℤ → (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)) = (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)))
76	75	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐹‘𝑁) + 𝑁) ∈ ℤ → (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) = (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)))
77	39, 76	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) = (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)))
78	77	eleq2d 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ↔ 𝑧 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))))
79	78	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 𝑧 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)))
80		oveq1 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑗 = 𝑧 → (𝑗 − (𝐹‘𝑁)) = (𝑧 − (𝐹‘𝑁)))
81	80	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑗 = 𝑧 → ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) = ((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))))
82	81, 80	oveq12d 7441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 = 𝑧 → (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) = (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))))
83	82	breq2d 5126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 = 𝑧 → (1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) ↔ 1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁)))))
84	83	rspcv 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁)))))
85	79, 84	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁)))))
86	51	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℂ)
87		elfzoelz 13706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℤ)
88	87	zcnd 12719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℂ)
89		pncan3 11483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐹‘𝑁) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) = 𝑧)
90	86, 88, 89	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → ((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) = 𝑧)
91	90	oveq1d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) = (𝑧 gcd (𝑧 − (𝐹‘𝑁))))
92	87	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℤ)
93		zsubcl 12654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑧 ∈ ℤ ∧ (𝐹‘𝑁) ∈ ℤ) → (𝑧 − (𝐹‘𝑁)) ∈ ℤ)
94	87, 26, 93	syl2anr 609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹‘𝑁)) ∈ ℤ)
95	92, 94	gcdcomd 16597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 gcd (𝑧 − (𝐹‘𝑁))) = ((𝑧 − (𝐹‘𝑁)) gcd 𝑧))
96	91, 95	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) = ((𝑧 − (𝐹‘𝑁)) gcd 𝑧))
97	96	breq2d 5126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) ↔ 1 < ((𝑧 − (𝐹‘𝑁)) gcd 𝑧)))
98		elfzo2 13709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ↔ (𝑧 ∈ (ℤ≥‘((𝐹‘𝑁) + 2)) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹‘𝑁) + 𝑁) + 1)))
99		eluz2 12886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑧 ∈ (ℤ≥‘((𝐹‘𝑁) + 2)) ↔ (((𝐹‘𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧))
100		nnre 12258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐹‘𝑁) ∈ ℕ → (𝐹‘𝑁) ∈ ℝ)
101	100	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (𝐹‘𝑁) ∈ ℝ)
102		2rp 13039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ 2 ∈ ℝ+
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 2 ∈ ℝ+)
104	101, 103	ltaddrpd 13111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (𝐹‘𝑁) < ((𝐹‘𝑁) + 2))
105		2re 12333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 2 ∈ ℝ
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝐹‘𝑁) ∈ ℕ → 2 ∈ ℝ)
107	100, 106	readdcld 11256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐹‘𝑁) ∈ ℕ → ((𝐹‘𝑁) + 2) ∈ ℝ)
108	107	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → ((𝐹‘𝑁) + 2) ∈ ℝ)
109		zre 12613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
110	109	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 𝑧 ∈ ℝ)
111		ltletr 11320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝐹‘𝑁) ∈ ℝ ∧ ((𝐹‘𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐹‘𝑁) < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → (𝐹‘𝑁) < 𝑧))
112	101, 108, 110, 111	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (((𝐹‘𝑁) < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → (𝐹‘𝑁) < 𝑧))
113	104, 112	mpand 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (((𝐹‘𝑁) + 2) ≤ 𝑧 → (𝐹‘𝑁) < 𝑧))
114	113	impancom 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧))
115	114	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝐹‘𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧))
116	99, 115	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 ∈ (ℤ≥‘((𝐹‘𝑁) + 2)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧))
117	116	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑧 ∈ (ℤ≥‘((𝐹‘𝑁) + 2)) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧))
118	98, 117	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧))
119	118	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝐹‘𝑁) < 𝑧)
120	100	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℝ)
121	87	zred 12718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℝ)
122		posdif 11725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐹‘𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹‘𝑁))))
123	120, 121, 122	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → ((𝐹‘𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹‘𝑁))))
124	119, 123	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 0 < (𝑧 − (𝐹‘𝑁)))
125		elnnz 12619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑧 − (𝐹‘𝑁)) ∈ ℕ ↔ ((𝑧 − (𝐹‘𝑁)) ∈ ℤ ∧ 0 < (𝑧 − (𝐹‘𝑁))))
126	94, 124, 125	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹‘𝑁)) ∈ ℕ)
127	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 2 ∈ ℝ)
128		nngt0 12285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝐹‘𝑁) ∈ ℕ → 0 < (𝐹‘𝑁))
129	128	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 < (𝐹‘𝑁))
130		2pos 12363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 0 < 2
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 < 2)
132	101, 127, 129, 131	addgt0d 11807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 < ((𝐹‘𝑁) + 2))
133		0red 11229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 ∈ ℝ)
134		ltletr 11320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((0 ∈ ℝ ∧ ((𝐹‘𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((0 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
135	133, 108, 110, 134	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → ((0 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
136	132, 135	mpand 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (((𝐹‘𝑁) + 2) ≤ 𝑧 → 0 < 𝑧))
137	136	impancom 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧))
138	137	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝐹‘𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧))
139	99, 138	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ (ℤ≥‘((𝐹‘𝑁) + 2)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧))
140	139	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑧 ∈ (ℤ≥‘((𝐹‘𝑁) + 2)) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧))
141	98, 140	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧))
142	141	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 0 < 𝑧)
143		elnnz 12619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ ℕ ↔ (𝑧 ∈ ℤ ∧ 0 < 𝑧))
144	92, 142, 143	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℕ)
145	128	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < (𝐹‘𝑁))
146	145	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 0 < (𝐹‘𝑁))
147		ltsubpos 11724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐹‘𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 < (𝐹‘𝑁) ↔ (𝑧 − (𝐹‘𝑁)) < 𝑧))
148	120, 121, 147	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (0 < (𝐹‘𝑁) ↔ (𝑧 − (𝐹‘𝑁)) < 𝑧))
149	146, 148	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹‘𝑁)) < 𝑧)
150		ncoprmlnprm 16812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑧 − (𝐹‘𝑁)) ∈ ℕ ∧ 𝑧 ∈ ℕ ∧ (𝑧 − (𝐹‘𝑁)) < 𝑧) → (1 < ((𝑧 − (𝐹‘𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
151	126, 144, 149, 150	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (1 < ((𝑧 − (𝐹‘𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
152	97, 151	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) → 𝑧 ∉ ℙ))
153	85, 152	syld 48	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 𝑧 ∉ ℙ))
154	153	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 𝑧 ∉ ℙ)))
155	154	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
156	74, 155	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
157	49, 156	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
158	157	ex 418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐹‘𝑁) ∈ ℕ → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))))
159	46, 158	mpid 45	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐹‘𝑁) ∈ ℕ → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
160	159	imp 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
161	160	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
162	161	impcom 413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → 𝑧 ∉ ℙ)
163	162	a1d 26	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
164	163	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
165		neleq1 3073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = 𝑧 → (𝑠 ∉ ℙ ↔ 𝑧 ∉ ℙ))
166	165	rspcv 3580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → (∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ → 𝑧 ∉ ℙ))
167	166	adantld 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → ((((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ) → 𝑧 ∉ ℙ))
168	167	adantld 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
169	168	a1d 26	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
170	164, 169	jaoi 871	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
171	170	com12 33	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
172	45, 171	syldc 49	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
173	38, 172	jaoi 871	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
174	173	com12 33	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
175	33, 174	syld 48	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
176	175	com23 87	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → 𝑧 ∉ ℙ)))
177	176	imp31 423	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → 𝑧 ∉ ℙ)
178	177	ralrimiva 3160	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)
179	23, 24, 178	3jca 1146	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
180	179	ex 418	. . . . . 6 ⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
181	180	reximdva 3181	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
182	181	reximdva 3181	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
183	22, 182	biimtrrid 246	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
184	16, 21, 183	mp2and 712	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
185	5, 184	mpdan 700	1 ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ∉ wnel 3067  ∀wral 3082  ∃wrex 3092  Vcvv 3458  [wsbc 3747  ⦋csb 3856   class class class wbr 5114  ⟶wf 6539  ‘cfv 6543  (class class class)co 7423   ↑_m cmap 8833  ℂcc 11116  ℝcr 11117  0cc0 11118  1c1 11119   + caddc 11121   < clt 11261   ≤ cle 11262   − cmin 11459  ℕcn 12251  2c2 12313  3c3 12314  ℤcz 12609  ℤ_≥cuz 12880  ℝ⁺crp 13034  ...cfz 13553  ..^cfzo 13701   gcd cgcd 16577  ℙcprime 16754

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195  ax-pre-sup 11196

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8703  df-map 8835  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-sup 9412  df-inf 9413  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-div 11890  df-nn 12252  df-2 12321  df-3 12322  df-n0 12523  df-z 12610  df-uz 12881  df-rp 13035  df-fz 13554  df-fzo 13702  df-seq 14058  df-exp 14118  df-fac 14330  df-cj 15176  df-re 15177  df-im 15178  df-sqrt 15312  df-abs 15313  df-dvds 16336  df-gcd 16578  df-prm 16755

This theorem is used by:  prmgaplem8  17143