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