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

Theorem prmgaplem7 16936
Description: Lemma for prmgap 16938. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.)
Hypotheses
Ref Expression
prmgaplem7.n (πœ‘ β†’ 𝑁 ∈ β„•)
prmgaplem7.f (πœ‘ β†’ 𝐹 ∈ (β„• ↑m β„•))
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 (πœ‘ β†’ 𝐹 ∈ (β„• ↑m β„•))
2 elmapi 8794 . . . 4 (𝐹 ∈ (β„• ↑m β„•) β†’ 𝐹:β„•βŸΆβ„•)
31, 2syl 17 . . 3 (πœ‘ β†’ 𝐹:β„•βŸΆβ„•)
4 prmgaplem7.n . . 3 (πœ‘ β†’ 𝑁 ∈ β„•)
53, 4ffvelcdmd 7041 . 2 (πœ‘ β†’ (πΉβ€˜π‘) ∈ β„•)
6 simpr 486 . . . . . . 7 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) ∈ β„•)
7 elnnuz 12814 . . . . . . 7 ((πΉβ€˜π‘) ∈ β„• ↔ (πΉβ€˜π‘) ∈ (β„€β‰₯β€˜1))
86, 7sylib 217 . . . . . 6 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) ∈ (β„€β‰₯β€˜1))
9 2z 12542 . . . . . . 7 2 ∈ β„€
109eluzaddi 12801 . . . . . 6 ((πΉβ€˜π‘) ∈ (β„€β‰₯β€˜1) β†’ ((πΉβ€˜π‘) + 2) ∈ (β„€β‰₯β€˜(1 + 2)))
118, 10syl 17 . . . . 5 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ((πΉβ€˜π‘) + 2) ∈ (β„€β‰₯β€˜(1 + 2)))
12 1p2e3 12303 . . . . . . 7 (1 + 2) = 3
1312eqcomi 2746 . . . . . 6 3 = (1 + 2)
1413fveq2i 6850 . . . . 5 (β„€β‰₯β€˜3) = (β„€β‰₯β€˜(1 + 2))
1511, 14eleqtrrdi 2849 . . . 4 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ((πΉβ€˜π‘) + 2) ∈ (β„€β‰₯β€˜3))
16 prmgaplem5 16934 . . . 4 (((πΉβ€˜π‘) + 2) ∈ (β„€β‰₯β€˜3) β†’ βˆƒπ‘ ∈ β„™ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™))
1715, 16syl 17 . . 3 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ βˆƒπ‘ ∈ β„™ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™))
184anim1ci 617 . . . . 5 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ((πΉβ€˜π‘) ∈ β„• ∧ 𝑁 ∈ β„•))
19 nnaddcl 12183 . . . . 5 (((πΉβ€˜π‘) ∈ β„• ∧ 𝑁 ∈ β„•) β†’ ((πΉβ€˜π‘) + 𝑁) ∈ β„•)
2018, 19syl 17 . . . 4 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ((πΉβ€˜π‘) + 𝑁) ∈ β„•)
21 prmgaplem6 16935 . . . 4 (((πΉβ€˜π‘) + 𝑁) ∈ β„• β†’ βˆƒπ‘ž ∈ β„™ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™))
2220, 21syl 17 . . 3 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ βˆƒπ‘ž ∈ β„™ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™))
23 reeanv 3220 . . . 4 (βˆƒπ‘ ∈ β„™ βˆƒπ‘ž ∈ β„™ ((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) ↔ (βˆƒπ‘ ∈ β„™ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ βˆƒπ‘ž ∈ β„™ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)))
24 simprll 778 . . . . . . . 8 (((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) ∧ ((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™))) β†’ 𝑝 < ((πΉβ€˜π‘) + 2))
25 simprrl 780 . . . . . . . 8 (((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) ∧ ((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™))) β†’ ((πΉβ€˜π‘) + 𝑁) < π‘ž)
26 nnz 12527 . . . . . . . . . . . . . . . . . 18 ((πΉβ€˜π‘) ∈ β„• β†’ (πΉβ€˜π‘) ∈ β„€)
2726adantl 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) ∈ β„€)
289a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ 2 ∈ β„€)
2927, 28zaddcld 12618 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ((πΉβ€˜π‘) + 2) ∈ β„€)
3029ad2antrr 725 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ ((πΉβ€˜π‘) + 2) ∈ β„€)
3130anim1ci 617 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) ∧ 𝑧 ∈ ((𝑝 + 1)..^π‘ž)) β†’ (𝑧 ∈ ((𝑝 + 1)..^π‘ž) ∧ ((πΉβ€˜π‘) + 2) ∈ β„€))
32 fzospliti 13611 . . . . . . . . . . . . . 14 ((𝑧 ∈ ((𝑝 + 1)..^π‘ž) ∧ ((πΉβ€˜π‘) + 2) ∈ β„€) β†’ (𝑧 ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2)) ∨ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž)))
3331, 32syl 17 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) ∧ 𝑧 ∈ ((𝑝 + 1)..^π‘ž)) β†’ (𝑧 ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2)) ∨ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž)))
3433ex 414 . . . . . . . . . . . 12 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (𝑧 ∈ ((𝑝 + 1)..^π‘ž) β†’ (𝑧 ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2)) ∨ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž))))
35 neleq1 3055 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ = 𝑧 β†’ (π‘Ÿ βˆ‰ β„™ ↔ 𝑧 βˆ‰ β„™))
3635rspcv 3580 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2)) β†’ (βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™ β†’ 𝑧 βˆ‰ β„™))
3736adantld 492 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2)) β†’ ((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) β†’ 𝑧 βˆ‰ β„™))
3837adantrd 493 . . . . . . . . . . . . . . 15 (𝑧 ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2)) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™))
3938a1d 25 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2)) β†’ ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™)))
4020nnzd 12533 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ((πΉβ€˜π‘) + 𝑁) ∈ β„€)
4140peano2zd 12617 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (((πΉβ€˜π‘) + 𝑁) + 1) ∈ β„€)
4241ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (((πΉβ€˜π‘) + 𝑁) + 1) ∈ β„€)
4342anim1ci 617 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž)) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž) ∧ (((πΉβ€˜π‘) + 𝑁) + 1) ∈ β„€))
44 fzospliti 13611 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž) ∧ (((πΉβ€˜π‘) + 𝑁) + 1) ∈ β„€) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)))
4543, 44syl 17 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž)) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)))
4645ex 414 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž))))
47 prmgaplem7.i . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆ€π‘– ∈ (2...𝑁)1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖))
484nnzd 12533 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝑁 ∈ β„€)
49 fzshftral 13536 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ (πΉβ€˜π‘) ∈ β„€) β†’ (βˆ€π‘– ∈ (2...𝑁)1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖) ↔ βˆ€π‘— ∈ ((2 + (πΉβ€˜π‘))...(𝑁 + (πΉβ€˜π‘)))[(𝑗 βˆ’ (πΉβ€˜π‘)) / 𝑖]1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖)))
509, 48, 26, 49mp3an3an 1468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (βˆ€π‘– ∈ (2...𝑁)1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖) ↔ βˆ€π‘— ∈ ((2 + (πΉβ€˜π‘))...(𝑁 + (πΉβ€˜π‘)))[(𝑗 βˆ’ (πΉβ€˜π‘)) / 𝑖]1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖)))
51 2cnd 12238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 2 ∈ β„‚)
52 nncn 12168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πΉβ€˜π‘) ∈ β„• β†’ (πΉβ€˜π‘) ∈ β„‚)
53 addcom 11348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ β„‚ ∧ (πΉβ€˜π‘) ∈ β„‚) β†’ (2 + (πΉβ€˜π‘)) = ((πΉβ€˜π‘) + 2))
5451, 52, 53syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (2 + (πΉβ€˜π‘)) = ((πΉβ€˜π‘) + 2))
554nncnd 12176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 𝑁 ∈ β„‚)
56 addcom 11348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ β„‚ ∧ (πΉβ€˜π‘) ∈ β„‚) β†’ (𝑁 + (πΉβ€˜π‘)) = ((πΉβ€˜π‘) + 𝑁))
5755, 52, 56syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (𝑁 + (πΉβ€˜π‘)) = ((πΉβ€˜π‘) + 𝑁))
5854, 57oveq12d 7380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ((2 + (πΉβ€˜π‘))...(𝑁 + (πΉβ€˜π‘))) = (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁)))
59 ovex 7395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 βˆ’ (πΉβ€˜π‘)) ∈ V
60 sbcbr2g 5168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 βˆ’ (πΉβ€˜π‘)) ∈ V β†’ ([(𝑗 βˆ’ (πΉβ€˜π‘)) / 𝑖]1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖) ↔ 1 < ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ(((πΉβ€˜π‘) + 𝑖) gcd 𝑖)))
6159, 60mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ([(𝑗 βˆ’ (πΉβ€˜π‘)) / 𝑖]1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖) ↔ 1 < ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ(((πΉβ€˜π‘) + 𝑖) gcd 𝑖)))
62 csbov12g 7406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 βˆ’ (πΉβ€˜π‘)) ∈ V β†’ ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ(((πΉβ€˜π‘) + 𝑖) gcd 𝑖) = (⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ((πΉβ€˜π‘) + 𝑖) gcd ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œπ‘–))
6359, 62mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ(((πΉβ€˜π‘) + 𝑖) gcd 𝑖) = (⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ((πΉβ€˜π‘) + 𝑖) gcd ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œπ‘–))
64 csbov2g 7408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 βˆ’ (πΉβ€˜π‘)) ∈ V β†’ ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ((πΉβ€˜π‘) + 𝑖) = ((πΉβ€˜π‘) + ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œπ‘–))
6559, 64mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ((πΉβ€˜π‘) + 𝑖) = ((πΉβ€˜π‘) + ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œπ‘–))
66 csbvarg 4396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 βˆ’ (πΉβ€˜π‘)) ∈ V β†’ ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œπ‘– = (𝑗 βˆ’ (πΉβ€˜π‘)))
6766oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 βˆ’ (πΉβ€˜π‘)) ∈ V β†’ ((πΉβ€˜π‘) + ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œπ‘–) = ((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))))
6859, 67mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ((πΉβ€˜π‘) + ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œπ‘–) = ((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))))
6965, 68eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ((πΉβ€˜π‘) + 𝑖) = ((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))))
7059, 66mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œπ‘– = (𝑗 βˆ’ (πΉβ€˜π‘)))
7169, 70oveq12d 7380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ((πΉβ€˜π‘) + 𝑖) gcd ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œπ‘–) = (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘))))
7263, 71eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ(((πΉβ€˜π‘) + 𝑖) gcd 𝑖) = (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘))))
7372breq2d 5122 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (1 < ⦋(𝑗 βˆ’ (πΉβ€˜π‘)) / π‘–β¦Œ(((πΉβ€˜π‘) + 𝑖) gcd 𝑖) ↔ 1 < (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘)))))
7461, 73bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ([(𝑗 βˆ’ (πΉβ€˜π‘)) / 𝑖]1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖) ↔ 1 < (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘)))))
7558, 74raleqbidv 3322 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (βˆ€π‘— ∈ ((2 + (πΉβ€˜π‘))...(𝑁 + (πΉβ€˜π‘)))[(𝑗 βˆ’ (πΉβ€˜π‘)) / 𝑖]1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖) ↔ βˆ€π‘— ∈ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁))1 < (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘)))))
76 fzval3 13648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πΉβ€˜π‘) + 𝑁) ∈ β„€ β†’ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁)) = (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)))
7776eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πΉβ€˜π‘) + 𝑁) ∈ β„€ β†’ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) = (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁)))
7840, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) = (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁)))
7978eleq2d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) ↔ 𝑧 ∈ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁))))
8079biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ 𝑧 ∈ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁)))
81 oveq1 7369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 𝑧 β†’ (𝑗 βˆ’ (πΉβ€˜π‘)) = (𝑧 βˆ’ (πΉβ€˜π‘)))
8281oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 𝑧 β†’ ((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) = ((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))))
8382, 81oveq12d 7380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 𝑧 β†’ (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘))) = (((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) gcd (𝑧 βˆ’ (πΉβ€˜π‘))))
8483breq2d 5122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑗 = 𝑧 β†’ (1 < (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘))) ↔ 1 < (((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) gcd (𝑧 βˆ’ (πΉβ€˜π‘)))))
8584rspcv 3580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 ∈ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁)) β†’ (βˆ€π‘— ∈ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁))1 < (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘))) β†’ 1 < (((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) gcd (𝑧 βˆ’ (πΉβ€˜π‘)))))
8680, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (βˆ€π‘— ∈ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁))1 < (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘))) β†’ 1 < (((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) gcd (𝑧 βˆ’ (πΉβ€˜π‘)))))
8752adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) ∈ β„‚)
88 elfzoelz 13579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 ∈ β„€)
8988zcnd 12615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 ∈ β„‚)
90 pncan3 11416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πΉβ€˜π‘) ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ ((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) = 𝑧)
9187, 89, 90syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ ((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) = 𝑧)
9291oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) gcd (𝑧 βˆ’ (πΉβ€˜π‘))) = (𝑧 gcd (𝑧 βˆ’ (πΉβ€˜π‘))))
9388adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ 𝑧 ∈ β„€)
94 zsubcl 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ β„€ ∧ (πΉβ€˜π‘) ∈ β„€) β†’ (𝑧 βˆ’ (πΉβ€˜π‘)) ∈ β„€)
9588, 27, 94syl2anr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (𝑧 βˆ’ (πΉβ€˜π‘)) ∈ β„€)
9693, 95gcdcomd 16401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (𝑧 gcd (𝑧 βˆ’ (πΉβ€˜π‘))) = ((𝑧 βˆ’ (πΉβ€˜π‘)) gcd 𝑧))
9792, 96eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) gcd (𝑧 βˆ’ (πΉβ€˜π‘))) = ((𝑧 βˆ’ (πΉβ€˜π‘)) gcd 𝑧))
9897breq2d 5122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (1 < (((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) gcd (𝑧 βˆ’ (πΉβ€˜π‘))) ↔ 1 < ((𝑧 βˆ’ (πΉβ€˜π‘)) gcd 𝑧)))
99 elfzo2 13582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) ↔ (𝑧 ∈ (β„€β‰₯β€˜((πΉβ€˜π‘) + 2)) ∧ (((πΉβ€˜π‘) + 𝑁) + 1) ∈ β„€ ∧ 𝑧 < (((πΉβ€˜π‘) + 𝑁) + 1)))
100 eluz2 12776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 ∈ (β„€β‰₯β€˜((πΉβ€˜π‘) + 2)) ↔ (((πΉβ€˜π‘) + 2) ∈ β„€ ∧ 𝑧 ∈ β„€ ∧ ((πΉβ€˜π‘) + 2) ≀ 𝑧))
101 nnre 12167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((πΉβ€˜π‘) ∈ β„• β†’ (πΉβ€˜π‘) ∈ ℝ)
102101ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ (πΉβ€˜π‘) ∈ ℝ)
103 2rp 12927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 2 ∈ ℝ+
104103a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ 2 ∈ ℝ+)
105102, 104ltaddrpd 12997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ (πΉβ€˜π‘) < ((πΉβ€˜π‘) + 2))
106 2re 12234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 2 ∈ ℝ
107106a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((πΉβ€˜π‘) ∈ β„• β†’ 2 ∈ ℝ)
108101, 107readdcld 11191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((πΉβ€˜π‘) ∈ β„• β†’ ((πΉβ€˜π‘) + 2) ∈ ℝ)
109108ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ ((πΉβ€˜π‘) + 2) ∈ ℝ)
110 zre 12510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑧 ∈ β„€ β†’ 𝑧 ∈ ℝ)
111110adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ 𝑧 ∈ ℝ)
112 ltletr 11254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((πΉβ€˜π‘) ∈ ℝ ∧ ((πΉβ€˜π‘) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ (((πΉβ€˜π‘) < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 2) ≀ 𝑧) β†’ (πΉβ€˜π‘) < 𝑧))
113102, 109, 111, 112syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ (((πΉβ€˜π‘) < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 2) ≀ 𝑧) β†’ (πΉβ€˜π‘) < 𝑧))
114105, 113mpand 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ (((πΉβ€˜π‘) + 2) ≀ 𝑧 β†’ (πΉβ€˜π‘) < 𝑧))
115114impancom 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ β„€ ∧ ((πΉβ€˜π‘) + 2) ≀ 𝑧) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) < 𝑧))
1161153adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((πΉβ€˜π‘) + 2) ∈ β„€ ∧ 𝑧 ∈ β„€ ∧ ((πΉβ€˜π‘) + 2) ≀ 𝑧) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) < 𝑧))
117100, 116sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 ∈ (β„€β‰₯β€˜((πΉβ€˜π‘) + 2)) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) < 𝑧))
1181173ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧 ∈ (β„€β‰₯β€˜((πΉβ€˜π‘) + 2)) ∧ (((πΉβ€˜π‘) + 𝑁) + 1) ∈ β„€ ∧ 𝑧 < (((πΉβ€˜π‘) + 𝑁) + 1)) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) < 𝑧))
11999, 118sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) < 𝑧))
120119impcom 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (πΉβ€˜π‘) < 𝑧)
121101adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (πΉβ€˜π‘) ∈ ℝ)
12288zred 12614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 ∈ ℝ)
123 posdif 11655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πΉβ€˜π‘) ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ ((πΉβ€˜π‘) < 𝑧 ↔ 0 < (𝑧 βˆ’ (πΉβ€˜π‘))))
124121, 122, 123syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ ((πΉβ€˜π‘) < 𝑧 ↔ 0 < (𝑧 βˆ’ (πΉβ€˜π‘))))
125120, 124mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ 0 < (𝑧 βˆ’ (πΉβ€˜π‘)))
126 elnnz 12516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 βˆ’ (πΉβ€˜π‘)) ∈ β„• ↔ ((𝑧 βˆ’ (πΉβ€˜π‘)) ∈ β„€ ∧ 0 < (𝑧 βˆ’ (πΉβ€˜π‘))))
12795, 125, 126sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (𝑧 βˆ’ (πΉβ€˜π‘)) ∈ β„•)
128106a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ 2 ∈ ℝ)
129 nngt0 12191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((πΉβ€˜π‘) ∈ β„• β†’ 0 < (πΉβ€˜π‘))
130129ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ 0 < (πΉβ€˜π‘))
131 2pos 12263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 0 < 2
132131a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ 0 < 2)
133102, 128, 130, 132addgt0d 11737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ 0 < ((πΉβ€˜π‘) + 2))
134 0red 11165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ 0 ∈ ℝ)
135 ltletr 11254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((0 ∈ ℝ ∧ ((πΉβ€˜π‘) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ ((0 < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 2) ≀ 𝑧) β†’ 0 < 𝑧))
136134, 109, 111, 135syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ ((0 < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 2) ≀ 𝑧) β†’ 0 < 𝑧))
137133, 136mpand 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑧 ∈ β„€ ∧ (πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•)) β†’ (((πΉβ€˜π‘) + 2) ≀ 𝑧 β†’ 0 < 𝑧))
138137impancom 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑧 ∈ β„€ ∧ ((πΉβ€˜π‘) + 2) ≀ 𝑧) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ 0 < 𝑧))
1391383adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((πΉβ€˜π‘) + 2) ∈ β„€ ∧ 𝑧 ∈ β„€ ∧ ((πΉβ€˜π‘) + 2) ≀ 𝑧) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ 0 < 𝑧))
140100, 139sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 ∈ (β„€β‰₯β€˜((πΉβ€˜π‘) + 2)) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ 0 < 𝑧))
1411403ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 ∈ (β„€β‰₯β€˜((πΉβ€˜π‘) + 2)) ∧ (((πΉβ€˜π‘) + 𝑁) + 1) ∈ β„€ ∧ 𝑧 < (((πΉβ€˜π‘) + 𝑁) + 1)) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ 0 < 𝑧))
14299, 141sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ 0 < 𝑧))
143142impcom 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ 0 < 𝑧)
144 elnnz 12516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 ∈ β„• ↔ (𝑧 ∈ β„€ ∧ 0 < 𝑧))
14593, 143, 144sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ 𝑧 ∈ β„•)
146129adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ 0 < (πΉβ€˜π‘))
147146adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ 0 < (πΉβ€˜π‘))
148 ltsubpos 11654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πΉβ€˜π‘) ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ (0 < (πΉβ€˜π‘) ↔ (𝑧 βˆ’ (πΉβ€˜π‘)) < 𝑧))
149121, 122, 148syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (0 < (πΉβ€˜π‘) ↔ (𝑧 βˆ’ (πΉβ€˜π‘)) < 𝑧))
150147, 149mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (𝑧 βˆ’ (πΉβ€˜π‘)) < 𝑧)
151 ncoprmlnprm 16610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑧 βˆ’ (πΉβ€˜π‘)) ∈ β„• ∧ 𝑧 ∈ β„• ∧ (𝑧 βˆ’ (πΉβ€˜π‘)) < 𝑧) β†’ (1 < ((𝑧 βˆ’ (πΉβ€˜π‘)) gcd 𝑧) β†’ 𝑧 βˆ‰ β„™))
152127, 145, 150, 151syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (1 < ((𝑧 βˆ’ (πΉβ€˜π‘)) gcd 𝑧) β†’ 𝑧 βˆ‰ β„™))
15398, 152sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (1 < (((πΉβ€˜π‘) + (𝑧 βˆ’ (πΉβ€˜π‘))) gcd (𝑧 βˆ’ (πΉβ€˜π‘))) β†’ 𝑧 βˆ‰ β„™))
15486, 153syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1))) β†’ (βˆ€π‘— ∈ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁))1 < (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘))) β†’ 𝑧 βˆ‰ β„™))
155154ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ (βˆ€π‘— ∈ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁))1 < (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘))) β†’ 𝑧 βˆ‰ β„™)))
156155com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (βˆ€π‘— ∈ (((πΉβ€˜π‘) + 2)...((πΉβ€˜π‘) + 𝑁))1 < (((πΉβ€˜π‘) + (𝑗 βˆ’ (πΉβ€˜π‘))) gcd (𝑗 βˆ’ (πΉβ€˜π‘))) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 βˆ‰ β„™)))
15775, 156sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (βˆ€π‘— ∈ ((2 + (πΉβ€˜π‘))...(𝑁 + (πΉβ€˜π‘)))[(𝑗 βˆ’ (πΉβ€˜π‘)) / 𝑖]1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 βˆ‰ β„™)))
15850, 157sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (βˆ€π‘– ∈ (2...𝑁)1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 βˆ‰ β„™)))
159158ex 414 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((πΉβ€˜π‘) ∈ β„• β†’ (βˆ€π‘– ∈ (2...𝑁)1 < (((πΉβ€˜π‘) + 𝑖) gcd 𝑖) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 βˆ‰ β„™))))
16047, 159mpid 44 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((πΉβ€˜π‘) ∈ β„• β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 βˆ‰ β„™)))
161160imp 408 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 βˆ‰ β„™))
162161ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ 𝑧 βˆ‰ β„™))
163162impcom 409 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) ∧ (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™)) β†’ 𝑧 βˆ‰ β„™)
164163a1d 25 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) ∧ (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™)) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™))
165164ex 414 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) β†’ ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™)))
166 neleq1 3055 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑧 β†’ (𝑠 βˆ‰ β„™ ↔ 𝑧 βˆ‰ β„™))
167166rspcv 3580 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž) β†’ (βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™ β†’ 𝑧 βˆ‰ β„™))
168167adantld 492 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž) β†’ ((((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™) β†’ 𝑧 βˆ‰ β„™))
169168adantld 492 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™))
170169a1d 25 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž) β†’ ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™)))
171165, 170jaoi 856 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)) β†’ ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™)))
172171com12 32 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ ((𝑧 ∈ (((πΉβ€˜π‘) + 2)..^(((πΉβ€˜π‘) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™)))
17346, 172syldc 48 . . . . . . . . . . . . . 14 (𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž) β†’ ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™)))
17439, 173jaoi 856 . . . . . . . . . . . . 13 ((𝑧 ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2)) ∨ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž)) β†’ ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™)))
175174com12 32 . . . . . . . . . . . 12 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ ((𝑧 ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2)) ∨ 𝑧 ∈ (((πΉβ€˜π‘) + 2)..^π‘ž)) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™)))
17634, 175syld 47 . . . . . . . . . . 11 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (𝑧 ∈ ((𝑝 + 1)..^π‘ž) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ 𝑧 βˆ‰ β„™)))
177176com23 86 . . . . . . . . . 10 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ (𝑧 ∈ ((𝑝 + 1)..^π‘ž) β†’ 𝑧 βˆ‰ β„™)))
178177imp31 419 . . . . . . . . 9 ((((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) ∧ ((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™))) ∧ 𝑧 ∈ ((𝑝 + 1)..^π‘ž)) β†’ 𝑧 βˆ‰ β„™)
179178ralrimiva 3144 . . . . . . . 8 (((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) ∧ ((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™))) β†’ βˆ€π‘§ ∈ ((𝑝 + 1)..^π‘ž)𝑧 βˆ‰ β„™)
18024, 25, 1793jca 1129 . . . . . . 7 (((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) ∧ ((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™))) β†’ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘§ ∈ ((𝑝 + 1)..^π‘ž)𝑧 βˆ‰ β„™))
181180ex 414 . . . . . 6 ((((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) ∧ π‘ž ∈ β„™) β†’ (((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘§ ∈ ((𝑝 + 1)..^π‘ž)𝑧 βˆ‰ β„™)))
182181reximdva 3166 . . . . 5 (((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) ∧ 𝑝 ∈ β„™) β†’ (βˆƒπ‘ž ∈ β„™ ((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ βˆƒπ‘ž ∈ β„™ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘§ ∈ ((𝑝 + 1)..^π‘ž)𝑧 βˆ‰ β„™)))
183182reximdva 3166 . . . 4 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ (βˆƒπ‘ ∈ β„™ βˆƒπ‘ž ∈ β„™ ((𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ βˆƒπ‘ ∈ β„™ βˆƒπ‘ž ∈ β„™ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘§ ∈ ((𝑝 + 1)..^π‘ž)𝑧 βˆ‰ β„™)))
18423, 183biimtrrid 242 . . 3 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ ((βˆƒπ‘ ∈ β„™ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ βˆ€π‘Ÿ ∈ ((𝑝 + 1)..^((πΉβ€˜π‘) + 2))π‘Ÿ βˆ‰ β„™) ∧ βˆƒπ‘ž ∈ β„™ (((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘  ∈ ((((πΉβ€˜π‘) + 𝑁) + 1)..^π‘ž)𝑠 βˆ‰ β„™)) β†’ βˆƒπ‘ ∈ β„™ βˆƒπ‘ž ∈ β„™ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘§ ∈ ((𝑝 + 1)..^π‘ž)𝑧 βˆ‰ β„™)))
18517, 22, 184mp2and 698 . 2 ((πœ‘ ∧ (πΉβ€˜π‘) ∈ β„•) β†’ βˆƒπ‘ ∈ β„™ βˆƒπ‘ž ∈ β„™ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘§ ∈ ((𝑝 + 1)..^π‘ž)𝑧 βˆ‰ β„™))
1865, 185mpdan 686 1 (πœ‘ β†’ βˆƒπ‘ ∈ β„™ βˆƒπ‘ž ∈ β„™ (𝑝 < ((πΉβ€˜π‘) + 2) ∧ ((πΉβ€˜π‘) + 𝑁) < π‘ž ∧ βˆ€π‘§ ∈ ((𝑝 + 1)..^π‘ž)𝑧 βˆ‰ β„™))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   βˆ‰ wnel 3050  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448  [wsbc 3744  β¦‹csb 3860   class class class wbr 5110  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ↑m cmap 8772  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  β„•cn 12160  2c2 12215  3c3 12216  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  ...cfz 13431  ..^cfzo 13574   gcd cgcd 16381  β„™cprime 16554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-fz 13432  df-fzo 13575  df-seq 13914  df-exp 13975  df-fac 14181  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-dvds 16144  df-gcd 16382  df-prm 16555
This theorem is referenced by:  prmgaplem8  16937
  Copyright terms: Public domain W3C validator