Metamath Proof Explorer

Theorem oddprmdvds

Description: Every positive integer which is not a power of two is divisible by an odd prime number. (Contributed by AV, 6-Aug-2021)

Ref Expression
Assertion oddprmdvds ( ( 𝐾 ∈ ℕ ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 )

Proof

Step Hyp Ref Expression
1 2prm ⊢ 2 ∈ ℙ
2 pcndvds2 ⊢ ( ( 2 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) )
3 1 2 mpan ⊢ ( 𝐾 ∈ ℕ → ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) )
4 pcdvds ⊢ ( ( 2 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∥ 𝐾 )
5 1 4 mpan ⊢ ( 𝐾 ∈ ℕ → ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∥ 𝐾 )
6 2nn ⊢ 2 ∈ ℕ
7 6 a1i ⊢ ( 𝐾 ∈ ℕ → 2 ∈ ℕ )
8 1 a1i ⊢ ( 𝐾 ∈ ℕ → 2 ∈ ℙ )
9 id ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ )
10 8 9 pccld ⊢ ( 𝐾 ∈ ℕ → ( 2 pCnt 𝐾 ) ∈ ℕ0 )
11 7 10 nnexpcld ⊢ ( 𝐾 ∈ ℕ → ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℕ )
12 nndivdvds ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℕ ) → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∥ 𝐾 ↔ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ℕ ) )
13 11 12 mpdan ⊢ ( 𝐾 ∈ ℕ → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∥ 𝐾 ↔ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ℕ ) )
14 13 adantr ⊢ ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∥ 𝐾 ↔ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ℕ ) )
15 elnn1uz2 ⊢ ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ℕ ↔ ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) = 1 ∨ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ( ℤ≥ ‘ 2 ) ) )
16 nncn ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℂ )
17 nncn ⊢ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℕ → ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ )
18 nnne0 ⊢ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℕ → ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 )
19 17 18 jca ⊢ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℕ → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 ) )
20 11 19 syl ⊢ ( 𝐾 ∈ ℕ → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 ) )
21 3anass ⊢ ( ( 𝐾 ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 ) ↔ ( 𝐾 ∈ ℂ ∧ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 ) ) )
22 16 20 21 sylanbrc ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 ) )
23 22 adantr ⊢ ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( 𝐾 ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 ) )
24 diveq1 ⊢ ( ( 𝐾 ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 ) → ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) = 1 ↔ 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) )
25 23 24 syl ⊢ ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) = 1 ↔ 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) )
26 10 adantr ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( 2 pCnt 𝐾 ) ∈ ℕ0 )
27 oveq2 ⊢ ( 𝑛 = ( 2 pCnt 𝐾 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 2 pCnt 𝐾 ) ) )
28 27 eqeq2d ⊢ ( 𝑛 = ( 2 pCnt 𝐾 ) → ( 𝐾 = ( 2 ↑ 𝑛 ) ↔ 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) )
29 28 adantl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∧ 𝑛 = ( 2 pCnt 𝐾 ) ) → ( 𝐾 = ( 2 ↑ 𝑛 ) ↔ 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) )
30 simpr ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) )
31 26 29 30 rspcedvd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) )
32 31 ex ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) )
33 pm2.24 ⊢ ( ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) )
34 32 33 syl6 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
35 34 adantr ⊢ ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( 𝐾 = ( 2 ↑ ( 2 pCnt 𝐾 ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
36 25 35 sylbid ⊢ ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) = 1 → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
37 36 com12 ⊢ ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) = 1 → ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
38 exprmfct ⊢ ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑞 ∈ ℙ 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) )
39 breq1 ⊢ ( 𝑞 = 2 → ( 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ↔ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) )
40 39 biimpcd ⊢ ( 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( 𝑞 = 2 → 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) )
41 40 adantl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( 𝑞 = 2 → 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) )
42 41 necon3bd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → 𝑞 ≠ 2 ) )
43 42 ex ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → 𝑞 ≠ 2 ) ) )
44 prmnn ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℕ )
45 5 13 mpbid ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ℕ )
46 nndivides ⊢ ( ( 𝑞 ∈ ℕ ∧ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ℕ ) → ( 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ↔ ∃ 𝑚 ∈ ℕ ( 𝑚 · 𝑞 ) = ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) )
47 44 45 46 syl2anr ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ↔ ∃ 𝑚 ∈ ℕ ( 𝑚 · 𝑞 ) = ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) )
48 eqcom ⊢ ( ( 𝑚 · 𝑞 ) = ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ↔ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) = ( 𝑚 · 𝑞 ) )
49 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → 𝐾 ∈ ℂ )
50 simpr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
51 44 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → 𝑞 ∈ ℕ )
52 50 51 nnmulcld ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 · 𝑞 ) ∈ ℕ )
53 52 nncnd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 · 𝑞 ) ∈ ℂ )
54 11 ad2antrr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℕ )
55 54 19 syl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 ) )
56 divmul ⊢ ( ( 𝐾 ∈ ℂ ∧ ( 𝑚 · 𝑞 ) ∈ ℂ ∧ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ ( 2 ↑ ( 2 pCnt 𝐾 ) ) ≠ 0 ) ) → ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) = ( 𝑚 · 𝑞 ) ↔ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) )
57 49 53 55 56 syl3anc ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) = ( 𝑚 · 𝑞 ) ↔ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) )
58 48 57 syl5bb ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 · 𝑞 ) = ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ↔ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) )
59 simpr ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → 𝑞 ∈ ℙ )
60 59 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → 𝑞 ∈ ℙ )
61 60 anim1i ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) → ( 𝑞 ∈ ℙ ∧ 𝑞 ≠ 2 ) )
62 eldifsn ⊢ ( 𝑞 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑞 ∈ ℙ ∧ 𝑞 ≠ 2 ) )
63 61 62 sylibr ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) → 𝑞 ∈ ( ℙ ∖ { 2 } ) )
64 63 adantr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) ∧ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) → 𝑞 ∈ ( ℙ ∖ { 2 } ) )
65 breq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∥ 𝐾 ↔ 𝑞 ∥ 𝐾 ) )
66 65 adantl ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) ∧ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) ∧ 𝑝 = 𝑞 ) → ( 𝑝 ∥ 𝐾 ↔ 𝑞 ∥ 𝐾 ) )
67 54 50 nnmulcld ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · 𝑚 ) ∈ ℕ )
68 67 nnzd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · 𝑚 ) ∈ ℤ )
69 44 nnzd ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ )
70 69 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → 𝑞 ∈ ℤ )
71 68 70 jca ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · 𝑚 ) ∈ ℤ ∧ 𝑞 ∈ ℤ ) )
72 71 adantr ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) → ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · 𝑚 ) ∈ ℤ ∧ 𝑞 ∈ ℤ ) )
73 dvdsmul2 ⊢ ( ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · 𝑚 ) ∈ ℤ ∧ 𝑞 ∈ ℤ ) → 𝑞 ∥ ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · 𝑚 ) · 𝑞 ) )
74 72 73 syl ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) → 𝑞 ∥ ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · 𝑚 ) · 𝑞 ) )
75 2nn0 ⊢ 2 ∈ ℕ0
76 75 a1i ⊢ ( 𝐾 ∈ ℕ → 2 ∈ ℕ0 )
77 76 10 nn0expcld ⊢ ( 𝐾 ∈ ℕ → ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℕ0 )
78 77 ad2antrr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℕ0 )
79 78 nn0cnd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ )
80 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
81 80 adantl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
82 44 nncnd ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℂ )
83 82 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → 𝑞 ∈ ℂ )
84 79 81 83 3jca ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑞 ∈ ℂ ) )
85 84 adantr ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑞 ∈ ℂ ) )
86 mulass ⊢ ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑞 ∈ ℂ ) → ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · 𝑚 ) · 𝑞 ) = ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) )
87 85 86 syl ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) → ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · 𝑚 ) · 𝑞 ) = ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) )
88 74 87 breqtrd ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) → 𝑞 ∥ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) )
89 88 adantr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) ∧ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) → 𝑞 ∥ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) )
90 breq2 ⊢ ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 → ( 𝑞 ∥ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) ↔ 𝑞 ∥ 𝐾 ) )
91 90 adantl ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) ∧ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) → ( 𝑞 ∥ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) ↔ 𝑞 ∥ 𝐾 ) )
92 89 91 mpbid ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) ∧ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) → 𝑞 ∥ 𝐾 )
93 64 66 92 rspcedvd ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) ∧ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 )
94 93 a1d ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑞 ≠ 2 ) ∧ ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) )
95 94 exp31 ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( 𝑞 ≠ 2 → ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) ) )
96 95 com23 ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) · ( 𝑚 · 𝑞 ) ) = 𝐾 → ( 𝑞 ≠ 2 → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) ) )
97 58 96 sylbid ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 · 𝑞 ) = ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( 𝑞 ≠ 2 → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) ) )
98 97 rexlimdva ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( ∃ 𝑚 ∈ ℕ ( 𝑚 · 𝑞 ) = ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( 𝑞 ≠ 2 → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) ) )
99 47 98 sylbid ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( 𝑞 ≠ 2 → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) ) )
100 43 99 syldd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) ) )
101 100 rexlimdva ⊢ ( 𝐾 ∈ ℕ → ( ∃ 𝑞 ∈ ℙ 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) ) )
102 101 com12 ⊢ ( ∃ 𝑞 ∈ ℙ 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( 𝐾 ∈ ℕ → ( ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) ) )
103 102 impd ⊢ ( ∃ 𝑞 ∈ ℙ 𝑞 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
104 38 103 syl ⊢ ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
105 37 104 jaoi ⊢ ( ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) = 1 ∨ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
106 15 105 sylbi ⊢ ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ℕ → ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
107 106 com12 ⊢ ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ∈ ℕ → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
108 14 107 sylbid ⊢ ( ( 𝐾 ∈ ℕ ∧ ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) ) → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∥ 𝐾 → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) )
109 108 ex ⊢ ( 𝐾 ∈ ℕ → ( ¬ 2 ∥ ( 𝐾 / ( 2 ↑ ( 2 pCnt 𝐾 ) ) ) → ( ( 2 ↑ ( 2 pCnt 𝐾 ) ) ∥ 𝐾 → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) ) ) )
110 3 5 109 mp2d ⊢ ( 𝐾 ∈ ℕ → ( ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 ) )
111 110 imp ⊢ ( ( 𝐾 ∈ ℕ ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 )