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

Theorem prmgaplem7 15963
Description: Lemma for prmgap 15965. (Contributed by AV, 12-Aug-2020.)
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 8045 . . . 4 (𝐹 ∈ (ℕ ↑𝑚 ℕ) → 𝐹:ℕ⟶ℕ)
31, 2syl 17 . . 3 (𝜑𝐹:ℕ⟶ℕ)
4 prmgaplem7.n . . 3 (𝜑𝑁 ∈ ℕ)
53, 4ffvelrnd 6523 . 2 (𝜑 → (𝐹𝑁) ∈ ℕ)
6 simpr 479 . . . . . . 7 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℕ)
7 elnnuz 11917 . . . . . . 7 ((𝐹𝑁) ∈ ℕ ↔ (𝐹𝑁) ∈ (ℤ‘1))
86, 7sylib 208 . . . . . 6 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ (ℤ‘1))
9 1z 11599 . . . . . . 7 1 ∈ ℤ
10 2z 11601 . . . . . . 7 2 ∈ ℤ
119, 10eluzaddi 11906 . . . . . 6 ((𝐹𝑁) ∈ (ℤ‘1) → ((𝐹𝑁) + 2) ∈ (ℤ‘(1 + 2)))
128, 11syl 17 . . . . 5 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ (ℤ‘(1 + 2)))
13 1p2e3 11344 . . . . . . 7 (1 + 2) = 3
1413eqcomi 2769 . . . . . 6 3 = (1 + 2)
1514fveq2i 6355 . . . . 5 (ℤ‘3) = (ℤ‘(1 + 2))
1612, 15syl6eleqr 2850 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ (ℤ‘3))
17 prmgaplem5 15961 . . . 4 (((𝐹𝑁) + 2) ∈ (ℤ‘3) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ))
1816, 17syl 17 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ))
194anim1i 593 . . . . . 6 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑁 ∈ ℕ ∧ (𝐹𝑁) ∈ ℕ))
2019ancomd 466 . . . . 5 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ))
21 nnaddcl 11234 . . . . 5 (((𝐹𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℕ)
2220, 21syl 17 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℕ)
23 prmgaplem6 15962 . . . 4 (((𝐹𝑁) + 𝑁) ∈ ℕ → ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
2422, 23syl 17 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
25 reeanv 3245 . . . 4 (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) ↔ (∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)))
26 simprll 821 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → 𝑝 < ((𝐹𝑁) + 2))
27 simprrl 823 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ((𝐹𝑁) + 𝑁) < 𝑞)
28 nnz 11591 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℤ)
2928adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℤ)
3010a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 2 ∈ ℤ)
3129, 30zaddcld 11678 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ ℤ)
3231ad2antrr 764 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝐹𝑁) + 2) ∈ ℤ)
3332anim1i 593 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)))
3433ancomd 466 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹𝑁) + 2) ∈ ℤ))
35 fzospliti 12694 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹𝑁) + 2) ∈ ℤ) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
3634, 35syl 17 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
3736ex 449 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞))))
38 neleq1 3040 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑧 → (𝑟 ∉ ℙ ↔ 𝑧 ∉ ℙ))
3938rspcv 3445 . . . . . . . . . . . . . . . . 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 11673 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℤ)
4443peano2zd 11677 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ)
4544ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ)
4645anim1i 593 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → ((((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
4746ancomd 466 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ))
48 fzospliti 12694 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)))
4947, 48syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)))
5049ex 449 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞))))
51 prmgaplem7.i . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖))
524nnzd 11673 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ ℤ)
5352adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 𝑁 ∈ ℤ)
54 fzshftral 12621 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐹𝑁) ∈ ℤ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖)))
5530, 53, 29, 54syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖)))
56 2cnd 11285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → 2 ∈ ℂ)
57 nncn 11220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℂ)
58 addcom 10414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℂ ∧ (𝐹𝑁) ∈ ℂ) → (2 + (𝐹𝑁)) = ((𝐹𝑁) + 2))
5956, 57, 58syl2an 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (2 + (𝐹𝑁)) = ((𝐹𝑁) + 2))
604nncnd 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℂ)
61 addcom 10414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℂ ∧ (𝐹𝑁) ∈ ℂ) → (𝑁 + (𝐹𝑁)) = ((𝐹𝑁) + 𝑁))
6260, 57, 61syl2an 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑁 + (𝐹𝑁)) = ((𝐹𝑁) + 𝑁))
6359, 62oveq12d 6831 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁))) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
64 ovex 6841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 − (𝐹𝑁)) ∈ V
65 sbcbr2g 4862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 − (𝐹𝑁)) ∈ V → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖)))
6664, 65mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖)))
67 csbov12g 6852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
6864, 67mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
69 csbov2g 6854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
7064, 69mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
71 csbvarg 4146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖𝑖 = (𝑗 − (𝐹𝑁)))
7271oveq2d 6829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 − (𝐹𝑁)) ∈ V → ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7364, 72mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7470, 73eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7564, 71mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖𝑖 = (𝑗 − (𝐹𝑁)))
7674, 75oveq12d 6831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))))
7768, 76eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))))
7877breq2d 4816 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
7966, 78bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
8063, 79raleqbidv 3291 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
81 fzval3 12731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) + 𝑁) ∈ ℤ → (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)) = (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)))
8281eqcomd 2766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐹𝑁) + 𝑁) ∈ ℤ → (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
8343, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
8483eleq2d 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ↔ 𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))))
8584biimpa 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
86 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 𝑧 → (𝑗 − (𝐹𝑁)) = (𝑧 − (𝐹𝑁)))
8786oveq2d 6829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 𝑧 → ((𝐹𝑁) + (𝑗 − (𝐹𝑁))) = ((𝐹𝑁) + (𝑧 − (𝐹𝑁))))
8887, 86oveq12d 6831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑧 → (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) = (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))))
8988breq2d 4816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑧 → (1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) ↔ 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
9089rspcv 3445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
9185, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
9257adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℂ)
93 elfzoelz 12664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℤ)
9493zcnd 11675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℂ)
95 pncan3 10481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝐹𝑁) + (𝑧 − (𝐹𝑁))) = 𝑧)
9692, 94, 95syl2an 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → ((𝐹𝑁) + (𝑧 − (𝐹𝑁))) = 𝑧)
9796oveq1d 6828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) = (𝑧 gcd (𝑧 − (𝐹𝑁))))
9893adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℤ)
99 zsubcl 11611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ ℤ ∧ (𝐹𝑁) ∈ ℤ) → (𝑧 − (𝐹𝑁)) ∈ ℤ)
10093, 29, 99syl2anr 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) ∈ ℤ)
101 gcdcom 15437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑧 ∈ ℤ ∧ (𝑧 − (𝐹𝑁)) ∈ ℤ) → (𝑧 gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
10298, 100, 101syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
10397, 102eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
104103breq2d 4816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) ↔ 1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧)))
105 elfzo2 12667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ↔ (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)))
106 eluz2 11885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ↔ (((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧))
107 2pos 11304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 0 < 2
108107a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < 2)
109 2re 11282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 2 ∈ ℝ
110109a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑧 ∈ ℤ → 2 ∈ ℝ)
111 nnre 11219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℝ)
112111adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℝ)
113 ltaddpos 10710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((2 ∈ ℝ ∧ (𝐹𝑁) ∈ ℝ) → (0 < 2 ↔ (𝐹𝑁) < ((𝐹𝑁) + 2)))
114110, 112, 113syl2an 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (0 < 2 ↔ (𝐹𝑁) < ((𝐹𝑁) + 2)))
115108, 114mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (𝐹𝑁) < ((𝐹𝑁) + 2))
116111ad2antll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (𝐹𝑁) ∈ ℝ)
117109a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐹𝑁) ∈ ℕ → 2 ∈ ℝ)
118111, 117readdcld 10261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐹𝑁) ∈ ℕ → ((𝐹𝑁) + 2) ∈ ℝ)
119118ad2antll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → ((𝐹𝑁) + 2) ∈ ℝ)
120 zre 11573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
121120adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 𝑧 ∈ ℝ)
122 ltletr 10321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝐹𝑁) ∈ ℝ ∧ ((𝐹𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐹𝑁) < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → (𝐹𝑁) < 𝑧))
123116, 119, 121, 122syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → (𝐹𝑁) < 𝑧))
124115, 123mpand 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) + 2) ≤ 𝑧 → (𝐹𝑁) < 𝑧))
125124impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
1261253adant1 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
127106, 126sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
1281273ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
129105, 128sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
130129impcom 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝐹𝑁) < 𝑧)
13193zred 11674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℝ)
132 posdif 10713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹𝑁))))
133112, 131, 132syl2an 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → ((𝐹𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹𝑁))))
134130, 133mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < (𝑧 − (𝐹𝑁)))
135 elnnz 11579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 − (𝐹𝑁)) ∈ ℕ ↔ ((𝑧 − (𝐹𝑁)) ∈ ℤ ∧ 0 < (𝑧 − (𝐹𝑁))))
136100, 134, 135sylanbrc 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) ∈ ℕ)
137109a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 2 ∈ ℝ)
138 nngt0 11241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐹𝑁) ∈ ℕ → 0 < (𝐹𝑁))
139138ad2antll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < (𝐹𝑁))
140116, 137, 139, 108addgt0d 10794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < ((𝐹𝑁) + 2))
141 0red 10233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 ∈ ℝ)
142 ltletr 10321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((0 ∈ ℝ ∧ ((𝐹𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((0 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
143141, 119, 121, 142syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → ((0 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
144140, 143mpand 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) + 2) ≤ 𝑧 → 0 < 𝑧))
145144impancom 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
1461453adant1 1125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
147106, 146sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
1481473ad2ant1 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
149105, 148sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
150149impcom 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < 𝑧)
151 elnnz 11579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 ∈ ℕ ↔ (𝑧 ∈ ℤ ∧ 0 < 𝑧))
15298, 150, 151sylanbrc 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℕ)
153138adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < (𝐹𝑁))
154153adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < (𝐹𝑁))
155 ltsubpos 10712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐹𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 < (𝐹𝑁) ↔ (𝑧 − (𝐹𝑁)) < 𝑧))
156112, 131, 155syl2an 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (0 < (𝐹𝑁) ↔ (𝑧 − (𝐹𝑁)) < 𝑧))
157154, 156mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) < 𝑧)
158 ncoprmlnprm 15638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑧 − (𝐹𝑁)) ∈ ℕ ∧ 𝑧 ∈ ℕ ∧ (𝑧 − (𝐹𝑁)) < 𝑧) → (1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
159136, 152, 157, 158syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
160104, 159sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) → 𝑧 ∉ ℙ))
16191, 160syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 𝑧 ∉ ℙ))
162161ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 𝑧 ∉ ℙ)))
163162com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
16480, 163sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
16555, 164sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
166165ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐹𝑁) ∈ ℕ → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))))
16751, 166mpid 44 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐹𝑁) ∈ ℕ → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
168167imp 444 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
169168ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
170169impcom 445 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → 𝑧 ∉ ℙ)
171170a1d 25 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
172171ex 449 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
173 neleq1 3040 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑧 → (𝑠 ∉ ℙ ↔ 𝑧 ∉ ℙ))
174173rspcv 3445 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → (∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ → 𝑧 ∉ ℙ))
175174adantld 484 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → ((((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ) → 𝑧 ∉ ℙ))
176175adantld 484 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
177176a1d 25 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
178172, 177jaoi 393 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
179178com12 32 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
18050, 179syldc 48 . . . . . . . . . . . . . 14 (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
18142, 180jaoi 393 . . . . . . . . . . . . 13 ((𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
182181com12 32 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
18337, 182syld 47 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
184183com23 86 . . . . . . . . . 10 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → 𝑧 ∉ ℙ)))
185184imp31 447 . . . . . . . . 9 ((((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → 𝑧 ∉ ℙ)
186185ralrimiva 3104 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)
18726, 27, 1863jca 1123 . . . . . . 7 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
188187ex 449 . . . . . 6 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
189188reximdva 3155 . . . . 5 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
190189reximdva 3155 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
19125, 190syl5bir 233 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
19218, 24, 191mp2and 717 . 2 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
1935, 192mpdan 705 1 (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wcel 2139  wnel 3035  wral 3050  wrex 3051  Vcvv 3340  [wsbc 3576  csb 3674   class class class wbr 4804  wf 6045  cfv 6049  (class class class)co 6813  𝑚 cmap 8023  cc 10126  cr 10127  0cc0 10128  1c1 10129   + caddc 10131   < clt 10266  cle 10267  cmin 10458  cn 11212  2c2 11262  3c3 11263  cz 11569  cuz 11879  ...cfz 12519  ..^cfzo 12659   gcd cgcd 15418  cprime 15587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-inf 8514  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-z 11570  df-uz 11880  df-rp 12026  df-fz 12520  df-fzo 12660  df-seq 12996  df-exp 13055  df-fac 13255  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-dvds 15183  df-gcd 15419  df-prm 15588
This theorem is referenced by:  prmgaplem8  15964
  Copyright terms: Public domain W3C validator