pc2dvds - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pc2dvds		Structured version Visualization version GIF version

Theorem pc2dvds 16945

Description: A characterization of divisibility in terms of prime count. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)

**Assertion**
Ref	Expression
pc2dvds	⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))

Distinct variable groups: 𝐴,𝑝 𝐵,𝑝

**Proof of Theorem pc2dvds**
Step	Hyp	Ref	Expression
1		pcdvdstr 16942	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
2	1	ancoms 463	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
3	2	ralrimiva 3156	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
4	3	3expia 1138	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
5		oveq2 7420	. . . . . 6 ⊢ (𝐴 = 0 → (𝑝 pCnt 𝐴) = (𝑝 pCnt 0))
6	5	breq1d 5118	. . . . 5 ⊢ (𝐴 = 0 → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)))
7	6	ralbidv 3187	. . . 4 ⊢ (𝐴 = 0 → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)))
8		breq1 5111	. . . 4 ⊢ (𝐴 = 0 → (𝐴 ∥ 𝐵 ↔ 0 ∥ 𝐵))
9	7, 8	imbi12d 347	. . 3 ⊢ (𝐴 = 0 → ((∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵) ↔ (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵)))
10		gcddvds 16567	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
11	10	simpld 499	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐴)
12		gcdcl 16570	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
13	12	nn0zd 12622	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ)
14		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈ ℤ)
15		dvdsabsb 16339	. . . . . . . . . . . 12 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴)))
16	13, 14, 15	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴)))
17	11, 16	mpbid 235	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴))
18	17	adantr 485	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴))
19		simpl 487	. . . . . . . . . . . . 13 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → 𝐴 = 0)
20	19	necon3ai 2982	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 0 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
21		gcdn0cl 16566	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
22	20, 21	sylan2 604	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℕ)
23	22	nnzd 12623	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℤ)
24	22	nnne0d 12292	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ≠ 0)
25		nnabscl 15384	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
26	25	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
27	26	nnzd 12623	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℤ)
28		dvdsval2 16319	. . . . . . . . . 10 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ (abs‘𝐴) ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ))
29	23, 24, 27, 28	syl3anc 1397	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ))
30	18, 29	mpbid 235	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ)
31		nnre 12246	. . . . . . . . . . 11 ⊢ ((abs‘𝐴) ∈ ℕ → (abs‘𝐴) ∈ ℝ)
32		nngt0 12273	. . . . . . . . . . 11 ⊢ ((abs‘𝐴) ∈ ℕ → 0 < (abs‘𝐴))
33	31, 32	jca 520	. . . . . . . . . 10 ⊢ ((abs‘𝐴) ∈ ℕ → ((abs‘𝐴) ∈ ℝ ∧ 0 < (abs‘𝐴)))
34		nnre 12246	. . . . . . . . . . 11 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → (𝐴 gcd 𝐵) ∈ ℝ)
35		nngt0 12273	. . . . . . . . . . 11 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → 0 < (𝐴 gcd 𝐵))
36	34, 35	jca 520	. . . . . . . . . 10 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵)))
37		divgt0 12089	. . . . . . . . . 10 ⊢ ((((abs‘𝐴) ∈ ℝ ∧ 0 < (abs‘𝐴)) ∧ ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵))) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
38	33, 36, 37	syl2an 607	. . . . . . . . 9 ⊢ (((abs‘𝐴) ∈ ℕ ∧ (𝐴 gcd 𝐵) ∈ ℕ) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
39	26, 22, 38	syl2anc 595	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
40		elnnz 12607	. . . . . . . 8 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ ↔ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ ∧ 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵))))
41	30, 39, 40	sylanbrc 594	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ)
42		elnn1uz2 12955	. . . . . . 7 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ ↔ (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)))
43	41, 42	sylib 221	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)))
44	10	simprd 500	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐵)
45	44	adantr 485	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ 𝐵)
46		breq1 5111	. . . . . . . . 9 ⊢ ((𝐴 gcd 𝐵) = (abs‘𝐴) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
47	45, 46	syl5ibcom 248	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) = (abs‘𝐴) → (abs‘𝐴) ∥ 𝐵))
48	26	nncnd 12255	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℂ)
49	22	nncnd 12255	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℂ)
50		1cnd 11208	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 1 ∈ ℂ)
51	48, 49, 50, 24	divmuld 12019	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ ((𝐴 gcd 𝐵) · 1) = (abs‘𝐴)))
52	49	mulridd 11232	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) · 1) = (𝐴 gcd 𝐵))
53	52	eqeq1d 2764	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((𝐴 gcd 𝐵) · 1) = (abs‘𝐴) ↔ (𝐴 gcd 𝐵) = (abs‘𝐴)))
54	51, 53	bitrd 282	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ (𝐴 gcd 𝐵) = (abs‘𝐴)))
55		absdvdsb 16338	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
56	55	adantr 485	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
57	47, 54, 56	3imtr4d 297	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 → 𝐴 ∥ 𝐵))
58		exprmfct 16769	. . . . . . . 8 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))
59		simprl 782	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∈ ℙ)
60	26	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℕ)
61	60	nnzd 12623	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℤ)
62	60	nnne0d 12292	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ≠ 0)
63	22	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 𝐵) ∈ ℕ)
64		pcdiv 16918	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ ((abs‘𝐴) ∈ ℤ ∧ (abs‘𝐴) ≠ 0) ∧ (𝐴 gcd 𝐵) ∈ ℕ) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))))
65	59, 61, 62, 63, 64	syl121anc 1401	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))))
66		simplll 786	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℤ)
67		zq 12984	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
68	66, 67	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℚ)
69		pcabs 16941	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴))
70	59, 68, 69	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴))
71	70	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))))
72	65, 71	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))))
73		simprr 784	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))
74	41	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ)
75		pcelnn 16936	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ) → ((𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵))))
76	59, 74, 75	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵))))
77	73, 76	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ)
78	72, 77	eqeltrrd 2863	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ)
79	59, 63	pccld 16916	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℕ₀)
80	79	nn0zd 12622	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ)
81		simplr 780	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ≠ 0)
82		pczcl 16914	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑝 pCnt 𝐴) ∈ ℕ₀)
83	59, 66, 81, 82	syl12anc 849	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℕ₀)
84	83	nn0zd 12622	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℤ)
85		znnsub 12646	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝑝 pCnt 𝐴) ∈ ℤ) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ))
86	80, 84, 85	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ))
87	78, 86	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴))
88	79	nn0red 12572	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℝ)
89	83	nn0red 12572	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℝ)
90	88, 89	ltnled 11363	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵))))
91	87, 90	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)))
92		simpllr 787	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ∈ ℤ)
93		nprmdvds1 16771	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1)
94	93	ad2antrl 740	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ 1)
95		gcdid0 16584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴))
96	66, 95	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 0) = (abs‘𝐴))
97	96	oveq2d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = ((abs‘𝐴) / (abs‘𝐴)))
98	48	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℂ)
99	98, 62	dividd 11995	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (abs‘𝐴)) = 1)
100	97, 99	eqtrd 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = 1)
101	100	breq2d 5120	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) ↔ 𝑝 ∥ 1))
102	94, 101	mtbird 328	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)))
103		oveq2 7420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 = 0 → (𝐴 gcd 𝐵) = (𝐴 gcd 0))
104	103	oveq2d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 = 0 → ((abs‘𝐴) / (𝐴 gcd 𝐵)) = ((abs‘𝐴) / (𝐴 gcd 0)))
105	104	breq2d 5120	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 0 → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0))))
106	73, 105	syl5ibcom 248	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐵 = 0 → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0))))
107	106	necon3bd 2971	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) → 𝐵 ≠ 0))
108	102, 107	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ≠ 0)
109		pczcl 16914	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℕ₀)
110	59, 92, 108, 109	syl12anc 849	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈ ℕ₀)
111	110	nn0red 12572	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈ ℝ)
112		lemin 13224	. . . . . . . . . . . . . 14 ⊢ (((𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐵) ∈ ℝ) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
113	89, 89, 111, 112	syl3anc 1397	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
114		pcgcd 16944	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)))
115	59, 66, 92, 114	syl3anc 1397	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)))
116	115	breq2d 5120	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)) ↔ (𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))))
117	89	leidd 11786	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴))
118	117	biantrurd 541	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
119	113, 116, 118	3bitr4rd 315	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵))))
120	91, 119	mtbird 328	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
121	120	expr 461	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
122	121	reximdva 3177	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
123		rexnal 3116	. . . . . . . . 9 ⊢ (∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
124	122, 123	imbitrdi 254	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
125	58, 124	syl5 35	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2) → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
126	57, 125	orim12d 978	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)) → (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
127	43, 126	mpd 16	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
128	127	ord 877	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (¬ 𝐴 ∥ 𝐵 → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
129	128	con4d 116	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵))
130		2prm 16756	. . . . . 6 ⊢ 2 ∈ ℙ
131	130	ne0ii 4296	. . . . 5 ⊢ ℙ ≠ ∅
132		r19.2z 4459	. . . . 5 ⊢ ((ℙ ≠ ∅ ∧ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))
133	131, 132	mpan 702	. . . 4 ⊢ (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))
134		id 23	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
135		zq 12984	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℚ)
136	135	adantl 486	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℚ)
137		pcxcl 16927	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℙ ∧ 𝐵 ∈ ℚ) → (𝑝 pCnt 𝐵) ∈ ℝ^*)
138	134, 136, 137	syl2anr 608	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ∈ ℝ^*)
139		pnfge 13161	. . . . . . . . . 10 ⊢ ((𝑝 pCnt 𝐵) ∈ ℝ^* → (𝑝 pCnt 𝐵) ≤ +∞)
140	138, 139	syl 18	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ≤ +∞)
141	140	biantrurd 541	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (+∞ ≤ (𝑝 pCnt 𝐵) ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
142		pc0 16920	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → (𝑝 pCnt 0) = +∞)
143	142	adantl 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 0) = +∞)
144	143	breq1d 5118	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ +∞ ≤ (𝑝 pCnt 𝐵)))
145		pnfxr 11269	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
146		xrletri3 13185	. . . . . . . . 9 ⊢ (((𝑝 pCnt 𝐵) ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
147	138, 145, 146	sylancl 597	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
148	141, 144, 147	3bitr4d 314	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 𝐵) = +∞))
149		pnfnre 11256	. . . . . . . . . 10 ⊢ +∞ ∉ ℝ
150	149	neli 3065	. . . . . . . . 9 ⊢ ¬ +∞ ∈ ℝ
151		eleq1 2850	. . . . . . . . 9 ⊢ ((𝑝 pCnt 𝐵) = +∞ → ((𝑝 pCnt 𝐵) ∈ ℝ ↔ +∞ ∈ ℝ))
152	150, 151	mtbiri 330	. . . . . . . 8 ⊢ ((𝑝 pCnt 𝐵) = +∞ → ¬ (𝑝 pCnt 𝐵) ∈ ℝ)
153	109	nn0red 12572	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
154	153	adantll 726	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℙ) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
155	154	an4s 672	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑝 ∈ ℙ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
156	155	expr 461	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝐵 ≠ 0 → (𝑝 pCnt 𝐵) ∈ ℝ))
157	156	necon1bd 2975	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (¬ (𝑝 pCnt 𝐵) ∈ ℝ → 𝐵 = 0))
158	152, 157	syl5 35	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ → 𝐵 = 0))
159	148, 158	sylbid 243	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0))
160	159	rexlimdva 3165	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0))
161		0dvds 16340	. . . . . 6 ⊢ (𝐵 ∈ ℤ → (0 ∥ 𝐵 ↔ 𝐵 = 0))
162	161	adantl 486	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ∥ 𝐵 ↔ 𝐵 = 0))
163	160, 162	sylibrd 262	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵))
164	133, 163	syl5 35	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵))
165	9, 129, 164	pm2.61ne 3042	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵))
166	4, 165	impbid 215	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 ∅c0 4285 ifcif 4486 class class class wbr 5108 ‘cfv 6536 (class class class)co 7412 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 · cmul 11111 +∞cpnf 11246 ℝ^*cxr 11248 < clt 11249 ≤ cle 11250 − cmin 11447 / cdiv 11877 ℕcn 12239 2c2 12301 ℕ₀cn0 12510 ℤcz 12597 ℤ_≥cuz 12868 ℚcq 12978 abscabs 15292 ∥ cdvds 16316 gcd cgcd 16558 ℙcprime 16735 pCnt cpc 16902

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-er 8692 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9400 df-inf 9401 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-n0 12511 df-z 12598 df-uz 12869 df-q 12979 df-rp 13023 df-fz 13542 df-fl 13832 df-mod 13910 df-seq 14045 df-exp 14105 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-dvds 16317 df-gcd 16559 df-prm 16736 df-pc 16903

This theorem is used by: pc11 16946 pcz 16947 pcprmpw2 16948 pockthg 16972 pgpfi 19681 fislw 19701 gexexlem 19928 ablfac1c 20149 sqff1o 27357 chtublem 27386 bposlem6 27464 aks4d1p7d1 42877 aks4d1p8d2 42880

W3C validator