aks4d1p8d2

Description: Any prime power dividing a positive integer is less than that integer if that integer has another prime factor. (Contributed by metakunt, 13-Nov-2024)

	Ref	Expression
Hypotheses	aks4d1p8d2.1	$⊢ φ \to R \in ℕ$
	aks4d1p8d2.2	$⊢ φ \to N \in ℕ$
	aks4d1p8d2.3	$⊢ φ \to P \in ℙ$
	aks4d1p8d2.4	$⊢ φ \to Q \in ℙ$
	aks4d1p8d2.5	$⊢ φ \to P ∥ R$
	aks4d1p8d2.6	$⊢ φ \to Q ∥ R$
	aks4d1p8d2.7	$⊢ φ \to \neg P ∥ N$
	aks4d1p8d2.8	$⊢ φ \to Q ∥ N$
Assertion	aks4d1p8d2	$⊢ φ \to P^{P pCnt R} < R$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p8d2.1	$⊢ φ \to R \in ℕ$
2		aks4d1p8d2.2	$⊢ φ \to N \in ℕ$
3		aks4d1p8d2.3	$⊢ φ \to P \in ℙ$
4		aks4d1p8d2.4	$⊢ φ \to Q \in ℙ$
5		aks4d1p8d2.5	$⊢ φ \to P ∥ R$
6		aks4d1p8d2.6	$⊢ φ \to Q ∥ R$
7		aks4d1p8d2.7	$⊢ φ \to \neg P ∥ N$
8		aks4d1p8d2.8	$⊢ φ \to Q ∥ N$
9		prmnn	$⊢ P \in ℙ \to P \in ℕ$
10	3 9	syl	$⊢ φ \to P \in ℕ$
11	10	nnred	$⊢ φ \to P \in ℝ$
12	3 1	pccld	$⊢ φ \to P pCnt R \in ℕ_{0}$
13	11 12	reexpcld	$⊢ φ \to P^{P pCnt R} \in ℝ$
14		prmnn	$⊢ Q \in ℙ \to Q \in ℕ$
15	4 14	syl	$⊢ φ \to Q \in ℕ$
16	15	nnred	$⊢ φ \to Q \in ℝ$
17	13 16	remulcld	$⊢ φ \to P^{P pCnt R} Q \in ℝ$
18	1	nnred	$⊢ φ \to R \in ℝ$
19	13	recnd	$⊢ φ \to P^{P pCnt R} \in ℂ$
20	19	mulid1d	$⊢ φ \to P^{P pCnt R} \cdot 1 = P^{P pCnt R}$
21		1red	$⊢ φ \to 1 \in ℝ$
22	10	nnrpd	$⊢ φ \to P \in ℝ^{+}$
23	12	nn0zd	$⊢ φ \to P pCnt R \in ℤ$
24	22 23	rpexpcld	$⊢ φ \to P^{P pCnt R} \in ℝ^{+}$
25		prmgt1	$⊢ Q \in ℙ \to 1 < Q$
26	4 25	syl	$⊢ φ \to 1 < Q$
27	21 16 24 26	ltmul2dd	$⊢ φ \to P^{P pCnt R} \cdot 1 < P^{P pCnt R} Q$
28	20 27	eqbrtrrd	$⊢ φ \to P^{P pCnt R} < P^{P pCnt R} Q$
29	10	nnzd	$⊢ φ \to P \in ℤ$
30	29 12	zexpcld	$⊢ φ \to P^{P pCnt R} \in ℤ$
31	15	nnzd	$⊢ φ \to Q \in ℤ$
32	1	nnzd	$⊢ φ \to R \in ℤ$
33	30 31	gcdcomd	$⊢ φ \to P^{P pCnt R} \gcd Q = Q \gcd P^{P pCnt R}$
34		0lt1	$⊢ 0 < 1$
35	34	a1i	$⊢ φ \to 0 < 1$
36		0red	$⊢ φ \to 0 \in ℝ$
37	36 21	ltnled	$⊢ φ \to (0 < 1 \leftrightarrow \neg 1 \leq 0)$
38	35 37	mpbid	$⊢ φ \to \neg 1 \leq 0$
39	16	recnd	$⊢ φ \to Q \in ℂ$
40	39	exp1d	$⊢ φ \to Q^{1} = Q$
41	40	eqcomd	$⊢ φ \to Q = Q^{1}$
42	41	oveq2d	$⊢ φ \to Q pCnt Q = Q pCnt Q^{1}$
43		1zzd	$⊢ φ \to 1 \in ℤ$
44		pcid	$⊢ (Q \in ℙ \land 1 \in ℤ) \to Q pCnt Q^{1} = 1$
45	4 43 44	syl2anc	$⊢ φ \to Q pCnt Q^{1} = 1$
46	42 45	eqtrd	$⊢ φ \to Q pCnt Q = 1$
47	8	adantr	$⊢ (φ \land P = Q) \to Q ∥ N$
48		breq1	$⊢ P = Q \to (P ∥ N \leftrightarrow Q ∥ N)$
49	48	adantl	$⊢ (φ \land P = Q) \to (P ∥ N \leftrightarrow Q ∥ N)$
50	49	bicomd	$⊢ (φ \land P = Q) \to (Q ∥ N \leftrightarrow P ∥ N)$
51	50	biimpd	$⊢ (φ \land P = Q) \to (Q ∥ N \to P ∥ N)$
52	47 51	mpd	$⊢ (φ \land P = Q) \to P ∥ N$
53	7	adantr	$⊢ (φ \land P = Q) \to \neg P ∥ N$
54	52 53	pm2.65da	$⊢ φ \to \neg P = Q$
55	54	neqcomd	$⊢ φ \to \neg Q = P$
56		pcelnn	$⊢ (P \in ℙ \land R \in ℕ) \to (P pCnt R \in ℕ \leftrightarrow P ∥ R)$
57	3 1 56	syl2anc	$⊢ φ \to (P pCnt R \in ℕ \leftrightarrow P ∥ R)$
58	5 57	mpbird	$⊢ φ \to P pCnt R \in ℕ$
59		prmdvdsexpb	$⊢ (Q \in ℙ \land P \in ℙ \land P pCnt R \in ℕ) \to (Q ∥ P^{P pCnt R} \leftrightarrow Q = P)$
60	4 3 58 59	syl3anc	$⊢ φ \to (Q ∥ P^{P pCnt R} \leftrightarrow Q = P)$
61	60	notbid	$⊢ φ \to (\neg Q ∥ P^{P pCnt R} \leftrightarrow \neg Q = P)$
62	55 61	mpbird	$⊢ φ \to \neg Q ∥ P^{P pCnt R}$
63	10 12	nnexpcld	$⊢ φ \to P^{P pCnt R} \in ℕ$
64		pceq0	$⊢ (Q \in ℙ \land P^{P pCnt R} \in ℕ) \to (Q pCnt P^{P pCnt R} = 0 \leftrightarrow \neg Q ∥ P^{P pCnt R})$
65	4 63 64	syl2anc	$⊢ φ \to (Q pCnt P^{P pCnt R} = 0 \leftrightarrow \neg Q ∥ P^{P pCnt R})$
66	62 65	mpbird	$⊢ φ \to Q pCnt P^{P pCnt R} = 0$
67	46 66	breq12d	$⊢ φ \to (Q pCnt Q \leq Q pCnt P^{P pCnt R} \leftrightarrow 1 \leq 0)$
68	67	notbid	$⊢ φ \to (\neg Q pCnt Q \leq Q pCnt P^{P pCnt R} \leftrightarrow \neg 1 \leq 0)$
69	38 68	mpbird	$⊢ φ \to \neg Q pCnt Q \leq Q pCnt P^{P pCnt R}$
70	69	adantr	$⊢ (φ \land p = Q) \to \neg Q pCnt Q \leq Q pCnt P^{P pCnt R}$
71		simpr	$⊢ (φ \land p = Q) \to p = Q$
72	71	oveq1d	$⊢ (φ \land p = Q) \to p pCnt Q = Q pCnt Q$
73	71	oveq1d	$⊢ (φ \land p = Q) \to p pCnt P^{P pCnt R} = Q pCnt P^{P pCnt R}$
74	72 73	breq12d	$⊢ (φ \land p = Q) \to (p pCnt Q \leq p pCnt P^{P pCnt R} \leftrightarrow Q pCnt Q \leq Q pCnt P^{P pCnt R})$
75	74	notbid	$⊢ (φ \land p = Q) \to (\neg p pCnt Q \leq p pCnt P^{P pCnt R} \leftrightarrow \neg Q pCnt Q \leq Q pCnt P^{P pCnt R})$
76	70 75	mpbird	$⊢ (φ \land p = Q) \to \neg p pCnt Q \leq p pCnt P^{P pCnt R}$
77	76 4	rspcime	$⊢ φ \to \exists p \in ℙ \neg p pCnt Q \leq p pCnt P^{P pCnt R}$
78		rexnal	$⊢ \exists p \in ℙ \neg p pCnt Q \leq p pCnt P^{P pCnt R} \leftrightarrow \neg \forall p \in ℙ p pCnt Q \leq p pCnt P^{P pCnt R}$
79	78	a1i	$⊢ φ \to (\exists p \in ℙ \neg p pCnt Q \leq p pCnt P^{P pCnt R} \leftrightarrow \neg \forall p \in ℙ p pCnt Q \leq p pCnt P^{P pCnt R})$
80	77 79	mpbid	$⊢ φ \to \neg \forall p \in ℙ p pCnt Q \leq p pCnt P^{P pCnt R}$
81		pc2dvds	$⊢ (Q \in ℤ \land P^{P pCnt R} \in ℤ) \to (Q ∥ P^{P pCnt R} \leftrightarrow \forall p \in ℙ p pCnt Q \leq p pCnt P^{P pCnt R})$
82	31 30 81	syl2anc	$⊢ φ \to (Q ∥ P^{P pCnt R} \leftrightarrow \forall p \in ℙ p pCnt Q \leq p pCnt P^{P pCnt R})$
83	82	notbid	$⊢ φ \to (\neg Q ∥ P^{P pCnt R} \leftrightarrow \neg \forall p \in ℙ p pCnt Q \leq p pCnt P^{P pCnt R})$
84	80 83	mpbird	$⊢ φ \to \neg Q ∥ P^{P pCnt R}$
85		coprm	$⊢ (Q \in ℙ \land P^{P pCnt R} \in ℤ) \to (\neg Q ∥ P^{P pCnt R} \leftrightarrow Q \gcd P^{P pCnt R} = 1)$
86	4 30 85	syl2anc	$⊢ φ \to (\neg Q ∥ P^{P pCnt R} \leftrightarrow Q \gcd P^{P pCnt R} = 1)$
87	84 86	mpbid	$⊢ φ \to Q \gcd P^{P pCnt R} = 1$
88	33 87	eqtrd	$⊢ φ \to P^{P pCnt R} \gcd Q = 1$
89		pcdvds	$⊢ (P \in ℙ \land R \in ℕ) \to P^{P pCnt R} ∥ R$
90	3 1 89	syl2anc	$⊢ φ \to P^{P pCnt R} ∥ R$
91	30 31 32 88 90 6	coprmdvds2d	$⊢ φ \to P^{P pCnt R} Q ∥ R$
92	30 31	zmulcld	$⊢ φ \to P^{P pCnt R} Q \in ℤ$
93		dvdsle	$⊢ (P^{P pCnt R} Q \in ℤ \land R \in ℕ) \to (P^{P pCnt R} Q ∥ R \to P^{P pCnt R} Q \leq R)$
94	92 1 93	syl2anc	$⊢ φ \to (P^{P pCnt R} Q ∥ R \to P^{P pCnt R} Q \leq R)$
95	91 94	mpd	$⊢ φ \to P^{P pCnt R} Q \leq R$
96	13 17 18 28 95	ltletrd	$⊢ φ \to P^{P pCnt R} < R$

Metamath Proof Explorer

Theorem aks4d1p8d2

Proof