Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . . . 5
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
2 | 1 | elrnmpt 4901 |
. . . 4
⊢ (𝑦 ∈ V → (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))) |
3 | 2 | elv 2760 |
. . 3
⊢ (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
4 | | iftrue 3558 |
. . . . . . . . . 10
⊢ ((𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑥 · 2)) |
5 | 4 | eqeq2d 2201 |
. . . . . . . . 9
⊢ ((𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2))) |
6 | 5 | adantr 276 |
. . . . . . . 8
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2))) |
7 | | elfz1b 10142 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝐻) ↔ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻)) |
8 | | id 19 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) |
9 | | 2nn 9129 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℕ |
10 | 9 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℕ → 2 ∈
ℕ) |
11 | 8, 10 | nnmulcld 9017 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℕ) |
12 | 11 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℕ) |
13 | 12 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ∈ ℕ) |
14 | | gausslemma2d.h |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐻 = ((𝑃 − 1) / 2) |
15 | 14 | eleq1i 2255 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐻 ∈ ℕ ↔ ((𝑃 − 1) / 2) ∈
ℕ) |
16 | 15 | biimpi 120 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻 ∈ ℕ → ((𝑃 − 1) / 2) ∈
ℕ) |
17 | 16 | 3ad2ant2 1021 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → ((𝑃 − 1) / 2) ∈
ℕ) |
18 | 17 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑃 − 1) / 2) ∈
ℕ) |
19 | | gausslemma2d.p |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
20 | | nnoddn2prm 12372 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℕ
∧ ¬ 2 ∥ 𝑃)) |
21 | | nnz 9322 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) |
22 | 21 | anim1i 340 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃)) |
23 | 20, 22 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)) |
24 | | nnz 9322 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
25 | | 2z 9331 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℤ |
26 | 25 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℕ → 2 ∈
ℤ) |
27 | 24, 26 | zmulcld 9431 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℤ) |
28 | 27 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℤ) |
29 | 23, 28 | anim12i 338 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ (𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈
ℤ)) |
30 | | df-3an 982 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
↔ ((𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)
∧ (𝑥 · 2) ∈
ℤ)) |
31 | 29, 30 | sylibr 134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ (𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) |
32 | 31 | ex 115 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ))) |
33 | 19, 32 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ))) |
34 | 33 | impcom 125 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) |
35 | | ltoddhalfle 12008 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
→ ((𝑥 · 2) <
(𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) /
2))) |
36 | 34, 35 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2))) |
37 | 36 | biimp3a 1356 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ≤ ((𝑃 − 1) / 2)) |
38 | 13, 18, 37 | 3jca 1179 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) |
39 | 38 | 3exp 1204 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))))) |
40 | 7, 39 | sylbi 121 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))))) |
41 | 40 | impcom 125 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2)))) |
42 | 41 | impcom 125 |
. . . . . . . . . 10
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) |
43 | 14 | oveq2i 5917 |
. . . . . . . . . . . 12
⊢
(1...𝐻) =
(1...((𝑃 − 1) /
2)) |
44 | 43 | eleq2i 2256 |
. . . . . . . . . . 11
⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...((𝑃 − 1) / 2))) |
45 | | elfz1b 10142 |
. . . . . . . . . . 11
⊢ ((𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)) ↔ ((𝑥 · 2) ∈ ℕ
∧ ((𝑃 − 1) / 2)
∈ ℕ ∧ (𝑥
· 2) ≤ ((𝑃
− 1) / 2))) |
46 | 44, 45 | bitri 184 |
. . . . . . . . . 10
⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) |
47 | 42, 46 | sylibr 134 |
. . . . . . . . 9
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ (1...𝐻)) |
48 | | eleq1 2252 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥 · 2) → (𝑦 ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...𝐻))) |
49 | 47, 48 | syl5ibrcom 157 |
. . . . . . . 8
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑥 · 2) → 𝑦 ∈ (1...𝐻))) |
50 | 6, 49 | sylbid 150 |
. . . . . . 7
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
51 | 50 | ancoms 268 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
52 | | iffalse 3561 |
. . . . . . . . . 10
⊢ (¬
(𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑥 · 2))) |
53 | 52 | eqeq2d 2201 |
. . . . . . . . 9
⊢ (¬
(𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2)))) |
54 | 53 | adantr 276 |
. . . . . . . 8
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2)))) |
55 | | eldifi 3277 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
56 | | prmz 12223 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
57 | 19, 55, 56 | 3syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℤ) |
58 | 57 | ad2antrl 490 |
. . . . . . . . . . . 12
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝑃 ∈ ℤ) |
59 | | elfzelz 10077 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...𝐻) → 𝑥 ∈ ℤ) |
60 | 25 | a1i 9 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...𝐻) → 2 ∈ ℤ) |
61 | 59, 60 | zmulcld 9431 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℤ) |
62 | 61 | ad2antll 491 |
. . . . . . . . . . . 12
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ ℤ) |
63 | 58, 62 | zsubcld 9430 |
. . . . . . . . . . 11
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈
ℤ) |
64 | 56 | zred 9425 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
65 | 14 | breq2i 4033 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ≤ 𝐻 ↔ 𝑥 ≤ ((𝑃 − 1) / 2)) |
66 | | nnre 8975 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
67 | 66 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑥 ∈
ℝ) |
68 | | peano2rem 8272 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
69 | 68 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − 1) ∈
ℝ) |
70 | | 2re 9038 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
71 | | 2pos 9059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
2 |
72 | 70, 71 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ ∧ 0 < 2) |
73 | 72 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (2
∈ ℝ ∧ 0 < 2)) |
74 | | lemuldiv 8886 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
75 | 67, 69, 73, 74 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
76 | 65, 75 | bitr4id 199 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 ↔ (𝑥 · 2) ≤ (𝑃 − 1))) |
77 | 11 | nnred 8981 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℝ) |
78 | 77 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 · 2) ∈
ℝ) |
79 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℝ) |
80 | 78, 69, 79 | lesub2d 8558 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ (𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)))) |
81 | | recn 7991 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℝ → 𝑃 ∈
ℂ) |
82 | | 1cnd 8021 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℝ → 1 ∈
ℂ) |
83 | 81, 82 | nncand 8321 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 − 1)) = 1) |
84 | 83 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 − 1)) = 1) |
85 | 84 | breq1d 4035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) ↔ 1 ≤ (𝑃 − (𝑥 · 2)))) |
86 | 85 | biimpd 144 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
87 | 80, 86 | sylbid 150 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
88 | 76, 87 | sylbid 150 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 → 1 ≤ (𝑃 − (𝑥 · 2)))) |
89 | 88 | impancom 260 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) |
90 | 89 | 3adant2 1018 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) |
91 | 7, 90 | sylbi 121 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) |
92 | 91 | com12 30 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℝ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
93 | 19, 55, 64, 92 | 4syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
94 | 93 | imp 124 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 1 ≤ (𝑃 − (𝑥 · 2))) |
95 | 94 | adantl 277 |
. . . . . . . . . . 11
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 1 ≤ (𝑃 − (𝑥 · 2))) |
96 | | elnnz1 9326 |
. . . . . . . . . . 11
⊢ ((𝑃 − (𝑥 · 2)) ∈ ℕ ↔ ((𝑃 − (𝑥 · 2)) ∈ ℤ ∧ 1 ≤
(𝑃 − (𝑥 · 2)))) |
97 | 63, 95, 96 | sylanbrc 417 |
. . . . . . . . . 10
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈
ℕ) |
98 | 7 | simp2bi 1015 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1...𝐻) → 𝐻 ∈ ℕ) |
99 | 98 | ad2antll 491 |
. . . . . . . . . 10
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝐻 ∈ ℕ) |
100 | | nnre 8975 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
101 | 100 | rehalfcld 9215 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈
ℝ) |
102 | 101 | adantr 276 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 / 2) ∈
ℝ) |
103 | 61 | zred 9425 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℝ) |
104 | | lenlt 8081 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑥 · 2) ∈
ℝ) → ((𝑃 / 2)
≤ (𝑥 · 2) ↔
¬ (𝑥 · 2) <
(𝑃 / 2))) |
105 | 102, 103,
104 | syl2an 289 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2))) |
106 | 22, 61 | anim12i 338 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈
ℤ)) |
107 | 106, 30 | sylibr 134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) |
108 | | halfleoddlt 12009 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
→ ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
109 | 107, 108 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
110 | 109 | biimpa 296 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 / 2) < (𝑥 · 2)) |
111 | | nncn 8976 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℂ) |
112 | | subhalfhalf 9203 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℂ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
113 | 111, 112 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
114 | 113 | breq1d 4035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℕ → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
115 | 114 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
116 | 110, 115 | mpbird 167 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑃 / 2)) < (𝑥 · 2)) |
117 | 100 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℝ) |
118 | 101 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℝ) |
119 | 103 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℝ) |
120 | 117, 118,
119 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈
ℝ)) |
121 | 120 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈
ℝ)) |
122 | | ltsub23 8447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧
(𝑥 · 2) ∈
ℝ) → ((𝑃 −
(𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2))) |
123 | 121, 122 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2))) |
124 | 116, 123 | mpbid 147 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) < (𝑃 / 2)) |
125 | 21 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ) |
126 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ¬ 2 ∥ 𝑃) |
127 | 61 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ) |
128 | 125, 127 | zsubcld 9430 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 − (𝑥 · 2)) ∈
ℤ) |
129 | 125, 126,
128 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈
ℤ)) |
130 | 129 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈
ℤ)) |
131 | | ltoddhalfle 12008 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) |
132 | 130, 131 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) |
133 | 124, 132 | mpbid 147 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)) |
134 | 133 | ex 115 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) |
135 | 14 | breq2i 4033 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 − (𝑥 · 2)) ≤ 𝐻 ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)) |
136 | 134, 135 | imbitrrdi 162 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
137 | 105, 136 | sylbird 170 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
138 | 137 | ex 115 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))) |
139 | 19, 20, 138 | 3syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))) |
140 | 139 | imp 124 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
141 | 140 | impcom 125 |
. . . . . . . . . 10
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ≤ 𝐻) |
142 | | elfz1b 10142 |
. . . . . . . . . 10
⊢ ((𝑃 − (𝑥 · 2)) ∈ (1...𝐻) ↔ ((𝑃 − (𝑥 · 2)) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
143 | 97, 99, 141, 142 | syl3anbrc 1183 |
. . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ (1...𝐻)) |
144 | | eleq1 2252 |
. . . . . . . . 9
⊢ (𝑦 = (𝑃 − (𝑥 · 2)) → (𝑦 ∈ (1...𝐻) ↔ (𝑃 − (𝑥 · 2)) ∈ (1...𝐻))) |
145 | 143, 144 | syl5ibrcom 157 |
. . . . . . . 8
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑃 − (𝑥 · 2)) → 𝑦 ∈ (1...𝐻))) |
146 | 54, 145 | sylbid 150 |
. . . . . . 7
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
147 | 146 | ancoms 268 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝐻)) ∧ ¬ (𝑥 · 2) < (𝑃 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
148 | 61 | adantl 277 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ) |
149 | | zq 9677 |
. . . . . . . . 9
⊢ ((𝑥 · 2) ∈ ℤ
→ (𝑥 · 2)
∈ ℚ) |
150 | 148, 149 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℚ) |
151 | 57 | adantr 276 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ) |
152 | | znq 9675 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ 2 ∈
ℕ) → (𝑃 / 2)
∈ ℚ) |
153 | 151, 9, 152 | sylancl 413 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℚ) |
154 | | qdclt 10301 |
. . . . . . . 8
⊢ (((𝑥 · 2) ∈ ℚ
∧ (𝑃 / 2) ∈
ℚ) → DECID (𝑥 · 2) < (𝑃 / 2)) |
155 | 150, 153,
154 | syl2anc 411 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → DECID (𝑥 · 2) < (𝑃 / 2)) |
156 | | exmiddc 837 |
. . . . . . 7
⊢
(DECID (𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) < (𝑃 / 2) ∨ ¬ (𝑥 · 2) < (𝑃 / 2))) |
157 | 155, 156 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) ∨ ¬ (𝑥 · 2) < (𝑃 / 2))) |
158 | 51, 147, 157 | mpjaodan 799 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
159 | 158 | rexlimdva 2607 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
160 | | elfz1b 10142 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (1...𝐻) ↔ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) |
161 | | simp1 999 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℕ) |
162 | | simpl 109 |
. . . . . . . . . . . . . . 15
⊢ ((2
∥ 𝑦 ∧ 𝜑) → 2 ∥ 𝑦) |
163 | | nnehalf 12019 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 2 ∥
𝑦) → (𝑦 / 2) ∈
ℕ) |
164 | 161, 162,
163 | syl2anr 290 |
. . . . . . . . . . . . . 14
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ∈ ℕ) |
165 | | simpr2 1006 |
. . . . . . . . . . . . . 14
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ) |
166 | | nnre 8975 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
167 | 166 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → 𝑦 ∈ ℝ) |
168 | | nnrp 9715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻 ∈ ℕ → 𝐻 ∈
ℝ+) |
169 | 168 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → 𝐻 ∈
ℝ+) |
170 | 169 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → 𝐻 ∈
ℝ+) |
171 | | 2rp 9710 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ+ |
172 | | 1le2 9176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ≤
2 |
173 | 171, 172 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 ∈
ℝ+ ∧ 1 ≤ 2) |
174 | 173 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → (2 ∈
ℝ+ ∧ 1 ≤ 2)) |
175 | | ledivge1le 9778 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+
∧ (2 ∈ ℝ+ ∧ 1 ≤ 2)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)) |
176 | 167, 170,
174, 175 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)) |
177 | 176 | ex 115 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻))) |
178 | 177 | com23 78 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻))) |
179 | 178 | 3impia 1202 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻)) |
180 | 179 | impcom 125 |
. . . . . . . . . . . . . 14
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ≤ 𝐻) |
181 | 164, 165,
180 | 3jca 1179 |
. . . . . . . . . . . . 13
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) |
182 | 181 | ex 115 |
. . . . . . . . . . . 12
⊢ ((2
∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))) |
183 | 160, 182 | biimtrid 152 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))) |
184 | 183 | 3impia 1202 |
. . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) |
185 | | elfz1b 10142 |
. . . . . . . . . 10
⊢ ((𝑦 / 2) ∈ (1...𝐻) ↔ ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) |
186 | 184, 185 | sylibr 134 |
. . . . . . . . 9
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑦 / 2) ∈ (1...𝐻)) |
187 | | oveq1 5913 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 / 2) → (𝑥 · 2) = ((𝑦 / 2) · 2)) |
188 | 187 | breq1d 4035 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ ((𝑦 / 2) · 2) < (𝑃 / 2))) |
189 | 187 | oveq2d 5922 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − ((𝑦 / 2) · 2))) |
190 | 188, 187,
189 | ifbieq12d 3579 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))) |
191 | 190 | eqeq2d 2201 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))) |
192 | 191 | adantl 277 |
. . . . . . . . 9
⊢ (((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = (𝑦 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))) |
193 | | elfzelz 10077 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℤ) |
194 | 193 | zcnd 9426 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℂ) |
195 | 194 | 3ad2ant3 1022 |
. . . . . . . . . . . . 13
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ) |
196 | | 2cnd 9041 |
. . . . . . . . . . . . 13
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ) |
197 | | 2ap0 9061 |
. . . . . . . . . . . . . 14
⊢ 2 #
0 |
198 | 197 | a1i 9 |
. . . . . . . . . . . . 13
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 # 0) |
199 | 195, 196,
198 | divcanap1d 8796 |
. . . . . . . . . . . 12
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) = 𝑦) |
200 | 14 | breq2i 4033 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ≤ 𝐻 ↔ 𝑦 ≤ ((𝑃 − 1) / 2)) |
201 | | nnz 9322 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
202 | 19, 20, 22 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃)) |
203 | 202 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃)) |
204 | 201, 203 | anim12ci 339 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ)) |
205 | | df-3an 982 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ 𝑦 ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ 𝑦 ∈
ℤ)) |
206 | 204, 205 | sylibr 134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ)) |
207 | | ltoddhalfle 12008 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ 𝑦 ∈ ℤ) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2))) |
208 | 206, 207 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2))) |
209 | 208 | exbiri 382 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℕ → ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → 𝑦 < (𝑃 / 2)))) |
210 | 209 | com23 78 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))) |
211 | 200, 210 | biimtrid 152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))) |
212 | 211 | a1d 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))))) |
213 | 212 | 3imp 1195 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))) |
214 | 160, 213 | sylbi 121 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (1...𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))) |
215 | 214 | com12 30 |
. . . . . . . . . . . . 13
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → 𝑦 < (𝑃 / 2))) |
216 | 215 | 3impia 1202 |
. . . . . . . . . . . 12
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 < (𝑃 / 2)) |
217 | 199, 216 | eqbrtrd 4047 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) < (𝑃 / 2)) |
218 | 217 | iftrued 3560 |
. . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))) = ((𝑦 / 2) · 2)) |
219 | 218, 199 | eqtr2d 2223 |
. . . . . . . . 9
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))) |
220 | 186, 192,
219 | rspcedvd 2866 |
. . . . . . . 8
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
221 | 220 | 3expb 1206 |
. . . . . . 7
⊢ ((2
∥ 𝑦 ∧ (𝜑 ∧ 𝑦 ∈ (1...𝐻))) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
222 | 221 | ancoms 268 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 2 ∥ 𝑦) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
223 | 55, 56 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℤ) |
224 | 223 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℤ) |
225 | 201 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℤ) |
226 | 225 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℤ) |
227 | 224, 226 | zsubcld 9430 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℤ) |
228 | 166 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑦 ∈
ℝ) |
229 | 68 | rehalfcld 9215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → ((𝑃 − 1) / 2) ∈
ℝ) |
230 | 229 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → ((𝑃 − 1) / 2) ∈
ℝ) |
231 | | simpl 109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑃 ∈
ℝ) |
232 | 228, 230,
231 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈
ℝ)) |
233 | 232 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈
ℝ))) |
234 | 55, 64, 233 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ))) |
235 | 234 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ))) |
236 | 235 | impcom 125 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ)) |
237 | | lesub2 8462 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈ ℝ)
→ (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦))) |
238 | 236, 237 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦))) |
239 | 56 | zcnd 9426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
240 | | id 19 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℂ → 𝑃 ∈
ℂ) |
241 | | 1cnd 8021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℂ → 1 ∈
ℂ) |
242 | | 2cnd 9041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℂ → 2 ∈
ℂ) |
243 | 197 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℂ → 2 #
0) |
244 | 240, 241,
242, 243 | divsubdirapd 8835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℂ → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 /
2))) |
245 | 244 | oveq2d 5922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = (𝑃 − ((𝑃 / 2) − (1 / 2)))) |
246 | | halfcl 9194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℂ → (𝑃 / 2) ∈
ℂ) |
247 | | halfcn 9182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (1 / 2)
∈ ℂ |
248 | 247 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℂ → (1 / 2)
∈ ℂ) |
249 | 240, 246,
248 | subsubd 8344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 / 2) − (1 / 2))) = ((𝑃 − (𝑃 / 2)) + (1 / 2))) |
250 | 112 | oveq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℂ → ((𝑃 − (𝑃 / 2)) + (1 / 2)) = ((𝑃 / 2) + (1 / 2))) |
251 | 245, 249,
250 | 3eqtrd 2226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2))) |
252 | 55, 239, 251 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 /
2))) |
253 | 252 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 /
2))) |
254 | 253 | breq1d 4035 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) ↔ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦))) |
255 | | prmnn 12222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
256 | | halfre 9181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (1 / 2)
∈ ℝ |
257 | 256 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℕ → (1 / 2)
∈ ℝ) |
258 | | nngt0 8993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℕ → 0 <
𝑃) |
259 | 72 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℕ → (2 ∈
ℝ ∧ 0 < 2)) |
260 | | divgt0 8877 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃 ∈ ℝ ∧ 0 <
𝑃) ∧ (2 ∈ ℝ
∧ 0 < 2)) → 0 < (𝑃 / 2)) |
261 | 100, 258,
259, 260 | syl21anc 1248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℕ → 0 <
(𝑃 / 2)) |
262 | | halfgt0 9183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 0 < (1
/ 2) |
263 | 262 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℕ → 0 < (1
/ 2)) |
264 | 101, 257,
261, 263 | addgt0d 8526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℕ → 0 <
((𝑃 / 2) + (1 /
2))) |
265 | 55, 255, 264 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 0 < ((𝑃 / 2) + (1
/ 2))) |
266 | 265 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ 0 < ((𝑃 / 2) + (1
/ 2))) |
267 | | 0red 8006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 0 ∈
ℝ) |
268 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℝ) |
269 | 268 | rehalfcld 9215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈
ℝ) |
270 | 256 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 / 2)
∈ ℝ) |
271 | 269, 270 | readdcld 8035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) + (1 / 2)) ∈
ℝ) |
272 | | resubcl 8269 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ) |
273 | 272 | ancoms 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ) |
274 | 267, 271,
273 | 3jca 1179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)) |
275 | 274 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
276 | 166, 275 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
277 | 276 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
278 | 277 | com12 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
279 | 55, 64, 278 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
280 | 279 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
281 | 280 | impcom 125 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)) |
282 | | ltletr 8095 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦)) → 0 < (𝑃 − 𝑦))) |
283 | 281, 282 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((0 < ((𝑃 / 2) +
(1 / 2)) ∧ ((𝑃 / 2) +
(1 / 2)) ≤ (𝑃 −
𝑦)) → 0 < (𝑃 − 𝑦))) |
284 | 266, 283 | mpand 429 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (((𝑃 / 2) + (1 / 2))
≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦))) |
285 | 254, 284 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦))) |
286 | 238, 285 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ≤ ((𝑃 − 1) / 2) → 0 <
(𝑃 − 𝑦))) |
287 | 286 | ex 115 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑦 ≤ ((𝑃 − 1) / 2) → 0 <
(𝑃 − 𝑦)))) |
288 | 287 | com23 78 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦)))) |
289 | 200, 288 | biimtrid 152 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦)))) |
290 | 289 | 3impia 1202 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦))) |
291 | 290 | impcom 125 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 0 < (𝑃 − 𝑦)) |
292 | | elnnz 9313 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 − 𝑦) ∈ ℕ ↔ ((𝑃 − 𝑦) ∈ ℤ ∧ 0 < (𝑃 − 𝑦))) |
293 | 227, 291,
292 | sylanbrc 417 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℕ) |
294 | 23 | adantr 276 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)) |
295 | | simpr 110 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ¬ 2 ∥ 𝑦) |
296 | 295, 225 | anim12ci 339 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦)) |
297 | | omoe 12011 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ (𝑦 ∈ ℤ ∧ ¬ 2
∥ 𝑦)) → 2
∥ (𝑃 − 𝑦)) |
298 | 294, 296,
297 | syl2an2r 595 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 2 ∥ (𝑃 − 𝑦)) |
299 | | nnehalf 12019 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 − 𝑦) ∈ ℕ ∧ 2 ∥ (𝑃 − 𝑦)) → ((𝑃 − 𝑦) / 2) ∈ ℕ) |
300 | 293, 298,
299 | syl2anc 411 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ∈ ℕ) |
301 | | simpr2 1006 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ) |
302 | | 1red 8020 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 1 ∈
ℝ) |
303 | 166 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℝ) |
304 | 303 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℝ) |
305 | 55, 64 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℝ) |
306 | 305 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℝ) |
307 | | nnge1 8991 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℕ → 1 ≤
𝑦) |
308 | 307 | 3ad2ant1 1020 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 1 ≤ 𝑦) |
309 | 308 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 1 ≤ 𝑦) |
310 | 302, 304,
306, 309 | lesub2dd 8567 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ≤ (𝑃 − 1)) |
311 | 306, 304 | resubcld 8386 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℝ) |
312 | 55, 64, 68 | 3syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − 1) ∈
ℝ) |
313 | 312 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 1) ∈ ℝ) |
314 | 72 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (2 ∈ ℝ
∧ 0 < 2)) |
315 | | lediv1 8874 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 − 𝑦) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))) |
316 | 311, 313,
314, 315 | syl3anc 1249 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))) |
317 | 310, 316 | mpbid 147 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)) |
318 | 14 | breq2i 4033 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 − 𝑦) / 2) ≤ 𝐻 ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)) |
319 | 317, 318 | sylibr 134 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ 𝐻) |
320 | 300, 301,
319 | 3jca 1179 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)) |
321 | 320 | ex 115 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻))) |
322 | | elfz1b 10142 |
. . . . . . . . . . . . 13
⊢ (((𝑃 − 𝑦) / 2) ∈ (1...𝐻) ↔ (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)) |
323 | 321, 160,
322 | 3imtr4g 205 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))) |
324 | 323 | ex 115 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (¬ 2 ∥ 𝑦
→ (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))) |
325 | 19, 324 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))) |
326 | 325 | 3imp21 1200 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)) |
327 | | oveq1 5913 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑥 · 2) = (((𝑃 − 𝑦) / 2) · 2)) |
328 | 327 | breq1d 4035 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2))) |
329 | 327 | oveq2d 5922 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) |
330 | 328, 327,
329 | ifbieq12d 3579 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))) |
331 | 330 | eqeq2d 2201 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))) |
332 | 331 | adantl 277 |
. . . . . . . . 9
⊢ (((¬
2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = ((𝑃 − 𝑦) / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))) |
333 | 19, 55, 239 | 3syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℂ) |
334 | 333 | 3ad2ant2 1021 |
. . . . . . . . . . . . . 14
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑃 ∈ ℂ) |
335 | 194 | 3ad2ant3 1022 |
. . . . . . . . . . . . . 14
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ) |
336 | 334, 335 | subcld 8316 |
. . . . . . . . . . . . 13
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − 𝑦) ∈ ℂ) |
337 | | 2cnd 9041 |
. . . . . . . . . . . . 13
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ) |
338 | 197 | a1i 9 |
. . . . . . . . . . . . 13
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 # 0) |
339 | 336, 337,
338 | divcanap1d 8796 |
. . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (((𝑃 − 𝑦) / 2) · 2) = (𝑃 − 𝑦)) |
340 | | zre 9307 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℝ) |
341 | | halfge0 9184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ≤ (1
/ 2) |
342 | | rehalfcl 9195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈
ℝ) |
343 | 342 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈
ℝ) |
344 | 343, 270 | subge02d 8542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ≤
(1 / 2) ↔ ((𝑃 / 2)
− (1 / 2)) ≤ (𝑃 /
2))) |
345 | 341, 344 | mpbii 148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ≤
(𝑃 / 2)) |
346 | | simpl 109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑦 ∈
ℝ) |
347 | 256 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → (1 / 2)
∈ ℝ) |
348 | 342, 347 | resubcld 8386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) − (1 / 2)) ∈
ℝ) |
349 | 348 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ∈
ℝ) |
350 | | letr 8088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 / 2) − (1 / 2)) ∈
ℝ ∧ (𝑃 / 2)
∈ ℝ) → ((𝑦
≤ ((𝑃 / 2) − (1 /
2)) ∧ ((𝑃 / 2) −
(1 / 2)) ≤ (𝑃 / 2))
→ 𝑦 ≤ (𝑃 / 2))) |
351 | 346, 349,
343, 350 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤
(𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2))) |
352 | 345, 351 | mpan2d 428 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 / 2) − (1 / 2)) → 𝑦 ≤ (𝑃 / 2))) |
353 | 81 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℂ) |
354 | 353, 244 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 /
2))) |
355 | 354 | breq2d 4037 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ 𝑦 ≤ ((𝑃 / 2) − (1 / 2)))) |
356 | | lesub 8446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃 / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2)))) |
357 | 343, 268,
346, 356 | syl3anc 1249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2)))) |
358 | 269, 273 | lenltd 8123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
359 | | 2cnd 9041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑃 ∈ ℝ → 2 ∈
ℂ) |
360 | 197 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑃 ∈ ℝ → 2 #
0) |
361 | 81, 359, 360 | divcanap1d 8796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = 𝑃) |
362 | 361 | eqcomd 2195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → 𝑃 = ((𝑃 / 2) · 2)) |
363 | 362 | oveq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (((𝑃 / 2) · 2) − (𝑃 / 2))) |
364 | 342 | recnd 8034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈
ℂ) |
365 | 364, 359 | mulcomd 8027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = (2 ·
(𝑃 / 2))) |
366 | 365 | oveq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → (((𝑃 / 2) · 2) − (𝑃 / 2)) = ((2 · (𝑃 / 2)) − (𝑃 / 2))) |
367 | 359, 364 | mulsubfacd 8423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → ((2
· (𝑃 / 2)) −
(𝑃 / 2)) = ((2 − 1)
· (𝑃 /
2))) |
368 | | 2m1e1 9086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (2
− 1) = 1 |
369 | 368 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑃 ∈ ℝ → (2
− 1) = 1) |
370 | 369 | oveq1d 5921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → ((2
− 1) · (𝑃 /
2)) = (1 · (𝑃 /
2))) |
371 | 364 | mullidd 8023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → (1
· (𝑃 / 2)) = (𝑃 / 2)) |
372 | 367, 370,
371 | 3eqtrd 2226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → ((2
· (𝑃 / 2)) −
(𝑃 / 2)) = (𝑃 / 2)) |
373 | 363, 366,
372 | 3eqtrd 2226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
374 | 373 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
375 | 374 | breq2d 4037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ (𝑃 − (𝑃 / 2)) ↔ 𝑦 ≤ (𝑃 / 2))) |
376 | 357, 358,
375 | 3bitr3d 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (¬
(𝑃 − 𝑦) < (𝑃 / 2) ↔ 𝑦 ≤ (𝑃 / 2))) |
377 | 352, 355,
376 | 3imtr4d 203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
378 | 377 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
379 | 166, 378 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
380 | 379 | com3l 81 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
381 | 340, 380 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℤ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
382 | 19, 55, 56, 381 | 4syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
383 | 382 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
384 | 383 | com13 80 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((¬ 2 ∥
𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
385 | 200, 384 | biimtrid 152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
386 | 385 | a1d 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))) |
387 | 386 | 3imp 1195 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
388 | 387 | com12 30 |
. . . . . . . . . . . . . 14
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
389 | 160, 388 | biimtrid 152 |
. . . . . . . . . . . . 13
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
390 | 389 | 3impia 1202 |
. . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)) |
391 | 339, 390 | eqnbrtrd 4043 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2)) |
392 | 391 | iffalsed 3563 |
. . . . . . . . . 10
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) |
393 | 339 | oveq2d 5922 |
. . . . . . . . . 10
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (((𝑃 − 𝑦) / 2) · 2)) = (𝑃 − (𝑃 − 𝑦))) |
394 | 333, 194 | anim12i 338 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
395 | 394 | 3adant1 1017 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
396 | | nncan 8234 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑃 − (𝑃 − 𝑦)) = 𝑦) |
397 | 395, 396 | syl 14 |
. . . . . . . . . 10
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (𝑃 − 𝑦)) = 𝑦) |
398 | 392, 393,
397 | 3eqtrrd 2227 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))) |
399 | 326, 332,
398 | rspcedvd 2866 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
400 | 399 | 3expb 1206 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑦 ∧ (𝜑 ∧ 𝑦 ∈ (1...𝐻))) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
401 | 400 | ancoms 268 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ ¬ 2 ∥ 𝑦) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
402 | 9 | a1i 9 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℕ) |
403 | 193 | adantl 277 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℤ) |
404 | | dvdsdc 11915 |
. . . . . . . 8
⊢ ((2
∈ ℕ ∧ 𝑦
∈ ℤ) → DECID 2 ∥ 𝑦) |
405 | 402, 403,
404 | syl2anc 411 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → DECID 2 ∥
𝑦) |
406 | | exmiddc 837 |
. . . . . . 7
⊢
(DECID 2 ∥ 𝑦 → (2 ∥ 𝑦 ∨ ¬ 2 ∥ 𝑦)) |
407 | 405, 406 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (2 ∥ 𝑦 ∨ ¬ 2 ∥ 𝑦)) |
408 | 222, 401,
407 | mpjaodan 799 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
409 | 408 | ex 115 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))) |
410 | 159, 409 | impbid 129 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 ∈ (1...𝐻))) |
411 | 3, 410 | bitrid 192 |
. 2
⊢ (𝜑 → (𝑦 ∈ ran 𝑅 ↔ 𝑦 ∈ (1...𝐻))) |
412 | 411 | eqrdv 2187 |
1
⊢ (𝜑 → ran 𝑅 = (1...𝐻)) |