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 syl5bi ( 𝑘 ∈ ℤ → ( ( 𝑀 + 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 ) ) )