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	syl6bi	⊢ ( 𝑅 = 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	syl6bi	⊢ ( 𝑅 = 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	syl6bi	⊢ ( 𝑅 = ( 𝑁 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 } ) )