Metamath Proof Explorer

Theorem gausslemma2dlem2

Description: Lemma 2 for gausslemma2d . (Contributed by AV, 4-Jul-2021)

Ref Expression
Hypotheses gausslemma2d.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2d.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
gausslemma2d.r ⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
gausslemma2d.m ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
Assertion gausslemma2dlem2 ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) )

Proof

Step Hyp Ref Expression
1 gausslemma2d.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 gausslemma2d.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
3 gausslemma2d.r ⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
4 gausslemma2d.m ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
5 oveq1 ⊢ ( 𝑥 = 𝑘 → ( 𝑥 · 2 ) = ( 𝑘 · 2 ) )
6 5 breq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) )
7 5 oveq2d ⊢ ( 𝑥 = 𝑘 → ( 𝑃 − ( 𝑥 · 2 ) ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
8 6 5 7 ifbieq12d ⊢ ( 𝑥 = 𝑘 → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = if ( ( 𝑘 · 2 ) < ( 𝑃 / 2 ) , ( 𝑘 · 2 ) , ( 𝑃 − ( 𝑘 · 2 ) ) ) )
9 8 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑘 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = if ( ( 𝑘 · 2 ) < ( 𝑃 / 2 ) , ( 𝑘 · 2 ) , ( 𝑃 − ( 𝑘 · 2 ) ) ) )
10 elfz1b ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑘 ≤ 𝑀 ) )
11 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
12 11 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → 𝑘 ∈ ℝ )
13 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
14 13 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℝ )
15 2re ⊢ 2 ∈ ℝ
16 2pos ⊢ 0 < 2
17 15 16 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
18 17 a1i ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
19 lemul1 ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝑘 ≤ 𝑀 ↔ ( 𝑘 · 2 ) ≤ ( 𝑀 · 2 ) ) )
20 12 14 18 19 syl3anc ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑘 ≤ 𝑀 ↔ ( 𝑘 · 2 ) ≤ ( 𝑀 · 2 ) ) )
21 1 4 gausslemma2dlem0e ⊢ ( 𝜑 → ( 𝑀 · 2 ) < ( 𝑃 / 2 ) )
22 21 adantl ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 𝜑 ) → ( 𝑀 · 2 ) < ( 𝑃 / 2 ) )
23 15 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℝ )
24 11 23 remulcld ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 · 2 ) ∈ ℝ )
25 24 adantr ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑘 · 2 ) ∈ ℝ )
26 15 a1i ⊢ ( 𝑀 ∈ ℕ → 2 ∈ ℝ )
27 13 26 remulcld ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 · 2 ) ∈ ℝ )
28 27 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 · 2 ) ∈ ℝ )
29 1 gausslemma2dlem0a ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
30 29 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
31 30 rehalfcld ⊢ ( 𝜑 → ( 𝑃 / 2 ) ∈ ℝ )
32 lelttr ⊢ ( ( ( 𝑘 · 2 ) ∈ ℝ ∧ ( 𝑀 · 2 ) ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ) → ( ( ( 𝑘 · 2 ) ≤ ( 𝑀 · 2 ) ∧ ( 𝑀 · 2 ) < ( 𝑃 / 2 ) ) → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) )
33 25 28 31 32 syl2an3an ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 𝜑 ) → ( ( ( 𝑘 · 2 ) ≤ ( 𝑀 · 2 ) ∧ ( 𝑀 · 2 ) < ( 𝑃 / 2 ) ) → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) )
34 22 33 mpan2d ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ 𝜑 ) → ( ( 𝑘 · 2 ) ≤ ( 𝑀 · 2 ) → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) )
35 34 ex ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝜑 → ( ( 𝑘 · 2 ) ≤ ( 𝑀 · 2 ) → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) ) )
36 35 com23 ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑘 · 2 ) ≤ ( 𝑀 · 2 ) → ( 𝜑 → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) ) )
37 20 36 sylbid ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑘 ≤ 𝑀 → ( 𝜑 → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) ) )
38 37 3impia ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑘 ≤ 𝑀 ) → ( 𝜑 → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) )
39 10 38 sylbi ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → ( 𝜑 → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) )
40 39 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) )
41 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑘 ) → ( 𝑘 · 2 ) < ( 𝑃 / 2 ) )
42 41 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑘 ) → if ( ( 𝑘 · 2 ) < ( 𝑃 / 2 ) , ( 𝑘 · 2 ) , ( 𝑃 − ( 𝑘 · 2 ) ) ) = ( 𝑘 · 2 ) )
43 9 42 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝑘 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = ( 𝑘 · 2 ) )
44 1 4 gausslemma2dlem0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
45 44 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
46 1 2 gausslemma2dlem0b ⊢ ( 𝜑 → 𝐻 ∈ ℕ )
47 46 nnzd ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
48 1 4 2 gausslemma2dlem0g ⊢ ( 𝜑 → 𝑀 ≤ 𝐻 )
49 eluz2 ⊢ ( 𝐻 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑀 ≤ 𝐻 ) )
50 45 47 48 49 syl3anbrc ⊢ ( 𝜑 → 𝐻 ∈ ( ℤ≥ ‘ 𝑀 ) )
51 fzss2 ⊢ ( 𝐻 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 1 ... 𝑀 ) ⊆ ( 1 ... 𝐻 ) )
52 50 51 syl ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ⊆ ( 1 ... 𝐻 ) )
53 52 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑘 ∈ ( 1 ... 𝐻 ) )
54 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 · 2 ) ∈ V )
55 3 43 53 54 fvmptd2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) )
56 55 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) )