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

Theorem prmgaplem7 15696
 Description: Lemma for prmgap 15698. (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 7831 . . . 4 (𝐹 ∈ (ℕ ↑𝑚 ℕ) → 𝐹:ℕ⟶ℕ)
31, 2syl 17 . . 3 (𝜑𝐹:ℕ⟶ℕ)
4 prmgaplem7.n . . 3 (𝜑𝑁 ∈ ℕ)
53, 4ffvelrnd 6321 . 2 (𝜑 → (𝐹𝑁) ∈ ℕ)
6 simpr 477 . . . . . . 7 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℕ)
7 elnnuz 11676 . . . . . . 7 ((𝐹𝑁) ∈ ℕ ↔ (𝐹𝑁) ∈ (ℤ‘1))
86, 7sylib 208 . . . . . 6 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ (ℤ‘1))
9 1z 11359 . . . . . . 7 1 ∈ ℤ
10 2z 11361 . . . . . . 7 2 ∈ ℤ
119, 10eluzaddi 11666 . . . . . 6 ((𝐹𝑁) ∈ (ℤ‘1) → ((𝐹𝑁) + 2) ∈ (ℤ‘(1 + 2)))
128, 11syl 17 . . . . 5 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ (ℤ‘(1 + 2)))
13 1p2e3 11104 . . . . . . 7 (1 + 2) = 3
1413eqcomi 2630 . . . . . 6 3 = (1 + 2)
1514fveq2i 6156 . . . . 5 (ℤ‘3) = (ℤ‘(1 + 2))
1612, 15syl6eleqr 2709 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ (ℤ‘3))
17 prmgaplem5 15694 . . . 4 (((𝐹𝑁) + 2) ∈ (ℤ‘3) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ))
1816, 17syl 17 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ))
194anim1i 591 . . . . . 6 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑁 ∈ ℕ ∧ (𝐹𝑁) ∈ ℕ))
2019ancomd 467 . . . . 5 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ))
21 nnaddcl 10994 . . . . 5 (((𝐹𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℕ)
2220, 21syl 17 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℕ)
23 prmgaplem6 15695 . . . 4 (((𝐹𝑁) + 𝑁) ∈ ℕ → ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
2422, 23syl 17 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))
25 reeanv 3100 . . . 4 (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) ↔ (∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)))
26 simprll 801 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → 𝑝 < ((𝐹𝑁) + 2))
27 simprrl 803 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ((𝐹𝑁) + 𝑁) < 𝑞)
28 nnz 11351 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℤ)
2928adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℤ)
3010a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 2 ∈ ℤ)
3129, 30zaddcld 11438 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 2) ∈ ℤ)
3231ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝐹𝑁) + 2) ∈ ℤ)
3332anim1i 591 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)))
3433ancomd 467 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹𝑁) + 2) ∈ ℤ))
35 fzospliti 12449 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹𝑁) + 2) ∈ ℤ) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
3634, 35syl 17 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
3736ex 450 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞))))
38 neleq1 2898 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑧 → (𝑟 ∉ ℙ ↔ 𝑧 ∉ ℙ))
3938rspcv 3294 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → (∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ → 𝑧 ∉ ℙ))
4039adantld 483 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) → 𝑧 ∉ ℙ))
4140adantrd 484 . . . . . . . . . . . . . . 15 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
4241a1d 25 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
4322nnzd 11433 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + 𝑁) ∈ ℤ)
4443peano2zd 11437 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ)
4544ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ)
4645anim1i 591 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → ((((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)))
4746ancomd 467 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ))
48 fzospliti 12449 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)))
4947, 48syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)))
5049ex 450 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^𝑞) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞))))
51 prmgaplem7.i . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖))
524nnzd 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ ℤ)
5352adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 𝑁 ∈ ℤ)
54 fzshftral 12377 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐹𝑁) ∈ ℤ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖)))
5530, 53, 29, 54syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖)))
56 2cnd 11045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → 2 ∈ ℂ)
57 nncn 10980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℂ)
58 addcom 10174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℂ ∧ (𝐹𝑁) ∈ ℂ) → (2 + (𝐹𝑁)) = ((𝐹𝑁) + 2))
5956, 57, 58syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (2 + (𝐹𝑁)) = ((𝐹𝑁) + 2))
604nncnd 10988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℂ)
61 addcom 10174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℂ ∧ (𝐹𝑁) ∈ ℂ) → (𝑁 + (𝐹𝑁)) = ((𝐹𝑁) + 𝑁))
6260, 57, 61syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑁 + (𝐹𝑁)) = ((𝐹𝑁) + 𝑁))
6359, 62oveq12d 6628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁))) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
64 ovex 6638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 − (𝐹𝑁)) ∈ V
65 sbcbr2g 4675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 − (𝐹𝑁)) ∈ V → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖)))
6664, 65mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖)))
67 csbov12g 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
6864, 67mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
69 csbov2g 6651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
7064, 69mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖))
71 csbvarg 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 − (𝐹𝑁)) ∈ V → (𝑗 − (𝐹𝑁)) / 𝑖𝑖 = (𝑗 − (𝐹𝑁)))
7271oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 − (𝐹𝑁)) ∈ V → ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7364, 72mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝐹𝑁) + (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7470, 73eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) = ((𝐹𝑁) + (𝑗 − (𝐹𝑁))))
7564, 71mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖𝑖 = (𝑗 − (𝐹𝑁)))
7674, 75oveq12d 6628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((𝑗 − (𝐹𝑁)) / 𝑖((𝐹𝑁) + 𝑖) gcd (𝑗 − (𝐹𝑁)) / 𝑖𝑖) = (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))))
7768, 76eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) = (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))))
7877breq2d 4630 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (1 < (𝑗 − (𝐹𝑁)) / 𝑖(((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
7966, 78bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ([(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
8063, 79raleqbidv 3144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹𝑁))...(𝑁 + (𝐹𝑁)))[(𝑗 − (𝐹𝑁)) / 𝑖]1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁)))))
81 fzval3 12485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) + 𝑁) ∈ ℤ → (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)) = (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)))
8281eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐹𝑁) + 𝑁) ∈ ℤ → (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
8343, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) = (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
8483eleq2d 2684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ↔ 𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))))
8584biimpa 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)))
86 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 𝑧 → (𝑗 − (𝐹𝑁)) = (𝑧 − (𝐹𝑁)))
8786oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 𝑧 → ((𝐹𝑁) + (𝑗 − (𝐹𝑁))) = ((𝐹𝑁) + (𝑧 − (𝐹𝑁))))
8887, 86oveq12d 6628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑧 → (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) = (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))))
8988breq2d 4630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑧 → (1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) ↔ 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
9089rspcv 3294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁)) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
9185, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁)))))
9257adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℂ)
93 elfzoelz 12419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℤ)
9493zcnd 11435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℂ)
95 pncan3 10241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝐹𝑁) + (𝑧 − (𝐹𝑁))) = 𝑧)
9692, 94, 95syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → ((𝐹𝑁) + (𝑧 − (𝐹𝑁))) = 𝑧)
9796oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) = (𝑧 gcd (𝑧 − (𝐹𝑁))))
9893adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℤ)
99 zsubcl 11371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ ℤ ∧ (𝐹𝑁) ∈ ℤ) → (𝑧 − (𝐹𝑁)) ∈ ℤ)
10093, 29, 99syl2anr 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) ∈ ℤ)
101 gcdcom 15170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑧 ∈ ℤ ∧ (𝑧 − (𝐹𝑁)) ∈ ℤ) → (𝑧 gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
10298, 100, 101syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
10397, 102eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) = ((𝑧 − (𝐹𝑁)) gcd 𝑧))
104103breq2d 4630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) ↔ 1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧)))
105 elfzo2 12422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ↔ (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)))
106 eluz2 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ↔ (((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧))
107 2pos 11064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 0 < 2
108107a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < 2)
109 2re 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 2 ∈ ℝ
110109a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑧 ∈ ℤ → 2 ∈ ℝ)
111 nnre 10979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐹𝑁) ∈ ℕ → (𝐹𝑁) ∈ ℝ)
112111adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) ∈ ℝ)
113 ltaddpos 10470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((2 ∈ ℝ ∧ (𝐹𝑁) ∈ ℝ) → (0 < 2 ↔ (𝐹𝑁) < ((𝐹𝑁) + 2)))
114110, 112, 113syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (0 < 2 ↔ (𝐹𝑁) < ((𝐹𝑁) + 2)))
115108, 114mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (𝐹𝑁) < ((𝐹𝑁) + 2))
116111ad2antll 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (𝐹𝑁) ∈ ℝ)
117109a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝐹𝑁) ∈ ℕ → 2 ∈ ℝ)
118111, 117readdcld 10021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐹𝑁) ∈ ℕ → ((𝐹𝑁) + 2) ∈ ℝ)
119118ad2antll 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → ((𝐹𝑁) + 2) ∈ ℝ)
120 zre 11333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
121120adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 𝑧 ∈ ℝ)
122 ltletr 10081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝐹𝑁) ∈ ℝ ∧ ((𝐹𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐹𝑁) < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → (𝐹𝑁) < 𝑧))
123116, 119, 121, 122syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → (𝐹𝑁) < 𝑧))
124115, 123mpand 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) + 2) ≤ 𝑧 → (𝐹𝑁) < 𝑧))
125124impancom 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
1261253adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
127106, 126sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
1281273ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
129105, 128sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝐹𝑁) < 𝑧))
130129impcom 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝐹𝑁) < 𝑧)
13193zred 11434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℝ)
132 posdif 10473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐹𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹𝑁))))
133112, 131, 132syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → ((𝐹𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹𝑁))))
134130, 133mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < (𝑧 − (𝐹𝑁)))
135 elnnz 11339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 − (𝐹𝑁)) ∈ ℕ ↔ ((𝑧 − (𝐹𝑁)) ∈ ℤ ∧ 0 < (𝑧 − (𝐹𝑁))))
136100, 134, 135sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) ∈ ℕ)
137109a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 2 ∈ ℝ)
138 nngt0 11001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐹𝑁) ∈ ℕ → 0 < (𝐹𝑁))
139138ad2antll 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < (𝐹𝑁))
140116, 137, 139, 108addgt0d 10554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 < ((𝐹𝑁) + 2))
141 0red 9993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → 0 ∈ ℝ)
142 ltletr 10081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((0 ∈ ℝ ∧ ((𝐹𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((0 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
143141, 119, 121, 142syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → ((0 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → 0 < 𝑧))
144140, 143mpand 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹𝑁) ∈ ℕ)) → (((𝐹𝑁) + 2) ≤ 𝑧 → 0 < 𝑧))
145144impancom 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
1461453adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝐹𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
147106, 146sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
1481473ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ (ℤ‘((𝐹𝑁) + 2)) ∧ (((𝐹𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
149105, 148sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < 𝑧))
150149impcom 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < 𝑧)
151 elnnz 11339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 ∈ ℕ ↔ (𝑧 ∈ ℤ ∧ 0 < 𝑧))
15298, 150, 151sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℕ)
153138adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → 0 < (𝐹𝑁))
154153adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → 0 < (𝐹𝑁))
155 ltsubpos 10472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐹𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 < (𝐹𝑁) ↔ (𝑧 − (𝐹𝑁)) < 𝑧))
156112, 131, 155syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (0 < (𝐹𝑁) ↔ (𝑧 − (𝐹𝑁)) < 𝑧))
157154, 156mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹𝑁)) < 𝑧)
158 ncoprmlnprm 15371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑧 − (𝐹𝑁)) ∈ ℕ ∧ 𝑧 ∈ ℕ ∧ (𝑧 − (𝐹𝑁)) < 𝑧) → (1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
159136, 152, 157, 158syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < ((𝑧 − (𝐹𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ))
160104, 159sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (1 < (((𝐹𝑁) + (𝑧 − (𝐹𝑁))) gcd (𝑧 − (𝐹𝑁))) → 𝑧 ∉ ℙ))
16191, 160syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹𝑁) + 2)...((𝐹𝑁) + 𝑁))1 < (((𝐹𝑁) + (𝑗 − (𝐹𝑁))) gcd (𝑗 − (𝐹𝑁))) → 𝑧 ∉ ℙ))
162161ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐹𝑁) ∈ ℕ → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))))
16751, 166mpid 44 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐹𝑁) ∈ ℕ → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))
168167imp 445 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
169168ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))
170169impcom 446 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → 𝑧 ∉ ℙ)
171170a1d 25 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
172171ex 450 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (((𝐹𝑁) + 2)..^(((𝐹𝑁) + 𝑁) + 1)) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
173 neleq1 2898 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑧 → (𝑠 ∉ ℙ ↔ 𝑧 ∉ ℙ))
174173rspcv 3294 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → (∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ → 𝑧 ∉ ℙ))
175174adantld 483 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → ((((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ) → 𝑧 ∉ ℙ))
176175adantld 483 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))
177176a1d 25 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞) → ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)))
178172, 177jaoi 394 . . . . . . . . . . . . . . . 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 394 . . . . . . . . . . . . 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 448 . . . . . . . . 9 ((((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → 𝑧 ∉ ℙ)
186185ralrimiva 2961 . . . . . . . 8 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)
18726, 27, 1863jca 1240 . . . . . . 7 (((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
188187ex 450 . . . . . 6 ((((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
189188reximdva 3012 . . . . 5 (((𝜑 ∧ (𝐹𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
190189reximdva 3012 . . . 4 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
19125, 190syl5bir 233 . . 3 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ((∃𝑝 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)))
19218, 24, 191mp2and 714 . 2 ((𝜑 ∧ (𝐹𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
1935, 192mpdan 701 1 (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹𝑁) + 2) ∧ ((𝐹𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ∉ wnel 2893  ∀wral 2907  ∃wrex 2908  Vcvv 3189  [wsbc 3421  ⦋csb 3518   class class class wbr 4618  ⟶wf 5848  ‘cfv 5852  (class class class)co 6610   ↑𝑚 cmap 7809  ℂcc 9886  ℝcr 9887  0cc0 9888  1c1 9889   + caddc 9891   < clt 10026   ≤ cle 10027   − cmin 10218  ℕcn 10972  2c2 11022  3c3 11023  ℤcz 11329  ℤ≥cuz 11639  ...cfz 12276  ..^cfzo 12414   gcd cgcd 15151  ℙcprime 15320 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-sup 8300  df-inf 8301  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-n0 11245  df-z 11330  df-uz 11640  df-rp 11785  df-fz 12277  df-fzo 12415  df-seq 12750  df-exp 12809  df-fac 13009  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-dvds 14919  df-gcd 15152  df-prm 15321 This theorem is referenced by:  prmgaplem8  15697
 Copyright terms: Public domain W3C validator