Metamath Proof Explorer

Theorem 2lgsoddprmlem3

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

Ref Expression
Assertion 2lgsoddprmlem3 ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = ( 𝑁 mod 8 ) ) → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) ↔ 𝑅 ∈ { 1 , 7 } ) )

Proof

Step Hyp Ref Expression
1 lgsdir2lem3 ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑁 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) )
2 eleq1 ⊢ ( ( 𝑁 mod 8 ) = 𝑅 → ( ( 𝑁 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) ↔ 𝑅 ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) ) )
3 2 eqcoms ⊢ ( 𝑅 = ( 𝑁 mod 8 ) → ( ( 𝑁 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) ↔ 𝑅 ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) ) )
4 elun ⊢ ( 𝑅 ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) ↔ ( 𝑅 ∈ { 1 , 7 } ∨ 𝑅 ∈ { 3 , 5 } ) )
5 elpri ⊢ ( 𝑅 ∈ { 3 , 5 } → ( 𝑅 = 3 ∨ 𝑅 = 5 ) )
6 oveq1 ⊢ ( 𝑅 = 3 → ( 𝑅 ↑ 2 ) = ( 3 ↑ 2 ) )
7 6 oveq1d ⊢ ( 𝑅 = 3 → ( ( 𝑅 ↑ 2 ) − 1 ) = ( ( 3 ↑ 2 ) − 1 ) )
8 7 oveq1d ⊢ ( 𝑅 = 3 → ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) = ( ( ( 3 ↑ 2 ) − 1 ) / 8 ) )
9 2lgsoddprmlem3b ⊢ ( ( ( 3 ↑ 2 ) − 1 ) / 8 ) = 1
10 8 9 eqtrdi ⊢ ( 𝑅 = 3 → ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) = 1 )
11 10 breq2d ⊢ ( 𝑅 = 3 → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) ↔ 2 ∥ 1 ) )
12 n2dvds1 ⊢ ¬ 2 ∥ 1
13 12 pm2.21i ⊢ ( 2 ∥ 1 → 𝑅 ∈ { 1 , 7 } )
14 11 13 biimtrdi ⊢ ( 𝑅 = 3 → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) → 𝑅 ∈ { 1 , 7 } ) )
15 oveq1 ⊢ ( 𝑅 = 5 → ( 𝑅 ↑ 2 ) = ( 5 ↑ 2 ) )
16 15 oveq1d ⊢ ( 𝑅 = 5 → ( ( 𝑅 ↑ 2 ) − 1 ) = ( ( 5 ↑ 2 ) − 1 ) )
17 16 oveq1d ⊢ ( 𝑅 = 5 → ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) = ( ( ( 5 ↑ 2 ) − 1 ) / 8 ) )
18 17 breq2d ⊢ ( 𝑅 = 5 → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) ↔ 2 ∥ ( ( ( 5 ↑ 2 ) − 1 ) / 8 ) ) )
19 2lgsoddprmlem3c ⊢ ( ( ( 5 ↑ 2 ) − 1 ) / 8 ) = 3
20 19 breq2i ⊢ ( 2 ∥ ( ( ( 5 ↑ 2 ) − 1 ) / 8 ) ↔ 2 ∥ 3 )
21 18 20 bitrdi ⊢ ( 𝑅 = 5 → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) ↔ 2 ∥ 3 ) )
22 n2dvds3 ⊢ ¬ 2 ∥ 3
23 22 pm2.21i ⊢ ( 2 ∥ 3 → 𝑅 ∈ { 1 , 7 } )
24 21 23 biimtrdi ⊢ ( 𝑅 = 5 → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) → 𝑅 ∈ { 1 , 7 } ) )
25 14 24 jaoi ⊢ ( ( 𝑅 = 3 ∨ 𝑅 = 5 ) → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) → 𝑅 ∈ { 1 , 7 } ) )
26 5 25 syl ⊢ ( 𝑅 ∈ { 3 , 5 } → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) → 𝑅 ∈ { 1 , 7 } ) )
27 26 jao1i ⊢ ( ( 𝑅 ∈ { 1 , 7 } ∨ 𝑅 ∈ { 3 , 5 } ) → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) → 𝑅 ∈ { 1 , 7 } ) )
28 4 27 sylbi ⊢ ( 𝑅 ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) → 𝑅 ∈ { 1 , 7 } ) )
29 elpri ⊢ ( 𝑅 ∈ { 1 , 7 } → ( 𝑅 = 1 ∨ 𝑅 = 7 ) )
30 z0even ⊢ 2 ∥ 0
31 oveq1 ⊢ ( 𝑅 = 1 → ( 𝑅 ↑ 2 ) = ( 1 ↑ 2 ) )
32 31 oveq1d ⊢ ( 𝑅 = 1 → ( ( 𝑅 ↑ 2 ) − 1 ) = ( ( 1 ↑ 2 ) − 1 ) )
33 32 oveq1d ⊢ ( 𝑅 = 1 → ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) = ( ( ( 1 ↑ 2 ) − 1 ) / 8 ) )
34 2lgsoddprmlem3a ⊢ ( ( ( 1 ↑ 2 ) − 1 ) / 8 ) = 0
35 33 34 eqtrdi ⊢ ( 𝑅 = 1 → ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) = 0 )
36 30 35 breqtrrid ⊢ ( 𝑅 = 1 → 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) )
37 2z ⊢ 2 ∈ ℤ
38 3z ⊢ 3 ∈ ℤ
39 dvdsmul1 ⊢ ( ( 2 ∈ ℤ ∧ 3 ∈ ℤ ) → 2 ∥ ( 2 · 3 ) )
40 37 38 39 mp2an ⊢ 2 ∥ ( 2 · 3 )
41 oveq1 ⊢ ( 𝑅 = 7 → ( 𝑅 ↑ 2 ) = ( 7 ↑ 2 ) )
42 41 oveq1d ⊢ ( 𝑅 = 7 → ( ( 𝑅 ↑ 2 ) − 1 ) = ( ( 7 ↑ 2 ) − 1 ) )
43 42 oveq1d ⊢ ( 𝑅 = 7 → ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) = ( ( ( 7 ↑ 2 ) − 1 ) / 8 ) )
44 2lgsoddprmlem3d ⊢ ( ( ( 7 ↑ 2 ) − 1 ) / 8 ) = ( 2 · 3 )
45 43 44 eqtrdi ⊢ ( 𝑅 = 7 → ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) = ( 2 · 3 ) )
46 40 45 breqtrrid ⊢ ( 𝑅 = 7 → 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) )
47 36 46 jaoi ⊢ ( ( 𝑅 = 1 ∨ 𝑅 = 7 ) → 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) )
48 29 47 syl ⊢ ( 𝑅 ∈ { 1 , 7 } → 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) )
49 28 48 impbid1 ⊢ ( 𝑅 ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) ↔ 𝑅 ∈ { 1 , 7 } ) )
50 3 49 biimtrdi ⊢ ( 𝑅 = ( 𝑁 mod 8 ) → ( ( 𝑁 mod 8 ) ∈ ( { 1 , 7 } ∪ { 3 , 5 } ) → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) ↔ 𝑅 ∈ { 1 , 7 } ) ) )
51 1 50 syl5com ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑅 = ( 𝑁 mod 8 ) → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) ↔ 𝑅 ∈ { 1 , 7 } ) ) )
52 51 3impia ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑅 = ( 𝑁 mod 8 ) ) → ( 2 ∥ ( ( ( 𝑅 ↑ 2 ) − 1 ) / 8 ) ↔ 𝑅 ∈ { 1 , 7 } ) )