Metamath Proof Explorer

Theorem fppr2odd

Description: A Fermat pseudoprime to the base 2 is odd. (Contributed by AV, 5-Jun-2023)

Ref Expression
Assertion fppr2odd ( 𝑋 ∈ ( FPPr ‘ 2 ) → 𝑋 ∈ Odd )

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 fpprel ⊢ ( 2 ∈ ℕ → ( 𝑋 ∈ ( FPPr ‘ 2 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) ) )
3 1 2 ax-mp ⊢ ( 𝑋 ∈ ( FPPr ‘ 2 ) ↔ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) )
4 eluz4nn ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ℕ )
5 4 adantr ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → 𝑋 ∈ ℕ )
6 eluzelz ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ℤ )
7 zeo2ALTV ⊢ ( 𝑋 ∈ ℤ → ( 𝑋 ∈ Even ↔ ¬ 𝑋 ∈ Odd ) )
8 6 7 syl ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑋 ∈ Even ↔ ¬ 𝑋 ∈ Odd ) )
9 8 adantr ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → ( 𝑋 ∈ Even ↔ ¬ 𝑋 ∈ Odd ) )
10 9 biimprd ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → ( ¬ 𝑋 ∈ Odd → 𝑋 ∈ Even ) )
11 nnennexALTV ⊢ ( ( 𝑋 ∈ ℕ ∧ 𝑋 ∈ Even ) → ∃ 𝑦 ∈ ℕ 𝑋 = ( 2 · 𝑦 ) )
12 5 10 11 syl6an ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → ( ¬ 𝑋 ∈ Odd → ∃ 𝑦 ∈ ℕ 𝑋 = ( 2 · 𝑦 ) ) )
13 oveq1 ⊢ ( 𝑋 = ( 2 · 𝑦 ) → ( 𝑋 − 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
14 13 oveq2d ⊢ ( 𝑋 = ( 2 · 𝑦 ) → ( 2 ↑ ( 𝑋 − 1 ) ) = ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) )
15 id ⊢ ( 𝑋 = ( 2 · 𝑦 ) → 𝑋 = ( 2 · 𝑦 ) )
16 14 15 oveq12d ⊢ ( 𝑋 = ( 2 · 𝑦 ) → ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) mod ( 2 · 𝑦 ) ) )
17 16 eqeq1d ⊢ ( 𝑋 = ( 2 · 𝑦 ) → ( ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ↔ ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) mod ( 2 · 𝑦 ) ) = 1 ) )
18 17 adantl ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑋 = ( 2 · 𝑦 ) ) → ( ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ↔ ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) mod ( 2 · 𝑦 ) ) = 1 ) )
19 2z ⊢ 2 ∈ ℤ
20 1 a1i ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℕ )
21 id ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ )
22 20 21 nnmulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℕ )
23 nnm1nn0 ⊢ ( ( 2 · 𝑦 ) ∈ ℕ → ( ( 2 · 𝑦 ) − 1 ) ∈ ℕ0 )
24 22 23 syl ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) − 1 ) ∈ ℕ0 )
25 zexpcl ⊢ ( ( 2 ∈ ℤ ∧ ( ( 2 · 𝑦 ) − 1 ) ∈ ℕ0 ) → ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ℤ )
26 19 24 25 sylancr ⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ℤ )
27 22 nnrpd ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℝ+ )
28 modmuladdim ⊢ ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ℤ ∧ ( 2 · 𝑦 ) ∈ ℝ+ ) → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) mod ( 2 · 𝑦 ) ) = 1 → ∃ 𝑚 ∈ ℤ ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) = ( ( 𝑚 · ( 2 · 𝑦 ) ) + 1 ) ) )
29 26 27 28 syl2anc ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) mod ( 2 · 𝑦 ) ) = 1 → ∃ 𝑚 ∈ ℤ ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) = ( ( 𝑚 · ( 2 · 𝑦 ) ) + 1 ) ) )
30 24 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 · 𝑦 ) − 1 ) ∈ ℕ0 )
31 19 30 25 sylancr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ℤ )
32 31 zcnd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ℂ )
33 zcn ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℂ )
34 33 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℂ )
35 2cnd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → 2 ∈ ℂ )
36 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
37 36 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → 𝑦 ∈ ℂ )
38 35 37 mulcld ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 · 𝑦 ) ∈ ℂ )
39 34 38 mulcld ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 𝑚 · ( 2 · 𝑦 ) ) ∈ ℂ )
40 1cnd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → 1 ∈ ℂ )
41 subadd ⊢ ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ℂ ∧ ( 𝑚 · ( 2 · 𝑦 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) − ( 𝑚 · ( 2 · 𝑦 ) ) ) = 1 ↔ ( ( 𝑚 · ( 2 · 𝑦 ) ) + 1 ) = ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) ) )
42 eqcom ⊢ ( ( ( 𝑚 · ( 2 · 𝑦 ) ) + 1 ) = ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) ↔ ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) = ( ( 𝑚 · ( 2 · 𝑦 ) ) + 1 ) )
43 41 42 bitrdi ⊢ ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) ∈ ℂ ∧ ( 𝑚 · ( 2 · 𝑦 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) − ( 𝑚 · ( 2 · 𝑦 ) ) ) = 1 ↔ ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) = ( ( 𝑚 · ( 2 · 𝑦 ) ) + 1 ) ) )
44 32 39 40 43 syl3anc ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) − ( 𝑚 · ( 2 · 𝑦 ) ) ) = 1 ↔ ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) = ( ( 𝑚 · ( 2 · 𝑦 ) ) + 1 ) ) )
45 2cnd ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℂ )
46 45 36 mulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℂ )
47 1cnd ⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℂ )
48 46 47 subcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) − 1 ) ∈ ℂ )
49 48 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 · 𝑦 ) − 1 ) ∈ ℂ )
50 npcan1 ⊢ ( ( ( 2 · 𝑦 ) − 1 ) ∈ ℂ → ( ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) + 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
51 49 50 syl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) + 1 ) = ( ( 2 · 𝑦 ) − 1 ) )
52 51 eqcomd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 · 𝑦 ) − 1 ) = ( ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) + 1 ) )
53 52 oveq2d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) = ( 2 ↑ ( ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) + 1 ) ) )
54 2t1e2 ⊢ ( 2 · 1 ) = 2
55 54 eqcomi ⊢ 2 = ( 2 · 1 )
56 55 oveq2i ⊢ ( ( 2 · 𝑦 ) − 2 ) = ( ( 2 · 𝑦 ) − ( 2 · 1 ) )
57 sub1m1 ⊢ ( ( 2 · 𝑦 ) ∈ ℂ → ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) = ( ( 2 · 𝑦 ) − 2 ) )
58 38 57 syl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) = ( ( 2 · 𝑦 ) − 2 ) )
59 35 37 40 subdid ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 · ( 𝑦 − 1 ) ) = ( ( 2 · 𝑦 ) − ( 2 · 1 ) ) )
60 56 58 59 3eqtr4a ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) = ( 2 · ( 𝑦 − 1 ) ) )
61 2nn0 ⊢ 2 ∈ ℕ0
62 61 a1i ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → 2 ∈ ℕ0 )
63 nnm1nn0 ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 − 1 ) ∈ ℕ0 )
64 63 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 𝑦 − 1 ) ∈ ℕ0 )
65 62 64 nn0mulcld ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 · ( 𝑦 − 1 ) ) ∈ ℕ0 )
66 60 65 eqeltrd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ∈ ℕ0 )
67 35 66 expp1d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 ↑ ( ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) + 1 ) ) = ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) · 2 ) )
68 35 66 expcld ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) ∈ ℂ )
69 68 35 mulcomd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) · 2 ) = ( 2 · ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) ) )
70 67 69 eqtrd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 ↑ ( ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) + 1 ) ) = ( 2 · ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) ) )
71 53 70 eqtrd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) = ( 2 · ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) ) )
72 34 35 37 mul12d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 𝑚 · ( 2 · 𝑦 ) ) = ( 2 · ( 𝑚 · 𝑦 ) ) )
73 71 72 oveq12d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) − ( 𝑚 · ( 2 · 𝑦 ) ) ) = ( ( 2 · ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) ) − ( 2 · ( 𝑚 · 𝑦 ) ) ) )
74 34 37 mulcld ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 𝑚 · 𝑦 ) ∈ ℂ )
75 35 68 74 subdid ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) = ( ( 2 · ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) ) − ( 2 · ( 𝑚 · 𝑦 ) ) ) )
76 75 eqcomd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 · ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) ) − ( 2 · ( 𝑚 · 𝑦 ) ) ) = ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) )
77 73 76 eqtrd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) − ( 𝑚 · ( 2 · 𝑦 ) ) ) = ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) )
78 77 eqeq1d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) − ( 𝑚 · ( 2 · 𝑦 ) ) ) = 1 ↔ ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) = 1 ) )
79 zexpcl ⊢ ( ( 2 ∈ ℤ ∧ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ∈ ℕ0 ) → ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) ∈ ℤ )
80 19 66 79 sylancr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) ∈ ℤ )
81 simpr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ )
82 nnz ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
83 82 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → 𝑦 ∈ ℤ )
84 81 83 zmulcld ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 𝑚 · 𝑦 ) ∈ ℤ )
85 80 84 zsubcld ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ∈ ℤ )
86 m2even ⊢ ( ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ∈ ℤ → ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) ∈ Even )
87 85 86 syl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) ∈ Even )
88 1oddALTV ⊢ 1 ∈ Odd
89 zneoALTV ⊢ ( ( ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) ∈ Even ∧ 1 ∈ Odd ) → ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) ≠ 1 )
90 87 88 89 sylancl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) ≠ 1 )
91 eqneqall ⊢ ( ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) = 1 → ( ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) ≠ 1 → 𝑋 ∈ Odd ) )
92 90 91 syl5com ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 · ( ( 2 ↑ ( ( ( 2 · 𝑦 ) − 1 ) − 1 ) ) − ( 𝑚 · 𝑦 ) ) ) = 1 → 𝑋 ∈ Odd ) )
93 78 92 sylbid ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) − ( 𝑚 · ( 2 · 𝑦 ) ) ) = 1 → 𝑋 ∈ Odd ) )
94 44 93 sylbird ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ ) → ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) = ( ( 𝑚 · ( 2 · 𝑦 ) ) + 1 ) → 𝑋 ∈ Odd ) )
95 94 rexlimdva ⊢ ( 𝑦 ∈ ℕ → ( ∃ 𝑚 ∈ ℤ ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) = ( ( 𝑚 · ( 2 · 𝑦 ) ) + 1 ) → 𝑋 ∈ Odd ) )
96 29 95 syld ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) mod ( 2 · 𝑦 ) ) = 1 → 𝑋 ∈ Odd ) )
97 96 adantl ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑦 ∈ ℕ ) → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) mod ( 2 · 𝑦 ) ) = 1 → 𝑋 ∈ Odd ) )
98 97 adantr ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑋 = ( 2 · 𝑦 ) ) → ( ( ( 2 ↑ ( ( 2 · 𝑦 ) − 1 ) ) mod ( 2 · 𝑦 ) ) = 1 → 𝑋 ∈ Odd ) )
99 18 98 sylbid ⊢ ( ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑋 = ( 2 · 𝑦 ) ) → ( ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 → 𝑋 ∈ Odd ) )
100 99 ex ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑦 ∈ ℕ ) → ( 𝑋 = ( 2 · 𝑦 ) → ( ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 → 𝑋 ∈ Odd ) ) )
101 100 rexlimdva ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → ( ∃ 𝑦 ∈ ℕ 𝑋 = ( 2 · 𝑦 ) → ( ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 → 𝑋 ∈ Odd ) ) )
102 101 com23 ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → ( ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 → ( ∃ 𝑦 ∈ ℕ 𝑋 = ( 2 · 𝑦 ) → 𝑋 ∈ Odd ) ) )
103 102 imp ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → ( ∃ 𝑦 ∈ ℕ 𝑋 = ( 2 · 𝑦 ) → 𝑋 ∈ Odd ) )
104 12 103 syld ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → ( ¬ 𝑋 ∈ Odd → 𝑋 ∈ Odd ) )
105 104 3adant2 ⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑋 ∉ ℙ ∧ ( ( 2 ↑ ( 𝑋 − 1 ) ) mod 𝑋 ) = 1 ) → ( ¬ 𝑋 ∈ Odd → 𝑋 ∈ Odd ) )
106 3 105 sylbi ⊢ ( 𝑋 ∈ ( FPPr ‘ 2 ) → ( ¬ 𝑋 ∈ Odd → 𝑋 ∈ Odd ) )
107 106 pm2.18d ⊢ ( 𝑋 ∈ ( FPPr ‘ 2 ) → 𝑋 ∈ Odd )