Metamath Proof Explorer

Theorem sfprmdvdsmersenne

Description: If Q is a safe prime (i.e. Q = ( ( 2 x. P ) + 1 ) for a prime P ) with Q == 7 (mod 8 ), then Q divides the P-th Mersenne number M_P. (Contributed by AV, 20-Aug-2021)

Ref Expression
Assertion sfprmdvdsmersenne 
|- ( ( P e. Prime /\ ( Q e. Prime /\ ( Q mod 8 ) = 7 /\ Q = ( ( 2 x. P ) + 1 ) ) ) -> Q || ( ( 2 ^ P ) - 1 ) )

Proof

Step Hyp Ref Expression
1 olc 
 |-  ( ( Q mod 8 ) = 7 -> ( ( Q mod 8 ) = 1 \/ ( Q mod 8 ) = 7 ) )
2 ovex 
 |-  ( Q mod 8 ) e. _V
3 elprg 
 |-  ( ( Q mod 8 ) e. _V -> ( ( Q mod 8 ) e. { 1 , 7 } <-> ( ( Q mod 8 ) = 1 \/ ( Q mod 8 ) = 7 ) ) )
4 2 3 mp1i 
 |-  ( ( Q mod 8 ) = 7 -> ( ( Q mod 8 ) e. { 1 , 7 } <-> ( ( Q mod 8 ) = 1 \/ ( Q mod 8 ) = 7 ) ) )
5 1 4 mpbird 
 |-  ( ( Q mod 8 ) = 7 -> ( Q mod 8 ) e. { 1 , 7 } )
6 2lgs 
 |-  ( Q e. Prime -> ( ( 2 /L Q ) = 1 <-> ( Q mod 8 ) e. { 1 , 7 } ) )
7 6 ad2antlr 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( 2 /L Q ) = 1 <-> ( Q mod 8 ) e. { 1 , 7 } ) )
8 2z 
 |-  2 e. ZZ
9 simpr 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> Q e. Prime )
10 9 adantr 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> Q e. Prime )
11 2re 
 |-  2 e. RR
12 11 a1i 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> 2 e. RR )
13 2m1e1 
 |-  ( 2 - 1 ) = 1
14 11 a1i 
 |-  ( P e. Prime -> 2 e. RR )
15 prmnn 
 |-  ( P e. Prime -> P e. NN )
16 15 nnred 
 |-  ( P e. Prime -> P e. RR )
17 1lt2 
 |-  1 < 2
18 17 a1i 
 |-  ( P e. Prime -> 1 < 2 )
19 prmgt1 
 |-  ( P e. Prime -> 1 < P )
20 14 16 18 19 mulgt1d 
 |-  ( P e. Prime -> 1 < ( 2 x. P ) )
21 13 20 eqbrtrid 
 |-  ( P e. Prime -> ( 2 - 1 ) < ( 2 x. P ) )
22 1red 
 |-  ( P e. Prime -> 1 e. RR )
23 2nn 
 |-  2 e. NN
24 23 a1i 
 |-  ( P e. Prime -> 2 e. NN )
25 24 15 nnmulcld 
 |-  ( P e. Prime -> ( 2 x. P ) e. NN )
26 25 nnred 
 |-  ( P e. Prime -> ( 2 x. P ) e. RR )
27 14 22 26 ltsubaddd 
 |-  ( P e. Prime -> ( ( 2 - 1 ) < ( 2 x. P ) <-> 2 < ( ( 2 x. P ) + 1 ) ) )
28 21 27 mpbid 
 |-  ( P e. Prime -> 2 < ( ( 2 x. P ) + 1 ) )
29 28 ad2antrr 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> 2 < ( ( 2 x. P ) + 1 ) )
30 breq2 
 |-  ( Q = ( ( 2 x. P ) + 1 ) -> ( 2 < Q <-> 2 < ( ( 2 x. P ) + 1 ) ) )
31 30 adantl 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( 2 < Q <-> 2 < ( ( 2 x. P ) + 1 ) ) )
32 29 31 mpbird 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> 2 < Q )
33 12 32 gtned 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> Q =/= 2 )
34 eldifsn 
 |-  ( Q e. ( Prime \ { 2 } ) <-> ( Q e. Prime /\ Q =/= 2 ) )
35 10 33 34 sylanbrc 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> Q e. ( Prime \ { 2 } ) )
36 lgsqrmodndvds 
 |-  ( ( 2 e. ZZ /\ Q e. ( Prime \ { 2 } ) ) -> ( ( 2 /L Q ) = 1 -> E. m e. ZZ ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) /\ -. Q || m ) ) )
