Metamath Proof Explorer

Theorem 2lgslem3

Description: Lemma 3 for 2lgs . (Contributed by AV, 16-Jul-2021)

Ref Expression
Hypothesis 2lgslem2.n ⊢N=P−12−P4
Assertion 2lgslem3 ⊢P∈ℕ∧¬2∥P→Nmod2=ifPmod8∈1701

Proof

Step Hyp Ref Expression
1 2lgslem2.n ⊢N=P−12−P4
2 nnz ⊢P∈ℕ→P∈ℤ
3 lgsdir2lem3 ⊢P∈ℤ∧¬2∥P→Pmod8∈17∪35
4 2 3 sylan ⊢P∈ℕ∧¬2∥P→Pmod8∈17∪35
5 elun ⊢Pmod8∈17∪35↔Pmod8∈17∨Pmod8∈35
6 ovex ⊢Pmod8∈V
7 6 elpr ⊢Pmod8∈17↔Pmod8=1∨Pmod8=7
8 1 2lgslem3a1 ⊢P∈ℕ∧Pmod8=1→Nmod2=0
9 8 a1d ⊢P∈ℕ∧Pmod8=1→¬2∥P→Nmod2=0
10 9 expcom ⊢Pmod8=1→P∈ℕ→¬2∥P→Nmod2=0
11 10 impd ⊢Pmod8=1→P∈ℕ∧¬2∥P→Nmod2=0
12 1 2lgslem3d1 ⊢P∈ℕ∧Pmod8=7→Nmod2=0
13 12 a1d ⊢P∈ℕ∧Pmod8=7→¬2∥P→Nmod2=0
14 13 expcom ⊢Pmod8=7→P∈ℕ→¬2∥P→Nmod2=0
15 14 impd ⊢Pmod8=7→P∈ℕ∧¬2∥P→Nmod2=0
16 11 15 jaoi ⊢Pmod8=1∨Pmod8=7→P∈ℕ∧¬2∥P→Nmod2=0
17 7 16 sylbi ⊢Pmod8∈17→P∈ℕ∧¬2∥P→Nmod2=0
18 17 imp ⊢Pmod8∈17∧P∈ℕ∧¬2∥P→Nmod2=0
19 iftrue ⊢Pmod8∈17→ifPmod8∈1701=0
20 19 adantr ⊢Pmod8∈17∧P∈ℕ∧¬2∥P→ifPmod8∈1701=0
21 18 20 eqtr4d ⊢Pmod8∈17∧P∈ℕ∧¬2∥P→Nmod2=ifPmod8∈1701
22 21 ex ⊢Pmod8∈17→P∈ℕ∧¬2∥P→Nmod2=ifPmod8∈1701
23 6 elpr ⊢Pmod8∈35↔Pmod8=3∨Pmod8=5
24 1 2lgslem3b1 ⊢P∈ℕ∧Pmod8=3→Nmod2=1
25 24 expcom ⊢Pmod8=3→P∈ℕ→Nmod2=1
26 1 2lgslem3c1 ⊢P∈ℕ∧Pmod8=5→Nmod2=1
27 26 expcom ⊢Pmod8=5→P∈ℕ→Nmod2=1
28 25 27 jaoi ⊢Pmod8=3∨Pmod8=5→P∈ℕ→Nmod2=1
29 28 imp ⊢Pmod8=3∨Pmod8=5∧P∈ℕ→Nmod2=1
30 1re ⊢1∈ℝ
31 1lt3 ⊢1<3
32 30 31 ltneii ⊢1≠3
33 32 nesymi ⊢¬3=1
34 3re ⊢3∈ℝ
35 3lt7 ⊢3<7
36 34 35 ltneii ⊢3≠7
37 36 neii ⊢¬3=7
38 33 37 pm3.2i ⊢¬3=1∧¬3=7
39 eqeq1 ⊢Pmod8=3→Pmod8=1↔3=1
40 39 notbid ⊢Pmod8=3→¬Pmod8=1↔¬3=1
41 eqeq1 ⊢Pmod8=3→Pmod8=7↔3=7
42 41 notbid ⊢Pmod8=3→¬Pmod8=7↔¬3=7
43 40 42 anbi12d ⊢Pmod8=3→¬Pmod8=1∧¬Pmod8=7↔¬3=1∧¬3=7
44 38 43 mpbiri ⊢Pmod8=3→¬Pmod8=1∧¬Pmod8=7
45 1lt5 ⊢1<5
46 30 45 ltneii ⊢1≠5
47 46 nesymi ⊢¬5=1
48 5re ⊢5∈ℝ
49 5lt7 ⊢5<7
50 48 49 ltneii ⊢5≠7
51 50 neii ⊢¬5=7
52 47 51 pm3.2i ⊢¬5=1∧¬5=7
53 eqeq1 ⊢Pmod8=5→Pmod8=1↔5=1
54 53 notbid ⊢Pmod8=5→¬Pmod8=1↔¬5=1
55 eqeq1 ⊢Pmod8=5→Pmod8=7↔5=7
56 55 notbid ⊢Pmod8=5→¬Pmod8=7↔¬5=7
57 54 56 anbi12d ⊢Pmod8=5→¬Pmod8=1∧¬Pmod8=7↔¬5=1∧¬5=7
58 52 57 mpbiri ⊢Pmod8=5→¬Pmod8=1∧¬Pmod8=7
59 44 58 jaoi ⊢Pmod8=3∨Pmod8=5→¬Pmod8=1∧¬Pmod8=7
60 59 adantr ⊢Pmod8=3∨Pmod8=5∧P∈ℕ→¬Pmod8=1∧¬Pmod8=7
61 ioran ⊢¬Pmod8=1∨Pmod8=7↔¬Pmod8=1∧¬Pmod8=7
62 61 7 xchnxbir ⊢¬Pmod8∈17↔¬Pmod8=1∧¬Pmod8=7
63 60 62 sylibr ⊢Pmod8=3∨Pmod8=5∧P∈ℕ→¬Pmod8∈17
64 63 iffalsed ⊢Pmod8=3∨Pmod8=5∧P∈ℕ→ifPmod8∈1701=1
65 29 64 eqtr4d ⊢Pmod8=3∨Pmod8=5∧P∈ℕ→Nmod2=ifPmod8∈1701
66 65 a1d ⊢Pmod8=3∨Pmod8=5∧P∈ℕ→¬2∥P→Nmod2=ifPmod8∈1701
67 66 expimpd ⊢Pmod8=3∨Pmod8=5→P∈ℕ∧¬2∥P→Nmod2=ifPmod8∈1701
68 23 67 sylbi ⊢Pmod8∈35→P∈ℕ∧¬2∥P→Nmod2=ifPmod8∈1701
69 22 68 jaoi ⊢Pmod8∈17∨Pmod8∈35→P∈ℕ∧¬2∥P→Nmod2=ifPmod8∈1701
70 5 69 sylbi ⊢Pmod8∈17∪35→P∈ℕ∧¬2∥P→Nmod2=ifPmod8∈1701
71 4 70 mpcom ⊢P∈ℕ∧¬2∥P→Nmod2=ifPmod8∈1701