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 ) ) )