37 8 35 36 sylancr 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( 2 /L Q ) = 1 -> E. m e. ZZ ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) /\ -. Q || m ) ) )
38 prmnn 
 |-  ( Q e. Prime -> Q e. NN )
39 38 nncnd 
 |-  ( Q e. Prime -> Q e. CC )
40 39 adantl 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> Q e. CC )
41 1cnd 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> 1 e. CC )
42 2cnd 
 |-  ( P e. Prime -> 2 e. CC )
43 15 nncnd 
 |-  ( P e. Prime -> P e. CC )
44 42 43 mulcld 
 |-  ( P e. Prime -> ( 2 x. P ) e. CC )
45 44 adantr 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( 2 x. P ) e. CC )
46 40 41 45 subadd2d 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( ( Q - 1 ) = ( 2 x. P ) <-> ( ( 2 x. P ) + 1 ) = Q ) )
47 prmz 
 |-  ( Q e. Prime -> Q e. ZZ )
48 peano2zm 
 |-  ( Q e. ZZ -> ( Q - 1 ) e. ZZ )
49 47 48 syl 
 |-  ( Q e. Prime -> ( Q - 1 ) e. ZZ )
50 49 zcnd 
 |-  ( Q e. Prime -> ( Q - 1 ) e. CC )
51 50 adantl 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( Q - 1 ) e. CC )
52 43 adantr 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> P e. CC )
53 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
54 53 a1i 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( 2 e. CC /\ 2 =/= 0 ) )
55 divmul2 
 |-  ( ( ( Q - 1 ) e. CC /\ P e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( Q - 1 ) / 2 ) = P <-> ( Q - 1 ) = ( 2 x. P ) ) )
56 51 52 54 55 syl3anc 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( ( ( Q - 1 ) / 2 ) = P <-> ( Q - 1 ) = ( 2 x. P ) ) )
57 eqcom 
 |-  ( Q = ( ( 2 x. P ) + 1 ) <-> ( ( 2 x. P ) + 1 ) = Q )
58 57 a1i 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( Q = ( ( 2 x. P ) + 1 ) <-> ( ( 2 x. P ) + 1 ) = Q ) )
59 46 56 58 3bitr4rd 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( Q = ( ( 2 x. P ) + 1 ) <-> ( ( Q - 1 ) / 2 ) = P ) )
60 59 biimpa 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( Q - 1 ) / 2 ) = P )
61 oveq2 
 |-  ( ( ( Q - 1 ) / 2 ) = P -> ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) )
62 zsqcl 
 |-  ( m e. ZZ -> ( m ^ 2 ) e. ZZ )
63 62 ad2antlr 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) ) -> ( m ^ 2 ) e. ZZ )
64 8 a1i 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) ) -> 2 e. ZZ )
65 oveq1 
 |-  ( Q = ( ( 2 x. P ) + 1 ) -> ( Q - 1 ) = ( ( ( 2 x. P ) + 1 ) - 1 ) )
66 65 adantl 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( Q - 1 ) = ( ( ( 2 x. P ) + 1 ) - 1 ) )
67 66 oveq1d 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( Q - 1 ) / 2 ) = ( ( ( ( 2 x. P ) + 1 ) - 1 ) / 2 ) )
68 pncan1 
 |-  ( ( 2 x. P ) e. CC -> ( ( ( 2 x. P ) + 1 ) - 1 ) = ( 2 x. P ) )
69 44 68 syl 
 |-  ( P e. Prime -> ( ( ( 2 x. P ) + 1 ) - 1 ) = ( 2 x. P ) )
70 69 oveq1d 
 |-  ( P e. Prime -> ( ( ( ( 2 x. P ) + 1 ) - 1 ) / 2 ) = ( ( 2 x. P ) / 2 ) )
71 2ne0 
 |-  2 =/= 0
72 71 a1i 
 |-  ( P e. Prime -> 2 =/= 0 )
73 43 42 72 divcan3d 
 |-  ( P e. Prime -> ( ( 2 x. P ) / 2 ) = P )
74 70 73 eqtrd 
 |-  ( P e. Prime -> ( ( ( ( 2 x. P ) + 1 ) - 1 ) / 2 ) = P )
75 74 ad2antrr 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( ( ( 2 x. P ) + 1 ) - 1 ) / 2 ) = P )
76 67 75 eqtrd 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( Q - 1 ) / 2 ) = P )
77 15 nnnn0d 
 |-  ( P e. Prime -> P e. NN0 )
