Metamath Proof Explorer

Theorem gausslemma2dlem3

Description: Lemma 3 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 gausslemma2dlem3 ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝑀 + 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 1 gausslemma2dlem0a ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
11 elfz2 ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ↔ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻 ) ) )
12 4 oveq1i ⊢ ( 𝑀 + 1 ) = ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 )
13 12 breq1i ⊢ ( ( 𝑀 + 1 ) ≤ 𝑘 ↔ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 )
14 nnre ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ )
15 4re ⊢ 4 ∈ ℝ
16 15 a1i ⊢ ( 𝑃 ∈ ℕ → 4 ∈ ℝ )
17 4ne0 ⊢ 4 ≠ 0
18 17 a1i ⊢ ( 𝑃 ∈ ℕ → 4 ≠ 0 )
19 14 16 18 redivcld ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 / 4 ) ∈ ℝ )
20 19 adantl ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( 𝑃 / 4 ) ∈ ℝ )
21 fllelt ⊢ ( ( 𝑃 / 4 ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( 𝑃 / 4 ) ∧ ( 𝑃 / 4 ) < ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ) )
22 20 21 syl ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( 𝑃 / 4 ) ∧ ( 𝑃 / 4 ) < ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ) )
23 19 flcld ⊢ ( 𝑃 ∈ ℕ → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ )
24 23 zred ⊢ ( 𝑃 ∈ ℕ → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℝ )
25 peano2re ⊢ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℝ )
26 24 25 syl ⊢ ( 𝑃 ∈ ℕ → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℝ )
27 26 adantl ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℝ )
28 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
29 28 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → 𝑘 ∈ ℝ )
30 ltleletr ⊢ ( ( ( 𝑃 / 4 ) ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝑃 / 4 ) < ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∧ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 ) → ( 𝑃 / 4 ) ≤ 𝑘 ) )
31 20 27 29 30 syl3anc ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( ( 𝑃 / 4 ) < ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ∧ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 ) → ( 𝑃 / 4 ) ≤ 𝑘 ) )
32 31 expd ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( 𝑃 / 4 ) < ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) → ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 → ( 𝑃 / 4 ) ≤ 𝑘 ) ) )
33 32 adantld ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( 𝑃 / 4 ) ∧ ( 𝑃 / 4 ) < ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ) → ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 → ( 𝑃 / 4 ) ≤ 𝑘 ) ) )
34 22 33 mpd ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 → ( 𝑃 / 4 ) ≤ 𝑘 ) )
35 34 imp ⊢ ( ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) ∧ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 ) → ( 𝑃 / 4 ) ≤ 𝑘 )
36 14 rehalfcld ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ∈ ℝ )
37 36 adantl ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( 𝑃 / 2 ) ∈ ℝ )
38 2re ⊢ 2 ∈ ℝ
39 38 a1i ⊢ ( 𝑘 ∈ ℤ → 2 ∈ ℝ )
40 28 39 remulcld ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 · 2 ) ∈ ℝ )
41 40 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( 𝑘 · 2 ) ∈ ℝ )
42 2pos ⊢ 0 < 2
43 38 42 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
44 43 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
45 lediv1 ⊢ ( ( ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑘 · 2 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ↔ ( ( 𝑃 / 2 ) / 2 ) ≤ ( ( 𝑘 · 2 ) / 2 ) ) )
46 37 41 44 45 syl3anc ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ↔ ( ( 𝑃 / 2 ) / 2 ) ≤ ( ( 𝑘 · 2 ) / 2 ) ) )
47 nncn ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℂ )
48 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
49 48 a1i ⊢ ( 𝑃 ∈ ℕ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
50 divdiv1 ⊢ ( ( 𝑃 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑃 / 2 ) / 2 ) = ( 𝑃 / ( 2 · 2 ) ) )
51 47 49 49 50 syl3anc ⊢ ( 𝑃 ∈ ℕ → ( ( 𝑃 / 2 ) / 2 ) = ( 𝑃 / ( 2 · 2 ) ) )
52 2t2e4 ⊢ ( 2 · 2 ) = 4
53 52 oveq2i ⊢ ( 𝑃 / ( 2 · 2 ) ) = ( 𝑃 / 4 )
54 51 53 eqtrdi ⊢ ( 𝑃 ∈ ℕ → ( ( 𝑃 / 2 ) / 2 ) = ( 𝑃 / 4 ) )
55 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
56 2cnd ⊢ ( 𝑘 ∈ ℤ → 2 ∈ ℂ )
57 2ne0 ⊢ 2 ≠ 0
58 57 a1i ⊢ ( 𝑘 ∈ ℤ → 2 ≠ 0 )
59 55 56 58 divcan4d ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑘 · 2 ) / 2 ) = 𝑘 )
60 54 59 breqan12rd ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( ( 𝑃 / 2 ) / 2 ) ≤ ( ( 𝑘 · 2 ) / 2 ) ↔ ( 𝑃 / 4 ) ≤ 𝑘 ) )
61 46 60 bitrd ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ↔ ( 𝑃 / 4 ) ≤ 𝑘 ) )
62 61 adantr ⊢ ( ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) ∧ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 ) → ( ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ↔ ( 𝑃 / 4 ) ≤ 𝑘 ) )
63 35 62 mpbird ⊢ ( ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℕ ) ∧ ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 ) → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) )
64 63 exp31 ⊢ ( 𝑘 ∈ ℤ → ( 𝑃 ∈ ℕ → ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ) ) )
65 64 com23 ⊢ ( 𝑘 ∈ ℤ → ( ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ 𝑘 → ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ) ) )
66 13 65 biimtrid ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑘 → ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ) ) )
67 66 3ad2ant3 ⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑘 → ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ) ) )
68 67 com12 ⊢ ( ( 𝑀 + 1 ) ≤ 𝑘 → ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ) ) )
69 68 adantr ⊢ ( ( ( 𝑀 + 1 ) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻 ) → ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ) ) )
70 69 impcom ⊢ ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( ( 𝑀 + 1 ) ≤ 𝑘 ∧ 𝑘 ≤ 𝐻 ) ) → ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ) )
71 11 70 sylbi ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ) )
72 71 impcom ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) )
73 elfzelz ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 𝑘 ∈ ℤ )
74 73 zred ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 𝑘 ∈ ℝ )
75 38 a1i ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 2 ∈ ℝ )
76 74 75 remulcld ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℝ )
77 lenlt ⊢ ( ( ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑘 · 2 ) ∈ ℝ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ↔ ¬ ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) )
78 36 76 77 syl2an ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑘 · 2 ) ↔ ¬ ( 𝑘 · 2 ) < ( 𝑃 / 2 ) ) )
79 72 78 mpbid ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ¬ ( 𝑘 · 2 ) < ( 𝑃 / 2 ) )
80 10 79 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ¬ ( 𝑘 · 2 ) < ( 𝑃 / 2 ) )
81 80 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) ∧ 𝑥 = 𝑘 ) → ¬ ( 𝑘 · 2 ) < ( 𝑃 / 2 ) )
82 81 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) ∧ 𝑥 = 𝑘 ) → if ( ( 𝑘 · 2 ) < ( 𝑃 / 2 ) , ( 𝑘 · 2 ) , ( 𝑃 − ( 𝑘 · 2 ) ) ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
83 9 82 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) ∧ 𝑥 = 𝑘 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
84 1 4 gausslemma2dlem0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
85 nn0p1nn ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ )
86 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
87 85 86 eleqtrdi ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
88 84 87 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
89 fzss1 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝑀 + 1 ) ... 𝐻 ) ⊆ ( 1 ... 𝐻 ) )
90 88 89 syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝐻 ) ⊆ ( 1 ... 𝐻 ) )
91 90 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → 𝑘 ∈ ( 1 ... 𝐻 ) )
92 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑃 − ( 𝑘 · 2 ) ) ∈ V )
93 3 83 91 92 fvmptd2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
94 93 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) )