Step | Hyp | Ref
| Expression |
1 | | prmgaplem7.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m
ℕ)) |
2 | | elmapi 8414 |
. . . 4
⊢ (𝐹 ∈ (ℕ
↑m ℕ) → 𝐹:ℕ⟶ℕ) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹:ℕ⟶ℕ) |
4 | | prmgaplem7.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 3, 4 | ffvelrnd 6838 |
. 2
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℕ) |
6 | | simpr 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℕ) |
7 | | elnnuz 12269 |
. . . . . . 7
⊢ ((𝐹‘𝑁) ∈ ℕ ↔ (𝐹‘𝑁) ∈
(ℤ≥‘1)) |
8 | 6, 7 | sylib 220 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈
(ℤ≥‘1)) |
9 | | 1z 11999 |
. . . . . . 7
⊢ 1 ∈
ℤ |
10 | | 2z 12001 |
. . . . . . 7
⊢ 2 ∈
ℤ |
11 | 9, 10 | eluzaddi 12258 |
. . . . . 6
⊢ ((𝐹‘𝑁) ∈ (ℤ≥‘1)
→ ((𝐹‘𝑁) + 2) ∈
(ℤ≥‘(1 + 2))) |
12 | 8, 11 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 2) ∈
(ℤ≥‘(1 + 2))) |
13 | | 1p2e3 11767 |
. . . . . . 7
⊢ (1 + 2) =
3 |
14 | 13 | eqcomi 2830 |
. . . . . 6
⊢ 3 = (1 +
2) |
15 | 14 | fveq2i 6659 |
. . . . 5
⊢
(ℤ≥‘3) = (ℤ≥‘(1 +
2)) |
16 | 12, 15 | eleqtrrdi 2924 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 2) ∈
(ℤ≥‘3)) |
17 | | prmgaplem5 16374 |
. . . 4
⊢ (((𝐹‘𝑁) + 2) ∈
(ℤ≥‘3) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ)) |
18 | 16, 17 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ)) |
19 | 4 | anim1ci 617 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
20 | | nnaddcl 11647 |
. . . . 5
⊢ (((𝐹‘𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹‘𝑁) + 𝑁) ∈ ℕ) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 𝑁) ∈ ℕ) |
22 | | prmgaplem6 16375 |
. . . 4
⊢ (((𝐹‘𝑁) + 𝑁) ∈ ℕ → ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) |
23 | 21, 22 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) |
24 | | reeanv 3367 |
. . . 4
⊢
(∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) ↔ (∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) |
25 | | simprll 777 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → 𝑝 < ((𝐹‘𝑁) + 2)) |
26 | | simprrl 779 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ((𝐹‘𝑁) + 𝑁) < 𝑞) |
27 | | nnz 11991 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑁) ∈ ℕ → (𝐹‘𝑁) ∈ ℤ) |
28 | 27 | adantl 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℤ) |
29 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 2 ∈
ℤ) |
30 | 28, 29 | zaddcld 12078 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 2) ∈ ℤ) |
31 | 30 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝐹‘𝑁) + 2) ∈ ℤ) |
32 | 31 | anim1ci 617 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹‘𝑁) + 2) ∈ ℤ)) |
33 | | fzospliti 13059 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ((𝑝 + 1)..^𝑞) ∧ ((𝐹‘𝑁) + 2) ∈ ℤ) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞))) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞))) |
35 | 34 | ex 415 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)))) |
36 | | neleq1 3128 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑧 → (𝑟 ∉ ℙ ↔ 𝑧 ∉ ℙ)) |
37 | 36 | rspcv 3610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → (∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ → 𝑧 ∉ ℙ)) |
38 | 37 | adantld 493 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) → 𝑧 ∉ ℙ)) |
39 | 38 | adantrd 494 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)) |
40 | 39 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
41 | 21 | nnzd 12073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + 𝑁) ∈ ℤ) |
42 | 41 | peano2zd 12077 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ) |
43 | 42 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ) |
44 | 43 | anim1ci 617 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ)) |
45 | | fzospliti 13059 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞))) |
47 | 46 | ex 415 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)))) |
48 | | prmgaplem7.i |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖)) |
49 | 4 | nnzd 12073 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑁 ∈ ℤ) |
50 | | fzshftral 12985 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ (𝐹‘𝑁) ∈ ℤ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))) |
51 | 10, 49, 27, 50 | mp3an3an 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))) |
52 | | 2cnd 11702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 2 ∈
ℂ) |
53 | | nncn 11632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹‘𝑁) ∈ ℕ → (𝐹‘𝑁) ∈ ℂ) |
54 | | addcom 10812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((2
∈ ℂ ∧ (𝐹‘𝑁) ∈ ℂ) → (2 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 2)) |
55 | 52, 53, 54 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (2 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 2)) |
56 | 4 | nncnd 11640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑁 ∈ ℂ) |
57 | | addcom 10812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈ ℂ ∧ (𝐹‘𝑁) ∈ ℂ) → (𝑁 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 𝑁)) |
58 | 56, 53, 57 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑁 + (𝐹‘𝑁)) = ((𝐹‘𝑁) + 𝑁)) |
59 | 55, 58 | oveq12d 7160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁))) = (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))) |
60 | | ovex 7175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 − (𝐹‘𝑁)) ∈ V |
61 | | sbcbr2g 5110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ([(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖))) |
62 | 60, 61 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ([(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖))) |
63 | | csbov12g 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) = (⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) gcd ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖)) |
64 | 60, 63 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) = (⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) gcd ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖)) |
65 | | csbov2g 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) = ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖)) |
66 | 60, 65 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) = ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖)) |
67 | | csbvarg 4369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖 = (𝑗 − (𝐹‘𝑁))) |
68 | 67 | oveq2d 7158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 − (𝐹‘𝑁)) ∈ V → ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖) = ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁)))) |
69 | 60, 68 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((𝐹‘𝑁) + ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖) = ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁)))) |
70 | 66, 69 | eqtrd 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) = ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁)))) |
71 | 60, 67 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌𝑖 = (𝑗 − (𝐹‘𝑁))) |
72 | 70, 71 | oveq12d 7160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
(⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌((𝐹‘𝑁) + 𝑖) gcd ⦋(𝑗 − (𝐹‘𝑁)) / 𝑖⦌𝑖) = (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁)))) |
73 | 64, 72 | eqtrd 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) →
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) = (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁)))) |
74 | 73 | breq2d 5064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (1 <
⦋(𝑗 −
(𝐹‘𝑁)) / 𝑖⦌(((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))))) |
75 | 62, 74 | bitrd 281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ([(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ 1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))))) |
76 | 59, 75 | raleqbidv 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) ↔ ∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))))) |
77 | | fzval3 13096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐹‘𝑁) + 𝑁) ∈ ℤ → (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)) = (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) |
78 | 77 | eqcomd 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐹‘𝑁) + 𝑁) ∈ ℤ → (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) = (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))) |
79 | 41, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) = (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))) |
80 | 79 | eleq2d 2898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ↔ 𝑧 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)))) |
81 | 80 | biimpa 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 𝑧 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))) |
82 | | oveq1 7149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑗 = 𝑧 → (𝑗 − (𝐹‘𝑁)) = (𝑧 − (𝐹‘𝑁))) |
83 | 82 | oveq2d 7158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑗 = 𝑧 → ((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) = ((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁)))) |
84 | 83, 82 | oveq12d 7160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑗 = 𝑧 → (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) = (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁)))) |
85 | 84 | breq2d 5064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑗 = 𝑧 → (1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) ↔ 1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))))) |
86 | 85 | rspcv 3610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁)) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))))) |
87 | 81, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))))) |
88 | 53 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℂ) |
89 | | elfzoelz 13028 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℤ) |
90 | 89 | zcnd 12075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℂ) |
91 | | pncan3 10880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐹‘𝑁) ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) = 𝑧) |
92 | 88, 90, 91 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → ((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) = 𝑧) |
93 | 92 | oveq1d 7157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) = (𝑧 gcd (𝑧 − (𝐹‘𝑁)))) |
94 | 89 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℤ) |
95 | | zsubcl 12011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑧 ∈ ℤ ∧ (𝐹‘𝑁) ∈ ℤ) → (𝑧 − (𝐹‘𝑁)) ∈ ℤ) |
96 | 89, 28, 95 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹‘𝑁)) ∈ ℤ) |
97 | | gcdcom 15845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑧 ∈ ℤ ∧ (𝑧 − (𝐹‘𝑁)) ∈ ℤ) → (𝑧 gcd (𝑧 − (𝐹‘𝑁))) = ((𝑧 − (𝐹‘𝑁)) gcd 𝑧)) |
98 | 94, 96, 97 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 gcd (𝑧 − (𝐹‘𝑁))) = ((𝑧 − (𝐹‘𝑁)) gcd 𝑧)) |
99 | 93, 98 | eqtrd 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) = ((𝑧 − (𝐹‘𝑁)) gcd 𝑧)) |
100 | 99 | breq2d 5064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) ↔ 1 < ((𝑧 − (𝐹‘𝑁)) gcd 𝑧))) |
101 | | elfzo2 13031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ↔ (𝑧 ∈ (ℤ≥‘((𝐹‘𝑁) + 2)) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹‘𝑁) + 𝑁) + 1))) |
102 | | eluz2 12236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) ↔ (((𝐹‘𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧)) |
103 | | nnre 11631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐹‘𝑁) ∈ ℕ → (𝐹‘𝑁) ∈ ℝ) |
104 | 103 | ad2antll 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (𝐹‘𝑁) ∈ ℝ) |
105 | | 2rp 12381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ 2 ∈
ℝ+ |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 2 ∈
ℝ+) |
107 | 104, 106 | ltaddrpd 12451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (𝐹‘𝑁) < ((𝐹‘𝑁) + 2)) |
108 | | 2re 11698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 2 ∈
ℝ |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐹‘𝑁) ∈ ℕ → 2 ∈
ℝ) |
110 | 103, 109 | readdcld 10656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐹‘𝑁) ∈ ℕ → ((𝐹‘𝑁) + 2) ∈ ℝ) |
111 | 110 | ad2antll 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → ((𝐹‘𝑁) + 2) ∈ ℝ) |
112 | | zre 11972 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
113 | 112 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 𝑧 ∈ ℝ) |
114 | | ltletr 10718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝐹‘𝑁) ∈ ℝ ∧ ((𝐹‘𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝐹‘𝑁) < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → (𝐹‘𝑁) < 𝑧)) |
115 | 104, 111,
113, 114 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (((𝐹‘𝑁) < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → (𝐹‘𝑁) < 𝑧)) |
116 | 107, 115 | mpand 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (((𝐹‘𝑁) + 2) ≤ 𝑧 → (𝐹‘𝑁) < 𝑧)) |
117 | 116 | impancom 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
118 | 117 | 3adant1 1126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((𝐹‘𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
119 | 102, 118 | sylbi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
120 | 119 | 3ad2ant1 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
121 | 101, 120 | sylbi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) < 𝑧)) |
122 | 121 | impcom 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝐹‘𝑁) < 𝑧) |
123 | 103 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝐹‘𝑁) ∈ ℝ) |
124 | 89 | zred 12074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∈ ℝ) |
125 | | posdif 11119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐹‘𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹‘𝑁)))) |
126 | 123, 124,
125 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → ((𝐹‘𝑁) < 𝑧 ↔ 0 < (𝑧 − (𝐹‘𝑁)))) |
127 | 122, 126 | mpbid 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 0 < (𝑧 − (𝐹‘𝑁))) |
128 | | elnnz 11978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑧 − (𝐹‘𝑁)) ∈ ℕ ↔ ((𝑧 − (𝐹‘𝑁)) ∈ ℤ ∧ 0 < (𝑧 − (𝐹‘𝑁)))) |
129 | 96, 127, 128 | sylanbrc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹‘𝑁)) ∈ ℕ) |
130 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 2 ∈
ℝ) |
131 | | nngt0 11655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝐹‘𝑁) ∈ ℕ → 0 < (𝐹‘𝑁)) |
132 | 131 | ad2antll 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 < (𝐹‘𝑁)) |
133 | | 2pos 11727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ 0 <
2 |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 <
2) |
135 | 104, 130,
132, 134 | addgt0d 11201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 < ((𝐹‘𝑁) + 2)) |
136 | | 0red 10630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → 0 ∈
ℝ) |
137 | | ltletr 10718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((0
∈ ℝ ∧ ((𝐹‘𝑁) + 2) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((0 <
((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → 0 < 𝑧)) |
138 | 136, 111,
113, 137 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → ((0 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → 0 < 𝑧)) |
139 | 135, 138 | mpand 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑧 ∈ ℤ ∧ (𝜑 ∧ (𝐹‘𝑁) ∈ ℕ)) → (((𝐹‘𝑁) + 2) ≤ 𝑧 → 0 < 𝑧)) |
140 | 139 | impancom 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
141 | 140 | 3adant1 1126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝐹‘𝑁) + 2) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ((𝐹‘𝑁) + 2) ≤ 𝑧) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
142 | 102, 141 | sylbi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
143 | 142 | 3ad2ant1 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑧 ∈
(ℤ≥‘((𝐹‘𝑁) + 2)) ∧ (((𝐹‘𝑁) + 𝑁) + 1) ∈ ℤ ∧ 𝑧 < (((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
144 | 101, 143 | sylbi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < 𝑧)) |
145 | 144 | impcom 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 0 < 𝑧) |
146 | | elnnz 11978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 ∈ ℕ ↔ (𝑧 ∈ ℤ ∧ 0 <
𝑧)) |
147 | 94, 145, 146 | sylanbrc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 𝑧 ∈ ℕ) |
148 | 131 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → 0 < (𝐹‘𝑁)) |
149 | 148 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → 0 < (𝐹‘𝑁)) |
150 | | ltsubpos 11118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐹‘𝑁) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (0 < (𝐹‘𝑁) ↔ (𝑧 − (𝐹‘𝑁)) < 𝑧)) |
151 | 123, 124,
150 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (0 < (𝐹‘𝑁) ↔ (𝑧 − (𝐹‘𝑁)) < 𝑧)) |
152 | 149, 151 | mpbid 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (𝑧 − (𝐹‘𝑁)) < 𝑧) |
153 | | ncoprmlnprm 16051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑧 − (𝐹‘𝑁)) ∈ ℕ ∧ 𝑧 ∈ ℕ ∧ (𝑧 − (𝐹‘𝑁)) < 𝑧) → (1 < ((𝑧 − (𝐹‘𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ)) |
154 | 129, 147,
152, 153 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (1 < ((𝑧 − (𝐹‘𝑁)) gcd 𝑧) → 𝑧 ∉ ℙ)) |
155 | 100, 154 | sylbid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (1 < (((𝐹‘𝑁) + (𝑧 − (𝐹‘𝑁))) gcd (𝑧 − (𝐹‘𝑁))) → 𝑧 ∉ ℙ)) |
156 | 87, 155 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1))) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 𝑧 ∉ ℙ)) |
157 | 156 | ex 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → 𝑧 ∉ ℙ))) |
158 | 157 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑗 ∈ (((𝐹‘𝑁) + 2)...((𝐹‘𝑁) + 𝑁))1 < (((𝐹‘𝑁) + (𝑗 − (𝐹‘𝑁))) gcd (𝑗 − (𝐹‘𝑁))) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))) |
159 | 76, 158 | sylbid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑗 ∈ ((2 + (𝐹‘𝑁))...(𝑁 + (𝐹‘𝑁)))[(𝑗 − (𝐹‘𝑁)) / 𝑖]1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))) |
160 | 51, 159 | sylbid 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))) |
161 | 160 | ex 415 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐹‘𝑁) ∈ ℕ → (∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)))) |
162 | 48, 161 | mpid 44 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝐹‘𝑁) ∈ ℕ → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ))) |
163 | 162 | imp 409 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)) |
164 | 163 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → 𝑧 ∉ ℙ)) |
165 | 164 | impcom 410 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → 𝑧 ∉ ℙ) |
166 | 165 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∧ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)) |
167 | 166 | ex 415 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
168 | | neleq1 3128 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = 𝑧 → (𝑠 ∉ ℙ ↔ 𝑧 ∉ ℙ)) |
169 | 168 | rspcv 3610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → (∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ → 𝑧 ∉ ℙ)) |
170 | 169 | adantld 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → ((((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ) → 𝑧 ∉ ℙ)) |
171 | 170 | adantld 493 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ)) |
172 | 171 | a1d 25 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
173 | 167, 172 | jaoi 853 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
174 | 173 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ (((𝐹‘𝑁) + 2)..^(((𝐹‘𝑁) + 𝑁) + 1)) ∨ 𝑧 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
175 | 47, 174 | syldc 48 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
176 | 40, 175 | jaoi 853 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
177 | 176 | com12 32 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑧 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2)) ∨ 𝑧 ∈ (((𝐹‘𝑁) + 2)..^𝑞)) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
178 | 35, 177 | syld 47 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → 𝑧 ∉ ℙ))) |
179 | 178 | com23 86 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑧 ∈ ((𝑝 + 1)..^𝑞) → 𝑧 ∉ ℙ))) |
180 | 179 | imp31 420 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) ∧ 𝑧 ∈ ((𝑝 + 1)..^𝑞)) → 𝑧 ∉ ℙ) |
181 | 180 | ralrimiva 3182 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ) |
182 | 25, 26, 181 | 3jca 1124 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) ∧ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ))) → (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) |
183 | 182 | ex 415 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → (((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))) |
184 | 183 | reximdva 3274 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) ∧ 𝑝 ∈ ℙ) → (∃𝑞 ∈ ℙ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))) |
185 | 184 | reximdva 3274 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ((𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))) |
186 | 24, 185 | syl5bir 245 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ((∃𝑝 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ∀𝑟 ∈ ((𝑝 + 1)..^((𝐹‘𝑁) + 2))𝑟 ∉ ℙ) ∧ ∃𝑞 ∈ ℙ (((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑠 ∈ ((((𝐹‘𝑁) + 𝑁) + 1)..^𝑞)𝑠 ∉ ℙ)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))) |
187 | 18, 23, 186 | mp2and 697 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝑁) ∈ ℕ) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) |
188 | 5, 187 | mpdan 685 |
1
⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) |