Metamath Proof Explorer

Theorem 2lgslem3

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

Ref Expression
Hypothesis 2lgslem2.n ⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
Assertion 2lgslem3 ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) )

Proof

Step Hyp Ref Expression
1 2lgslem2.n ⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
2 nnz ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℤ )
3 lgsdir2lem3 ⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑃 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) )
4 2 3 sylan ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑃 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) )
5 elun ⊢ ( ( 𝑃 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) ↔ ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } ∨ ( 𝑃 mod 8 ) ∈ { 3 , 5 } ) )
6 ovex ⊢ ( 𝑃 mod 8 ) ∈ V
7 6 elpr ⊢ ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } ↔ ( ( 𝑃 mod 8 ) = 1 ∨ ( 𝑃 mod 8 ) = 7 ) )
8 1 2lgslem3a1 ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 mod 8 ) = 1 ) → ( 𝑁 mod 2 ) = 0 )
9 8 a1d ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 mod 8 ) = 1 ) → ( ¬ 2 ∥ 𝑃 → ( 𝑁 mod 2 ) = 0 ) )
10 9 expcom ⊢ ( ( 𝑃 mod 8 ) = 1 → ( 𝑃 ∈ ℕ → ( ¬ 2 ∥ 𝑃 → ( 𝑁 mod 2 ) = 0 ) ) )
11 10 impd ⊢ ( ( 𝑃 mod 8 ) = 1 → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = 0 ) )
12 1 2lgslem3d1 ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 mod 8 ) = 7 ) → ( 𝑁 mod 2 ) = 0 )
13 12 a1d ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 mod 8 ) = 7 ) → ( ¬ 2 ∥ 𝑃 → ( 𝑁 mod 2 ) = 0 ) )
14 13 expcom ⊢ ( ( 𝑃 mod 8 ) = 7 → ( 𝑃 ∈ ℕ → ( ¬ 2 ∥ 𝑃 → ( 𝑁 mod 2 ) = 0 ) ) )
15 14 impd ⊢ ( ( 𝑃 mod 8 ) = 7 → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = 0 ) )
16 11 15 jaoi ⊢ ( ( ( 𝑃 mod 8 ) = 1 ∨ ( 𝑃 mod 8 ) = 7 ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = 0 ) )
17 7 16 sylbi ⊢ ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = 0 ) )
18 17 imp ⊢ ( ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } ∧ ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ) → ( 𝑁 mod 2 ) = 0 )
19 iftrue ⊢ ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } → if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) = 0 )
20 19 adantr ⊢ ( ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } ∧ ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ) → if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) = 0 )
21 18 20 eqtr4d ⊢ ( ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } ∧ ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ) → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) )
22 21 ex ⊢ ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) ) )
23 6 elpr ⊢ ( ( 𝑃 mod 8 ) ∈ { 3 , 5 } ↔ ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) )
24 1 2lgslem3b1 ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 mod 8 ) = 3 ) → ( 𝑁 mod 2 ) = 1 )
25 24 expcom ⊢ ( ( 𝑃 mod 8 ) = 3 → ( 𝑃 ∈ ℕ → ( 𝑁 mod 2 ) = 1 ) )
26 1 2lgslem3c1 ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 mod 8 ) = 5 ) → ( 𝑁 mod 2 ) = 1 )
27 26 expcom ⊢ ( ( 𝑃 mod 8 ) = 5 → ( 𝑃 ∈ ℕ → ( 𝑁 mod 2 ) = 1 ) )
28 25 27 jaoi ⊢ ( ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) → ( 𝑃 ∈ ℕ → ( 𝑁 mod 2 ) = 1 ) )
29 28 imp ⊢ ( ( ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) ∧ 𝑃 ∈ ℕ ) → ( 𝑁 mod 2 ) = 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 ⊢ ( ( 𝑃 mod 8 ) = 3 → ( ( 𝑃 mod 8 ) = 1 ↔ 3 = 1 ) )
40 39 notbid ⊢ ( ( 𝑃 mod 8 ) = 3 → ( ¬ ( 𝑃 mod 8 ) = 1 ↔ ¬ 3 = 1 ) )
41 eqeq1 ⊢ ( ( 𝑃 mod 8 ) = 3 → ( ( 𝑃 mod 8 ) = 7 ↔ 3 = 7 ) )
42 41 notbid ⊢ ( ( 𝑃 mod 8 ) = 3 → ( ¬ ( 𝑃 mod 8 ) = 7 ↔ ¬ 3 = 7 ) )
43 40 42 anbi12d ⊢ ( ( 𝑃 mod 8 ) = 3 → ( ( ¬ ( 𝑃 mod 8 ) = 1 ∧ ¬ ( 𝑃 mod 8 ) = 7 ) ↔ ( ¬ 3 = 1 ∧ ¬ 3 = 7 ) ) )
44 38 43 mpbiri ⊢ ( ( 𝑃 mod 8 ) = 3 → ( ¬ ( 𝑃 mod 8 ) = 1 ∧ ¬ ( 𝑃 mod 8 ) = 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 ⊢ ( ( 𝑃 mod 8 ) = 5 → ( ( 𝑃 mod 8 ) = 1 ↔ 5 = 1 ) )
54 53 notbid ⊢ ( ( 𝑃 mod 8 ) = 5 → ( ¬ ( 𝑃 mod 8 ) = 1 ↔ ¬ 5 = 1 ) )
55 eqeq1 ⊢ ( ( 𝑃 mod 8 ) = 5 → ( ( 𝑃 mod 8 ) = 7 ↔ 5 = 7 ) )
56 55 notbid ⊢ ( ( 𝑃 mod 8 ) = 5 → ( ¬ ( 𝑃 mod 8 ) = 7 ↔ ¬ 5 = 7 ) )
57 54 56 anbi12d ⊢ ( ( 𝑃 mod 8 ) = 5 → ( ( ¬ ( 𝑃 mod 8 ) = 1 ∧ ¬ ( 𝑃 mod 8 ) = 7 ) ↔ ( ¬ 5 = 1 ∧ ¬ 5 = 7 ) ) )
58 52 57 mpbiri ⊢ ( ( 𝑃 mod 8 ) = 5 → ( ¬ ( 𝑃 mod 8 ) = 1 ∧ ¬ ( 𝑃 mod 8 ) = 7 ) )
59 44 58 jaoi ⊢ ( ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) → ( ¬ ( 𝑃 mod 8 ) = 1 ∧ ¬ ( 𝑃 mod 8 ) = 7 ) )
60 59 adantr ⊢ ( ( ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) ∧ 𝑃 ∈ ℕ ) → ( ¬ ( 𝑃 mod 8 ) = 1 ∧ ¬ ( 𝑃 mod 8 ) = 7 ) )
61 ioran ⊢ ( ¬ ( ( 𝑃 mod 8 ) = 1 ∨ ( 𝑃 mod 8 ) = 7 ) ↔ ( ¬ ( 𝑃 mod 8 ) = 1 ∧ ¬ ( 𝑃 mod 8 ) = 7 ) )
62 61 7 xchnxbir ⊢ ( ¬ ( 𝑃 mod 8 ) ∈ { 1 , 7 } ↔ ( ¬ ( 𝑃 mod 8 ) = 1 ∧ ¬ ( 𝑃 mod 8 ) = 7 ) )
63 60 62 sylibr ⊢ ( ( ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) ∧ 𝑃 ∈ ℕ ) → ¬ ( 𝑃 mod 8 ) ∈ { 1 , 7 } )
64 63 iffalsed ⊢ ( ( ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) ∧ 𝑃 ∈ ℕ ) → if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) = 1 )
65 29 64 eqtr4d ⊢ ( ( ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) ∧ 𝑃 ∈ ℕ ) → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) )
66 65 a1d ⊢ ( ( ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) ∧ 𝑃 ∈ ℕ ) → ( ¬ 2 ∥ 𝑃 → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) ) )
67 66 expimpd ⊢ ( ( ( 𝑃 mod 8 ) = 3 ∨ ( 𝑃 mod 8 ) = 5 ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) ) )
68 23 67 sylbi ⊢ ( ( 𝑃 mod 8 ) ∈ { 3 , 5 } → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) ) )
69 22 68 jaoi ⊢ ( ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } ∨ ( 𝑃 mod 8 ) ∈ { 3 , 5 } ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) ) )
70 5 69 sylbi ⊢ ( ( 𝑃 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) → ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) ) )
71 4 70 mpcom ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑁 mod 2 ) = if ( ( 𝑃 mod 8 ) ∈ { 1 , 7 } , 0 , 1 ) )