78 77 ad2antrr 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> P e. NN0 )
79 76 78 eqeltrd 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( Q - 1 ) / 2 ) e. NN0 )
80 38 nnrpd 
 |-  ( Q e. Prime -> Q e. RR+ )
81 80 ad2antlr 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> Q e. RR+ )
82 79 81 jca 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( ( Q - 1 ) / 2 ) e. NN0 /\ Q e. RR+ ) )
83 82 ad2antrr 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) ) -> ( ( ( Q - 1 ) / 2 ) e. NN0 /\ Q e. RR+ ) )
84 simpr 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) ) -> ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) )
85 modexp 
 |-  ( ( ( ( m ^ 2 ) e. ZZ /\ 2 e. ZZ ) /\ ( ( ( Q - 1 ) / 2 ) e. NN0 /\ Q e. RR+ ) /\ ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) ) -> ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) mod Q ) )
86 63 64 83 84 85 syl211anc 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) ) -> ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) mod Q ) )
87 86 ex 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) -> ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) mod Q ) ) )
88 87 adantr 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) -> ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) -> ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) mod Q ) ) )
89 2cnd 
 |-  ( Q e. Prime -> 2 e. CC )
90 71 a1i 
 |-  ( Q e. Prime -> 2 =/= 0 )
91 50 89 90 divcan2d 
 |-  ( Q e. Prime -> ( 2 x. ( ( Q - 1 ) / 2 ) ) = ( Q - 1 ) )
92 91 eqcomd 
 |-  ( Q e. Prime -> ( Q - 1 ) = ( 2 x. ( ( Q - 1 ) / 2 ) ) )
93 92 oveq2d 
 |-  ( Q e. Prime -> ( m ^ ( Q - 1 ) ) = ( m ^ ( 2 x. ( ( Q - 1 ) / 2 ) ) ) )
94 93 ad3antlr 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( m ^ ( Q - 1 ) ) = ( m ^ ( 2 x. ( ( Q - 1 ) / 2 ) ) ) )
95 zcn 
 |-  ( m e. ZZ -> m e. CC )
96 95 adantl 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> m e. CC )
97 79 adantr 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( ( Q - 1 ) / 2 ) e. NN0 )
98 2nn0 
 |-  2 e. NN0
99 98 a1i 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> 2 e. NN0 )
100 96 97 99 expmuld 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( m ^ ( 2 x. ( ( Q - 1 ) / 2 ) ) ) = ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) )
101 94 100 eqtr2d 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) = ( m ^ ( Q - 1 ) ) )
102 101 oveq1d 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( m ^ ( Q - 1 ) ) mod Q ) )
103 102 adantr 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) -> ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( m ^ ( Q - 1 ) ) mod Q ) )
104 vfermltl 
 |-  ( ( Q e. Prime /\ m e. ZZ /\ -. Q || m ) -> ( ( m ^ ( Q - 1 ) ) mod Q ) = 1 )
105 104 ad5ant245 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) -> ( ( m ^ ( Q - 1 ) ) mod Q ) = 1 )
106 103 105 eqtrd 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) -> ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = 1 )
107 oveq1 
 |-  ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( 2 ^ P ) mod Q ) )
108 106 107 eqeqan12d 
 |-  ( ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) /\ ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) ) -> ( ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) mod Q ) <-> 1 = ( ( 2 ^ P ) mod Q ) ) )
109 id 
 |-  ( 1 = ( ( 2 ^ P ) mod Q ) -> 1 = ( ( 2 ^ P ) mod Q ) )
110 109 eqcomd 
 |-  ( 1 = ( ( 2 ^ P ) mod Q ) -> ( ( 2 ^ P ) mod Q ) = 1 )
111 38 nnred 
 |-  ( Q e. Prime -> Q e. RR )
112 prmgt1 
 |-  ( Q e. Prime -> 1 < Q )
113 1mod 
 |-  ( ( Q e. RR /\ 1 < Q ) -> ( 1 mod Q ) = 1 )
114 111 112 113 syl2anc 
 |-  ( Q e. Prime -> ( 1 mod Q ) = 1 )
115 114 eqcomd 
 |-  ( Q e. Prime -> 1 = ( 1 mod Q ) )
116 115 ad3antlr 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> 1 = ( 1 mod Q ) )
117 110 116 sylan9eqr 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ 1 = ( ( 2 ^ P ) mod Q ) ) -> ( ( 2 ^ P ) mod Q ) = ( 1 mod Q ) )
118 38 ad4antlr 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ 1 = ( ( 2 ^ P ) mod Q ) ) -> Q e. NN )
119 zexpcl 
 |-  ( ( 2 e. ZZ /\ P e. NN0 ) -> ( 2 ^ P ) e. ZZ )
