Metamath Proof Explorer

Theorem prmgaplem7

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

Ref Expression
Hypotheses prmgaplem7.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
prmgaplem7.f ⊢ ( 𝜑 → 𝐹 ∈ ( ℕ ↑m ℕ ) )
prmgaplem7.i ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 2 ... 𝑁 ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) )
Assertion prmgaplem7 ( 𝜑 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )

Proof

Step Hyp Ref Expression
1 prmgaplem7.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 prmgaplem7.f ⊢ ( 𝜑 → 𝐹 ∈ ( ℕ ↑m ℕ ) )
3 prmgaplem7.i ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 2 ... 𝑁 ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) )
4 elmapi ⊢ ( 𝐹 ∈ ( ℕ ↑m ℕ ) → 𝐹 : ℕ ⟶ ℕ )
5 2 4 syl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℕ )
6 5 1 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℕ )
7 simpr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℕ )
8 elnnuz ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ ↔ ( 𝐹 ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
9 7 8 sylib ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) )
10 2z ⊢ 2 ∈ ℤ
11 10 eluzaddi ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ( ℤ≥ ‘ ( 1 + 2 ) ) )
12 9 11 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ( ℤ≥ ‘ ( 1 + 2 ) ) )
13 1p2e3 ⊢ ( 1 + 2 ) = 3
14 13 eqcomi ⊢ 3 = ( 1 + 2 )
15 14 fveq2i ⊢ ( ℤ≥ ‘ 3 ) = ( ℤ≥ ‘ ( 1 + 2 ) )
16 12 15 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ( ℤ≥ ‘ 3 ) )
17 prmgaplem5 ⊢ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) )
18 16 17 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ∃ 𝑝 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) )
19 1 anim1ci ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
20 nnaddcl ⊢ ( ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ∈ ℕ )
21 19 20 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ∈ ℕ )
22 prmgaplem6 ⊢ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ∈ ℕ → ∃ 𝑞 ∈ ℙ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) )
23 21 22 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ∃ 𝑞 ∈ ℙ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) )
24 reeanv ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) ↔ ( ∃ 𝑝 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ∃ 𝑞 ∈ ℙ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) )
25 simprll ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) ) → 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) )
26 simprrl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) ) → ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 )
27 nnz ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ → ( 𝐹 ‘ 𝑁 ) ∈ ℤ )
28 27 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℤ )
29 10 a1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → 2 ∈ ℤ )
30 28 29 zaddcld ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℤ )
31 30 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℤ )
32 31 anim1ci ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) ) → ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℤ ) )
33 fzospliti ⊢ ( ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℤ ) → ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) ∨ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) ) )
34 32 33 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) ) → ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) ∨ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) ) )
35 34 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) → ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) ∨ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) ) ) )
36 neleq1 ⊢ ( 𝑟 = 𝑧 → ( 𝑟 ∉ ℙ ↔ 𝑧 ∉ ℙ ) )
37 36 rspcv ⊢ ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) → ( ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ → 𝑧 ∉ ℙ ) )
38 37 adantld ⊢ ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) → ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) → 𝑧 ∉ ℙ ) )
39 38 adantrd ⊢ ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) )
40 39 a1d ⊢ ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) → ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) ) )
41 21 nnzd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ∈ ℤ )
42 41 peano2zd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ∈ ℤ )
43 42 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ∈ ℤ )
44 43 anim1ci ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ∈ ℤ ) )
45 fzospliti ⊢ ( ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ∈ ℤ ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ∨ 𝑧 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) ) )
46 44 45 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ∨ 𝑧 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) ) )
47 46 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ∨ 𝑧 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) ) ) )
48 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
49 fzshftral ⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℤ ) → ( ∀ 𝑖 ∈ ( 2 ... 𝑁 ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ↔ ∀ 𝑗 ∈ ( ( 2 + ( 𝐹 ‘ 𝑁 ) ) ... ( 𝑁 + ( 𝐹 ‘ 𝑁 ) ) ) [ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ] 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ) )
50 10 48 27 49 mp3an3an ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ∀ 𝑖 ∈ ( 2 ... 𝑁 ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ↔ ∀ 𝑗 ∈ ( ( 2 + ( 𝐹 ‘ 𝑁 ) ) ... ( 𝑁 + ( 𝐹 ‘ 𝑁 ) ) ) [ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ] 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ) )
51 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
52 nncn ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
53 addcom ⊢ ( ( 2 ∈ ℂ ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℂ ) → ( 2 + ( 𝐹 ‘ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑁 ) + 2 ) )
54 51 52 53 syl2an ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 2 + ( 𝐹 ‘ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑁 ) + 2 ) )
55 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
56 addcom ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℂ ) → ( 𝑁 + ( 𝐹 ‘ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) )
57 55 52 56 syl2an ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝑁 + ( 𝐹 ‘ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) )
58 54 57 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( 2 + ( 𝐹 ‘ 𝑁 ) ) ... ( 𝑁 + ( 𝐹 ‘ 𝑁 ) ) ) = ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) )
59 ovex ⊢ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ∈ V
60 sbcbr2g ⊢ ( ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ∈ V → ( [ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ] 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ↔ 1 < ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ) )
61 59 60 mp1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( [ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ] 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ↔ 1 < ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ) )
62 csbov12g ⊢ ( ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ∈ V → ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) = ( ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ 𝑖 ) )
63 59 62 mp1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) = ( ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ 𝑖 ) )
64 csbov2g ⊢ ( ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ∈ V → ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) = ( ( 𝐹 ‘ 𝑁 ) + ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ 𝑖 ) )
65 59 64 mp1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) = ( ( 𝐹 ‘ 𝑁 ) + ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ 𝑖 ) )
66 csbvarg ⊢ ( ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ∈ V → ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ 𝑖 = ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) )
67 66 oveq2d ⊢ ( ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ∈ V → ( ( 𝐹 ‘ 𝑁 ) + ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ 𝑖 ) = ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) )
68 59 67 mp1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( 𝐹 ‘ 𝑁 ) + ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ 𝑖 ) = ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) )
69 65 68 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) = ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) )
70 59 66 mp1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ 𝑖 = ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) )
71 69 70 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ 𝑖 ) = ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) )
72 63 71 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) = ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) )
73 72 breq2d ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 1 < ⦋ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ⦌ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ↔ 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) ) )
74 61 73 bitrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( [ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ] 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ↔ 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) ) )
75 58 74 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ∀ 𝑗 ∈ ( ( 2 + ( 𝐹 ‘ 𝑁 ) ) ... ( 𝑁 + ( 𝐹 ‘ 𝑁 ) ) ) [ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ] 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) ↔ ∀ 𝑗 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) ) )
76 fzval3 ⊢ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ∈ ℤ → ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) = ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) )
77 76 eqcomd ⊢ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ∈ ℤ → ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) = ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) )
78 41 77 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) = ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) )
79 78 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ↔ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) ) )
80 79 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) )
81 oveq1 ⊢ ( 𝑗 = 𝑧 → ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) = ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) )
82 81 oveq2d ⊢ ( 𝑗 = 𝑧 → ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) = ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) )
83 82 81 oveq12d ⊢ ( 𝑗 = 𝑧 → ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) = ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) )
84 83 breq2d ⊢ ( 𝑗 = 𝑧 → ( 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) ↔ 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) ) )
85 84 rspcv ⊢ ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) → ( ∀ 𝑗 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) → 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) ) )
86 80 85 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( ∀ 𝑗 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) → 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) ) )
87 52 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
88 elfzoelz ⊢ ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∈ ℤ )
89 88 zcnd ⊢ ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∈ ℂ )
90 pncan3 ⊢ ( ( ( 𝐹 ‘ 𝑁 ) ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) = 𝑧 )
91 87 89 90 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) = 𝑧 )
92 91 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) = ( 𝑧 gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) )
93 88 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → 𝑧 ∈ ℤ )
94 zsubcl ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℤ ) → ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ∈ ℤ )
95 88 28 94 syl2anr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ∈ ℤ )
96 93 95 gcdcomd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( 𝑧 gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) = ( ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) gcd 𝑧 ) )
97 92 96 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) = ( ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) gcd 𝑧 ) )
98 97 breq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) ↔ 1 < ( ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) gcd 𝑧 ) ) )
99 elfzo2 ⊢ ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ↔ ( 𝑧 ∈ ( ℤ≥ ‘ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ∈ ℤ ∧ 𝑧 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) )
100 eluz2 ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) ↔ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 ) )
101 nnre ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
102 101 ad2antll ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
103 2rp ⊢ 2 ∈ ℝ+
104 103 a1i ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → 2 ∈ ℝ+ )
105 102 104 ltaddrpd ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → ( 𝐹 ‘ 𝑁 ) < ( ( 𝐹 ‘ 𝑁 ) + 2 ) )
106 2re ⊢ 2 ∈ ℝ
107 106 a1i ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ → 2 ∈ ℝ )
108 101 107 readdcld ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ → ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℝ )
109 108 ad2antll ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℝ )
110 zre ⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
111 110 adantr ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → 𝑧 ∈ ℝ )
112 ltletr ⊢ ( ( ( 𝐹 ‘ 𝑁 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑁 ) < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 ) → ( 𝐹 ‘ 𝑁 ) < 𝑧 ) )
113 102 109 111 112 syl3anc ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → ( ( ( 𝐹 ‘ 𝑁 ) < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 ) → ( 𝐹 ‘ 𝑁 ) < 𝑧 ) )
114 105 113 mpand ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 → ( 𝐹 ‘ 𝑁 ) < 𝑧 ) )
115 114 impancom ⊢ ( ( 𝑧 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) < 𝑧 ) )
116 115 3adant1 ⊢ ( ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) < 𝑧 ) )
117 100 116 sylbi ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) < 𝑧 ) )
118 117 3ad2ant1 ⊢ ( ( 𝑧 ∈ ( ℤ≥ ‘ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ∈ ℤ ∧ 𝑧 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) < 𝑧 ) )
119 99 118 sylbi ⊢ ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) < 𝑧 ) )
120 119 impcom ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( 𝐹 ‘ 𝑁 ) < 𝑧 )
121 101 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
122 88 zred ⊢ ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∈ ℝ )
123 posdif ⊢ ( ( ( 𝐹 ‘ 𝑁 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑁 ) < 𝑧 ↔ 0 < ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) )
124 121 122 123 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( ( 𝐹 ‘ 𝑁 ) < 𝑧 ↔ 0 < ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) )
125 120 124 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → 0 < ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) )
126 elnnz ⊢ ( ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ∈ ℕ ↔ ( ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ∈ ℤ ∧ 0 < ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) )
127 95 125 126 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ∈ ℕ )
128 106 a1i ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → 2 ∈ ℝ )
129 nngt0 ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ → 0 < ( 𝐹 ‘ 𝑁 ) )
130 129 ad2antll ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → 0 < ( 𝐹 ‘ 𝑁 ) )
131 2pos ⊢ 0 < 2
132 131 a1i ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → 0 < 2 )
133 102 128 130 132 addgt0d ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → 0 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) )
134 0red ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → 0 ∈ ℝ )
135 ltletr ⊢ ( ( 0 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 0 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 ) → 0 < 𝑧 ) )
136 134 109 111 135 syl3anc ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → ( ( 0 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 ) → 0 < 𝑧 ) )
137 133 136 mpand ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ) → ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 → 0 < 𝑧 ) )
138 137 impancom ⊢ ( ( 𝑧 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → 0 < 𝑧 ) )
139 138 3adant1 ⊢ ( ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ≤ 𝑧 ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → 0 < 𝑧 ) )
140 100 139 sylbi ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → 0 < 𝑧 ) )
141 140 3ad2ant1 ⊢ ( ( 𝑧 ∈ ( ℤ≥ ‘ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ∈ ℤ ∧ 𝑧 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → 0 < 𝑧 ) )
142 99 141 sylbi ⊢ ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → 0 < 𝑧 ) )
143 142 impcom ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → 0 < 𝑧 )
144 elnnz ⊢ ( 𝑧 ∈ ℕ ↔ ( 𝑧 ∈ ℤ ∧ 0 < 𝑧 ) )
145 93 143 144 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → 𝑧 ∈ ℕ )
146 129 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → 0 < ( 𝐹 ‘ 𝑁 ) )
147 146 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → 0 < ( 𝐹 ‘ 𝑁 ) )
148 ltsubpos ⊢ ( ( ( 𝐹 ‘ 𝑁 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 0 < ( 𝐹 ‘ 𝑁 ) ↔ ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) < 𝑧 ) )
149 121 122 148 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( 0 < ( 𝐹 ‘ 𝑁 ) ↔ ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) < 𝑧 ) )
150 147 149 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) < 𝑧 )
151 ncoprmlnprm ⊢ ( ( ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ∈ ℕ ∧ 𝑧 ∈ ℕ ∧ ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) < 𝑧 ) → ( 1 < ( ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) gcd 𝑧 ) → 𝑧 ∉ ℙ ) )
152 127 145 150 151 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( 1 < ( ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) gcd 𝑧 ) → 𝑧 ∉ ℙ ) )
153 98 152 sylbid ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑧 − ( 𝐹 ‘ 𝑁 ) ) ) → 𝑧 ∉ ℙ ) )
154 86 153 syld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ) → ( ∀ 𝑗 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) → 𝑧 ∉ ℙ ) )
155 154 ex ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → ( ∀ 𝑗 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) → 𝑧 ∉ ℙ ) ) )
156 155 com23 ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ∀ 𝑗 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ... ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) gcd ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∉ ℙ ) ) )
157 75 156 sylbid ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ∀ 𝑗 ∈ ( ( 2 + ( 𝐹 ‘ 𝑁 ) ) ... ( 𝑁 + ( 𝐹 ‘ 𝑁 ) ) ) [ ( 𝑗 − ( 𝐹 ‘ 𝑁 ) ) / 𝑖 ] 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∉ ℙ ) ) )
158 50 157 sylbid ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ∀ 𝑖 ∈ ( 2 ... 𝑁 ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∉ ℙ ) ) )
159 158 ex ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ → ( ∀ 𝑖 ∈ ( 2 ... 𝑁 ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∉ ℙ ) ) ) )
160 3 159 mpid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) ∈ ℕ → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∉ ℙ ) ) )
161 160 imp ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∉ ℙ ) )
162 161 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → 𝑧 ∉ ℙ ) )
163 162 impcom ⊢ ( ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ∧ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → 𝑧 ∉ ℙ )
164 163 a1d ⊢ ( ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ∧ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) )
165 164 ex ⊢ ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) → ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) ) )
166 neleq1 ⊢ ( 𝑠 = 𝑧 → ( 𝑠 ∉ ℙ ↔ 𝑧 ∉ ℙ ) )
167 166 rspcv ⊢ ( 𝑧 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) → ( ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ → 𝑧 ∉ ℙ ) )
168 167 adantld ⊢ ( 𝑧 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) → ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) → 𝑧 ∉ ℙ ) )
169 168 adantld ⊢ ( 𝑧 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) )
170 169 a1d ⊢ ( 𝑧 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) → ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) ) )
171 165 170 jaoi ⊢ ( ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ∨ 𝑧 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) ) → ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) ) )
172 171 com12 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ) ∨ 𝑧 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) ) )
173 47 172 syldc ⊢ ( 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) → ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) ) )
174 40 173 jaoi ⊢ ( ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) ∨ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) ) → ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) ) )
175 174 com12 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) ∨ 𝑧 ∈ ( ( ( 𝐹 ‘ 𝑁 ) + 2 ) ..^ 𝑞 ) ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) ) )
176 35 175 syld ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → 𝑧 ∉ ℙ ) ) )
177 176 com23 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → ( 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) → 𝑧 ∉ ℙ ) ) )
178 177 imp31 ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) ) ∧ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) ) → 𝑧 ∉ ℙ )
179 178 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) ) → ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ )
180 25 26 179 3jca ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) ) → ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )
181 180 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) ) )
182 181 reximdva ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) → ( ∃ 𝑞 ∈ ℙ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → ∃ 𝑞 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) ) )
183 182 reximdva ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) ) )
184 24 183 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ( ( ∃ 𝑝 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ∀ 𝑟 ∈ ( ( 𝑝 + 1 ) ..^ ( ( 𝐹 ‘ 𝑁 ) + 2 ) ) 𝑟 ∉ ℙ ) ∧ ∃ 𝑞 ∈ ℙ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑠 ∈ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ..^ 𝑞 ) 𝑠 ∉ ℙ ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) ) )
185 18 23 184 mp2and ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )
186 6 185 mpdan ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )