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 ( ( 𝑃 ∈ ℙ ∧ ( 𝑄 ∈ ℙ ∧ ( 𝑄 mod 8 ) = 7 ∧ 𝑄 = ( ( 2 · 𝑃 ) + 1 ) ) ) → 𝑄 ∥ ( ( 2 ↑ 𝑃 ) − 1 ) )

Proof

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