120 8 77 119 sylancr 
 |-  ( P e. Prime -> ( 2 ^ P ) e. ZZ )
121 120 ad4antr 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ 1 = ( ( 2 ^ P ) mod Q ) ) -> ( 2 ^ P ) e. ZZ )
122 1zzd 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ 1 = ( ( 2 ^ P ) mod Q ) ) -> 1 e. ZZ )
123 moddvds 
 |-  ( ( Q e. NN /\ ( 2 ^ P ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( 2 ^ P ) mod Q ) = ( 1 mod Q ) <-> Q || ( ( 2 ^ P ) - 1 ) ) )
124 118 121 122 123 syl3anc 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ 1 = ( ( 2 ^ P ) mod Q ) ) -> ( ( ( 2 ^ P ) mod Q ) = ( 1 mod Q ) <-> Q || ( ( 2 ^ P ) - 1 ) ) )
125 117 124 mpbid 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ 1 = ( ( 2 ^ P ) mod Q ) ) -> Q || ( ( 2 ^ P ) - 1 ) )
126 125 ex 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( 1 = ( ( 2 ^ P ) mod Q ) -> Q || ( ( 2 ^ P ) - 1 ) ) )
127 126 ad2antrr 
 |-  ( ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) /\ ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) ) -> ( 1 = ( ( 2 ^ P ) mod Q ) -> Q || ( ( 2 ^ P ) - 1 ) ) )
128 108 127 sylbid 
 |-  ( ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) /\ ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) ) -> ( ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) mod Q ) -> Q || ( ( 2 ^ P ) - 1 ) ) )
129 128 ex 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> ( ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) mod Q ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) )
130 129 com23 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) -> ( ( ( ( m ^ 2 ) ^ ( ( Q - 1 ) / 2 ) ) mod Q ) = ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) mod Q ) -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) )
131 88 130 syld 
 |-  ( ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) /\ -. Q || m ) -> ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) )
132 131 ex 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( -. Q || m -> ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) ) )
133 132 com23 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) -> ( -. Q || m -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) ) )
134 133 impd 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) /\ -. Q || m ) -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) )
135 134 com23 
 |-  ( ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) /\ m e. ZZ ) -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> ( ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) /\ -. Q || m ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) )
136 135 ex 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( m e. ZZ -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> ( ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) /\ -. Q || m ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) ) )
137 136 com23 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( 2 ^ ( ( Q - 1 ) / 2 ) ) = ( 2 ^ P ) -> ( m e. ZZ -> ( ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) /\ -. Q || m ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) ) )
138 61 137 syl5 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( ( Q - 1 ) / 2 ) = P -> ( m e. ZZ -> ( ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) /\ -. Q || m ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) ) )
139 60 138 mpd 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( m e. ZZ -> ( ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) /\ -. Q || m ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) )
140 139 rexlimdv 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( E. m e. ZZ ( ( ( m ^ 2 ) mod Q ) = ( 2 mod Q ) /\ -. Q || m ) -> Q || ( ( 2 ^ P ) - 1 ) ) )
141 37 140 syld 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( 2 /L Q ) = 1 -> Q || ( ( 2 ^ P ) - 1 ) ) )
142 7 141 sylbird 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( Q mod 8 ) e. { 1 , 7 } -> Q || ( ( 2 ^ P ) - 1 ) ) )
143 5 142 syl5 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ Q = ( ( 2 x. P ) + 1 ) ) -> ( ( Q mod 8 ) = 7 -> Q || ( ( 2 ^ P ) - 1 ) ) )
144 143 ex 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( Q = ( ( 2 x. P ) + 1 ) -> ( ( Q mod 8 ) = 7 -> Q || ( ( 2 ^ P ) - 1 ) ) ) )
145 144 com23 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( ( Q mod 8 ) = 7 -> ( Q = ( ( 2 x. P ) + 1 ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) )
146 145 ex 
 |-  ( P e. Prime -> ( Q e. Prime -> ( ( Q mod 8 ) = 7 -> ( Q = ( ( 2 x. P ) + 1 ) -> Q || ( ( 2 ^ P ) - 1 ) ) ) ) )
147 146 3imp2 
 |-  ( ( P e. Prime /\ ( Q e. Prime /\ ( Q mod 8 ) = 7 /\ Q = ( ( 2 x. P ) + 1 ) ) ) -> Q || ( ( 2 ^ P ) - 1 ) )