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	bitrid	⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑞 ∈ ℙ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 · 𝑞 ) = ( 𝐾 / ( 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 } ) 𝑝 ∥ 𝐾 )