Proof of Theorem bgoldbtbndlem3
Step | Hyp | Ref
| Expression |
1 | | fzo0ss1 12367 |
. . . . . 6
⊢
(1..^𝐷) ⊆
(0..^𝐷) |
2 | 1 | sseli 3564 |
. . . . 5
⊢ (𝐼 ∈ (1..^𝐷) → 𝐼 ∈ (0..^𝐷)) |
3 | | bgoldbtbnd.i |
. . . . 5
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)))) |
4 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → (𝐹‘𝑖) = (𝐹‘𝐼)) |
5 | 4 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → ((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ↔ (𝐹‘𝐼) ∈ (ℙ ∖
{2}))) |
6 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1)) |
7 | 6 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → (𝐹‘(𝑖 + 1)) = (𝐹‘(𝐼 + 1))) |
8 | 7, 4 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) = ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼))) |
9 | 8 | breq1d 4593 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ↔ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4))) |
10 | 8 | breq2d 4595 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) ↔ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) |
11 | 5, 9, 10 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑖 = 𝐼 → (((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) ↔ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼))))) |
12 | 11 | rspcv 3278 |
. . . . 5
⊢ (𝐼 ∈ (0..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))) → ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼))))) |
13 | 2, 3, 12 | syl2imc 40 |
. . . 4
⊢ (𝜑 → (𝐼 ∈ (1..^𝐷) → ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼))))) |
14 | 13 | a1d 25 |
. . 3
⊢ (𝜑 → (𝑋 ∈ Odd → (𝐼 ∈ (1..^𝐷) → ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))))) |
15 | 14 | 3imp 1249 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) |
16 | | bgoldbtbndlem3.s |
. . . . 5
⊢ 𝑆 = (𝑋 − (𝐹‘𝐼)) |
17 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → 𝑋 ∈ Odd ) |
18 | | oddprmALTV 40136 |
. . . . . . . . 9
⊢ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) → (𝐹‘𝐼) ∈ Odd ) |
19 | 18 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ (((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼))) → (𝐹‘𝐼) ∈ Odd ) |
20 | 17, 19 | anim12i 588 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) → (𝑋 ∈ Odd ∧ (𝐹‘𝐼) ∈ Odd )) |
21 | 20 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) ∧ (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆)) → (𝑋 ∈ Odd ∧ (𝐹‘𝐼) ∈ Odd )) |
22 | | omoeALTV 40134 |
. . . . . 6
⊢ ((𝑋 ∈ Odd ∧ (𝐹‘𝐼) ∈ Odd ) → (𝑋 − (𝐹‘𝐼)) ∈ Even ) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) ∧ (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆)) → (𝑋 − (𝐹‘𝐼)) ∈ Even ) |
24 | 16, 23 | syl5eqel 2692 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) ∧ (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆)) → 𝑆 ∈ Even ) |
25 | | eldifi 3694 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) → (𝐹‘𝐼) ∈ ℙ) |
26 | | prmz 15227 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝐼) ∈ ℙ → (𝐹‘𝐼) ∈ ℤ) |
27 | 26 | zred 11358 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝐼) ∈ ℙ → (𝐹‘𝐼) ∈ ℝ) |
28 | | fzofzp1 12431 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ (1..^𝐷) → (𝐼 + 1) ∈ (1...𝐷)) |
29 | | elfzo2 12342 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ (1..^𝐷) ↔ (𝐼 ∈ (ℤ≥‘1)
∧ 𝐷 ∈ ℤ
∧ 𝐼 < 𝐷)) |
30 | | 1zzd 11285 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈
(ℤ≥‘1) ∧ 𝐷 ∈ ℤ ∧ 𝐼 < 𝐷) → 1 ∈ ℤ) |
31 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈
(ℤ≥‘1) ∧ 𝐷 ∈ ℤ ∧ 𝐼 < 𝐷) → 𝐷 ∈ ℤ) |
32 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐼 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 1 ≤
𝐼)) |
33 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 ∈
ℤ → 1 ∈ ℝ) |
34 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
ℝ) |
35 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐷 ∈ ℤ → 𝐷 ∈
ℝ) |
36 | | leltletr 39940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((1
∈ ℝ ∧ 𝐼
∈ ℝ ∧ 𝐷
∈ ℝ) → ((1 ≤ 𝐼 ∧ 𝐼 < 𝐷) → 1 ≤ 𝐷)) |
37 | 33, 34, 35, 36 | syl3an 1360 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((1
∈ ℤ ∧ 𝐼
∈ ℤ ∧ 𝐷
∈ ℤ) → ((1 ≤ 𝐼 ∧ 𝐼 < 𝐷) → 1 ≤ 𝐷)) |
38 | 37 | exp5o 1278 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
ℤ → (𝐼 ∈
ℤ → (𝐷 ∈
ℤ → (1 ≤ 𝐼
→ (𝐼 < 𝐷 → 1 ≤ 𝐷))))) |
39 | 38 | com34 89 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
ℤ → (𝐼 ∈
ℤ → (1 ≤ 𝐼
→ (𝐷 ∈ ℤ
→ (𝐼 < 𝐷 → 1 ≤ 𝐷))))) |
40 | 39 | 3imp 1249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((1
∈ ℤ ∧ 𝐼
∈ ℤ ∧ 1 ≤ 𝐼) → (𝐷 ∈ ℤ → (𝐼 < 𝐷 → 1 ≤ 𝐷))) |
41 | 32, 40 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐼 ∈
(ℤ≥‘1) → (𝐷 ∈ ℤ → (𝐼 < 𝐷 → 1 ≤ 𝐷))) |
42 | 41 | 3imp 1249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈
(ℤ≥‘1) ∧ 𝐷 ∈ ℤ ∧ 𝐼 < 𝐷) → 1 ≤ 𝐷) |
43 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 1 ≤
𝐷)) |
44 | 30, 31, 42, 43 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈
(ℤ≥‘1) ∧ 𝐷 ∈ ℤ ∧ 𝐼 < 𝐷) → 𝐷 ∈
(ℤ≥‘1)) |
45 | 29, 44 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ (1..^𝐷) → 𝐷 ∈
(ℤ≥‘1)) |
46 | | fzisfzounsn 12445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈
(ℤ≥‘1) → (1...𝐷) = ((1..^𝐷) ∪ {𝐷})) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ (1..^𝐷) → (1...𝐷) = ((1..^𝐷) ∪ {𝐷})) |
48 | 47 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ (1..^𝐷) → ((𝐼 + 1) ∈ (1...𝐷) ↔ (𝐼 + 1) ∈ ((1..^𝐷) ∪ {𝐷}))) |
49 | | elun 3715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 + 1) ∈ ((1..^𝐷) ∪ {𝐷}) ↔ ((𝐼 + 1) ∈ (1..^𝐷) ∨ (𝐼 + 1) ∈ {𝐷})) |
50 | 48, 49 | syl6bb 275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ (1..^𝐷) → ((𝐼 + 1) ∈ (1...𝐷) ↔ ((𝐼 + 1) ∈ (1..^𝐷) ∨ (𝐼 + 1) ∈ {𝐷}))) |
51 | | bgoldbtbnd.d |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐷 ∈
(ℤ≥‘3)) |
52 | | eluzge3nn 11606 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∈
(ℤ≥‘3) → 𝐷 ∈ ℕ) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐷 ∈ ℕ) |
54 | 53 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ (1..^𝐷) ∧ (𝐼 + 1) ∈ (1..^𝐷)) ∧ (𝜑 ∧ 𝑋 ∈ Odd )) → 𝐷 ∈ ℕ) |
55 | | bgoldbtbnd.f |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷)) |
56 | 55 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ (1..^𝐷) ∧ (𝐼 + 1) ∈ (1..^𝐷)) ∧ (𝜑 ∧ 𝑋 ∈ Odd )) → 𝐹 ∈ (RePart‘𝐷)) |
57 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ (1..^𝐷) ∧ (𝐼 + 1) ∈ (1..^𝐷)) ∧ (𝜑 ∧ 𝑋 ∈ Odd )) → (𝐼 + 1) ∈ (1..^𝐷)) |
58 | 54, 56, 57 | iccpartipre 39959 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ (1..^𝐷) ∧ (𝐼 + 1) ∈ (1..^𝐷)) ∧ (𝜑 ∧ 𝑋 ∈ Odd )) → (𝐹‘(𝐼 + 1)) ∈ ℝ) |
59 | 58 | exp31 628 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ (1..^𝐷) → ((𝐼 + 1) ∈ (1..^𝐷) → ((𝜑 ∧ 𝑋 ∈ Odd ) → (𝐹‘(𝐼 + 1)) ∈ ℝ))) |
60 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 + 1) ∈ {𝐷} → (𝐼 + 1) = 𝐷) |
61 | | bgoldbtbnd.r |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ) |
62 | 61 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼 + 1) = 𝐷 ∧ (𝜑 ∧ 𝑋 ∈ Odd )) → (𝐹‘𝐷) ∈ ℝ) |
63 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐼 + 1) = 𝐷 → (𝐹‘(𝐼 + 1)) = (𝐹‘𝐷)) |
64 | 63 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 + 1) = 𝐷 → ((𝐹‘(𝐼 + 1)) ∈ ℝ ↔ (𝐹‘𝐷) ∈ ℝ)) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼 + 1) = 𝐷 ∧ (𝜑 ∧ 𝑋 ∈ Odd )) → ((𝐹‘(𝐼 + 1)) ∈ ℝ ↔ (𝐹‘𝐷) ∈ ℝ)) |
66 | 62, 65 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼 + 1) = 𝐷 ∧ (𝜑 ∧ 𝑋 ∈ Odd )) → (𝐹‘(𝐼 + 1)) ∈ ℝ) |
67 | 66 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 + 1) = 𝐷 → ((𝜑 ∧ 𝑋 ∈ Odd ) → (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
68 | 60, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 + 1) ∈ {𝐷} → ((𝜑 ∧ 𝑋 ∈ Odd ) → (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ (1..^𝐷) → ((𝐼 + 1) ∈ {𝐷} → ((𝜑 ∧ 𝑋 ∈ Odd ) → (𝐹‘(𝐼 + 1)) ∈ ℝ))) |
70 | 59, 69 | jaod 394 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ (1..^𝐷) → (((𝐼 + 1) ∈ (1..^𝐷) ∨ (𝐼 + 1) ∈ {𝐷}) → ((𝜑 ∧ 𝑋 ∈ Odd ) → (𝐹‘(𝐼 + 1)) ∈ ℝ))) |
71 | 50, 70 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ (1..^𝐷) → ((𝐼 + 1) ∈ (1...𝐷) → ((𝜑 ∧ 𝑋 ∈ Odd ) → (𝐹‘(𝐼 + 1)) ∈ ℝ))) |
72 | 28, 71 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ (1..^𝐷) → ((𝜑 ∧ 𝑋 ∈ Odd ) → (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
73 | 72 | com12 32 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ Odd ) → (𝐼 ∈ (1..^𝐷) → (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
74 | 73 | 3impia 1253 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝐹‘(𝐼 + 1)) ∈ ℝ) |
75 | | bgoldbtbnd.n |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11)) |
76 | | eluzelre 11574 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘;11)
→ 𝑁 ∈
ℝ) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℝ) |
78 | | oddz 40082 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ Odd → 𝑋 ∈
ℤ) |
79 | 78 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ Odd → 𝑋 ∈
ℝ) |
80 | | rexr 9964 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘(𝐼 + 1)) ∈ ℝ → (𝐹‘(𝐼 + 1)) ∈
ℝ*) |
81 | | rexr 9964 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝐼) ∈ ℝ → (𝐹‘𝐼) ∈
ℝ*) |
82 | 80, 81 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ) → ((𝐹‘𝐼) ∈ ℝ* ∧ (𝐹‘(𝐼 + 1)) ∈
ℝ*)) |
83 | 82 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → ((𝐹‘𝐼) ∈ ℝ* ∧ (𝐹‘(𝐼 + 1)) ∈
ℝ*)) |
84 | | elico1 12089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹‘𝐼) ∈ ℝ* ∧ (𝐹‘(𝐼 + 1)) ∈ ℝ*) →
(𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝐹‘𝐼) ≤ 𝑋 ∧ 𝑋 < (𝐹‘(𝐼 + 1))))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝐹‘𝐼) ≤ 𝑋 ∧ 𝑋 < (𝐹‘(𝐼 + 1))))) |
86 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → 𝑋 ∈ ℝ) |
87 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → (𝐹‘(𝐼 + 1)) ∈ ℝ) |
88 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → (𝐹‘𝐼) ∈ ℝ) |
89 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → 𝑋 < (𝐹‘(𝐼 + 1))) |
90 | 86, 87, 88, 89 | ltsub1dd 10518 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼))) |
91 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → 𝑋 ∈ ℝ) |
92 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (𝐹‘𝐼) ∈ ℝ) |
93 | 91, 92 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (𝑋 − (𝐹‘𝐼)) ∈ ℝ) |
94 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) ∈ ℝ) |
95 | 87, 88 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) ∈ ℝ) |
96 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → 𝑁 ∈ ℝ) |
97 | | 4re 10974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 4 ∈
ℝ |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → 4 ∈
ℝ) |
99 | 96, 98 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → (𝑁 − 4) ∈ ℝ) |
100 | | lttr 9993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑋 − (𝐹‘𝐼)) ∈ ℝ ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) ∈ ℝ ∧ (𝑁 − 4) ∈ ℝ) → (((𝑋 − (𝐹‘𝐼)) < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4)) → (𝑋 − (𝐹‘𝐼)) < (𝑁 − 4))) |
101 | 94, 95, 99, 100 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → (((𝑋 − (𝐹‘𝐼)) < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4)) → (𝑋 − (𝐹‘𝐼)) < (𝑁 − 4))) |
102 | 90, 101 | mpand 707 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → (𝑋 − (𝐹‘𝐼)) < (𝑁 − 4))) |
103 | 102 | impr 647 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ (𝑋 < (𝐹‘(𝐼 + 1)) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4))) → (𝑋 − (𝐹‘𝐼)) < (𝑁 − 4)) |
104 | | 4pos 10993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 <
4 |
105 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) → 4 ∈
ℝ) |
106 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) → 𝑁 ∈
ℝ) |
107 | 105, 106 | ltsubposd 10492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (0 <
4 ↔ (𝑁 − 4) <
𝑁)) |
108 | 104, 107 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑁 − 4) < 𝑁) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (𝑁 − 4) < 𝑁) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ (𝑋 < (𝐹‘(𝐼 + 1)) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4))) → (𝑁 − 4) < 𝑁) |
111 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → 𝑁 ∈ ℝ) |
112 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → 4 ∈
ℝ) |
113 | 111, 112 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (𝑁 − 4) ∈ ℝ) |
114 | | lttr 9993 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑋 − (𝐹‘𝐼)) ∈ ℝ ∧ (𝑁 − 4) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑋 − (𝐹‘𝐼)) < (𝑁 − 4) ∧ (𝑁 − 4) < 𝑁) → (𝑋 − (𝐹‘𝐼)) < 𝑁)) |
115 | 93, 113, 111, 114 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (((𝑋 − (𝐹‘𝐼)) < (𝑁 − 4) ∧ (𝑁 − 4) < 𝑁) → (𝑋 − (𝐹‘𝐼)) < 𝑁)) |
116 | 115 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ (𝑋 < (𝐹‘(𝐼 + 1)) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4))) → (((𝑋 − (𝐹‘𝐼)) < (𝑁 − 4) ∧ (𝑁 − 4) < 𝑁) → (𝑋 − (𝐹‘𝐼)) < 𝑁)) |
117 | 103, 110,
116 | mp2and 711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) ∧ (𝑋 < (𝐹‘(𝐼 + 1)) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4))) → (𝑋 − (𝐹‘𝐼)) < 𝑁) |
118 | 117 | exp32 629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (𝑋 < (𝐹‘(𝐼 + 1)) → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → (𝑋 − (𝐹‘𝐼)) < 𝑁))) |
119 | 118 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 < (𝐹‘(𝐼 + 1)) → (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → (𝑋 − (𝐹‘𝐼)) < 𝑁))) |
120 | 119 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ ℝ*
∧ (𝐹‘𝐼) ≤ 𝑋 ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → (𝑋 − (𝐹‘𝐼)) < 𝑁))) |
121 | 120 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → ((𝑋 ∈ ℝ*
∧ (𝐹‘𝐼) ≤ 𝑋 ∧ 𝑋 < (𝐹‘(𝐼 + 1))) → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → (𝑋 − (𝐹‘𝐼)) < 𝑁))) |
122 | 85, 121 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → (𝑋 − (𝐹‘𝐼)) < 𝑁))) |
123 | 122 | com23 84 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹‘(𝐼 + 1)) ∈ ℝ ∧ (𝐹‘𝐼) ∈ ℝ)) → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁))) |
124 | 123 | exp32 629 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((𝐹‘(𝐼 + 1)) ∈ ℝ → ((𝐹‘𝐼) ∈ ℝ → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁))))) |
125 | 124 | com34 89 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((𝐹‘(𝐼 + 1)) ∈ ℝ → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → ((𝐹‘𝐼) ∈ ℝ → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁))))) |
126 | 77, 79, 125 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ Odd ) → ((𝐹‘(𝐼 + 1)) ∈ ℝ → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → ((𝐹‘𝐼) ∈ ℝ → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁))))) |
127 | 126 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹‘(𝐼 + 1)) ∈ ℝ → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → ((𝐹‘𝐼) ∈ ℝ → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁))))) |
128 | 74, 127 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → ((𝐹‘𝐼) ∈ ℝ → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁)))) |
129 | 128 | com13 86 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝐼) ∈ ℝ → (((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁)))) |
130 | 25, 27, 129 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) →
(((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) → ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁)))) |
131 | 130 | imp 444 |
. . . . . . . . 9
⊢ (((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4)) → ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁))) |
132 | 131 | 3adant3 1074 |
. . . . . . . 8
⊢ (((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼))) → ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁))) |
133 | 132 | impcom 445 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) → (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝑋 − (𝐹‘𝐼)) < 𝑁)) |
134 | 133 | imp 444 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) ∧ 𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1)))) → (𝑋 − (𝐹‘𝐼)) < 𝑁) |
135 | 134 | adantrr 749 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) ∧ (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆)) → (𝑋 − (𝐹‘𝐼)) < 𝑁) |
136 | 16, 135 | syl5eqbr 4618 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) ∧ (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆)) → 𝑆 < 𝑁) |
137 | | simprr 792 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) ∧ (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆)) → 4 < 𝑆) |
138 | 24, 136, 137 | 3jca 1235 |
. . 3
⊢ ((((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) ∧ (𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆)) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆)) |
139 | 138 | ex 449 |
. 2
⊢ (((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹‘𝐼)))) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆))) |
140 | 15, 139 | mpdan 699 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆))) |