Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmgaplem7 Structured version   Visualization version   GIF version

Theorem prmgaplem7 16390
 Description: Lemma for prmgap 16392. (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.
StepHypRef Expression
1 prmgaplem7.f . . . 4 (𝜑𝐹 ∈ (ℕ ↑m ℕ))
2 elmapi 8418 . . . 4 (𝐹 ∈ (ℕ ↑m ℕ) → 𝐹:ℕ⟶ℕ)
31, 2syl 17 . . 3 (𝜑𝐹:ℕ⟶ℕ)
4 prmgaplem7.n . . 3 (𝜑𝑁 ∈ ℕ)
53, 4ffvelrnd 6834 . 2 (𝜑 → (𝐹𝑁) ∈ ℕ)
6 simpr 488 . . . . . . 7 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℕ)
7 elnnuz 12277 . . . . . . 7 ((𝐹𝑁) ∈ ℕ ↔ (𝐹𝑁) ∈ (ℤ‘1))
86, 7sylib 221 . . . . . 6 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ (ℤ‘1))
9 1z 12007 . . . . . . 7 1 ∈ ℤ
10 2z 12009 . . . . . . 7 2 ∈ ℤ
119, 10eluzaddi 12266 . . . . . 6 ((𝐹𝑁) ∈ (ℤ‘1) → ((𝐹𝑁) + 2) ∈ (ℤ‘(1 + 2)))
128, 11syl 17 . . . . 5 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ (ℤ‘(1 + 2)))
13 1p2e3 11775 . . . . . . 7 (1 + 2) = 3
1413eqcomi 2807 . . . . . 6 3 = (1 + 2)
1514fveq2i 6653 . . . . 5 (ℤ‘3) = (ℤ‘(1 + 2))
1612, 15eleqtrrdi 2901 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ (ℤ‘3))
17 prmgaplem5 16388 . . . 4 (((𝐹𝑁) + 2) ∈ (ℤ‘3) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ))
1816, 17syl 17 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ))
194anim1ci 618 . . . . 5 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ))
20 nnaddcl 11655 . . . . 5 (((𝐹𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℕ)
2119, 20syl 17 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℕ)
22 prmgaplem6 16389 . . . 4 (((𝐹𝑁) + 𝑁) ∈ ℕ → ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
2321, 22syl 17 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
24 reeanv 3320 . . . 4 (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) ↔ (∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)))
25 simprll 778 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → 𝑝 < ((𝐹𝑁) + 2))
26 simprrl 780 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ((𝐹𝑁) + 𝑁) < 𝑞)
27 nnz 11999 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℤ)
2827adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℤ)
2910a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 2 ∈ ℤ)
3028, 29zaddcld 12086 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ ℤ)
3130ad2antrr 725 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝐹𝑁) + 2) ∈ ℤ)
3231anim1ci 618 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹𝑁) + 2) ∈ ℤ))
33 fzospliti 13071 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹𝑁) + 2) ∈ ℤ) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
3432, 33syl 17 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
3534ex 416 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞))))
36 neleq1 3096 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑧 → (𝑟 ∉ ℙ ↔ 𝑧 ∉ ℙ))
3736rspcv 3566 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → (∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ → 𝑧 ∉ ℙ))
3837adantld 494 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) → 𝑧 ∉ ℙ))
3938adantrd 495 . . . . . . . . . . . . . . 15 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
4039a1d 25 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
4121nnzd 12081 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℤ)
4241peano2zd 12085 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ)
4342ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ)
4443anim1ci 618 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ))
45 fzospliti 13071 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)))
4644, 45syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)))
4746ex 416 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞))))
48 prmgaplem7.i . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖))
494nnzd 12081 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℤ)
50 fzshftral 12997 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐹𝑁) ∈ ℤ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖)))
5110, 49, 27, 50mp3an3an 1464 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖)))
52 2cnd 11710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → 2 ∈ ℂ)
53 nncn 11640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℂ)
54 addcom 10822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℂ ∧ (𝐹𝑁) ∈ ℂ) → (2 + (𝐹𝑁)) = ((𝐹𝑁) + 2))
5552, 53, 54syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (2 + (𝐹𝑁)) = ((𝐹𝑁) + 2))
564nncnd 11648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℂ)
57 addcom 10822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℂ ∧ (𝐹𝑁) ∈ ℂ) → (𝑁 + (𝐹𝑁)) = ((𝐹𝑁) + 𝑁))
5856, 53, 57syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑁 + (𝐹𝑁)) = ((𝐹𝑁) + 𝑁))
5955, 58oveq12d 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁))) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
60 ovex 7173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 − (𝐹𝑁)) ∈ V
61 sbcbr2g 5089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 − (𝐹𝑁)) ∈ V → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖)))
6260, 61mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖)))
63 csbov12g 7184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
6460, 63mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
65 csbov2g 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
6660, 65mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
67 csbvarg 4339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖𝑖 = (𝑗 − (𝐹𝑁)))
6867oveq2d 7156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 − (𝐹𝑁)) ∈ V → ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
6960, 68mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7066, 69eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7160, 67mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖𝑖 = (𝑗 − (𝐹𝑁)))
7270, 71oveq12d 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))))
7364, 72eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))))
7473breq2d 5043 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
7562, 74bitrd 282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
7659, 75raleqbidv 3354 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
77 fzval3 13108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) + 𝑁) ∈ ℤ → (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)) = (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)))
7877eqcomd 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐹𝑁) + 𝑁) ∈ ℤ → (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
7941, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
8079eleq2d 2875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ↔ 𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))))
8180biimpa 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
82 oveq1 7147 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 𝑧 → (𝑗 − (𝐹𝑁)) = (𝑧 − (𝐹𝑁)))
8382oveq2d 7156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 𝑧 → ((𝐹𝑁) + (𝑗 − (𝐹𝑁))) = ((𝐹𝑁) + (𝑧 − (𝐹𝑁))))
8483, 82oveq12d 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑧 → (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) = (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))))
8584breq2d 5043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑧 → (1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) ↔ 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
8685rspcv 3566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
8781, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
8853adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℂ)
89 elfzoelz 13040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℤ)
9089zcnd 12083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℂ)
91 pncan3 10890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝐹𝑁) + (𝑧 − (𝐹𝑁))) = 𝑧)
9288, 90, 91syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → ((𝐹𝑁) + (𝑧 − (𝐹𝑁))) = 𝑧)
9392oveq1d 7155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) = (𝑧 gcd (𝑧 − (𝐹𝑁))))
9489adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℤ)
95 zsubcl 12019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ ℤ ∧ (𝐹𝑁) ∈ ℤ) → (𝑧 − (𝐹𝑁)) ∈ ℤ)
9689, 28, 95syl2anr 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) ∈ ℤ)
97 gcdcom 15859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑧 ∈ ℤ ∧ (𝑧 − (𝐹𝑁)) ∈ ℤ) → (𝑧 gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
9894, 96, 97syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
9993, 98eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
10099breq2d 5043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) ↔ 1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧)))
101 elfzo2 13043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ↔ (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)))
102 eluz2 12244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ↔ (((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧))
103 nnre 11639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℝ)
104103ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (𝐹𝑁) ∈ ℝ)
105 2rp 12389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 2 ∈ ℝ+
106105a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 2 ∈ ℝ+)
107104, 106ltaddrpd 12459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (𝐹𝑁) < ((𝐹𝑁) + 2))
108 2re 11706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 2 ∈ ℝ
109108a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐹𝑁) ∈ ℕ → 2 ∈ ℝ)
110103, 109readdcld 10666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐹𝑁) ∈ ℕ → ((𝐹𝑁) + 2) ∈ ℝ)
111110ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → ((𝐹𝑁) + 2) ∈ ℝ)
112 zre 11980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
113112adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 𝑧 ∈ ℝ)
114 ltletr 10728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝐹𝑁) ∈ ℝ ∧ ((𝐹𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐹𝑁) < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → (𝐹𝑁) < 𝑧))
115104, 111, 113, 114syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → (𝐹𝑁) < 𝑧))
116107, 115mpand 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) + 2) ≤ 𝑧 → (𝐹𝑁) < 𝑧))
117116impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
1181173adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
119102, 118sylbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
1201193ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
121101, 120sylbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
122121impcom 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝐹𝑁) < 𝑧)
123103adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℝ)
12489zred 12082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℝ)
125 posdif 11129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹𝑁))))
126123, 124, 125syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → ((𝐹𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹𝑁))))
127122, 126mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < (𝑧 − (𝐹𝑁)))
128 elnnz 11986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 − (𝐹𝑁)) ∈ ℕ ↔ ((𝑧 − (𝐹𝑁)) ∈ ℤ ∧ 0 < (𝑧 − (𝐹𝑁))))
12996, 127, 128sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) ∈ ℕ)
130108a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 2 ∈ ℝ)
131 nngt0 11663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐹𝑁) ∈ ℕ → 0 < (𝐹𝑁))
132131ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < (𝐹𝑁))
133 2pos 11735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 0 < 2
134133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < 2)
135104, 130, 132, 134addgt0d 11211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < ((𝐹𝑁) + 2))
136 0red 10640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 ∈ ℝ)
137 ltletr 10728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((0 ∈ ℝ ∧ ((𝐹𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((0 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
138136, 111, 113, 137syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → ((0 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
139135, 138mpand 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) + 2) ≤ 𝑧 → 0 < 𝑧))
140139impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
1411403adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
142102, 141sylbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
1431423ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
144101, 143sylbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
145144impcom 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < 𝑧)
146 elnnz 11986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 ∈ ℕ ↔ (𝑧 ∈ ℤ ∧ 0 < 𝑧))
14794, 145, 146sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℕ)
148131adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < (𝐹𝑁))
149148adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < (𝐹𝑁))
150 ltsubpos 11128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐹𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 < (𝐹𝑁) ↔ (𝑧 − (𝐹𝑁)) < 𝑧))
151123, 124, 150syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (0 < (𝐹𝑁) ↔ (𝑧 − (𝐹𝑁)) < 𝑧))
152149, 151mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) < 𝑧)
153 ncoprmlnprm 16065 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑧 − (𝐹𝑁)) ∈ ℕ ∧ 𝑧 ∈ ℕ ∧ (𝑧 − (𝐹𝑁)) < 𝑧) → (1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
154129, 147, 152, 153syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
155100, 154sylbid 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) → 𝑧 ∉ ℙ))
15687, 155syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 𝑧 ∉ ℙ))
157156ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 𝑧 ∉ ℙ)))
158157com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
15976, 158sylbid 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
16051, 159sylbid 243 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
161160ex 416 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐹𝑁) ∈ ℕ → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))))
16248, 161mpid 44 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐹𝑁) ∈ ℕ → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
163162imp 410 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
164163ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
165164impcom 411 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → 𝑧 ∉ ℙ)
166165a1d 25 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
167166ex 416 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
168 neleq1 3096 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑧 → (𝑠 ∉ ℙ ↔ 𝑧 ∉ ℙ))
169168rspcv 3566 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → (∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ → 𝑧 ∉ ℙ))
170169adantld 494 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → ((((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ) → 𝑧 ∉ ℙ))
171170adantld 494 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
172171a1d 25 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
173167, 172jaoi 854 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
174173com12 32 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
17547, 174syldc 48 . . . . . . . . . . . . . 14 (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
17640, 175jaoi 854 . . . . . . . . . . . . 13 ((𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
177176com12 32 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
17835, 177syld 47 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
179178com23 86 . . . . . . . . . 10 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → 𝑧 ∉ ℙ)))
180179imp31 421 . . . . . . . . 9 ((((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → 𝑧 ∉ ℙ)
181180ralrimiva 3149 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)
18225, 26, 1813jca 1125 . . . . . . 7 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
183182ex 416 . . . . . 6 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
184183reximdva 3233 . . . . 5 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
185184reximdva 3233 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
18624, 185syl5bir 246 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
18718, 23, 186mp2and 698 . 2 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
1885, 187mpdan 686 1 (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ∉ wnel 3091  ∀wral 3106  ∃wrex 3107  Vcvv 3441  [wsbc 3720  ⦋csb 3828   class class class wbr 5031  ⟶wf 6323  ‘cfv 6327  (class class class)co 7140   ↑m cmap 8396  ℂcc 10531  ℝcr 10532  0cc0 10533  1c1 10534   + caddc 10536   < clt 10671   ≤ cle 10672   − cmin 10866  ℕcn 11632  2c2 11687  3c3 11688  ℤcz 11976  ℤ≥cuz 12238  ℝ+crp 12384  ...cfz 12892  ..^cfzo 13035   gcd cgcd 15840  ℙcprime 16012 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7448  ax-cnex 10589  ax-resscn 10590  ax-1cn 10591  ax-icn 10592  ax-addcl 10593  ax-addrcl 10594  ax-mulcl 10595  ax-mulrcl 10596  ax-mulcom 10597  ax-addass 10598  ax-mulass 10599  ax-distr 10600  ax-i2m1 10601  ax-1ne0 10602  ax-1rid 10603  ax-rnegex 10604  ax-rrecex 10605  ax-cnre 10606  ax-pre-lttri 10607  ax-pre-lttrn 10608  ax-pre-ltadd 10609  ax-pre-mulgt0 10610  ax-pre-sup 10611 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6286  df-fun 6329  df-fn 6330  df-f 6331  df-f1 6332  df-fo 6333  df-f1o 6334  df-fv 6335  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7568  df-1st 7678  df-2nd 7679  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-2o 8093  df-er 8279  df-map 8398  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-sup 8897  df-inf 8898  df-pnf 10673  df-mnf 10674  df-xr 10675  df-ltxr 10676  df-le 10677  df-sub 10868  df-neg 10869  df-div 11294  df-nn 11633  df-2 11695  df-3 11696  df-n0 11893  df-z 11977  df-uz 12239  df-rp 12385  df-fz 12893  df-fzo 13036  df-seq 13372  df-exp 13433  df-fac 13637  df-cj 14457  df-re 14458  df-im 14459  df-sqrt 14593  df-abs 14594  df-dvds 15607  df-gcd 15841  df-prm 16013 This theorem is referenced by:  prmgaplem8  16391
 Copyright terms: Public domain W3C validator