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