Step | Hyp | Ref
| Expression |
1 | | prmgaplem7.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m
ℕ)) |
2 | | elmapi 8530 |
. . . 4
⊢ (𝐹 ∈ (ℕ
↑m ℕ) → 𝐹:ℕ⟶ℕ) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹:ℕ⟶ℕ) |
4 | | prmgaplem7.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 3, 4 | ffvelrnd 6905 |
. 2
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℕ) |
6 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℕ) |
7 | | elnnuz 12478 |
. . . . . . 7
⊢ ((𝐹‘𝑁) ∈ ℕ ↔ (𝐹‘𝑁) ∈
(ℤ≥‘1)) |
8 | 6, 7 | sylib 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈
(ℤ≥‘1)) |
9 | | 1z 12207 |
. . . . . . 7
⊢ 1 ∈
ℤ |
10 | | 2z 12209 |
. . . . . . 7
⊢ 2 ∈
ℤ |
11 | 9, 10 | eluzaddi 12467 |
. . . . . 6
⊢ ((𝐹‘𝑁) ∈ (ℤ≥‘1)
→ ((𝐹‘𝑁) + 2) ∈
(ℤ≥‘(1 + 2))) |
12 | 8, 11 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 2) ∈
(ℤ≥‘(1 + 2))) |
13 | | 1p2e3 11973 |
. . . . . . 7
⊢ (1 + 2) =
3 |
14 | 13 | eqcomi 2746 |
. . . . . 6
⊢ 3 = (1 +
2) |
15 | 14 | fveq2i 6720 |
. . . . 5
⊢
(ℤ≥‘3) = (ℤ≥‘(1 +
2)) |
16 | 12, 15 | eleqtrrdi 2849 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 2) ∈
(ℤ≥‘3)) |
17 | | prmgaplem5 16608 |
. . . 4
⊢ (((𝐹‘𝑁) + 2) ∈
(ℤ≥‘3) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ)) |
18 | 16, 17 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ)) |
19 | 4 | anim1ci 619 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
20 | | nnaddcl 11853 |
. . . . 5
⊢ (((𝐹‘𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹‘𝑁) + 𝑁) ∈ ℕ) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 𝑁) ∈ ℕ) |
22 | | prmgaplem6 16609 |
. . . 4
⊢ (((𝐹‘𝑁) + 𝑁) ∈ ℕ → ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) |
23 | 21, 22 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) |
24 | | reeanv 3279 |
. . . 4
⊢
(∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) ↔ (∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) |
25 | | simprll 779 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → 𝑝 < ((𝐹‘𝑁) + 2)) |
26 | | simprrl 781 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ((𝐹‘𝑁) + 𝑁) < 𝑞) |
27 | | nnz 12199 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑁) ∈ ℕ → (𝐹‘𝑁) ∈ ℤ) |
28 | 27 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℤ) |
29 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 2 ∈
ℤ) |
30 | 28, 29 | zaddcld 12286 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 2) ∈ ℤ) |
31 | 30 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝐹‘𝑁) + 2) ∈ ℤ) |
32 | 31 | anim1ci 619 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹‘𝑁) + 2) ∈ ℤ)) |
33 | | fzospliti 13274 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹‘𝑁) + 2) ∈ ℤ) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞))) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞))) |
35 | 34 | ex 416 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)))) |
36 | | neleq1 3051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑧 → (𝑟 ∉ ℙ ↔ 𝑧 ∉ ℙ)) |
37 | 36 | rspcv 3532 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → (∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ → 𝑧 ∉ ℙ)) |
38 | 37 | adantld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) → 𝑧 ∉ ℙ)) |
39 | 38 | adantrd 495 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)) |
40 | 39 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
41 | 21 | nnzd 12281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 𝑁) ∈ ℤ) |
42 | 41 | peano2zd 12285 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ) |
43 | 42 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ) |
44 | 43 | anim1ci 619 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ)) |
45 | | fzospliti 13274 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞))) |
47 | 46 | ex 416 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)))) |
48 | | prmgaplem7.i |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖)) |
49 | 4 | nnzd 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑁 ∈ ℤ) |
50 | | fzshftral 13200 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ (𝐹‘𝑁) ∈ ℤ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))) |
51 | 10, 49, 27, 50 | mp3an3an 1469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))) |
52 | | 2cnd 11908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 2 ∈
ℂ) |
53 | | nncn 11838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹‘𝑁) ∈ ℕ → (𝐹‘𝑁) ∈ ℂ) |
54 | | addcom 11018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((2
∈ ℂ ∧ (𝐹‘𝑁) ∈ ℂ) → (2 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 2)) |
55 | 52, 53, 54 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (2 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 2)) |
56 | 4 | nncnd 11846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℂ) |
57 | | addcom 11018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℂ ∧ (𝐹‘𝑁) ∈ ℂ) → (𝑁 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 𝑁)) |
58 | 56, 53, 57 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑁 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 𝑁)) |
59 | 55, 58 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁))) = (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))) |
60 | | ovex 7246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 − (𝐹‘𝑁)) ∈ V |
61 | | sbcbr2g 5111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ([(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖))) |
62 | 60, 61 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ([(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖))) |
63 | | csbov12g 7257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) = (⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) gcd ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖)) |
64 | 60, 63 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) = (⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) gcd ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖)) |
65 | | csbov2g 7259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) = ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖)) |
66 | 60, 65 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) = ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖)) |
67 | | csbvarg 4346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖 = (𝑗 − (𝐹‘𝑁))) |
68 | 67 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖) = ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁)))) |
69 | 60, 68 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖) = ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁)))) |
70 | 66, 69 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) = ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁)))) |
71 | 60, 67 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌𝑖 = (𝑗 − (𝐹‘𝑁))) |
72 | 70, 71 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
(⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) gcd ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖) = (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁)))) |
73 | 64, 72 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) = (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁)))) |
74 | 73 | breq2d 5065 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (1 <
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))))) |
75 | 62, 74 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ([(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))))) |
76 | 59, 75 | raleqbidv 3313 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))))) |
77 | | fzval3 13311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐹‘𝑁) + 𝑁) ∈ ℤ → (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)) = (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) |
78 | 77 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐹‘𝑁) + 𝑁) ∈ ℤ → (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) = (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))) |
79 | 41, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) = (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))) |
80 | 79 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ↔ 𝑧 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)))) |
81 | 80 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 𝑧 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))) |
82 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑗 = 𝑧 → (𝑗 − (𝐹‘𝑁)) = (𝑧 − (𝐹‘𝑁))) |
83 | 82 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑗 = 𝑧 → ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) = ((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁)))) |
84 | 83, 82 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑗 = 𝑧 → (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) = (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁)))) |
85 | 84 | breq2d 5065 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = 𝑧 → (1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) ↔ 1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))))) |
86 | 85 | rspcv 3532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))))) |
87 | 81, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))))) |
88 | 53 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℂ) |
89 | | elfzoelz 13243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℤ) |
90 | 89 | zcnd 12283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℂ) |
91 | | pncan3 11086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐹‘𝑁) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) = 𝑧) |
92 | 88, 90, 91 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → ((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) = 𝑧) |
93 | 92 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) = (𝑧 gcd (𝑧 − (𝐹‘𝑁)))) |
94 | 89 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℤ) |
95 | | zsubcl 12219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑧 ∈ ℤ ∧ (𝐹‘𝑁) ∈ ℤ) → (𝑧 − (𝐹‘𝑁)) ∈ ℤ) |
96 | 89, 28, 95 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹‘𝑁)) ∈ ℤ) |
97 | 94, 96 | gcdcomd 16073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 gcd (𝑧 − (𝐹‘𝑁))) = ((𝑧 − (𝐹‘𝑁)) gcd 𝑧)) |
98 | 93, 97 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) = ((𝑧 − (𝐹‘𝑁)) gcd 𝑧)) |
99 | 98 | breq2d 5065 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) ↔ 1 < ((𝑧 − (𝐹‘𝑁)) gcd 𝑧))) |
100 | | elfzo2 13246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ↔ (𝑧 ∈ (ℤ≥‘((𝐹‘𝑁) + 2)) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹‘𝑁) + 𝑁) + 1))) |
101 | | eluz2 12444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) ↔ (((𝐹‘𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧)) |
102 | | nnre 11837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐹‘𝑁) ∈ ℕ → (𝐹‘𝑁) ∈ ℝ) |
103 | 102 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (𝐹‘𝑁) ∈ ℝ) |
104 | | 2rp 12591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ 2 ∈
ℝ+ |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 2 ∈
ℝ+) |
106 | 103, 105 | ltaddrpd 12661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (𝐹‘𝑁) < ((𝐹‘𝑁) + 2)) |
107 | | 2re 11904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 2 ∈
ℝ |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐹‘𝑁) ∈ ℕ → 2 ∈
ℝ) |
109 | 102, 108 | readdcld 10862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐹‘𝑁) ∈ ℕ → ((𝐹‘𝑁) + 2) ∈ ℝ) |
110 | 109 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → ((𝐹‘𝑁) + 2) ∈ ℝ) |
111 | | zre 12180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
112 | 111 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 𝑧 ∈ ℝ) |
113 | | ltletr 10924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝐹‘𝑁) ∈ ℝ ∧ ((𝐹‘𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐹‘𝑁) < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → (𝐹‘𝑁) < 𝑧)) |
114 | 103, 110,
112, 113 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (((𝐹‘𝑁) < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → (𝐹‘𝑁) < 𝑧)) |
115 | 106, 114 | mpand 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (((𝐹‘𝑁) + 2) ≤ 𝑧 → (𝐹‘𝑁) < 𝑧)) |
116 | 115 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
117 | 116 | 3adant1 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((𝐹‘𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
118 | 101, 117 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
119 | 118 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
120 | 100, 119 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
121 | 120 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝐹‘𝑁) < 𝑧) |
122 | 102 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℝ) |
123 | 89 | zred 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℝ) |
124 | | posdif 11325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐹‘𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹‘𝑁)))) |
125 | 122, 123,
124 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → ((𝐹‘𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹‘𝑁)))) |
126 | 121, 125 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 0 < (𝑧 − (𝐹‘𝑁))) |
127 | | elnnz 12186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑧 − (𝐹‘𝑁)) ∈ ℕ ↔ ((𝑧 − (𝐹‘𝑁)) ∈ ℤ ∧ 0 < (𝑧 − (𝐹‘𝑁)))) |
128 | 96, 126, 127 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹‘𝑁)) ∈ ℕ) |
129 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 2 ∈
ℝ) |
130 | | nngt0 11861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝐹‘𝑁) ∈ ℕ → 0 < (𝐹‘𝑁)) |
131 | 130 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 < (𝐹‘𝑁)) |
132 | | 2pos 11933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 0 <
2 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 <
2) |
134 | 103, 129,
131, 133 | addgt0d 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 < ((𝐹‘𝑁) + 2)) |
135 | | 0red 10836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 ∈
ℝ) |
136 | | ltletr 10924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((0
∈ ℝ ∧ ((𝐹‘𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((0 <
((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → 0 < 𝑧)) |
137 | 135, 110,
112, 136 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → ((0 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → 0 < 𝑧)) |
138 | 134, 137 | mpand 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (((𝐹‘𝑁) + 2) ≤ 𝑧 → 0 < 𝑧)) |
139 | 138 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
140 | 139 | 3adant1 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝐹‘𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
141 | 101, 140 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
142 | 141 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
143 | 100, 142 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
144 | 143 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 0 < 𝑧) |
145 | | elnnz 12186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 ∈ ℕ ↔ (𝑧 ∈ ℤ ∧ 0 <
𝑧)) |
146 | 94, 144, 145 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℕ) |
147 | 130 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < (𝐹‘𝑁)) |
148 | 147 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 0 < (𝐹‘𝑁)) |
149 | | ltsubpos 11324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐹‘𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 < (𝐹‘𝑁) ↔ (𝑧 − (𝐹‘𝑁)) < 𝑧)) |
150 | 122, 123,
149 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (0 < (𝐹‘𝑁) ↔ (𝑧 − (𝐹‘𝑁)) < 𝑧)) |
151 | 148, 150 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹‘𝑁)) < 𝑧) |
152 | | ncoprmlnprm 16284 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑧 − (𝐹‘𝑁)) ∈ ℕ ∧ 𝑧 ∈ ℕ ∧ (𝑧 − (𝐹‘𝑁)) < 𝑧) → (1 < ((𝑧 − (𝐹‘𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ)) |
153 | 128, 146,
151, 152 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (1 < ((𝑧 − (𝐹‘𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ)) |
154 | 99, 153 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) → 𝑧 ∉ ℙ)) |
155 | 87, 154 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 𝑧 ∉ ℙ)) |
156 | 155 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 𝑧 ∉ ℙ))) |
157 | 156 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))) |
158 | 76, 157 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))) |
159 | 51, 158 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))) |
160 | 159 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐹‘𝑁) ∈ ℕ → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))) |
161 | 48, 160 | mpid 44 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝐹‘𝑁) ∈ ℕ → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))) |
162 | 161 | imp 410 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)) |
163 | 162 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)) |
164 | 163 | impcom 411 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → 𝑧 ∉ ℙ) |
165 | 164 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)) |
166 | 165 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
167 | | neleq1 3051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = 𝑧 → (𝑠 ∉ ℙ ↔ 𝑧 ∉ ℙ)) |
168 | 167 | rspcv 3532 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → (∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ → 𝑧 ∉ ℙ)) |
169 | 168 | adantld 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → ((((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ) → 𝑧 ∉ ℙ)) |
170 | 169 | adantld 494 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)) |
171 | 170 | a1d 25 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
172 | 166, 171 | jaoi 857 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
173 | 172 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
174 | 47, 173 | syldc 48 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
175 | 40, 174 | jaoi 857 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
176 | 175 | com12 32 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
177 | 35, 176 | syld 47 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
178 | 177 | com23 86 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → 𝑧 ∉ ℙ))) |
179 | 178 | imp31 421 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → 𝑧 ∉ ℙ) |
180 | 179 | ralrimiva 3105 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ) |
181 | 25, 26, 180 | 3jca 1130 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) |
182 | 181 | ex 416 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))) |
183 | 182 | reximdva 3193 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))) |
184 | 183 | reximdva 3193 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))) |
185 | 24, 184 | syl5bir 246 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))) |
186 | 18, 23, 185 | mp2and 699 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) |
187 | 5, 186 | mpdan 687 |
1
⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) |