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