Proof of Theorem gausslemma2dlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | gausslemma2d.r | . . 3
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) | 
| 2 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 · 2) = (𝑘 · 2)) | 
| 3 | 2 | breq1d 5153 | . . . . . 6
⊢ (𝑥 = 𝑘 → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑘 · 2) < (𝑃 / 2))) | 
| 4 | 2 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃 − (𝑥 · 2)) = (𝑃 − (𝑘 · 2))) | 
| 5 | 3, 2, 4 | ifbieq12d 4554 | . . . . 5
⊢ (𝑥 = 𝑘 → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) | 
| 6 | 5 | adantl 481 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2)))) | 
| 7 |  | elfz1b 13633 | . . . . . . . 8
⊢ (𝑘 ∈ (1...𝑀) ↔ (𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑘 ≤ 𝑀)) | 
| 8 |  | nnre 12273 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) | 
| 9 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → 𝑘 ∈
ℝ) | 
| 10 |  | nnre 12273 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) | 
| 11 | 10 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → 𝑀 ∈
ℝ) | 
| 12 |  | 2re 12340 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℝ | 
| 13 |  | 2pos 12369 | . . . . . . . . . . . . 13
⊢ 0 <
2 | 
| 14 | 12, 13 | pm3.2i 470 | . . . . . . . . . . . 12
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 15 | 14 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2
∈ ℝ ∧ 0 < 2)) | 
| 16 |  | lemul1 12119 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (𝑘 · 2) ≤ (𝑀 · 2))) | 
| 17 | 9, 11, 15, 16 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 ≤ 𝑀 ↔ (𝑘 · 2) ≤ (𝑀 · 2))) | 
| 18 |  | gausslemma2d.p | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) | 
| 19 |  | gausslemma2d.m | . . . . . . . . . . . . . . 15
⊢ 𝑀 = (⌊‘(𝑃 / 4)) | 
| 20 | 18, 19 | gausslemma2dlem0e 27404 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 · 2) < (𝑃 / 2)) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝜑) → (𝑀 · 2) < (𝑃 / 2)) | 
| 22 | 12 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 2 ∈
ℝ) | 
| 23 | 8, 22 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 · 2) ∈
ℝ) | 
| 24 | 23 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 · 2) ∈
ℝ) | 
| 25 | 12 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 2 ∈
ℝ) | 
| 26 | 10, 25 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → (𝑀 · 2) ∈
ℝ) | 
| 27 | 26 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑀 · 2) ∈
ℝ) | 
| 28 | 18 | gausslemma2dlem0a 27400 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 29 | 28 | nnred 12281 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 30 | 29 | rehalfcld 12513 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 / 2) ∈ ℝ) | 
| 31 |  | lelttr 11351 | . . . . . . . . . . . . . 14
⊢ (((𝑘 · 2) ∈ ℝ
∧ (𝑀 · 2) ∈
ℝ ∧ (𝑃 / 2)
∈ ℝ) → (((𝑘
· 2) ≤ (𝑀
· 2) ∧ (𝑀
· 2) < (𝑃 / 2))
→ (𝑘 · 2) <
(𝑃 / 2))) | 
| 32 | 24, 27, 30, 31 | syl2an3an 1424 | . . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝜑) → (((𝑘 · 2) ≤ (𝑀 · 2) ∧ (𝑀 · 2) < (𝑃 / 2)) → (𝑘 · 2) < (𝑃 / 2))) | 
| 33 | 21, 32 | mpan2d 694 | . . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ 𝜑) → ((𝑘 · 2) ≤ (𝑀 · 2) → (𝑘 · 2) < (𝑃 / 2))) | 
| 34 | 33 | ex 412 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝜑 → ((𝑘 · 2) ≤ (𝑀 · 2) → (𝑘 · 2) < (𝑃 / 2)))) | 
| 35 | 34 | com23 86 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → ((𝑘 · 2) ≤ (𝑀 · 2) → (𝜑 → (𝑘 · 2) < (𝑃 / 2)))) | 
| 36 | 17, 35 | sylbid 240 | . . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 ≤ 𝑀 → (𝜑 → (𝑘 · 2) < (𝑃 / 2)))) | 
| 37 | 36 | 3impia 1118 | . . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑘 ≤ 𝑀) → (𝜑 → (𝑘 · 2) < (𝑃 / 2))) | 
| 38 | 7, 37 | sylbi 217 | . . . . . . 7
⊢ (𝑘 ∈ (1...𝑀) → (𝜑 → (𝑘 · 2) < (𝑃 / 2))) | 
| 39 | 38 | impcom 407 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑘 · 2) < (𝑃 / 2)) | 
| 40 | 39 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → (𝑘 · 2) < (𝑃 / 2)) | 
| 41 | 40 | iftrued 4533 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → if((𝑘 · 2) < (𝑃 / 2), (𝑘 · 2), (𝑃 − (𝑘 · 2))) = (𝑘 · 2)) | 
| 42 | 6, 41 | eqtrd 2777 | . . 3
⊢ (((𝜑 ∧ 𝑘 ∈ (1...𝑀)) ∧ 𝑥 = 𝑘) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑘 · 2)) | 
| 43 | 18, 19 | gausslemma2dlem0d 27403 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 44 | 43 | nn0zd 12639 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 45 |  | gausslemma2d.h | . . . . . . . 8
⊢ 𝐻 = ((𝑃 − 1) / 2) | 
| 46 | 18, 45 | gausslemma2dlem0b 27401 | . . . . . . 7
⊢ (𝜑 → 𝐻 ∈ ℕ) | 
| 47 | 46 | nnzd 12640 | . . . . . 6
⊢ (𝜑 → 𝐻 ∈ ℤ) | 
| 48 | 18, 19, 45 | gausslemma2dlem0g 27406 | . . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝐻) | 
| 49 |  | eluz2 12884 | . . . . . 6
⊢ (𝐻 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑀 ≤ 𝐻)) | 
| 50 | 44, 47, 48, 49 | syl3anbrc 1344 | . . . . 5
⊢ (𝜑 → 𝐻 ∈ (ℤ≥‘𝑀)) | 
| 51 |  | fzss2 13604 | . . . . 5
⊢ (𝐻 ∈
(ℤ≥‘𝑀) → (1...𝑀) ⊆ (1...𝐻)) | 
| 52 | 50, 51 | syl 17 | . . . 4
⊢ (𝜑 → (1...𝑀) ⊆ (1...𝐻)) | 
| 53 | 52 | sselda 3983 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (1...𝐻)) | 
| 54 |  | ovexd 7466 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑘 · 2) ∈ V) | 
| 55 | 1, 42, 53, 54 | fvmptd2 7024 | . 2
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑅‘𝑘) = (𝑘 · 2)) | 
| 56 | 55 | ralrimiva 3146 | 1
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) |