Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . . 4
⊢ 𝑦 ∈ V |
2 | | gausslemma2d.r |
. . . . 5
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
3 | 2 | elrnmpt 5293 |
. . . 4
⊢ (𝑦 ∈ V → (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))) |
4 | 1, 3 | ax-mp 5 |
. . 3
⊢ (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
5 | | iftrue 4042 |
. . . . . . . . 9
⊢ ((𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑥 · 2)) |
6 | 5 | eqeq2d 2620 |
. . . . . . . 8
⊢ ((𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2))) |
7 | 6 | adantr 480 |
. . . . . . 7
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2))) |
8 | | elfz1b 12279 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝐻) ↔ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻)) |
9 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) |
10 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℕ |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ → 2 ∈
ℕ) |
12 | 9, 11 | nnmulcld 10945 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℕ) |
13 | 12 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℕ) |
14 | 13 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ∈ ℕ) |
15 | | gausslemma2d.h |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = ((𝑃 − 1) / 2) |
16 | 15 | eleq1i 2679 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻 ∈ ℕ ↔ ((𝑃 − 1) / 2) ∈
ℕ) |
17 | 16 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ ℕ → ((𝑃 − 1) / 2) ∈
ℕ) |
18 | 17 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → ((𝑃 − 1) / 2) ∈
ℕ) |
19 | 18 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑃 − 1) / 2) ∈
ℕ) |
20 | | gausslemma2d.p |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
21 | | nnoddn2prm 15354 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℕ
∧ ¬ 2 ∥ 𝑃)) |
22 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) |
23 | 22 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃)) |
24 | 21, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)) |
25 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
26 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℤ |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℕ → 2 ∈
ℤ) |
28 | 25, 27 | zmulcld 11364 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℤ) |
29 | 28 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℤ) |
30 | 24, 29 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ (𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈
ℤ)) |
31 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
↔ ((𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)
∧ (𝑥 · 2) ∈
ℤ)) |
32 | 30, 31 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ (𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) |
33 | 32 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ))) |
34 | 20, 33 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ))) |
35 | 34 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) |
36 | | ltoddhalfle 14923 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
→ ((𝑥 · 2) <
(𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) /
2))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2))) |
38 | 37 | biimp3a 1424 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ≤ ((𝑃 − 1) / 2)) |
39 | 14, 19, 38 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) |
40 | 39 | 3exp 1256 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))))) |
41 | 8, 40 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1...𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))))) |
42 | 41 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2)))) |
43 | 42 | impcom 445 |
. . . . . . . . 9
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) |
44 | 15 | oveq2i 6560 |
. . . . . . . . . . 11
⊢
(1...𝐻) =
(1...((𝑃 − 1) /
2)) |
45 | 44 | eleq2i 2680 |
. . . . . . . . . 10
⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...((𝑃 − 1) / 2))) |
46 | | elfz1b 12279 |
. . . . . . . . . 10
⊢ ((𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)) ↔ ((𝑥 · 2) ∈ ℕ
∧ ((𝑃 − 1) / 2)
∈ ℕ ∧ (𝑥
· 2) ≤ ((𝑃
− 1) / 2))) |
47 | 45, 46 | bitri 263 |
. . . . . . . . 9
⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) |
48 | 43, 47 | sylibr 223 |
. . . . . . . 8
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ (1...𝐻)) |
49 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 · 2) → (𝑦 ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...𝐻))) |
50 | 48, 49 | syl5ibrcom 236 |
. . . . . . 7
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑥 · 2) → 𝑦 ∈ (1...𝐻))) |
51 | 7, 50 | sylbid 229 |
. . . . . 6
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
52 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
(𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑥 · 2))) |
53 | 52 | eqeq2d 2620 |
. . . . . . . 8
⊢ (¬
(𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2)))) |
54 | 53 | adantr 480 |
. . . . . . 7
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2)))) |
55 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
56 | | prmz 15227 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
57 | 20, 55, 56 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℤ) |
58 | 57 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝑃 ∈ ℤ) |
59 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝐻) → 𝑥 ∈ ℤ) |
60 | 26 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝐻) → 2 ∈ ℤ) |
61 | 59, 60 | zmulcld 11364 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℤ) |
62 | 61 | ad2antll 761 |
. . . . . . . . . . 11
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ ℤ) |
63 | 58, 62 | zsubcld 11363 |
. . . . . . . . . 10
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈
ℤ) |
64 | 56 | zred 11358 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
65 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑥 ∈
ℝ) |
67 | | peano2rem 10227 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
68 | 67 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − 1) ∈
ℝ) |
69 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
70 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 |
71 | 69, 70 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ ∧ 0 < 2) |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (2
∈ ℝ ∧ 0 < 2)) |
73 | | lemuldiv 10782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
74 | 66, 68, 72, 73 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
75 | 15 | breq2i 4591 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ≤ 𝐻 ↔ 𝑥 ≤ ((𝑃 − 1) / 2)) |
76 | 74, 75 | syl6rbbr 278 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 ↔ (𝑥 · 2) ≤ (𝑃 − 1))) |
77 | 12 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℝ) |
78 | 77 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 · 2) ∈
ℝ) |
79 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℝ) |
80 | 78, 68, 79 | lesub2d 10514 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ (𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)))) |
81 | | recn 9905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℝ → 𝑃 ∈
ℂ) |
82 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℝ → 1 ∈
ℂ) |
83 | 81, 82 | nncand 10276 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 − 1)) = 1) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 − 1)) = 1) |
85 | 84 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) ↔ 1 ≤ (𝑃 − (𝑥 · 2)))) |
86 | 85 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
87 | 80, 86 | sylbid 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
88 | 76, 87 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 → 1 ≤ (𝑃 − (𝑥 · 2)))) |
89 | 88 | impancom 455 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) |
90 | 89 | 3adant2 1073 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) |
91 | 8, 90 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) |
92 | 91 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℝ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
93 | 64, 92 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
94 | 20, 55, 93 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
95 | 94 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 1 ≤ (𝑃 − (𝑥 · 2))) |
96 | 95 | adantl 481 |
. . . . . . . . . 10
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 1 ≤ (𝑃 − (𝑥 · 2))) |
97 | | elnnz1 11280 |
. . . . . . . . . 10
⊢ ((𝑃 − (𝑥 · 2)) ∈ ℕ ↔ ((𝑃 − (𝑥 · 2)) ∈ ℤ ∧ 1 ≤
(𝑃 − (𝑥 · 2)))) |
98 | 63, 96, 97 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈
ℕ) |
99 | 8 | simp2bi 1070 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...𝐻) → 𝐻 ∈ ℕ) |
100 | 99 | ad2antll 761 |
. . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝐻 ∈ ℕ) |
101 | | nnre 10904 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
102 | 101 | rehalfcld 11156 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈
ℝ) |
103 | 102 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 / 2) ∈
ℝ) |
104 | 61 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℝ) |
105 | | lenlt 9995 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑥 · 2) ∈
ℝ) → ((𝑃 / 2)
≤ (𝑥 · 2) ↔
¬ (𝑥 · 2) <
(𝑃 / 2))) |
106 | 103, 104,
105 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2))) |
107 | 23, 61 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈
ℤ)) |
108 | 107, 31 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) |
109 | | halfleoddlt 14924 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
→ ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
111 | 110 | biimpa 500 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 / 2) < (𝑥 · 2)) |
112 | | nncn 10905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℂ) |
113 | | subhalfhalf 11143 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℂ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℕ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
115 | 114 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℕ → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
116 | 115 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
117 | 111, 116 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑃 / 2)) < (𝑥 · 2)) |
118 | 101 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℝ) |
119 | 102 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℝ) |
120 | 104 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℝ) |
121 | 118, 119,
120 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈
ℝ)) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈
ℝ)) |
123 | | ltsub23 10387 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧
(𝑥 · 2) ∈
ℝ) → ((𝑃 −
(𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2))) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2))) |
125 | 117, 124 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) < (𝑃 / 2)) |
126 | 22 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ) |
127 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ¬ 2 ∥ 𝑃) |
128 | 61 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ) |
129 | 126, 128 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 − (𝑥 · 2)) ∈
ℤ) |
130 | 126, 127,
129 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈
ℤ)) |
131 | 130 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈
ℤ)) |
132 | | ltoddhalfle 14923 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) |
134 | 125, 133 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)) |
135 | 134 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) |
136 | 15 | breq2i 4591 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 − (𝑥 · 2)) ≤ 𝐻 ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)) |
137 | 135, 136 | syl6ibr 241 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
138 | 106, 137 | sylbird 249 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
139 | 138 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))) |
140 | 20, 21, 139 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))) |
141 | 140 | imp 444 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
142 | 141 | impcom 445 |
. . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ≤ 𝐻) |
143 | | elfz1b 12279 |
. . . . . . . . 9
⊢ ((𝑃 − (𝑥 · 2)) ∈ (1...𝐻) ↔ ((𝑃 − (𝑥 · 2)) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
144 | 98, 100, 142, 143 | syl3anbrc 1239 |
. . . . . . . 8
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ (1...𝐻)) |
145 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑦 = (𝑃 − (𝑥 · 2)) → (𝑦 ∈ (1...𝐻) ↔ (𝑃 − (𝑥 · 2)) ∈ (1...𝐻))) |
146 | 144, 145 | syl5ibrcom 236 |
. . . . . . 7
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑃 − (𝑥 · 2)) → 𝑦 ∈ (1...𝐻))) |
147 | 54, 146 | sylbid 229 |
. . . . . 6
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
148 | 51, 147 | pm2.61ian 827 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
149 | 148 | rexlimdva 3013 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
150 | | elfz1b 12279 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (1...𝐻) ↔ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) |
151 | | simp1 1054 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℕ) |
152 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((2
∥ 𝑦 ∧ 𝜑) → 2 ∥ 𝑦) |
153 | | nnehalf 14934 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 2 ∥
𝑦) → (𝑦 / 2) ∈
ℕ) |
154 | 151, 152,
153 | syl2anr 494 |
. . . . . . . . . . . 12
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ∈ ℕ) |
155 | | simpr2 1061 |
. . . . . . . . . . . 12
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ) |
156 | | nnre 10904 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
157 | 156 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → 𝑦 ∈ ℝ) |
158 | | nnrp 11718 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 ∈ ℕ → 𝐻 ∈
ℝ+) |
159 | 158 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → 𝐻 ∈
ℝ+) |
160 | 159 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → 𝐻 ∈
ℝ+) |
161 | | 2rp 11713 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ |
162 | | 1le2 11118 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ≤
2 |
163 | 161, 162 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 ∈
ℝ+ ∧ 1 ≤ 2) |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → (2 ∈
ℝ+ ∧ 1 ≤ 2)) |
165 | | ledivge1le 11777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+
∧ (2 ∈ ℝ+ ∧ 1 ≤ 2)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)) |
166 | 157, 160,
164, 165 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)) |
167 | 166 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻))) |
168 | 167 | com23 84 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻))) |
169 | 168 | 3impia 1253 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻)) |
170 | 169 | impcom 445 |
. . . . . . . . . . . 12
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ≤ 𝐻) |
171 | 154, 155,
170 | 3jca 1235 |
. . . . . . . . . . 11
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) |
172 | 171 | ex 449 |
. . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))) |
173 | 150, 172 | syl5bi 231 |
. . . . . . . . 9
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))) |
174 | 173 | 3impia 1253 |
. . . . . . . 8
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) |
175 | | elfz1b 12279 |
. . . . . . . 8
⊢ ((𝑦 / 2) ∈ (1...𝐻) ↔ ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) |
176 | 174, 175 | sylibr 223 |
. . . . . . 7
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑦 / 2) ∈ (1...𝐻)) |
177 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 / 2) → (𝑥 · 2) = ((𝑦 / 2) · 2)) |
178 | 177 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ ((𝑦 / 2) · 2) < (𝑃 / 2))) |
179 | 177 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − ((𝑦 / 2) · 2))) |
180 | 178, 177,
179 | ifbieq12d 4063 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))) |
181 | 180 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))) |
182 | 181 | adantl 481 |
. . . . . . 7
⊢ (((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = (𝑦 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))) |
183 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℤ) |
184 | 183 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℂ) |
185 | 184 | 3ad2ant3 1077 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ) |
186 | | 2cnd 10970 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ) |
187 | | 2ne0 10990 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
188 | 187 | a1i 11 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ≠ 0) |
189 | 185, 186,
188 | divcan1d 10681 |
. . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) = 𝑦) |
190 | 15 | breq2i 4591 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ≤ 𝐻 ↔ 𝑦 ≤ ((𝑃 − 1) / 2)) |
191 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
192 | 20, 21, 23 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃)) |
193 | 192 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃)) |
194 | 191, 193 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ)) |
195 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ 𝑦 ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ 𝑦 ∈
ℤ)) |
196 | 194, 195 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ)) |
197 | | ltoddhalfle 14923 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ 𝑦 ∈ ℤ) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2))) |
198 | 196, 197 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2))) |
199 | 198 | exbiri 650 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → 𝑦 < (𝑃 / 2)))) |
200 | 199 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))) |
201 | 190, 200 | syl5bi 231 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))) |
202 | 201 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))))) |
203 | 202 | 3imp 1249 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))) |
204 | 150, 203 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (1...𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))) |
205 | 204 | com12 32 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → 𝑦 < (𝑃 / 2))) |
206 | 205 | 3impia 1253 |
. . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 < (𝑃 / 2)) |
207 | 189, 206 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) < (𝑃 / 2)) |
208 | 207 | iftrued 4044 |
. . . . . . . 8
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))) = ((𝑦 / 2) · 2)) |
209 | 208, 189 | eqtr2d 2645 |
. . . . . . 7
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))) |
210 | 176, 182,
209 | rspcedvd 3289 |
. . . . . 6
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
211 | 210 | 3exp 1256 |
. . . . 5
⊢ (2
∥ 𝑦 → (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))) |
212 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℤ) |
213 | 212 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℤ) |
214 | 191 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℤ) |
215 | 214 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℤ) |
216 | 213, 215 | zsubcld 11363 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℤ) |
217 | 156 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑦 ∈
ℝ) |
218 | 67 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → ((𝑃 − 1) / 2) ∈
ℝ) |
219 | 218 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → ((𝑃 − 1) / 2) ∈
ℝ) |
220 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑃 ∈
ℝ) |
221 | 217, 219,
220 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈
ℝ)) |
222 | 221 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈
ℝ))) |
223 | 55, 64, 222 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ))) |
224 | 223 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ))) |
225 | 224 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ)) |
226 | | lesub2 10402 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈ ℝ)
→ (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦))) |
227 | 225, 226 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦))) |
228 | 56 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
229 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℂ → 1 ∈
ℂ) |
230 | | 2cnne0 11119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
231 | 230 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℂ → (2 ∈
ℂ ∧ 2 ≠ 0)) |
232 | | divsubdir 10600 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2))) |
233 | 229, 231,
232 | mpd3an23 1418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 /
2))) |
234 | 233 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = (𝑃 − ((𝑃 / 2) − (1 / 2)))) |
235 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → 𝑃 ∈
ℂ) |
236 | | halfcl 11134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → (𝑃 / 2) ∈
ℂ) |
237 | | halfcn 11124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 / 2)
∈ ℂ |
238 | 237 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → (1 / 2)
∈ ℂ) |
239 | 235, 236,
238 | subsubd 10299 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 / 2) − (1 / 2))) = ((𝑃 − (𝑃 / 2)) + (1 / 2))) |
240 | 113 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℂ → ((𝑃 − (𝑃 / 2)) + (1 / 2)) = ((𝑃 / 2) + (1 / 2))) |
241 | 234, 239,
240 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2))) |
242 | 55, 228, 241 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 /
2))) |
243 | 242 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 /
2))) |
244 | 243 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) ↔ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦))) |
245 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
246 | | halfre 11123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (1 / 2)
∈ ℝ |
247 | 246 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ → (1 / 2)
∈ ℝ) |
248 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℕ → 0 <
𝑃) |
249 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℕ → (2 ∈
ℝ ∧ 0 < 2)) |
250 | | divgt0 10770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑃 ∈ ℝ ∧ 0 <
𝑃) ∧ (2 ∈ ℝ
∧ 0 < 2)) → 0 < (𝑃 / 2)) |
251 | 101, 248,
249, 250 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ → 0 <
(𝑃 / 2)) |
252 | | halfgt0 11125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 < (1
/ 2) |
253 | 252 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ → 0 < (1
/ 2)) |
254 | 102, 247,
251, 253 | addgt0d 10481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℕ → 0 <
((𝑃 / 2) + (1 /
2))) |
255 | 55, 245, 254 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 0 < ((𝑃 / 2) + (1
/ 2))) |
256 | 255 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ 0 < ((𝑃 / 2) + (1
/ 2))) |
257 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 0 ∈
ℝ) |
258 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℝ) |
259 | 258 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈
ℝ) |
260 | 246 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 / 2)
∈ ℝ) |
261 | 259, 260 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) + (1 / 2)) ∈
ℝ) |
262 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ) |
263 | 262 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ) |
264 | 257, 261,
263 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)) |
265 | 264 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
266 | 156, 265 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
267 | 266 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
268 | 267 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
269 | 55, 64, 268 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
270 | 269 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
271 | 270 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)) |
272 | | ltletr 10008 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦)) → 0 < (𝑃 − 𝑦))) |
273 | 271, 272 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((0 < ((𝑃 / 2) +
(1 / 2)) ∧ ((𝑃 / 2) +
(1 / 2)) ≤ (𝑃 −
𝑦)) → 0 < (𝑃 − 𝑦))) |
274 | 256, 273 | mpand 707 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (((𝑃 / 2) + (1 / 2))
≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦))) |
275 | 244, 274 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦))) |
276 | 227, 275 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ≤ ((𝑃 − 1) / 2) → 0 <
(𝑃 − 𝑦))) |
277 | 276 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑦 ≤ ((𝑃 − 1) / 2) → 0 <
(𝑃 − 𝑦)))) |
278 | 277 | com23 84 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦)))) |
279 | 190, 278 | syl5bi 231 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦)))) |
280 | 279 | 3impia 1253 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦))) |
281 | 280 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 0 < (𝑃 − 𝑦)) |
282 | | elnnz 11264 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 − 𝑦) ∈ ℕ ↔ ((𝑃 − 𝑦) ∈ ℤ ∧ 0 < (𝑃 − 𝑦))) |
283 | 216, 281,
282 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℕ) |
284 | 24 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)) |
285 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ¬ 2 ∥ 𝑦) |
286 | 285, 214 | anim12ci 589 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦)) |
287 | | omoe 14926 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ (𝑦 ∈ ℤ ∧ ¬ 2
∥ 𝑦)) → 2
∥ (𝑃 − 𝑦)) |
288 | 284, 286,
287 | syl2an2r 872 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 2 ∥ (𝑃 − 𝑦)) |
289 | | nnehalf 14934 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 − 𝑦) ∈ ℕ ∧ 2 ∥ (𝑃 − 𝑦)) → ((𝑃 − 𝑦) / 2) ∈ ℕ) |
290 | 283, 288,
289 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ∈ ℕ) |
291 | | simpr2 1061 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ) |
292 | | 1red 9934 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 1 ∈
ℝ) |
293 | 156 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℝ) |
294 | 293 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℝ) |
295 | 55, 64 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℝ) |
296 | 295 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℝ) |
297 | | nnge1 10923 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 1 ≤
𝑦) |
298 | 297 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 1 ≤ 𝑦) |
299 | 298 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 1 ≤ 𝑦) |
300 | 292, 294,
296, 299 | lesub2dd 10523 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ≤ (𝑃 − 1)) |
301 | 296, 294 | resubcld 10337 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℝ) |
302 | 55, 64, 67 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − 1) ∈
ℝ) |
303 | 302 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 1) ∈ ℝ) |
304 | 71 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (2 ∈ ℝ
∧ 0 < 2)) |
305 | | lediv1 10767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 − 𝑦) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))) |
306 | 301, 303,
304, 305 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))) |
307 | 300, 306 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)) |
308 | 15 | breq2i 4591 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 − 𝑦) / 2) ≤ 𝐻 ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)) |
309 | 307, 308 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ 𝐻) |
310 | 290, 291,
309 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)) |
311 | 310 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻))) |
312 | | elfz1b 12279 |
. . . . . . . . . . 11
⊢ (((𝑃 − 𝑦) / 2) ∈ (1...𝐻) ↔ (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)) |
313 | 311, 150,
312 | 3imtr4g 284 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))) |
314 | 313 | ex 449 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (¬ 2 ∥ 𝑦
→ (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))) |
315 | 20, 314 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))) |
316 | 315 | 3imp21 1269 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)) |
317 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑥 · 2) = (((𝑃 − 𝑦) / 2) · 2)) |
318 | 317 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2))) |
319 | 317 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) |
320 | 318, 317,
319 | ifbieq12d 4063 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))) |
321 | 320 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))) |
322 | 321 | adantl 481 |
. . . . . . 7
⊢ (((¬
2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = ((𝑃 − 𝑦) / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))) |
323 | 20, 55, 228 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℂ) |
324 | 323 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑃 ∈ ℂ) |
325 | 184 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ) |
326 | 324, 325 | subcld 10271 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − 𝑦) ∈ ℂ) |
327 | | 2cnd 10970 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ) |
328 | 187 | a1i 11 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ≠ 0) |
329 | 326, 327,
328 | divcan1d 10681 |
. . . . . . . . . 10
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (((𝑃 − 𝑦) / 2) · 2) = (𝑃 − 𝑦)) |
330 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℝ) |
331 | | halfge0 11126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ≤ (1
/ 2) |
332 | | rehalfcl 11135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈
ℝ) |
333 | 332 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈
ℝ) |
334 | 333, 260 | subge02d 10498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ≤
(1 / 2) ↔ ((𝑃 / 2)
− (1 / 2)) ≤ (𝑃 /
2))) |
335 | 331, 334 | mpbii 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ≤
(𝑃 / 2)) |
336 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑦 ∈
ℝ) |
337 | 246 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → (1 / 2)
∈ ℝ) |
338 | 332, 337 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) − (1 / 2)) ∈
ℝ) |
339 | 338 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ∈
ℝ) |
340 | | letr 10010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 / 2) − (1 / 2)) ∈
ℝ ∧ (𝑃 / 2)
∈ ℝ) → ((𝑦
≤ ((𝑃 / 2) − (1 /
2)) ∧ ((𝑃 / 2) −
(1 / 2)) ≤ (𝑃 / 2))
→ 𝑦 ≤ (𝑃 / 2))) |
341 | 336, 339,
333, 340 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤
(𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2))) |
342 | 335, 341 | mpan2d 706 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 / 2) − (1 / 2)) → 𝑦 ≤ (𝑃 / 2))) |
343 | 81 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℂ) |
344 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 1 ∈
ℂ) |
345 | 230 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (2
∈ ℂ ∧ 2 ≠ 0)) |
346 | 343, 344,
345, 232 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 /
2))) |
347 | 346 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ 𝑦 ≤ ((𝑃 / 2) − (1 / 2)))) |
348 | | lesub 10386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑃 / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2)))) |
349 | 333, 258,
336, 348 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2)))) |
350 | 259, 263 | lenltd 10062 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
351 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃 ∈ ℝ → 2 ∈
ℂ) |
352 | 187 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃 ∈ ℝ → 2 ≠
0) |
353 | 81, 351, 352 | divcan1d 10681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = 𝑃) |
354 | 353 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → 𝑃 = ((𝑃 / 2) · 2)) |
355 | 354 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (((𝑃 / 2) · 2) − (𝑃 / 2))) |
356 | 332 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈
ℂ) |
357 | 356, 351 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = (2 ·
(𝑃 / 2))) |
358 | 357 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → (((𝑃 / 2) · 2) − (𝑃 / 2)) = ((2 · (𝑃 / 2)) − (𝑃 / 2))) |
359 | 351, 356 | mulsubfacd 10371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → ((2
· (𝑃 / 2)) −
(𝑃 / 2)) = ((2 − 1)
· (𝑃 /
2))) |
360 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (2
− 1) = 1 |
361 | 360 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → (2
− 1) = 1) |
362 | 361 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → ((2
− 1) · (𝑃 /
2)) = (1 · (𝑃 /
2))) |
363 | 356 | mulid2d 9937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → (1
· (𝑃 / 2)) = (𝑃 / 2)) |
364 | 359, 362,
363 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → ((2
· (𝑃 / 2)) −
(𝑃 / 2)) = (𝑃 / 2)) |
365 | 355, 358,
364 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
366 | 365 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
367 | 366 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ (𝑃 − (𝑃 / 2)) ↔ 𝑦 ≤ (𝑃 / 2))) |
368 | 349, 350,
367 | 3bitr3d 297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (¬
(𝑃 − 𝑦) < (𝑃 / 2) ↔ 𝑦 ≤ (𝑃 / 2))) |
369 | 342, 347,
368 | 3imtr4d 282 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
370 | 369 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
371 | 156, 370 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
372 | 371 | com3l 87 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
373 | 330, 372 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℤ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
374 | 55, 56, 373 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬
(𝑃 − 𝑦) < (𝑃 / 2)))) |
375 | 20, 374 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
376 | 375 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
377 | 376 | com13 86 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((¬ 2 ∥
𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
378 | 190, 377 | syl5bi 231 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
379 | 378 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))) |
380 | 379 | 3imp 1249 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
381 | 380 | com12 32 |
. . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
382 | 150, 381 | syl5bi 231 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
383 | 382 | 3impia 1253 |
. . . . . . . . . 10
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)) |
384 | 329, 383 | eqnbrtrd 4601 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2)) |
385 | 384 | iffalsed 4047 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) |
386 | 329 | oveq2d 6565 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (((𝑃 − 𝑦) / 2) · 2)) = (𝑃 − (𝑃 − 𝑦))) |
387 | 323, 184 | anim12i 588 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
388 | 387 | 3adant1 1072 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
389 | | nncan 10189 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑃 − (𝑃 − 𝑦)) = 𝑦) |
390 | 388, 389 | syl 17 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (𝑃 − 𝑦)) = 𝑦) |
391 | 385, 386,
390 | 3eqtrrd 2649 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))) |
392 | 316, 322,
391 | rspcedvd 3289 |
. . . . . 6
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
393 | 392 | 3exp 1256 |
. . . . 5
⊢ (¬ 2
∥ 𝑦 → (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))) |
394 | 211, 393 | pm2.61i 175 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))) |
395 | 149, 394 | impbid 201 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 ∈ (1...𝐻))) |
396 | 4, 395 | syl5bb 271 |
. 2
⊢ (𝜑 → (𝑦 ∈ ran 𝑅 ↔ 𝑦 ∈ (1...𝐻))) |
397 | 396 | eqrdv 2608 |
1
⊢ (𝜑 → ran 𝑅 = (1...𝐻)) |