Metamath Proof Explorer


Theorem 2lgsoddprmlem3

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

Ref Expression
Assertion 2lgsoddprmlem3 N ¬ 2 N R = N mod 8 2 R 2 1 8 R 1 7

Proof

Step Hyp Ref Expression
1 lgsdir2lem3 N ¬ 2 N N mod 8 1 7 3 5
2 eleq1 N mod 8 = R N mod 8 1 7 3 5 R 1 7 3 5
3 2 eqcoms R = N mod 8 N mod 8 1 7 3 5 R 1 7 3 5
4 elun R 1 7 3 5 R 1 7 R 3 5
5 elpri R 3 5 R = 3 R = 5
6 oveq1 R = 3 R 2 = 3 2
7 6 oveq1d R = 3 R 2 1 = 3 2 1
8 7 oveq1d R = 3 R 2 1 8 = 3 2 1 8
9 2lgsoddprmlem3b 3 2 1 8 = 1
10 8 9 eqtrdi R = 3 R 2 1 8 = 1
11 10 breq2d R = 3 2 R 2 1 8 2 1
12 n2dvds1 ¬ 2 1
13 12 pm2.21i 2 1 R 1 7
14 11 13 syl6bi R = 3 2 R 2 1 8 R 1 7
15 oveq1 R = 5 R 2 = 5 2
16 15 oveq1d R = 5 R 2 1 = 5 2 1
17 16 oveq1d R = 5 R 2 1 8 = 5 2 1 8
18 17 breq2d R = 5 2 R 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 syl6bb R = 5 2 R 2 1 8 2 3
22 n2dvds3 ¬ 2 3
23 22 pm2.21i 2 3 R 1 7
24 21 23 syl6bi R = 5 2 R 2 1 8 R 1 7
25 14 24 jaoi R = 3 R = 5 2 R 2 1 8 R 1 7
26 5 25 syl R 3 5 2 R 2 1 8 R 1 7
27 26 jao1i R 1 7 R 3 5 2 R 2 1 8 R 1 7
28 4 27 sylbi R 1 7 3 5 2 R 2 1 8 R 1 7
29 elpri R 1 7 R = 1 R = 7
30 z0even 2 0
31 oveq1 R = 1 R 2 = 1 2
32 31 oveq1d R = 1 R 2 1 = 1 2 1
33 32 oveq1d R = 1 R 2 1 8 = 1 2 1 8
34 2lgsoddprmlem3a 1 2 1 8 = 0
35 33 34 eqtrdi R = 1 R 2 1 8 = 0
36 30 35 breqtrrid R = 1 2 R 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 R = 7 R 2 = 7 2
42 41 oveq1d R = 7 R 2 1 = 7 2 1
43 42 oveq1d R = 7 R 2 1 8 = 7 2 1 8
44 2lgsoddprmlem3d 7 2 1 8 = 2 3
45 43 44 eqtrdi R = 7 R 2 1 8 = 2 3
46 40 45 breqtrrid R = 7 2 R 2 1 8
47 36 46 jaoi R = 1 R = 7 2 R 2 1 8
48 29 47 syl R 1 7 2 R 2 1 8
49 28 48 impbid1 R 1 7 3 5 2 R 2 1 8 R 1 7
50 3 49 syl6bi R = N mod 8 N mod 8 1 7 3 5 2 R 2 1 8 R 1 7
51 1 50 syl5com N ¬ 2 N R = N mod 8 2 R 2 1 8 R 1 7
52 51 3impia N ¬ 2 N R = N mod 8 2 R 2 1 8 R 1 7