Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.r |
. . . . 5
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
2 | 1 | elrnmpt 5962 |
. . . 4
⊢ (𝑦 ∈ V → (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))) |
3 | 2 | elv 3468 |
. . 3
⊢ (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
4 | | iftrue 4539 |
. . . . . . . . 9
⊢ ((𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑥 · 2)) |
5 | 4 | eqeq2d 2737 |
. . . . . . . 8
⊢ ((𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2))) |
6 | 5 | adantr 479 |
. . . . . . 7
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2))) |
7 | | elfz1b 13624 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝐻) ↔ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻)) |
8 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) |
9 | | 2nn 12337 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℕ |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ → 2 ∈
ℕ) |
11 | 8, 10 | nnmulcld 12317 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℕ) |
12 | 11 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℕ) |
13 | 12 | 3ad2ant1 1130 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ∈ ℕ) |
14 | | gausslemma2d.h |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = ((𝑃 − 1) / 2) |
15 | 14 | eleq1i 2817 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻 ∈ ℕ ↔ ((𝑃 − 1) / 2) ∈
ℕ) |
16 | 15 | biimpi 215 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ ℕ → ((𝑃 − 1) / 2) ∈
ℕ) |
17 | 16 | 3ad2ant2 1131 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → ((𝑃 − 1) / 2) ∈
ℕ) |
18 | 17 | 3ad2ant1 1130 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑃 − 1) / 2) ∈
ℕ) |
19 | | gausslemma2d.p |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
20 | | nnoddn2prm 16813 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℕ
∧ ¬ 2 ∥ 𝑃)) |
21 | | nnz 12631 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) |
22 | 21 | anim1i 613 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃)) |
23 | 20, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)) |
24 | | nnz 12631 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
25 | | 2z 12646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℤ |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℕ → 2 ∈
ℤ) |
27 | 24, 26 | zmulcld 12724 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℤ) |
28 | 27 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℤ) |
29 | 23, 28 | anim12i 611 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ (𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈
ℤ)) |
30 | | df-3an 1086 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
↔ ((𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)
∧ (𝑥 · 2) ∈
ℤ)) |
31 | 29, 30 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ (𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) |
32 | 31 | ex 411 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ))) |
33 | 19, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ))) |
34 | 33 | impcom 406 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) |
35 | | ltoddhalfle 16363 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
→ ((𝑥 · 2) <
(𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) /
2))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2))) |
37 | 36 | biimp3a 1466 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ≤ ((𝑃 − 1) / 2)) |
38 | 13, 18, 37 | 3jca 1125 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) |
39 | 38 | 3exp 1116 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))))) |
40 | 7, 39 | sylbi 216 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1...𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))))) |
41 | 40 | impcom 406 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2)))) |
42 | 41 | impcom 406 |
. . . . . . . . 9
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) |
43 | 14 | oveq2i 7435 |
. . . . . . . . . . 11
⊢
(1...𝐻) =
(1...((𝑃 − 1) /
2)) |
44 | 43 | eleq2i 2818 |
. . . . . . . . . 10
⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...((𝑃 − 1) / 2))) |
45 | | elfz1b 13624 |
. . . . . . . . . 10
⊢ ((𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)) ↔ ((𝑥 · 2) ∈ ℕ
∧ ((𝑃 − 1) / 2)
∈ ℕ ∧ (𝑥
· 2) ≤ ((𝑃
− 1) / 2))) |
46 | 44, 45 | bitri 274 |
. . . . . . . . 9
⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) |
47 | 42, 46 | sylibr 233 |
. . . . . . . 8
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ (1...𝐻)) |
48 | | eleq1 2814 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 · 2) → (𝑦 ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...𝐻))) |
49 | 47, 48 | syl5ibrcom 246 |
. . . . . . 7
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑥 · 2) → 𝑦 ∈ (1...𝐻))) |
50 | 6, 49 | sylbid 239 |
. . . . . 6
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
51 | | iffalse 4542 |
. . . . . . . . 9
⊢ (¬
(𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑥 · 2))) |
52 | 51 | eqeq2d 2737 |
. . . . . . . 8
⊢ (¬
(𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2)))) |
53 | 52 | adantr 479 |
. . . . . . 7
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2)))) |
54 | | eldifi 4126 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
55 | | prmz 16676 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
56 | 19, 54, 55 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℤ) |
57 | 56 | ad2antrl 726 |
. . . . . . . . . . 11
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝑃 ∈ ℤ) |
58 | | elfzelz 13555 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝐻) → 𝑥 ∈ ℤ) |
59 | 25 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝐻) → 2 ∈ ℤ) |
60 | 58, 59 | zmulcld 12724 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℤ) |
61 | 60 | ad2antll 727 |
. . . . . . . . . . 11
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ ℤ) |
62 | 57, 61 | zsubcld 12723 |
. . . . . . . . . 10
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈
ℤ) |
63 | 55 | zred 12718 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) |
64 | 14 | breq2i 5161 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ≤ 𝐻 ↔ 𝑥 ≤ ((𝑃 − 1) / 2)) |
65 | | nnre 12271 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
66 | 65 | adantr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑥 ∈
ℝ) |
67 | | peano2rem 11577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
68 | 67 | adantl 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − 1) ∈
ℝ) |
69 | | 2re 12338 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ |
70 | | 2pos 12367 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
2 |
71 | 69, 70 | pm3.2i 469 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℝ ∧ 0 < 2) |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (2
∈ ℝ ∧ 0 < 2)) |
73 | | lemuldiv 12146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
74 | 66, 68, 72, 73 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) |
75 | 64, 74 | bitr4id 289 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 ↔ (𝑥 · 2) ≤ (𝑃 − 1))) |
76 | 11 | nnred 12279 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℝ) |
77 | 76 | adantr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 · 2) ∈
ℝ) |
78 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℝ) |
79 | 77, 68, 78 | lesub2d 11872 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ (𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)))) |
80 | | recn 11248 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℝ → 𝑃 ∈
ℂ) |
81 | | 1cnd 11259 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℝ → 1 ∈
ℂ) |
82 | 80, 81 | nncand 11626 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 − 1)) = 1) |
83 | 82 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 − 1)) = 1) |
84 | 83 | breq1d 5163 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) ↔ 1 ≤ (𝑃 − (𝑥 · 2)))) |
85 | 84 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
86 | 79, 85 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
87 | 75, 86 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 → 1 ≤ (𝑃 − (𝑥 · 2)))) |
88 | 87 | impancom 450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) |
89 | 88 | 3adant2 1128 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) |
90 | 7, 89 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) |
91 | 90 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℝ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
92 | 19, 54, 63, 91 | 4syl 19 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2)))) |
93 | 92 | imp 405 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 1 ≤ (𝑃 − (𝑥 · 2))) |
94 | 93 | adantl 480 |
. . . . . . . . . 10
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 1 ≤ (𝑃 − (𝑥 · 2))) |
95 | | elnnz1 12640 |
. . . . . . . . . 10
⊢ ((𝑃 − (𝑥 · 2)) ∈ ℕ ↔ ((𝑃 − (𝑥 · 2)) ∈ ℤ ∧ 1 ≤
(𝑃 − (𝑥 · 2)))) |
96 | 62, 94, 95 | sylanbrc 581 |
. . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈
ℕ) |
97 | 7 | simp2bi 1143 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...𝐻) → 𝐻 ∈ ℕ) |
98 | 97 | ad2antll 727 |
. . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝐻 ∈ ℕ) |
99 | | nnre 12271 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
100 | 99 | rehalfcld 12511 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈
ℝ) |
101 | 100 | adantr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 / 2) ∈
ℝ) |
102 | 60 | zred 12718 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℝ) |
103 | | lenlt 11342 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑥 · 2) ∈
ℝ) → ((𝑃 / 2)
≤ (𝑥 · 2) ↔
¬ (𝑥 · 2) <
(𝑃 / 2))) |
104 | 101, 102,
103 | syl2an 594 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2))) |
105 | 22, 60 | anim12i 611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈
ℤ)) |
106 | 105, 30 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) |
107 | | halfleoddlt 16364 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
→ ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
109 | 108 | biimpa 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 / 2) < (𝑥 · 2)) |
110 | | nncn 12272 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℂ) |
111 | | subhalfhalf 12498 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℂ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℕ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
113 | 112 | breq1d 5163 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℕ → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
114 | 113 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) |
115 | 109, 114 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑃 / 2)) < (𝑥 · 2)) |
116 | 99 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℝ) |
117 | 100 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℝ) |
118 | 102 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℝ) |
119 | 116, 117,
118 | 3jca 1125 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈
ℝ)) |
120 | 119 | adantr 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈
ℝ)) |
121 | | ltsub23 11744 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧
(𝑥 · 2) ∈
ℝ) → ((𝑃 −
(𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2))) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2))) |
123 | 115, 122 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) < (𝑃 / 2)) |
124 | 21 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ) |
125 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ¬ 2 ∥ 𝑃) |
126 | 60 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ) |
127 | 124, 126 | zsubcld 12723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 − (𝑥 · 2)) ∈
ℤ) |
128 | 124, 125,
127 | 3jca 1125 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈
ℤ)) |
129 | 128 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈
ℤ)) |
130 | | ltoddhalfle 16363 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) |
132 | 123, 131 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)) |
133 | 132 | ex 411 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) |
134 | 14 | breq2i 5161 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 − (𝑥 · 2)) ≤ 𝐻 ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)) |
135 | 133, 134 | imbitrrdi 251 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
136 | 104, 135 | sylbird 259 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
137 | 136 | ex 411 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))) |
138 | 19, 20, 137 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))) |
139 | 138 | imp 405 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
140 | 139 | impcom 406 |
. . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ≤ 𝐻) |
141 | | elfz1b 13624 |
. . . . . . . . 9
⊢ ((𝑃 − (𝑥 · 2)) ∈ (1...𝐻) ↔ ((𝑃 − (𝑥 · 2)) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑃 − (𝑥 · 2)) ≤ 𝐻)) |
142 | 96, 98, 140, 141 | syl3anbrc 1340 |
. . . . . . . 8
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ (1...𝐻)) |
143 | | eleq1 2814 |
. . . . . . . 8
⊢ (𝑦 = (𝑃 − (𝑥 · 2)) → (𝑦 ∈ (1...𝐻) ↔ (𝑃 − (𝑥 · 2)) ∈ (1...𝐻))) |
144 | 142, 143 | syl5ibrcom 246 |
. . . . . . 7
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑃 − (𝑥 · 2)) → 𝑦 ∈ (1...𝐻))) |
145 | 53, 144 | sylbid 239 |
. . . . . 6
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
146 | 50, 145 | pm2.61ian 810 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
147 | 146 | rexlimdva 3145 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) |
148 | | elfz1b 13624 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (1...𝐻) ↔ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) |
149 | | simp1 1133 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℕ) |
150 | | simpl 481 |
. . . . . . . . . . . . 13
⊢ ((2
∥ 𝑦 ∧ 𝜑) → 2 ∥ 𝑦) |
151 | | nnehalf 16381 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 2 ∥
𝑦) → (𝑦 / 2) ∈
ℕ) |
152 | 149, 150,
151 | syl2anr 595 |
. . . . . . . . . . . 12
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ∈ ℕ) |
153 | | simpr2 1192 |
. . . . . . . . . . . 12
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ) |
154 | | nnre 12271 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
155 | 154 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → 𝑦 ∈ ℝ) |
156 | | nnrp 13039 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 ∈ ℕ → 𝐻 ∈
ℝ+) |
157 | 156 | adantl 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → 𝐻 ∈
ℝ+) |
158 | 157 | adantr 479 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → 𝐻 ∈
ℝ+) |
159 | | 2rp 13033 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ |
160 | | 1le2 12473 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ≤
2 |
161 | 159, 160 | pm3.2i 469 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 ∈
ℝ+ ∧ 1 ≤ 2) |
162 | 161 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → (2 ∈
ℝ+ ∧ 1 ≤ 2)) |
163 | | ledivge1le 13099 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+
∧ (2 ∈ ℝ+ ∧ 1 ≤ 2)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)) |
164 | 155, 158,
162, 163 | syl3anc 1368 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)) |
165 | 164 | ex 411 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻))) |
166 | 165 | com23 86 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻))) |
167 | 166 | 3impia 1114 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻)) |
168 | 167 | impcom 406 |
. . . . . . . . . . . 12
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ≤ 𝐻) |
169 | 152, 153,
168 | 3jca 1125 |
. . . . . . . . . . 11
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) |
170 | 169 | ex 411 |
. . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))) |
171 | 148, 170 | biimtrid 241 |
. . . . . . . . 9
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))) |
172 | 171 | 3impia 1114 |
. . . . . . . 8
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) |
173 | | elfz1b 13624 |
. . . . . . . 8
⊢ ((𝑦 / 2) ∈ (1...𝐻) ↔ ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) |
174 | 172, 173 | sylibr 233 |
. . . . . . 7
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑦 / 2) ∈ (1...𝐻)) |
175 | | oveq1 7431 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 / 2) → (𝑥 · 2) = ((𝑦 / 2) · 2)) |
176 | 175 | breq1d 5163 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ ((𝑦 / 2) · 2) < (𝑃 / 2))) |
177 | 175 | oveq2d 7440 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − ((𝑦 / 2) · 2))) |
178 | 176, 175,
177 | ifbieq12d 4561 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))) |
179 | 178 | eqeq2d 2737 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))) |
180 | 179 | adantl 480 |
. . . . . . 7
⊢ (((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = (𝑦 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))) |
181 | | elfzelz 13555 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℤ) |
182 | 181 | zcnd 12719 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℂ) |
183 | 182 | 3ad2ant3 1132 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ) |
184 | | 2cnd 12342 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ) |
185 | | 2ne0 12368 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
186 | 185 | a1i 11 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ≠ 0) |
187 | 183, 184,
186 | divcan1d 12042 |
. . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) = 𝑦) |
188 | 14 | breq2i 5161 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ≤ 𝐻 ↔ 𝑦 ≤ ((𝑃 − 1) / 2)) |
189 | | nnz 12631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
190 | 19, 20, 22 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃)) |
191 | 190 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃)) |
192 | 189, 191 | anim12ci 612 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ)) |
193 | | df-3an 1086 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ 𝑦 ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ 𝑦 ∈
ℤ)) |
194 | 192, 193 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ)) |
195 | | ltoddhalfle 16363 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ 𝑦 ∈ ℤ) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2))) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2))) |
197 | 196 | exbiri 809 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → 𝑦 < (𝑃 / 2)))) |
198 | 197 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))) |
199 | 188, 198 | biimtrid 241 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))) |
200 | 199 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))))) |
201 | 200 | 3imp 1108 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))) |
202 | 148, 201 | sylbi 216 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (1...𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))) |
203 | 202 | com12 32 |
. . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → 𝑦 < (𝑃 / 2))) |
204 | 203 | 3impia 1114 |
. . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 < (𝑃 / 2)) |
205 | 187, 204 | eqbrtrd 5175 |
. . . . . . . . 9
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) < (𝑃 / 2)) |
206 | 205 | iftrued 4541 |
. . . . . . . 8
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))) = ((𝑦 / 2) · 2)) |
207 | 206, 187 | eqtr2d 2767 |
. . . . . . 7
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))) |
208 | 174, 180,
207 | rspcedvd 3610 |
. . . . . 6
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
209 | 208 | 3exp 1116 |
. . . . 5
⊢ (2
∥ 𝑦 → (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))) |
210 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℤ) |
211 | 210 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℤ) |
212 | 189 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℤ) |
213 | 212 | adantl 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℤ) |
214 | 211, 213 | zsubcld 12723 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℤ) |
215 | 154 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑦 ∈
ℝ) |
216 | 67 | rehalfcld 12511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → ((𝑃 − 1) / 2) ∈
ℝ) |
217 | 216 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → ((𝑃 − 1) / 2) ∈
ℝ) |
218 | | simpl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑃 ∈
ℝ) |
219 | 215, 217,
218 | 3jca 1125 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈
ℝ)) |
220 | 219 | ex 411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈
ℝ))) |
221 | 54, 63, 220 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ))) |
222 | 221 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ))) |
223 | 222 | impcom 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ)) |
224 | | lesub2 11759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈ ℝ)
→ (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦))) |
225 | 223, 224 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦))) |
226 | 55 | zcnd 12719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
227 | | 1cnd 11259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℂ → 1 ∈
ℂ) |
228 | | 2cnne0 12474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
229 | 228 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℂ → (2 ∈
ℂ ∧ 2 ≠ 0)) |
230 | | divsubdir 11959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2))) |
231 | 227, 229,
230 | mpd3an23 1460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 /
2))) |
232 | 231 | oveq2d 7440 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = (𝑃 − ((𝑃 / 2) − (1 / 2)))) |
233 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → 𝑃 ∈
ℂ) |
234 | | halfcl 12489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → (𝑃 / 2) ∈
ℂ) |
235 | | halfcn 12479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 / 2)
∈ ℂ |
236 | 235 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → (1 / 2)
∈ ℂ) |
237 | 233, 234,
236 | subsubd 11649 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 / 2) − (1 / 2))) = ((𝑃 − (𝑃 / 2)) + (1 / 2))) |
238 | 111 | oveq1d 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℂ → ((𝑃 − (𝑃 / 2)) + (1 / 2)) = ((𝑃 / 2) + (1 / 2))) |
239 | 232, 237,
238 | 3eqtrd 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2))) |
240 | 54, 226, 239 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 /
2))) |
241 | 240 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 /
2))) |
242 | 241 | breq1d 5163 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) ↔ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦))) |
243 | | prmnn 16675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
244 | | halfre 12478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (1 / 2)
∈ ℝ |
245 | 244 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ → (1 / 2)
∈ ℝ) |
246 | | nngt0 12295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℕ → 0 <
𝑃) |
247 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℕ → (2 ∈
ℝ ∧ 0 < 2)) |
248 | | divgt0 12134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑃 ∈ ℝ ∧ 0 <
𝑃) ∧ (2 ∈ ℝ
∧ 0 < 2)) → 0 < (𝑃 / 2)) |
249 | 99, 246, 247, 248 | syl21anc 836 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ → 0 <
(𝑃 / 2)) |
250 | | halfgt0 12480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 < (1
/ 2) |
251 | 250 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ → 0 < (1
/ 2)) |
252 | 100, 245,
249, 251 | addgt0d 11839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℕ → 0 <
((𝑃 / 2) + (1 /
2))) |
253 | 54, 243, 252 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 0 < ((𝑃 / 2) + (1
/ 2))) |
254 | 253 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ 0 < ((𝑃 / 2) + (1
/ 2))) |
255 | | 0red 11267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 0 ∈
ℝ) |
256 | | simpr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℝ) |
257 | 256 | rehalfcld 12511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈
ℝ) |
258 | 244 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 / 2)
∈ ℝ) |
259 | 257, 258 | readdcld 11293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) + (1 / 2)) ∈
ℝ) |
260 | | resubcl 11574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ) |
261 | 260 | ancoms 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ) |
262 | 255, 259,
261 | 3jca 1125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)) |
263 | 262 | ex 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
264 | 154, 263 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
265 | 264 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
266 | 265 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
267 | 54, 63, 266 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
268 | 267 | adantr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) |
269 | 268 | impcom 406 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)) |
270 | | ltletr 11356 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦)) → 0 < (𝑃 − 𝑦))) |
271 | 269, 270 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((0 < ((𝑃 / 2) +
(1 / 2)) ∧ ((𝑃 / 2) +
(1 / 2)) ≤ (𝑃 −
𝑦)) → 0 < (𝑃 − 𝑦))) |
272 | 254, 271 | mpand 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (((𝑃 / 2) + (1 / 2))
≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦))) |
273 | 242, 272 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦))) |
274 | 225, 273 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ≤ ((𝑃 − 1) / 2) → 0 <
(𝑃 − 𝑦))) |
275 | 274 | ex 411 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑦 ≤ ((𝑃 − 1) / 2) → 0 <
(𝑃 − 𝑦)))) |
276 | 275 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦)))) |
277 | 188, 276 | biimtrid 241 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦)))) |
278 | 277 | 3impia 1114 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦))) |
279 | 278 | impcom 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 0 < (𝑃 − 𝑦)) |
280 | | elnnz 12620 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 − 𝑦) ∈ ℕ ↔ ((𝑃 − 𝑦) ∈ ℤ ∧ 0 < (𝑃 − 𝑦))) |
281 | 214, 279,
280 | sylanbrc 581 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℕ) |
282 | 23 | adantr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)) |
283 | | simpr 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ¬ 2 ∥ 𝑦) |
284 | 283, 212 | anim12ci 612 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦)) |
285 | | omoe 16366 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ (𝑦 ∈ ℤ ∧ ¬ 2
∥ 𝑦)) → 2
∥ (𝑃 − 𝑦)) |
286 | 282, 284,
285 | syl2an2r 683 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 2 ∥ (𝑃 − 𝑦)) |
287 | | nnehalf 16381 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 − 𝑦) ∈ ℕ ∧ 2 ∥ (𝑃 − 𝑦)) → ((𝑃 − 𝑦) / 2) ∈ ℕ) |
288 | 281, 286,
287 | syl2anc 582 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ∈ ℕ) |
289 | | simpr2 1192 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ) |
290 | | 1red 11265 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 1 ∈
ℝ) |
291 | 154 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℝ) |
292 | 291 | adantl 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℝ) |
293 | 54, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℝ) |
294 | 293 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℝ) |
295 | | nnge1 12292 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 1 ≤
𝑦) |
296 | 295 | 3ad2ant1 1130 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 1 ≤ 𝑦) |
297 | 296 | adantl 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 1 ≤ 𝑦) |
298 | 290, 292,
294, 297 | lesub2dd 11881 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ≤ (𝑃 − 1)) |
299 | 294, 292 | resubcld 11692 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℝ) |
300 | 54, 63, 67 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − 1) ∈
ℝ) |
301 | 300 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 1) ∈ ℝ) |
302 | 71 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (2 ∈ ℝ
∧ 0 < 2)) |
303 | | lediv1 12131 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 − 𝑦) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))) |
304 | 299, 301,
302, 303 | syl3anc 1368 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))) |
305 | 298, 304 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)) |
306 | 14 | breq2i 5161 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 − 𝑦) / 2) ≤ 𝐻 ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)) |
307 | 305, 306 | sylibr 233 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ 𝐻) |
308 | 288, 289,
307 | 3jca 1125 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)) |
309 | 308 | ex 411 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻))) |
310 | | elfz1b 13624 |
. . . . . . . . . . 11
⊢ (((𝑃 − 𝑦) / 2) ∈ (1...𝐻) ↔ (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)) |
311 | 309, 148,
310 | 3imtr4g 295 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))) |
312 | 311 | ex 411 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (¬ 2 ∥ 𝑦
→ (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))) |
313 | 19, 312 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))) |
314 | 313 | 3imp21 1111 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)) |
315 | | oveq1 7431 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑥 · 2) = (((𝑃 − 𝑦) / 2) · 2)) |
316 | 315 | breq1d 5163 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2))) |
317 | 315 | oveq2d 7440 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) |
318 | 316, 315,
317 | ifbieq12d 4561 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))) |
319 | 318 | eqeq2d 2737 |
. . . . . . . 8
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))) |
320 | 319 | adantl 480 |
. . . . . . 7
⊢ (((¬
2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = ((𝑃 − 𝑦) / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))) |
321 | 19, 54, 226 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℂ) |
322 | 321 | 3ad2ant2 1131 |
. . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑃 ∈ ℂ) |
323 | 182 | 3ad2ant3 1132 |
. . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ) |
324 | 322, 323 | subcld 11621 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − 𝑦) ∈ ℂ) |
325 | | 2cnd 12342 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ) |
326 | 185 | a1i 11 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ≠ 0) |
327 | 324, 325,
326 | divcan1d 12042 |
. . . . . . . . . 10
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (((𝑃 − 𝑦) / 2) · 2) = (𝑃 − 𝑦)) |
328 | | zre 12614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℝ) |
329 | | halfge0 12481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ≤ (1
/ 2) |
330 | | rehalfcl 12490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈
ℝ) |
331 | 330 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈
ℝ) |
332 | 331, 258 | subge02d 11856 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ≤
(1 / 2) ↔ ((𝑃 / 2)
− (1 / 2)) ≤ (𝑃 /
2))) |
333 | 329, 332 | mpbii 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ≤
(𝑃 / 2)) |
334 | | simpl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑦 ∈
ℝ) |
335 | 244 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → (1 / 2)
∈ ℝ) |
336 | 330, 335 | resubcld 11692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) − (1 / 2)) ∈
ℝ) |
337 | 336 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ∈
ℝ) |
338 | | letr 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 / 2) − (1 / 2)) ∈
ℝ ∧ (𝑃 / 2)
∈ ℝ) → ((𝑦
≤ ((𝑃 / 2) − (1 /
2)) ∧ ((𝑃 / 2) −
(1 / 2)) ≤ (𝑃 / 2))
→ 𝑦 ≤ (𝑃 / 2))) |
339 | 334, 337,
331, 338 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤
(𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2))) |
340 | 333, 339 | mpan2d 692 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 / 2) − (1 / 2)) → 𝑦 ≤ (𝑃 / 2))) |
341 | 80 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℂ) |
342 | | 1cnd 11259 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 1 ∈
ℂ) |
343 | 228 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (2
∈ ℂ ∧ 2 ≠ 0)) |
344 | 341, 342,
343, 230 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 /
2))) |
345 | 344 | breq2d 5165 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ 𝑦 ≤ ((𝑃 / 2) − (1 / 2)))) |
346 | | lesub 11743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2)))) |
347 | 331, 256,
334, 346 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2)))) |
348 | 257, 261 | lenltd 11410 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
349 | | 2cnd 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → 2 ∈
ℂ) |
350 | 185 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → 2 ≠
0) |
351 | 80, 349, 350 | divcan1d 12042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = 𝑃) |
352 | 351 | eqcomd 2732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → 𝑃 = ((𝑃 / 2) · 2)) |
353 | 352 | oveq1d 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (((𝑃 / 2) · 2) − (𝑃 / 2))) |
354 | 330 | recnd 11292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈
ℂ) |
355 | 354, 349 | mulcomd 11285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = (2 ·
(𝑃 / 2))) |
356 | 355 | oveq1d 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → (((𝑃 / 2) · 2) − (𝑃 / 2)) = ((2 · (𝑃 / 2)) − (𝑃 / 2))) |
357 | 349, 354 | mulsubfacd 11725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → ((2
· (𝑃 / 2)) −
(𝑃 / 2)) = ((2 − 1)
· (𝑃 /
2))) |
358 | | 2m1e1 12390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (2
− 1) = 1 |
359 | 358 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → (2
− 1) = 1) |
360 | 359 | oveq1d 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → ((2
− 1) · (𝑃 /
2)) = (1 · (𝑃 /
2))) |
361 | 354 | mullidd 11282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → (1
· (𝑃 / 2)) = (𝑃 / 2)) |
362 | 357, 360,
361 | 3eqtrd 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → ((2
· (𝑃 / 2)) −
(𝑃 / 2)) = (𝑃 / 2)) |
363 | 353, 356,
362 | 3eqtrd 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
364 | 363 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) |
365 | 364 | breq2d 5165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ (𝑃 − (𝑃 / 2)) ↔ 𝑦 ≤ (𝑃 / 2))) |
366 | 347, 348,
365 | 3bitr3d 308 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (¬
(𝑃 − 𝑦) < (𝑃 / 2) ↔ 𝑦 ≤ (𝑃 / 2))) |
367 | 340, 345,
366 | 3imtr4d 293 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
368 | 367 | ex 411 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
369 | 154, 368 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
370 | 369 | com3l 89 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
371 | 328, 370 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℤ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
372 | 19, 54, 55, 371 | 4syl 19 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
373 | 372 | adantl 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
374 | 373 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((¬ 2 ∥
𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
375 | 188, 374 | biimtrid 241 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) |
376 | 375 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))) |
377 | 376 | 3imp 1108 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
378 | 377 | com12 32 |
. . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
379 | 148, 378 | biimtrid 241 |
. . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) |
380 | 379 | 3impia 1114 |
. . . . . . . . . 10
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)) |
381 | 327, 380 | eqnbrtrd 5171 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2)) |
382 | 381 | iffalsed 4544 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) |
383 | 327 | oveq2d 7440 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (((𝑃 − 𝑦) / 2) · 2)) = (𝑃 − (𝑃 − 𝑦))) |
384 | 321, 182 | anim12i 611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
385 | 384 | 3adant1 1127 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
386 | | nncan 11539 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑃 − (𝑃 − 𝑦)) = 𝑦) |
387 | 385, 386 | syl 17 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (𝑃 − 𝑦)) = 𝑦) |
388 | 382, 383,
387 | 3eqtrrd 2771 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))) |
389 | 314, 320,
388 | rspcedvd 3610 |
. . . . . 6
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
390 | 389 | 3exp 1116 |
. . . . 5
⊢ (¬ 2
∥ 𝑦 → (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))) |
391 | 209, 390 | pm2.61i 182 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))) |
392 | 147, 391 | impbid 211 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 ∈ (1...𝐻))) |
393 | 3, 392 | bitrid 282 |
. 2
⊢ (𝜑 → (𝑦 ∈ ran 𝑅 ↔ 𝑦 ∈ (1...𝐻))) |
394 | 393 | eqrdv 2724 |
1
⊢ (𝜑 → ran 𝑅 = (1...𝐻)) |