Theorem 2lgslem1c

Description: Lemma 3 for 2lgslem1 . (Contributed by AV, 19-Jun-2021)

	Ref	Expression
Assertion	2lgslem1c	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2		nnnn0	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
3		oddnn02np1	⊢ ( 𝑃 ∈ ℕ0 → ( ¬ 2 ∥ 𝑃 ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) )
4	1 2 3	3syl	⊢ ( 𝑃 ∈ ℙ → ( ¬ 2 ∥ 𝑃 ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) )
5		iftrue	⊢ ( 2 ∥ 𝑛 → if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) = ( 𝑛 / 2 ) )
6	5	adantr	⊢ ( ( 2 ∥ 𝑛 ∧ 𝑛 ∈ ℕ0 ) → if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) = ( 𝑛 / 2 ) )
7		2nn	⊢ 2 ∈ ℕ
8		nn0ledivnn	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 2 ∈ ℕ ) → ( 𝑛 / 2 ) ≤ 𝑛 )
9	7 8	mpan2	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 / 2 ) ≤ 𝑛 )
10	9	adantl	⊢ ( ( 2 ∥ 𝑛 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 / 2 ) ≤ 𝑛 )
11	6 10	eqbrtrd	⊢ ( ( 2 ∥ 𝑛 ∧ 𝑛 ∈ ℕ0 ) → if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) ≤ 𝑛 )
12		iffalse	⊢ ( ¬ 2 ∥ 𝑛 → if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) = ( ( 𝑛 − 1 ) / 2 ) )
13	12	adantr	⊢ ( ( ¬ 2 ∥ 𝑛 ∧ 𝑛 ∈ ℕ0 ) → if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) = ( ( 𝑛 − 1 ) / 2 ) )
14		nn0re	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
15		peano2rem	⊢ ( 𝑛 ∈ ℝ → ( 𝑛 − 1 ) ∈ ℝ )
16	15	rehalfcld	⊢ ( 𝑛 ∈ ℝ → ( ( 𝑛 − 1 ) / 2 ) ∈ ℝ )
17	14 16	syl	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 − 1 ) / 2 ) ∈ ℝ )
18	14	rehalfcld	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 / 2 ) ∈ ℝ )
19	14	lem1d	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 − 1 ) ≤ 𝑛 )
20	14 15	syl	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 − 1 ) ∈ ℝ )
21		2re	⊢ 2 ∈ ℝ
22		2pos	⊢ 0 < 2
23	21 22	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
24	23	a1i	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ∈ ℝ ∧ 0 < 2 ) )
25		lediv1	⊢ ( ( ( 𝑛 − 1 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑛 − 1 ) ≤ 𝑛 ↔ ( ( 𝑛 − 1 ) / 2 ) ≤ ( 𝑛 / 2 ) ) )
26	20 14 24 25	syl3anc	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 − 1 ) ≤ 𝑛 ↔ ( ( 𝑛 − 1 ) / 2 ) ≤ ( 𝑛 / 2 ) ) )
27	19 26	mpbid	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 − 1 ) / 2 ) ≤ ( 𝑛 / 2 ) )
28	17 18 14 27 9	letrd	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 − 1 ) / 2 ) ≤ 𝑛 )
29	28	adantl	⊢ ( ( ¬ 2 ∥ 𝑛 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 − 1 ) / 2 ) ≤ 𝑛 )
30	13 29	eqbrtrd	⊢ ( ( ¬ 2 ∥ 𝑛 ∧ 𝑛 ∈ ℕ0 ) → if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) ≤ 𝑛 )
31	11 30	pm2.61ian	⊢ ( 𝑛 ∈ ℕ0 → if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) ≤ 𝑛 )
32	31	ad2antlr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) → if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) ≤ 𝑛 )
33		nn0z	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
34	33	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℤ )
35		eqcom	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ↔ 𝑃 = ( ( 2 · 𝑛 ) + 1 ) )
36	35	biimpi	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑃 → 𝑃 = ( ( 2 · 𝑛 ) + 1 ) )
37		flodddiv4	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑃 = ( ( 2 · 𝑛 ) + 1 ) ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) = if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) )
38	34 36 37	syl2an	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) = if ( 2 ∥ 𝑛 , ( 𝑛 / 2 ) , ( ( 𝑛 − 1 ) / 2 ) ) )
39		oveq1	⊢ ( 𝑃 = ( ( 2 · 𝑛 ) + 1 ) → ( 𝑃 − 1 ) = ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) )
40	39	eqcoms	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑃 → ( 𝑃 − 1 ) = ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) )
41	40	adantl	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) → ( 𝑃 − 1 ) = ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) )
42		2nn0	⊢ 2 ∈ ℕ0
43	42	a1i	⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ0 )
44		id	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 )
45	43 44	nn0mulcld	⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℕ0 )
46	45	nn0cnd	⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℂ )
47		pncan1	⊢ ( ( 2 · 𝑛 ) ∈ ℂ → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
48	46 47	syl	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
49	48	ad2antlr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
50	41 49	eqtrd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) → ( 𝑃 − 1 ) = ( 2 · 𝑛 ) )
51	50	oveq1d	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) → ( ( 𝑃 − 1 ) / 2 ) = ( ( 2 · 𝑛 ) / 2 ) )
52		nn0cn	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
53		2cnd	⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℂ )
54		2ne0	⊢ 2 ≠ 0
55	54	a1i	⊢ ( 𝑛 ∈ ℕ0 → 2 ≠ 0 )
56	52 53 55	divcan3d	⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 · 𝑛 ) / 2 ) = 𝑛 )
57	56	ad2antlr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) → ( ( 2 · 𝑛 ) / 2 ) = 𝑛 )
58	51 57	eqtrd	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) → ( ( 𝑃 − 1 ) / 2 ) = 𝑛 )
59	32 38 58	3brtr4d	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑃 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
60	59	rexlimdva2	⊢ ( 𝑃 ∈ ℙ → ( ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑃 → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
61	4 60	sylbid	⊢ ( 𝑃 ∈ ℙ → ( ¬ 2 ∥ 𝑃 → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
62	61	imp	⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 2 ∥ 𝑃 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )