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	$⊢ (K \in ℕ \land \neg \exists n \in ℕ_{0} K = 2^{n}) \to \exists p \in (ℙ ∖ \{2\}) p ∥ K$

Proof

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

Metamath Proof Explorer

Theorem oddprmdvds

Proof