| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | gausslemma2d.r | . . . . 5
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) | 
| 2 | 1 | elrnmpt 5969 | . . . 4
⊢ (𝑦 ∈ V → (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))) | 
| 3 | 2 | elv 3485 | . . 3
⊢ (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) | 
| 4 |  | iftrue 4531 | . . . . . . . . 9
⊢ ((𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑥 · 2)) | 
| 5 | 4 | eqeq2d 2748 | . . . . . . . 8
⊢ ((𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2))) | 
| 6 | 5 | adantr 480 | . . . . . . 7
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2))) | 
| 7 |  | elfz1b 13633 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝐻) ↔ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻)) | 
| 8 |  | id 22 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) | 
| 9 |  | 2nn 12339 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℕ | 
| 10 | 9 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ → 2 ∈
ℕ) | 
| 11 | 8, 10 | nnmulcld 12319 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℕ) | 
| 12 | 11 | 3ad2ant1 1134 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℕ) | 
| 13 | 12 | 3ad2ant1 1134 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ∈ ℕ) | 
| 14 |  | gausslemma2d.h | . . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = ((𝑃 − 1) / 2) | 
| 15 | 14 | eleq1i 2832 | . . . . . . . . . . . . . . . . 17
⊢ (𝐻 ∈ ℕ ↔ ((𝑃 − 1) / 2) ∈
ℕ) | 
| 16 | 15 | biimpi 216 | . . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ ℕ → ((𝑃 − 1) / 2) ∈
ℕ) | 
| 17 | 16 | 3ad2ant2 1135 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → ((𝑃 − 1) / 2) ∈
ℕ) | 
| 18 | 17 | 3ad2ant1 1134 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑃 − 1) / 2) ∈
ℕ) | 
| 19 |  | gausslemma2d.p | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) | 
| 20 |  | nnoddn2prm 16849 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℕ
∧ ¬ 2 ∥ 𝑃)) | 
| 21 |  | nnz 12634 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) | 
| 22 | 21 | anim1i 615 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃)) | 
| 23 | 20, 22 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)) | 
| 24 |  | nnz 12634 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) | 
| 25 |  | 2z 12649 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℤ | 
| 26 | 25 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℕ → 2 ∈
ℤ) | 
| 27 | 24, 26 | zmulcld 12728 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℤ) | 
| 28 | 27 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℤ) | 
| 29 | 23, 28 | anim12i 613 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ (𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈
ℤ)) | 
| 30 |  | df-3an 1089 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
↔ ((𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)
∧ (𝑥 · 2) ∈
ℤ)) | 
| 31 | 29, 30 | sylibr 234 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ (𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) | 
| 32 | 31 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑥 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ))) | 
| 33 | 19, 32 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ))) | 
| 34 | 33 | impcom 407 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) | 
| 35 |  | ltoddhalfle 16398 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
→ ((𝑥 · 2) <
(𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) /
2))) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2))) | 
| 37 | 36 | biimp3a 1471 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ≤ ((𝑃 − 1) / 2)) | 
| 38 | 13, 18, 37 | 3jca 1129 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) | 
| 39 | 38 | 3exp 1120 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))))) | 
| 40 | 7, 39 | sylbi 217 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (1...𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))))) | 
| 41 | 40 | impcom 407 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2)))) | 
| 42 | 41 | impcom 407 | . . . . . . . . 9
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) | 
| 43 | 14 | oveq2i 7442 | . . . . . . . . . . 11
⊢
(1...𝐻) =
(1...((𝑃 − 1) /
2)) | 
| 44 | 43 | eleq2i 2833 | . . . . . . . . . 10
⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...((𝑃 − 1) / 2))) | 
| 45 |  | elfz1b 13633 | . . . . . . . . . 10
⊢ ((𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)) ↔ ((𝑥 · 2) ∈ ℕ
∧ ((𝑃 − 1) / 2)
∈ ℕ ∧ (𝑥
· 2) ≤ ((𝑃
− 1) / 2))) | 
| 46 | 44, 45 | bitri 275 | . . . . . . . . 9
⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ
∧ (𝑥 · 2) ≤
((𝑃 − 1) /
2))) | 
| 47 | 42, 46 | sylibr 234 | . . . . . . . 8
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ (1...𝐻)) | 
| 48 |  | eleq1 2829 | . . . . . . . 8
⊢ (𝑦 = (𝑥 · 2) → (𝑦 ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...𝐻))) | 
| 49 | 47, 48 | syl5ibrcom 247 | . . . . . . 7
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑥 · 2) → 𝑦 ∈ (1...𝐻))) | 
| 50 | 6, 49 | sylbid 240 | . . . . . 6
⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) | 
| 51 |  | iffalse 4534 | . . . . . . . . 9
⊢ (¬
(𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑥 · 2))) | 
| 52 | 51 | eqeq2d 2748 | . . . . . . . 8
⊢ (¬
(𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2)))) | 
| 53 | 52 | adantr 480 | . . . . . . 7
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2)))) | 
| 54 |  | eldifi 4131 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) | 
| 55 |  | prmz 16712 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 56 | 19, 54, 55 | 3syl 18 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 57 | 56 | ad2antrl 728 | . . . . . . . . . . 11
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝑃 ∈ ℤ) | 
| 58 |  | elfzelz 13564 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝐻) → 𝑥 ∈ ℤ) | 
| 59 | 25 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...𝐻) → 2 ∈ ℤ) | 
| 60 | 58, 59 | zmulcld 12728 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℤ) | 
| 61 | 60 | ad2antll 729 | . . . . . . . . . . 11
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ ℤ) | 
| 62 | 57, 61 | zsubcld 12727 | . . . . . . . . . 10
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈
ℤ) | 
| 63 | 55 | zred 12722 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) | 
| 64 | 14 | breq2i 5151 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ≤ 𝐻 ↔ 𝑥 ≤ ((𝑃 − 1) / 2)) | 
| 65 |  | nnre 12273 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) | 
| 66 | 65 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑥 ∈
ℝ) | 
| 67 |  | peano2rem 11576 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) | 
| 68 | 67 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − 1) ∈
ℝ) | 
| 69 |  | 2re 12340 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ | 
| 70 |  | 2pos 12369 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
2 | 
| 71 | 69, 70 | pm3.2i 470 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 72 | 71 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (2
∈ ℝ ∧ 0 < 2)) | 
| 73 |  | lemuldiv 12148 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧
(2 ∈ ℝ ∧ 0 < 2)) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) | 
| 74 | 66, 68, 72, 73 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2))) | 
| 75 | 64, 74 | bitr4id 290 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 ↔ (𝑥 · 2) ≤ (𝑃 − 1))) | 
| 76 | 11 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈
ℝ) | 
| 77 | 76 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 · 2) ∈
ℝ) | 
| 78 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℝ) | 
| 79 | 77, 68, 78 | lesub2d 11871 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ (𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)))) | 
| 80 |  | recn 11245 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℝ → 𝑃 ∈
ℂ) | 
| 81 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℝ → 1 ∈
ℂ) | 
| 82 | 80, 81 | nncand 11625 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 − 1)) = 1) | 
| 83 | 82 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 − 1)) = 1) | 
| 84 | 83 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) ↔ 1 ≤ (𝑃 − (𝑥 · 2)))) | 
| 85 | 84 | biimpd 229 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) → 1 ≤ (𝑃 − (𝑥 · 2)))) | 
| 86 | 79, 85 | sylbid 240 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) → 1 ≤ (𝑃 − (𝑥 · 2)))) | 
| 87 | 75, 86 | sylbid 240 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 → 1 ≤ (𝑃 − (𝑥 · 2)))) | 
| 88 | 87 | impancom 451 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) | 
| 89 | 88 | 3adant2 1132 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2)))) | 
| 90 | 7, 89 | sylbi 217 | . . . . . . . . . . . . . 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 406 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 1 ≤ (𝑃 − (𝑥 · 2))) | 
| 94 | 93 | adantl 481 | . . . . . . . . . 10
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 1 ≤ (𝑃 − (𝑥 · 2))) | 
| 95 |  | elnnz1 12643 | . . . . . . . . . 10
⊢ ((𝑃 − (𝑥 · 2)) ∈ ℕ ↔ ((𝑃 − (𝑥 · 2)) ∈ ℤ ∧ 1 ≤
(𝑃 − (𝑥 · 2)))) | 
| 96 | 62, 94, 95 | sylanbrc 583 | . . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈
ℕ) | 
| 97 | 7 | simp2bi 1147 | . . . . . . . . . 10
⊢ (𝑥 ∈ (1...𝐻) → 𝐻 ∈ ℕ) | 
| 98 | 97 | ad2antll 729 | . . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝐻 ∈ ℕ) | 
| 99 |  | nnre 12273 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) | 
| 100 | 99 | rehalfcld 12513 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈
ℝ) | 
| 101 | 100 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 / 2) ∈
ℝ) | 
| 102 | 60 | zred 12722 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℝ) | 
| 103 |  | lenlt 11339 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 / 2) ∈ ℝ ∧
(𝑥 · 2) ∈
ℝ) → ((𝑃 / 2)
≤ (𝑥 · 2) ↔
¬ (𝑥 · 2) <
(𝑃 / 2))) | 
| 104 | 101, 102,
103 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2))) | 
| 105 | 22, 60 | anim12i 613 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈
ℤ)) | 
| 106 | 105, 30 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈
ℤ)) | 
| 107 |  | halfleoddlt 16399 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)
→ ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) | 
| 108 | 106, 107 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) | 
| 109 | 108 | biimpa 476 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 / 2) < (𝑥 · 2)) | 
| 110 |  | nncn 12274 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℂ) | 
| 111 |  | subhalfhalf 12500 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ ℂ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) | 
| 112 | 110, 111 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℕ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) | 
| 113 | 112 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℕ → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) | 
| 114 | 113 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2))) | 
| 115 | 109, 114 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑃 / 2)) < (𝑥 · 2)) | 
| 116 | 99 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℝ) | 
| 117 | 100 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℝ) | 
| 118 | 102 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℝ) | 
| 119 | 116, 117,
118 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈
ℝ)) | 
| 120 | 119 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈
ℝ)) | 
| 121 |  | ltsub23 11743 | . . . . . . . . . . . . . . . . . . 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 232 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) < (𝑃 / 2)) | 
| 124 | 21 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ) | 
| 125 |  | simplr 769 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ¬ 2 ∥ 𝑃) | 
| 126 | 60 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ) | 
| 127 | 124, 126 | zsubcld 12727 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 − (𝑥 · 2)) ∈
ℤ) | 
| 128 | 124, 125,
127 | 3jca 1129 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈
ℤ)) | 
| 129 | 128 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈
ℤ)) | 
| 130 |  | ltoddhalfle 16398 | . . . . . . . . . . . . . . . . . 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 232 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)) | 
| 133 | 132 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))) | 
| 134 | 14 | breq2i 5151 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 − (𝑥 · 2)) ≤ 𝐻 ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)) | 
| 135 | 133, 134 | imbitrrdi 252 | . . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) | 
| 136 | 104, 135 | sylbird 260 | . . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) | 
| 137 | 136 | ex 412 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))) | 
| 138 | 19, 20, 137 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))) | 
| 139 | 138 | imp 406 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)) | 
| 140 | 139 | impcom 407 | . . . . . . . . 9
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ≤ 𝐻) | 
| 141 |  | elfz1b 13633 | . . . . . . . . 9
⊢ ((𝑃 − (𝑥 · 2)) ∈ (1...𝐻) ↔ ((𝑃 − (𝑥 · 2)) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑃 − (𝑥 · 2)) ≤ 𝐻)) | 
| 142 | 96, 98, 140, 141 | syl3anbrc 1344 | . . . . . . . 8
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ (1...𝐻)) | 
| 143 |  | eleq1 2829 | . . . . . . . 8
⊢ (𝑦 = (𝑃 − (𝑥 · 2)) → (𝑦 ∈ (1...𝐻) ↔ (𝑃 − (𝑥 · 2)) ∈ (1...𝐻))) | 
| 144 | 142, 143 | syl5ibrcom 247 | . . . . . . 7
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑃 − (𝑥 · 2)) → 𝑦 ∈ (1...𝐻))) | 
| 145 | 53, 144 | sylbid 240 | . . . . . 6
⊢ ((¬
(𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) | 
| 146 | 50, 145 | pm2.61ian 812 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) | 
| 147 | 146 | rexlimdva 3155 | . . . 4
⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻))) | 
| 148 |  | elfz1b 13633 | . . . . . . . . . 10
⊢ (𝑦 ∈ (1...𝐻) ↔ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) | 
| 149 |  | simp1 1137 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℕ) | 
| 150 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((2
∥ 𝑦 ∧ 𝜑) → 2 ∥ 𝑦) | 
| 151 |  | nnehalf 16416 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 2 ∥
𝑦) → (𝑦 / 2) ∈
ℕ) | 
| 152 | 149, 150,
151 | syl2anr 597 | . . . . . . . . . . . 12
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ∈ ℕ) | 
| 153 |  | simpr2 1196 | . . . . . . . . . . . 12
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ) | 
| 154 |  | nnre 12273 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) | 
| 155 | 154 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → 𝑦 ∈ ℝ) | 
| 156 |  | nnrp 13046 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 ∈ ℕ → 𝐻 ∈
ℝ+) | 
| 157 | 156 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → 𝐻 ∈
ℝ+) | 
| 158 | 157 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → 𝐻 ∈
ℝ+) | 
| 159 |  | 2rp 13039 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ | 
| 160 |  | 1le2 12475 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ≤
2 | 
| 161 | 159, 160 | pm3.2i 470 | . . . . . . . . . . . . . . . . . 18
⊢ (2 ∈
ℝ+ ∧ 1 ≤ 2) | 
| 162 | 161 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → (2 ∈
ℝ+ ∧ 1 ≤ 2)) | 
| 163 |  | ledivge1le 13106 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+
∧ (2 ∈ ℝ+ ∧ 1 ≤ 2)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)) | 
| 164 | 155, 158,
162, 163 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2
∥ 𝑦 ∧ 𝜑)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)) | 
| 165 | 164 | ex 412 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻))) | 
| 166 | 165 | com23 86 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻))) | 
| 167 | 166 | 3impia 1118 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻)) | 
| 168 | 167 | impcom 407 | . . . . . . . . . . . 12
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ≤ 𝐻) | 
| 169 | 152, 153,
168 | 3jca 1129 | . . . . . . . . . . 11
⊢ (((2
∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) | 
| 170 | 169 | ex 412 | . . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))) | 
| 171 | 148, 170 | biimtrid 242 | . . . . . . . . 9
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))) | 
| 172 | 171 | 3impia 1118 | . . . . . . . 8
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) | 
| 173 |  | elfz1b 13633 | . . . . . . . 8
⊢ ((𝑦 / 2) ∈ (1...𝐻) ↔ ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)) | 
| 174 | 172, 173 | sylibr 234 | . . . . . . 7
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑦 / 2) ∈ (1...𝐻)) | 
| 175 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑦 / 2) → (𝑥 · 2) = ((𝑦 / 2) · 2)) | 
| 176 | 175 | breq1d 5153 | . . . . . . . . . 10
⊢ (𝑥 = (𝑦 / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ ((𝑦 / 2) · 2) < (𝑃 / 2))) | 
| 177 | 175 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑥 = (𝑦 / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − ((𝑦 / 2) · 2))) | 
| 178 | 176, 175,
177 | ifbieq12d 4554 | . . . . . . . . 9
⊢ (𝑥 = (𝑦 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))) | 
| 179 | 178 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑥 = (𝑦 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))) | 
| 180 | 179 | adantl 481 | . . . . . . 7
⊢ (((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = (𝑦 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))) | 
| 181 |  | elfzelz 13564 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℤ) | 
| 182 | 181 | zcnd 12723 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℂ) | 
| 183 | 182 | 3ad2ant3 1136 | . . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ) | 
| 184 |  | 2cnd 12344 | . . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ) | 
| 185 |  | 2ne0 12370 | . . . . . . . . . . . 12
⊢ 2 ≠
0 | 
| 186 | 185 | a1i 11 | . . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ≠ 0) | 
| 187 | 183, 184,
186 | divcan1d 12044 | . . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) = 𝑦) | 
| 188 | 14 | breq2i 5151 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ≤ 𝐻 ↔ 𝑦 ≤ ((𝑃 − 1) / 2)) | 
| 189 |  | nnz 12634 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) | 
| 190 | 19, 20, 22 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃)) | 
| 191 | 190 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃)) | 
| 192 | 189, 191 | anim12ci 614 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ)) | 
| 193 |  | df-3an 1089 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ 𝑦 ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ 𝑦 ∈
ℤ)) | 
| 194 | 192, 193 | sylibr 234 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ)) | 
| 195 |  | ltoddhalfle 16398 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃 ∧ 𝑦 ∈ ℤ) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2))) | 
| 196 | 194, 195 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ (2 ∥
𝑦 ∧ 𝜑)) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2))) | 
| 197 | 196 | exbiri 811 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → 𝑦 < (𝑃 / 2)))) | 
| 198 | 197 | com23 86 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))) | 
| 199 | 188, 198 | biimtrid 242 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))) | 
| 200 | 199 | a1d 25 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))))) | 
| 201 | 200 | 3imp 1111 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))) | 
| 202 | 148, 201 | sylbi 217 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (1...𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))) | 
| 203 | 202 | com12 32 | . . . . . . . . . . 11
⊢ ((2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → 𝑦 < (𝑃 / 2))) | 
| 204 | 203 | 3impia 1118 | . . . . . . . . . 10
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 < (𝑃 / 2)) | 
| 205 | 187, 204 | eqbrtrd 5165 | . . . . . . . . 9
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) < (𝑃 / 2)) | 
| 206 | 205 | iftrued 4533 | . . . . . . . 8
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))) = ((𝑦 / 2) · 2)) | 
| 207 | 206, 187 | eqtr2d 2778 | . . . . . . 7
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))) | 
| 208 | 174, 180,
207 | rspcedvd 3624 | . . . . . 6
⊢ ((2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) | 
| 209 | 208 | 3exp 1120 | . . . . 5
⊢ (2
∥ 𝑦 → (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))) | 
| 210 | 54, 55 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℤ) | 
| 211 | 210 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℤ) | 
| 212 | 189 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℤ) | 
| 213 | 212 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℤ) | 
| 214 | 211, 213 | zsubcld 12727 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℤ) | 
| 215 | 154 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑦 ∈
ℝ) | 
| 216 | 67 | rehalfcld 12513 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → ((𝑃 − 1) / 2) ∈
ℝ) | 
| 217 | 216 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → ((𝑃 − 1) / 2) ∈
ℝ) | 
| 218 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑃 ∈
ℝ) | 
| 219 | 215, 217,
218 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈
ℝ)) | 
| 220 | 219 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈
ℝ))) | 
| 221 | 54, 63, 220 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ))) | 
| 222 | 221 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ))) | 
| 223 | 222 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ∈ ℝ
∧ ((𝑃 − 1) / 2)
∈ ℝ ∧ 𝑃
∈ ℝ)) | 
| 224 |  | lesub2 11758 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ
∧ 𝑃 ∈ ℝ)
→ (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦))) | 
| 225 | 223, 224 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦))) | 
| 226 | 55 | zcnd 12723 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) | 
| 227 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℂ → 1 ∈
ℂ) | 
| 228 |  | 2cnne0 12476 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 229 | 228 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℂ → (2 ∈
ℂ ∧ 2 ≠ 0)) | 
| 230 |  | divsubdir 11961 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃 ∈ ℂ ∧ 1 ∈
ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2))) | 
| 231 | 227, 229,
230 | mpd3an23 1465 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 /
2))) | 
| 232 | 231 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = (𝑃 − ((𝑃 / 2) − (1 / 2)))) | 
| 233 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → 𝑃 ∈
ℂ) | 
| 234 |  | halfcl 12491 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → (𝑃 / 2) ∈
ℂ) | 
| 235 |  | halfcn 12481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 / 2)
∈ ℂ | 
| 236 | 235 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℂ → (1 / 2)
∈ ℂ) | 
| 237 | 233, 234,
236 | subsubd 11648 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 / 2) − (1 / 2))) = ((𝑃 − (𝑃 / 2)) + (1 / 2))) | 
| 238 | 111 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℂ → ((𝑃 − (𝑃 / 2)) + (1 / 2)) = ((𝑃 / 2) + (1 / 2))) | 
| 239 | 232, 237,
238 | 3eqtrd 2781 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2))) | 
| 240 | 54, 226, 239 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 /
2))) | 
| 241 | 240 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 /
2))) | 
| 242 | 241 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) ↔ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦))) | 
| 243 |  | prmnn 16711 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 244 |  | halfre 12480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (1 / 2)
∈ ℝ | 
| 245 | 244 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ → (1 / 2)
∈ ℝ) | 
| 246 |  | nngt0 12297 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℕ → 0 <
𝑃) | 
| 247 | 71 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℕ → (2 ∈
ℝ ∧ 0 < 2)) | 
| 248 |  | divgt0 12136 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑃 ∈ ℝ ∧ 0 <
𝑃) ∧ (2 ∈ ℝ
∧ 0 < 2)) → 0 < (𝑃 / 2)) | 
| 249 | 99, 246, 247, 248 | syl21anc 838 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ → 0 <
(𝑃 / 2)) | 
| 250 |  | halfgt0 12482 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 < (1
/ 2) | 
| 251 | 250 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℕ → 0 < (1
/ 2)) | 
| 252 | 100, 245,
249, 251 | addgt0d 11838 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℕ → 0 <
((𝑃 / 2) + (1 /
2))) | 
| 253 | 54, 243, 252 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 0 < ((𝑃 / 2) + (1
/ 2))) | 
| 254 | 253 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ 0 < ((𝑃 / 2) + (1
/ 2))) | 
| 255 |  | 0red 11264 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 0 ∈
ℝ) | 
| 256 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℝ) | 
| 257 | 256 | rehalfcld 12513 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈
ℝ) | 
| 258 | 244 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 / 2)
∈ ℝ) | 
| 259 | 257, 258 | readdcld 11290 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) + (1 / 2)) ∈
ℝ) | 
| 260 |  | resubcl 11573 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ) | 
| 261 | 260 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ) | 
| 262 | 255, 259,
261 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0
∈ ℝ ∧ ((𝑃 /
2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)) | 
| 263 | 262 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) | 
| 264 | 154, 263 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (0 ∈
ℝ ∧ ((𝑃 / 2) + (1
/ 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) | 
| 265 | 264 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ)
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))) | 
| 269 | 268 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)) | 
| 270 |  | ltletr 11353 | . . . . . . . . . . . . . . . . . . . . . . . 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 695 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (((𝑃 / 2) + (1 / 2))
≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦))) | 
| 273 | 242, 272 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦))) | 
| 274 | 225, 273 | sylbid 240 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦))
→ (𝑦 ≤ ((𝑃 − 1) / 2) → 0 <
(𝑃 − 𝑦))) | 
| 275 | 274 | ex 412 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑦 ≤ ((𝑃 − 1) / 2) → 0 <
(𝑃 − 𝑦)))) | 
| 276 | 275 | com23 86 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦)))) | 
| 277 | 188, 276 | biimtrid 242 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦)))) | 
| 278 | 277 | 3impia 1118 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2
∥ 𝑦) → 0 <
(𝑃 − 𝑦))) | 
| 279 | 278 | impcom 407 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 0 < (𝑃 − 𝑦)) | 
| 280 |  | elnnz 12623 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 − 𝑦) ∈ ℕ ↔ ((𝑃 − 𝑦) ∈ ℤ ∧ 0 < (𝑃 − 𝑦))) | 
| 281 | 214, 279,
280 | sylanbrc 583 | . . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℕ) | 
| 282 | 23 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑃 ∈ ℤ
∧ ¬ 2 ∥ 𝑃)) | 
| 283 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ¬ 2 ∥ 𝑦) | 
| 284 | 283, 212 | anim12ci 614 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦)) | 
| 285 |  | omoe 16401 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℤ ∧ ¬ 2
∥ 𝑃) ∧ (𝑦 ∈ ℤ ∧ ¬ 2
∥ 𝑦)) → 2
∥ (𝑃 − 𝑦)) | 
| 286 | 282, 284,
285 | syl2an2r 685 | . . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 2 ∥ (𝑃 − 𝑦)) | 
| 287 |  | nnehalf 16416 | . . . . . . . . . . . . . 14
⊢ (((𝑃 − 𝑦) ∈ ℕ ∧ 2 ∥ (𝑃 − 𝑦)) → ((𝑃 − 𝑦) / 2) ∈ ℕ) | 
| 288 | 281, 286,
287 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ∈ ℕ) | 
| 289 |  | simpr2 1196 | . . . . . . . . . . . . 13
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ) | 
| 290 |  | 1red 11262 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 1 ∈
ℝ) | 
| 291 | 154 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℝ) | 
| 292 | 291 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℝ) | 
| 293 | 54, 63 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℝ) | 
| 294 | 293 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℝ) | 
| 295 |  | nnge1 12294 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 1 ≤
𝑦) | 
| 296 | 295 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 1 ≤ 𝑦) | 
| 297 | 296 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → 1 ≤ 𝑦) | 
| 298 | 290, 292,
294, 297 | lesub2dd 11880 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ≤ (𝑃 − 1)) | 
| 299 | 294, 292 | resubcld 11691 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℝ) | 
| 300 | 54, 63, 67 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 − 1) ∈
ℝ) | 
| 301 | 300 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (𝑃 − 1) ∈ ℝ) | 
| 302 | 71 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (2 ∈ ℝ
∧ 0 < 2)) | 
| 303 |  | lediv1 12133 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 − 𝑦) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))) | 
| 304 | 299, 301,
302, 303 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))) | 
| 305 | 298, 304 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)) | 
| 306 | 14 | breq2i 5151 | . . . . . . . . . . . . . 14
⊢ (((𝑃 − 𝑦) / 2) ≤ 𝐻 ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)) | 
| 307 | 305, 306 | sylibr 234 | . . . . . . . . . . . . 13
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ 𝐻) | 
| 308 | 288, 289,
307 | 3jca 1129 | . . . . . . . . . . . 12
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
∧ (𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻)) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)) | 
| 309 | 308 | ex 412 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ ((𝑦 ∈ ℕ
∧ 𝐻 ∈ ℕ
∧ 𝑦 ≤ 𝐻) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻))) | 
| 310 |  | elfz1b 13633 | . . . . . . . . . . 11
⊢ (((𝑃 − 𝑦) / 2) ∈ (1...𝐻) ↔ (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)) | 
| 311 | 309, 148,
310 | 3imtr4g 296 | . . . . . . . . . 10
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 2 ∥ 𝑦)
→ (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))) | 
| 312 | 311 | ex 412 | . . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (¬ 2 ∥ 𝑦
→ (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))) | 
| 313 | 19, 312 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))) | 
| 314 | 313 | 3imp21 1114 | . . . . . . 7
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)) | 
| 315 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑥 · 2) = (((𝑃 − 𝑦) / 2) · 2)) | 
| 316 | 315 | breq1d 5153 | . . . . . . . . . 10
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2))) | 
| 317 | 315 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) | 
| 318 | 316, 315,
317 | ifbieq12d 4554 | . . . . . . . . 9
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))) | 
| 319 | 318 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))) | 
| 320 | 319 | adantl 481 | . . . . . . 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 1135 | . . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑃 ∈ ℂ) | 
| 323 | 182 | 3ad2ant3 1136 | . . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ) | 
| 324 | 322, 323 | subcld 11620 | . . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − 𝑦) ∈ ℂ) | 
| 325 |  | 2cnd 12344 | . . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ) | 
| 326 | 185 | a1i 11 | . . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ≠ 0) | 
| 327 | 324, 325,
326 | divcan1d 12044 | . . . . . . . . . 10
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (((𝑃 − 𝑦) / 2) · 2) = (𝑃 − 𝑦)) | 
| 328 |  | zre 12617 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℝ) | 
| 329 |  | halfge0 12483 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ≤ (1
/ 2) | 
| 330 |  | rehalfcl 12492 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈
ℝ) | 
| 331 | 330 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈
ℝ) | 
| 332 | 331, 258 | subge02d 11855 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ≤
(1 / 2) ↔ ((𝑃 / 2)
− (1 / 2)) ≤ (𝑃 /
2))) | 
| 333 | 329, 332 | mpbii 233 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ≤
(𝑃 / 2)) | 
| 334 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑦 ∈
ℝ) | 
| 335 | 244 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → (1 / 2)
∈ ℝ) | 
| 336 | 330, 335 | resubcld 11691 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) − (1 / 2)) ∈
ℝ) | 
| 337 | 336 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ∈
ℝ) | 
| 338 |  | letr 11355 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 / 2) − (1 / 2)) ∈
ℝ ∧ (𝑃 / 2)
∈ ℝ) → ((𝑦
≤ ((𝑃 / 2) − (1 /
2)) ∧ ((𝑃 / 2) −
(1 / 2)) ≤ (𝑃 / 2))
→ 𝑦 ≤ (𝑃 / 2))) | 
| 339 | 334, 337,
331, 338 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤
(𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2))) | 
| 340 | 333, 339 | mpan2d 694 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 / 2) − (1 / 2)) → 𝑦 ≤ (𝑃 / 2))) | 
| 341 | 80 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈
ℂ) | 
| 342 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 1 ∈
ℂ) | 
| 343 | 228 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (2
∈ ℂ ∧ 2 ≠ 0)) | 
| 344 | 341, 342,
343, 230 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 /
2))) | 
| 345 | 344 | breq2d 5155 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ 𝑦 ≤ ((𝑃 / 2) − (1 / 2)))) | 
| 346 |  | lesub 11742 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2)))) | 
| 347 | 331, 256,
334, 346 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2)))) | 
| 348 | 257, 261 | lenltd 11407 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ ¬ (𝑃 − 𝑦) < (𝑃 / 2))) | 
| 349 |  | 2cnd 12344 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → 2 ∈
ℂ) | 
| 350 | 185 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑃 ∈ ℝ → 2 ≠
0) | 
| 351 | 80, 349, 350 | divcan1d 12044 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = 𝑃) | 
| 352 | 351 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → 𝑃 = ((𝑃 / 2) · 2)) | 
| 353 | 352 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (((𝑃 / 2) · 2) − (𝑃 / 2))) | 
| 354 | 330 | recnd 11289 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈
ℂ) | 
| 355 | 354, 349 | mulcomd 11282 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = (2 ·
(𝑃 / 2))) | 
| 356 | 355 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → (((𝑃 / 2) · 2) − (𝑃 / 2)) = ((2 · (𝑃 / 2)) − (𝑃 / 2))) | 
| 357 | 349, 354 | mulsubfacd 11724 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → ((2
· (𝑃 / 2)) −
(𝑃 / 2)) = ((2 − 1)
· (𝑃 /
2))) | 
| 358 |  | 2m1e1 12392 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (2
− 1) = 1 | 
| 359 | 358 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑃 ∈ ℝ → (2
− 1) = 1) | 
| 360 | 359 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → ((2
− 1) · (𝑃 /
2)) = (1 · (𝑃 /
2))) | 
| 361 | 354 | mullidd 11279 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑃 ∈ ℝ → (1
· (𝑃 / 2)) = (𝑃 / 2)) | 
| 362 | 357, 360,
361 | 3eqtrd 2781 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃 ∈ ℝ → ((2
· (𝑃 / 2)) −
(𝑃 / 2)) = (𝑃 / 2)) | 
| 363 | 353, 356,
362 | 3eqtrd 2781 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) | 
| 364 | 363 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 / 2)) = (𝑃 / 2)) | 
| 365 | 364 | breq2d 5155 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ (𝑃 − (𝑃 / 2)) ↔ 𝑦 ≤ (𝑃 / 2))) | 
| 366 | 347, 348,
365 | 3bitr3d 309 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (¬
(𝑃 − 𝑦) < (𝑃 / 2) ↔ 𝑦 ≤ (𝑃 / 2))) | 
| 367 | 340, 345,
366 | 3imtr4d 294 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) | 
| 368 | 367 | ex 412 | . . . . . . . . . . . . . . . . . . . . . 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 481 | . . . . . . . . . . . . . . . . 17
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) | 
| 374 | 373 | com13 88 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((¬ 2 ∥
𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) | 
| 375 | 188, 374 | biimtrid 242 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))) | 
| 376 | 375 | a1d 25 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))) | 
| 377 | 376 | 3imp 1111 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) | 
| 378 | 377 | com12 32 | . . . . . . . . . . . 12
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) | 
| 379 | 148, 378 | biimtrid 242 | . . . . . . . . . . 11
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))) | 
| 380 | 379 | 3impia 1118 | . . . . . . . . . 10
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)) | 
| 381 | 327, 380 | eqnbrtrd 5161 | . . . . . . . . 9
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2)) | 
| 382 | 381 | iffalsed 4536 | . . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) | 
| 383 | 327 | oveq2d 7447 | . . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (((𝑃 − 𝑦) / 2) · 2)) = (𝑃 − (𝑃 − 𝑦))) | 
| 384 | 321, 182 | anim12i 613 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ)) | 
| 385 | 384 | 3adant1 1131 | . . . . . . . . 9
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ)) | 
| 386 |  | nncan 11538 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑃 − (𝑃 − 𝑦)) = 𝑦) | 
| 387 | 385, 386 | syl 17 | . . . . . . . 8
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (𝑃 − 𝑦)) = 𝑦) | 
| 388 | 382, 383,
387 | 3eqtrrd 2782 | . . . . . . 7
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))) | 
| 389 | 314, 320,
388 | rspcedvd 3624 | . . . . . 6
⊢ ((¬ 2
∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) | 
| 390 | 389 | 3exp 1120 | . . . . 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 212 | . . 3
⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 ∈ (1...𝐻))) | 
| 393 | 3, 392 | bitrid 283 | . 2
⊢ (𝜑 → (𝑦 ∈ ran 𝑅 ↔ 𝑦 ∈ (1...𝐻))) | 
| 394 | 393 | eqrdv 2735 | 1
⊢ (𝜑 → ran 𝑅 = (1...𝐻)) |