Metamath Proof Explorer

Theorem 2lgslem1a1

Description: Lemma 1 for 2lgslem1a . (Contributed by AV, 16-Jun-2021)

Ref Expression
Assertion 2lgslem1a1 ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ∀ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑖 · 2 ) = ( ( 𝑖 · 2 ) mod 𝑃 ) )

Proof

Step Hyp Ref Expression
1 nnrp ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ+ )
2 1 adantr ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → 𝑃 ∈ ℝ+ )
3 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑖 ∈ ℤ )
4 zre ⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℝ )
5 2re ⊢ 2 ∈ ℝ
6 5 a1i ⊢ ( 𝑖 ∈ ℤ → 2 ∈ ℝ )
7 4 6 remulcld ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 · 2 ) ∈ ℝ )
8 3 7 syl ⊢ ( 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 𝑖 · 2 ) ∈ ℝ )
9 2 8 anim12ci ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑖 · 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) )
10 elfznn ⊢ ( 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑖 ∈ ℕ )
11 nnre ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℝ )
12 nnnn0 ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℕ0 )
13 12 nn0ge0d ⊢ ( 𝑖 ∈ ℕ → 0 ≤ 𝑖 )
14 0le2 ⊢ 0 ≤ 2
15 5 14 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 ≤ 2 )
16 15 a1i ⊢ ( 𝑖 ∈ ℕ → ( 2 ∈ ℝ ∧ 0 ≤ 2 ) )
17 mulge0 ⊢ ( ( ( 𝑖 ∈ ℝ ∧ 0 ≤ 𝑖 ) ∧ ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ) → 0 ≤ ( 𝑖 · 2 ) )
18 11 13 16 17 syl21anc ⊢ ( 𝑖 ∈ ℕ → 0 ≤ ( 𝑖 · 2 ) )
19 10 18 syl ⊢ ( 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 0 ≤ ( 𝑖 · 2 ) )
20 19 adantl ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 0 ≤ ( 𝑖 · 2 ) )
21 elfz2 ⊢ ( 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 1 ≤ 𝑖 ∧ 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
22 4 3ad2ant3 ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → 𝑖 ∈ ℝ )
23 zre ⊢ ( ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
24 23 3ad2ant2 ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
25 2pos ⊢ 0 < 2
26 5 25 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
27 26 a1i ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
28 lemul1 ⊢ ( ( 𝑖 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) ↔ ( 𝑖 · 2 ) ≤ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) ) )
29 22 24 27 28 syl3anc ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) ↔ ( 𝑖 · 2 ) ≤ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) ) )
30 nncn ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℂ )
31 peano2cnm ⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − 1 ) ∈ ℂ )
32 30 31 syl ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℂ )
33 2cnd ⊢ ( 𝑃 ∈ ℕ → 2 ∈ ℂ )
34 2ne0 ⊢ 2 ≠ 0
35 34 a1i ⊢ ( 𝑃 ∈ ℕ → 2 ≠ 0 )
36 32 33 35 divcan1d ⊢ ( 𝑃 ∈ ℕ → ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) = ( 𝑃 − 1 ) )
37 36 adantr ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) = ( 𝑃 − 1 ) )
38 37 adantl ⊢ ( ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ) → ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) = ( 𝑃 − 1 ) )
39 38 breq2d ⊢ ( ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ) → ( ( 𝑖 · 2 ) ≤ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) ↔ ( 𝑖 · 2 ) ≤ ( 𝑃 − 1 ) ) )
40 id ⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℤ )
41 2z ⊢ 2 ∈ ℤ
42 41 a1i ⊢ ( 𝑖 ∈ ℤ → 2 ∈ ℤ )
43 40 42 zmulcld ⊢ ( 𝑖 ∈ ℤ → ( 𝑖 · 2 ) ∈ ℤ )
44 43 3ad2ant3 ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 · 2 ) ∈ ℤ )
45 nnz ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℤ )
46 45 adantr ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → 𝑃 ∈ ℤ )
47 zltlem1 ⊢ ( ( ( 𝑖 · 2 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑖 · 2 ) < 𝑃 ↔ ( 𝑖 · 2 ) ≤ ( 𝑃 − 1 ) ) )
48 44 46 47 syl2an ⊢ ( ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ) → ( ( 𝑖 · 2 ) < 𝑃 ↔ ( 𝑖 · 2 ) ≤ ( 𝑃 − 1 ) ) )
49 48 biimprd ⊢ ( ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ) → ( ( 𝑖 · 2 ) ≤ ( 𝑃 − 1 ) → ( 𝑖 · 2 ) < 𝑃 ) )
50 39 49 sylbid ⊢ ( ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ) → ( ( 𝑖 · 2 ) ≤ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) → ( 𝑖 · 2 ) < 𝑃 ) )
51 50 ex ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑖 · 2 ) ≤ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) → ( 𝑖 · 2 ) < 𝑃 ) ) )
52 51 com23 ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 𝑖 · 2 ) ≤ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑖 · 2 ) < 𝑃 ) ) )
53 29 52 sylbid ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑖 · 2 ) < 𝑃 ) ) )
54 53 a1d ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 1 ≤ 𝑖 → ( 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑖 · 2 ) < 𝑃 ) ) ) )
55 54 imp32 ⊢ ( ( ( 1 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 1 ≤ 𝑖 ∧ 𝑖 ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑖 · 2 ) < 𝑃 ) )
56 21 55 sylbi ⊢ ( 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑖 · 2 ) < 𝑃 ) )
57 56 impcom ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑖 · 2 ) < 𝑃 )
58 modid ⊢ ( ( ( ( 𝑖 · 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑖 · 2 ) ∧ ( 𝑖 · 2 ) < 𝑃 ) ) → ( ( 𝑖 · 2 ) mod 𝑃 ) = ( 𝑖 · 2 ) )
59 9 20 57 58 syl12anc ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑖 · 2 ) mod 𝑃 ) = ( 𝑖 · 2 ) )
60 59 eqcomd ⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑖 · 2 ) = ( ( 𝑖 · 2 ) mod 𝑃 ) )
61 60 ralrimiva ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ∀ 𝑖 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( 𝑖 · 2 ) = ( ( 𝑖 · 2 ) mod 𝑃 ) )