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

Theorem prmgaplem7 16043
Description: Lemma for prmgap 16045. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.)
Hypotheses
Ref Expression
prmgaplem7.n (𝜑𝑁 ∈ ℕ)
prmgaplem7.f (𝜑𝐹 ∈ (ℕ ↑𝑚 ℕ))
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 (𝜑𝐹 ∈ (ℕ ↑𝑚 ℕ))
2 elmapi 8084 . . . 4 (𝐹 ∈ (ℕ ↑𝑚 ℕ) → 𝐹:ℕ⟶ℕ)
31, 2syl 17 . . 3 (𝜑𝐹:ℕ⟶ℕ)
4 prmgaplem7.n . . 3 (𝜑𝑁 ∈ ℕ)
53, 4ffvelrnd 6552 . 2 (𝜑 → (𝐹𝑁) ∈ ℕ)
6 simpr 477 . . . . . . 7 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℕ)
7 elnnuz 11927 . . . . . . 7 ((𝐹𝑁) ∈ ℕ ↔ (𝐹𝑁) ∈ (ℤ‘1))
86, 7sylib 209 . . . . . 6 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ (ℤ‘1))
9 1z 11657 . . . . . . 7 1 ∈ ℤ
10 2z 11659 . . . . . . 7 2 ∈ ℤ
119, 10eluzaddi 11916 . . . . . 6 ((𝐹𝑁) ∈ (ℤ‘1) → ((𝐹𝑁) + 2) ∈ (ℤ‘(1 + 2)))
128, 11syl 17 . . . . 5 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ (ℤ‘(1 + 2)))
13 1p2e3 11424 . . . . . . 7 (1 + 2) = 3
1413eqcomi 2774 . . . . . 6 3 = (1 + 2)
1514fveq2i 6380 . . . . 5 (ℤ‘3) = (ℤ‘(1 + 2))
1612, 15syl6eleqr 2855 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ (ℤ‘3))
17 prmgaplem5 16041 . . . 4 (((𝐹𝑁) + 2) ∈ (ℤ‘3) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ))
1816, 17syl 17 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ))
194anim1i 608 . . . . . 6 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑁 ∈ ℕ ∧ (𝐹𝑁) ∈ ℕ))
2019ancomd 453 . . . . 5 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ))
21 nnaddcl 11300 . . . . 5 (((𝐹𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℕ)
2220, 21syl 17 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℕ)
23 prmgaplem6 16042 . . . 4 (((𝐹𝑁) + 𝑁) ∈ ℕ → ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
2422, 23syl 17 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
25 reeanv 3254 . . . 4 (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) ↔ (∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)))
26 simprll 797 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → 𝑝 < ((𝐹𝑁) + 2))
27 simprrl 799 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ((𝐹𝑁) + 𝑁) < 𝑞)
28 nnz 11649 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℤ)
2928adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℤ)
3010a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 2 ∈ ℤ)
3129, 30zaddcld 11736 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ ℤ)
3231ad2antrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝐹𝑁) + 2) ∈ ℤ)
3332anim1i 608 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)))
3433ancomd 453 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹𝑁) + 2) ∈ ℤ))
35 fzospliti 12711 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹𝑁) + 2) ∈ ℤ) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
3634, 35syl 17 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
3736ex 401 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞))))
38 neleq1 3045 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑧 → (𝑟 ∉ ℙ ↔ 𝑧 ∉ ℙ))
3938rspcv 3458 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → (∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ → 𝑧 ∉ ℙ))
4039adantld 484 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) → 𝑧 ∉ ℙ))
4140adantrd 485 . . . . . . . . . . . . . . 15 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
4241a1d 25 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
4322nnzd 11731 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℤ)
4443peano2zd 11735 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ)
4544ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ)
4645anim1i 608 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → ((((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
4746ancomd 453 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ))
48 fzospliti 12711 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)))
4947, 48syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)))
5049ex 401 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞))))
51 prmgaplem7.i . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖))
524nnzd 11731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℤ)
53 fzshftral 12638 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐹𝑁) ∈ ℤ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖)))
5410, 52, 28, 53mp3an3an 1591 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖)))
55 2cnd 11352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → 2 ∈ ℂ)
56 nncn 11285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℂ)
57 addcom 10478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℂ ∧ (𝐹𝑁) ∈ ℂ) → (2 + (𝐹𝑁)) = ((𝐹𝑁) + 2))
5855, 56, 57syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (2 + (𝐹𝑁)) = ((𝐹𝑁) + 2))
594nncnd 11294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℂ)
60 addcom 10478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℂ ∧ (𝐹𝑁) ∈ ℂ) → (𝑁 + (𝐹𝑁)) = ((𝐹𝑁) + 𝑁))
6159, 56, 60syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑁 + (𝐹𝑁)) = ((𝐹𝑁) + 𝑁))
6258, 61oveq12d 6862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁))) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
63 ovex 6876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 − (𝐹𝑁)) ∈ V
64 sbcbr2g 4869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 − (𝐹𝑁)) ∈ V → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖)))
6563, 64mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖)))
66 csbov12g 6887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
6763, 66mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
68 csbov2g 6889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
6963, 68mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
70 csbvarg 4166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖𝑖 = (𝑗 − (𝐹𝑁)))
7170oveq2d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 − (𝐹𝑁)) ∈ V → ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7263, 71mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7369, 72eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7463, 70mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖𝑖 = (𝑗 − (𝐹𝑁)))
7573, 74oveq12d 6862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))))
7667, 75eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))))
7776breq2d 4823 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
7865, 77bitrd 270 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
7962, 78raleqbidv 3300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
80 fzval3 12748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) + 𝑁) ∈ ℤ → (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)) = (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)))
8180eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐹𝑁) + 𝑁) ∈ ℤ → (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
8243, 81syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
8382eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ↔ 𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))))
8483biimpa 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
85 oveq1 6851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 𝑧 → (𝑗 − (𝐹𝑁)) = (𝑧 − (𝐹𝑁)))
8685oveq2d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 𝑧 → ((𝐹𝑁) + (𝑗 − (𝐹𝑁))) = ((𝐹𝑁) + (𝑧 − (𝐹𝑁))))
8786, 85oveq12d 6862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑧 → (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) = (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))))
8887breq2d 4823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑧 → (1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) ↔ 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
8988rspcv 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
9084, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
9156adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℂ)
92 elfzoelz 12681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℤ)
9392zcnd 11733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℂ)
94 pncan3 10545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝐹𝑁) + (𝑧 − (𝐹𝑁))) = 𝑧)
9591, 93, 94syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → ((𝐹𝑁) + (𝑧 − (𝐹𝑁))) = 𝑧)
9695oveq1d 6859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) = (𝑧 gcd (𝑧 − (𝐹𝑁))))
9792adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℤ)
98 zsubcl 11669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ ℤ ∧ (𝐹𝑁) ∈ ℤ) → (𝑧 − (𝐹𝑁)) ∈ ℤ)
9992, 29, 98syl2anr 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) ∈ ℤ)
100 gcdcom 15519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑧 ∈ ℤ ∧ (𝑧 − (𝐹𝑁)) ∈ ℤ) → (𝑧 gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
10197, 99, 100syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
10296, 101eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
103102breq2d 4823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) ↔ 1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧)))
104 elfzo2 12684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ↔ (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)))
105 eluz2 11895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ↔ (((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧))
106 nnre 11284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℝ)
107106ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (𝐹𝑁) ∈ ℝ)
108 2rp 12036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 2 ∈ ℝ+
109108a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 2 ∈ ℝ+)
110107, 109ltaddrpd 12106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (𝐹𝑁) < ((𝐹𝑁) + 2))
111 2re 11348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 2 ∈ ℝ
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐹𝑁) ∈ ℕ → 2 ∈ ℝ)
113106, 112readdcld 10325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐹𝑁) ∈ ℕ → ((𝐹𝑁) + 2) ∈ ℝ)
114113ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → ((𝐹𝑁) + 2) ∈ ℝ)
115 zre 11630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
116115adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 𝑧 ∈ ℝ)
117 ltletr 10385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝐹𝑁) ∈ ℝ ∧ ((𝐹𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐹𝑁) < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → (𝐹𝑁) < 𝑧))
118107, 114, 116, 117syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → (𝐹𝑁) < 𝑧))
119110, 118mpand 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) + 2) ≤ 𝑧 → (𝐹𝑁) < 𝑧))
120119impancom 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
1211203adant1 1160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
122105, 121sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
1231223ad2ant1 1163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
124104, 123sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
125124impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝐹𝑁) < 𝑧)
126106adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℝ)
12792zred 11732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℝ)
128 posdif 10777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹𝑁))))
129126, 127, 128syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → ((𝐹𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹𝑁))))
130125, 129mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < (𝑧 − (𝐹𝑁)))
131 elnnz 11636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 − (𝐹𝑁)) ∈ ℕ ↔ ((𝑧 − (𝐹𝑁)) ∈ ℤ ∧ 0 < (𝑧 − (𝐹𝑁))))
13299, 130, 131sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) ∈ ℕ)
133111a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 2 ∈ ℝ)
134 nngt0 11308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐹𝑁) ∈ ℕ → 0 < (𝐹𝑁))
135134ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < (𝐹𝑁))
136 2pos 11384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 0 < 2
137136a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < 2)
138107, 133, 135, 137addgt0d 10858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < ((𝐹𝑁) + 2))
139 0red 10299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 ∈ ℝ)
140 ltletr 10385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((0 ∈ ℝ ∧ ((𝐹𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((0 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
141139, 114, 116, 140syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → ((0 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
142138, 141mpand 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) + 2) ≤ 𝑧 → 0 < 𝑧))
143142impancom 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
1441433adant1 1160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
145105, 144sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
1461453ad2ant1 1163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
147104, 146sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
148147impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < 𝑧)
149 elnnz 11636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 ∈ ℕ ↔ (𝑧 ∈ ℤ ∧ 0 < 𝑧))
15097, 148, 149sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℕ)
151134adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < (𝐹𝑁))
152151adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < (𝐹𝑁))
153 ltsubpos 10776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐹𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 < (𝐹𝑁) ↔ (𝑧 − (𝐹𝑁)) < 𝑧))
154126, 127, 153syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (0 < (𝐹𝑁) ↔ (𝑧 − (𝐹𝑁)) < 𝑧))
155152, 154mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) < 𝑧)
156 ncoprmlnprm 15718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑧 − (𝐹𝑁)) ∈ ℕ ∧ 𝑧 ∈ ℕ ∧ (𝑧 − (𝐹𝑁)) < 𝑧) → (1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
157132, 150, 155, 156syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
158103, 157sylbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) → 𝑧 ∉ ℙ))
15990, 158syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 𝑧 ∉ ℙ))
160159ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 𝑧 ∉ ℙ)))
161160com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
16279, 161sylbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
16354, 162sylbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
164163ex 401 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐹𝑁) ∈ ℕ → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))))
16551, 164mpid 44 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐹𝑁) ∈ ℕ → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
166165imp 395 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
167166ad2antrr 717 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
168167impcom 396 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → 𝑧 ∉ ℙ)
169168a1d 25 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
170169ex 401 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
171 neleq1 3045 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑧 → (𝑠 ∉ ℙ ↔ 𝑧 ∉ ℙ))
172171rspcv 3458 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → (∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ → 𝑧 ∉ ℙ))
173172adantld 484 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → ((((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ) → 𝑧 ∉ ℙ))
174173adantld 484 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
175174a1d 25 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
176170, 175jaoi 883 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
177176com12 32 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
17850, 177syldc 48 . . . . . . . . . . . . . 14 (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
17942, 178jaoi 883 . . . . . . . . . . . . 13 ((𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
180179com12 32 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
18137, 180syld 47 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
182181com23 86 . . . . . . . . . 10 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → 𝑧 ∉ ℙ)))
183182imp31 408 . . . . . . . . 9 ((((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → 𝑧 ∉ ℙ)
184183ralrimiva 3113 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)
18526, 27, 1843jca 1158 . . . . . . 7 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
186185ex 401 . . . . . 6 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
187186reximdva 3163 . . . . 5 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
188187reximdva 3163 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
18925, 188syl5bir 234 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
19018, 24, 189mp2and 690 . 2 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
1915, 190mpdan 678 1 (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wnel 3040  wral 3055  wrex 3056  Vcvv 3350  [wsbc 3598  csb 3693   class class class wbr 4811  wf 6066  cfv 6070  (class class class)co 6844  𝑚 cmap 8062  cc 10189  cr 10190  0cc0 10191  1c1 10192   + caddc 10194   < clt 10330  cle 10331  cmin 10522  cn 11276  2c2 11329  3c3 11330  cz 11626  cuz 11889  +crp 12031  ...cfz 12536  ..^cfzo 12676   gcd cgcd 15500  cprime 15668
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-map 8064  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-sup 8557  df-inf 8558  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-n0 11541  df-z 11627  df-uz 11890  df-rp 12032  df-fz 12537  df-fzo 12677  df-seq 13012  df-exp 13071  df-fac 13268  df-cj 14127  df-re 14128  df-im 14129  df-sqrt 14263  df-abs 14264  df-dvds 15269  df-gcd 15501  df-prm 15669
This theorem is referenced by:  prmgaplem8  16044
  Copyright terms: Public domain W3C validator