Metamath Proof Explorer


Theorem 2lgslem1a

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

Ref Expression
Assertion 2lgslem1a P ¬ 2 P x | i 1 P 1 2 x = i 2 P 2 < x mod P = x | i P 4 + 1 P 1 2 x = i 2

Proof

Step Hyp Ref Expression
1 prmnn P P
2 1 nnnn0d P P 0
3 2 ad2antrr P ¬ 2 P x P 0
4 4nn 4
5 3 4 jctir P ¬ 2 P x P 0 4
6 fldivnn0 P 0 4 P 4 0
7 nn0p1nn P 4 0 P 4 + 1
8 5 6 7 3syl P ¬ 2 P x P 4 + 1
9 elnnuz P 4 + 1 P 4 + 1 1
10 8 9 sylib P ¬ 2 P x P 4 + 1 1
11 fzss1 P 4 + 1 1 P 4 + 1 P 1 2 1 P 1 2
12 rexss P 4 + 1 P 1 2 1 P 1 2 i P 4 + 1 P 1 2 x = i 2 i 1 P 1 2 i P 4 + 1 P 1 2 x = i 2
13 10 11 12 3syl P ¬ 2 P x i P 4 + 1 P 1 2 x = i 2 i 1 P 1 2 i P 4 + 1 P 1 2 x = i 2
14 ancom i P 4 + 1 P 1 2 x = i 2 x = i 2 i P 4 + 1 P 1 2
15 2 4 jctir P P 0 4
16 15 6 syl P P 4 0
17 16 nn0zd P P 4
18 17 ad2antrr P ¬ 2 P x P 4
19 elfzelz i 1 P 1 2 i
20 zltp1le P 4 i P 4 < i P 4 + 1 i
21 18 19 20 syl2an P ¬ 2 P x i 1 P 1 2 P 4 < i P 4 + 1 i
22 21 bicomd P ¬ 2 P x i 1 P 1 2 P 4 + 1 i P 4 < i
23 22 anbi1d P ¬ 2 P x i 1 P 1 2 P 4 + 1 i i P 1 2 P 4 < i i P 1 2
24 19 adantl P ¬ 2 P x i 1 P 1 2 i
25 17 peano2zd P P 4 + 1
26 25 adantr P ¬ 2 P P 4 + 1
27 26 ad2antrr P ¬ 2 P x i 1 P 1 2 P 4 + 1
28 prmz P P
29 oddm1d2 P ¬ 2 P P 1 2
30 28 29 syl P ¬ 2 P P 1 2
31 30 biimpa P ¬ 2 P P 1 2
32 31 ad2antrr P ¬ 2 P x i 1 P 1 2 P 1 2
33 elfz i P 4 + 1 P 1 2 i P 4 + 1 P 1 2 P 4 + 1 i i P 1 2
34 24 27 32 33 syl3anc P ¬ 2 P x i 1 P 1 2 i P 4 + 1 P 1 2 P 4 + 1 i i P 1 2
35 elfzle2 i 1 P 1 2 i P 1 2
36 35 adantl P ¬ 2 P x i 1 P 1 2 i P 1 2
37 36 biantrud P ¬ 2 P x i 1 P 1 2 P 4 < i P 4 < i i P 1 2
38 23 34 37 3bitr4d P ¬ 2 P x i 1 P 1 2 i P 4 + 1 P 1 2 P 4 < i
39 28 ad2antrr P ¬ 2 P x P
40 2lgslem1a2 P i P 4 < i P 2 < i 2
41 39 19 40 syl2an P ¬ 2 P x i 1 P 1 2 P 4 < i P 2 < i 2
42 38 41 bitrd P ¬ 2 P x i 1 P 1 2 i P 4 + 1 P 1 2 P 2 < i 2
43 2lgslem1a1 P ¬ 2 P k 1 P 1 2 k 2 = k 2 mod P
44 1 43 sylan P ¬ 2 P k 1 P 1 2 k 2 = k 2 mod P
45 44 adantr P ¬ 2 P x k 1 P 1 2 k 2 = k 2 mod P
46 oveq1 k = i k 2 = i 2
47 46 oveq1d k = i k 2 mod P = i 2 mod P
48 46 47 eqeq12d k = i k 2 = k 2 mod P i 2 = i 2 mod P
49 48 rspccva k 1 P 1 2 k 2 = k 2 mod P i 1 P 1 2 i 2 = i 2 mod P
50 45 49 sylan P ¬ 2 P x i 1 P 1 2 i 2 = i 2 mod P
51 50 breq2d P ¬ 2 P x i 1 P 1 2 P 2 < i 2 P 2 < i 2 mod P
52 42 51 bitrd P ¬ 2 P x i 1 P 1 2 i P 4 + 1 P 1 2 P 2 < i 2 mod P
53 oveq1 x = i 2 x mod P = i 2 mod P
54 53 eqcomd x = i 2 i 2 mod P = x mod P
55 54 breq2d x = i 2 P 2 < i 2 mod P P 2 < x mod P
56 52 55 sylan9bb P ¬ 2 P x i 1 P 1 2 x = i 2 i P 4 + 1 P 1 2 P 2 < x mod P
57 56 pm5.32da P ¬ 2 P x i 1 P 1 2 x = i 2 i P 4 + 1 P 1 2 x = i 2 P 2 < x mod P
58 14 57 syl5bb P ¬ 2 P x i 1 P 1 2 i P 4 + 1 P 1 2 x = i 2 x = i 2 P 2 < x mod P
59 58 rexbidva P ¬ 2 P x i 1 P 1 2 i P 4 + 1 P 1 2 x = i 2 i 1 P 1 2 x = i 2 P 2 < x mod P
60 13 59 bitrd P ¬ 2 P x i P 4 + 1 P 1 2 x = i 2 i 1 P 1 2 x = i 2 P 2 < x mod P
61 60 bicomd P ¬ 2 P x i 1 P 1 2 x = i 2 P 2 < x mod P i P 4 + 1 P 1 2 x = i 2
62 61 rabbidva P ¬ 2 P x | i 1 P 1 2 x = i 2 P 2 < x mod P = x | i P 4 + 1 P 1 2 x = i 2