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 16763

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 16760	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
2	1	ancoms 460	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
3	2	ralrimiva 3140	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
4	3	3expia 1122	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
5		oveq2 7371	. . . . . 6 ⊢ (𝐴 = 0 → (𝑝 pCnt 𝐴) = (𝑝 pCnt 0))
6	5	breq1d 5121	. . . . 5 ⊢ (𝐴 = 0 → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)))
7	6	ralbidv 3171	. . . 4 ⊢ (𝐴 = 0 → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)))
8		breq1 5114	. . . 4 ⊢ (𝐴 = 0 → (𝐴 ∥ 𝐵 ↔ 0 ∥ 𝐵))
9	7, 8	imbi12d 345	. . 3 ⊢ (𝐴 = 0 → ((∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵) ↔ (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵)))
10		gcddvds 16395	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
11	10	simpld 496	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐴)
12		gcdcl 16398	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
13	12	nn0zd 12535	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ)
14		simpl 484	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈ ℤ)
15		dvdsabsb 16170	. . . . . . . . . . . 12 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴)))
16	13, 14, 15	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴)))
17	11, 16	mpbid 231	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴))
18	17	adantr 482	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴))
19		simpl 484	. . . . . . . . . . . . 13 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → 𝐴 = 0)
20	19	necon3ai 2965	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 0 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
21		gcdn0cl 16394	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
22	20, 21	sylan2 594	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℕ)
23	22	nnzd 12536	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℤ)
24	22	nnne0d 12213	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ≠ 0)
25		nnabscl 15223	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
26	25	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
27	26	nnzd 12536	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℤ)
28		dvdsval2 16151	. . . . . . . . . 10 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ (abs‘𝐴) ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ))
29	23, 24, 27, 28	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ))
30	18, 29	mpbid 231	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ)
31		nnre 12170	. . . . . . . . . . 11 ⊢ ((abs‘𝐴) ∈ ℕ → (abs‘𝐴) ∈ ℝ)
32		nngt0 12194	. . . . . . . . . . 11 ⊢ ((abs‘𝐴) ∈ ℕ → 0 < (abs‘𝐴))
33	31, 32	jca 513	. . . . . . . . . 10 ⊢ ((abs‘𝐴) ∈ ℕ → ((abs‘𝐴) ∈ ℝ ∧ 0 < (abs‘𝐴)))
34		nnre 12170	. . . . . . . . . . 11 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → (𝐴 gcd 𝐵) ∈ ℝ)
35		nngt0 12194	. . . . . . . . . . 11 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → 0 < (𝐴 gcd 𝐵))
36	34, 35	jca 513	. . . . . . . . . 10 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵)))
37		divgt0 12033	. . . . . . . . . 10 ⊢ ((((abs‘𝐴) ∈ ℝ ∧ 0 < (abs‘𝐴)) ∧ ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵))) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
38	33, 36, 37	syl2an 597	. . . . . . . . 9 ⊢ (((abs‘𝐴) ∈ ℕ ∧ (𝐴 gcd 𝐵) ∈ ℕ) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
39	26, 22, 38	syl2anc 585	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
40		elnnz 12519	. . . . . . . 8 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ ↔ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ ∧ 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵))))
41	30, 39, 40	sylanbrc 584	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ)
42		elnn1uz2 12860	. . . . . . 7 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ ↔ (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)))
43	41, 42	sylib 217	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)))
44	10	simprd 497	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐵)
45	44	adantr 482	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ 𝐵)
46		breq1 5114	. . . . . . . . 9 ⊢ ((𝐴 gcd 𝐵) = (abs‘𝐴) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
47	45, 46	syl5ibcom 244	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) = (abs‘𝐴) → (abs‘𝐴) ∥ 𝐵))
48	26	nncnd 12179	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℂ)
49	22	nncnd 12179	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℂ)
50		1cnd 11160	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 1 ∈ ℂ)
51	48, 49, 50, 24	divmuld 11963	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ ((𝐴 gcd 𝐵) · 1) = (abs‘𝐴)))
52	49	mulridd 11182	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) · 1) = (𝐴 gcd 𝐵))
53	52	eqeq1d 2734	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((𝐴 gcd 𝐵) · 1) = (abs‘𝐴) ↔ (𝐴 gcd 𝐵) = (abs‘𝐴)))
54	51, 53	bitrd 279	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ (𝐴 gcd 𝐵) = (abs‘𝐴)))
55		absdvdsb 16169	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
56	55	adantr 482	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
57	47, 54, 56	3imtr4d 294	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 → 𝐴 ∥ 𝐵))
58		exprmfct 16592	. . . . . . . 8 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))
59		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∈ ℙ)
60	26	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℕ)
61	60	nnzd 12536	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℤ)
62	60	nnne0d 12213	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ≠ 0)
63	22	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 𝐵) ∈ ℕ)
64		pcdiv 16736	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ ((abs‘𝐴) ∈ ℤ ∧ (abs‘𝐴) ≠ 0) ∧ (𝐴 gcd 𝐵) ∈ ℕ) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))))
65	59, 61, 62, 63, 64	syl121anc 1376	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))))
66		simplll 774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℤ)
67		zq 12889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
68	66, 67	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℚ)
69		pcabs 16759	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴))
70	59, 68, 69	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴))
71	70	oveq1d 7378	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))))
72	65, 71	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))))
73		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))
74	41	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ)
75		pcelnn 16754	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ) → ((𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵))))
76	59, 74, 75	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵))))
77	73, 76	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ)
78	72, 77	eqeltrrd 2834	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ)
79	59, 63	pccld 16734	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℕ₀)
80	79	nn0zd 12535	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ)
81		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ≠ 0)
82		pczcl 16732	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑝 pCnt 𝐴) ∈ ℕ₀)
83	59, 66, 81, 82	syl12anc 836	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℕ₀)
84	83	nn0zd 12535	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℤ)
85		znnsub 12559	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝑝 pCnt 𝐴) ∈ ℤ) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ))
86	80, 84, 85	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ))
87	78, 86	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴))
88	79	nn0red 12484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℝ)
89	83	nn0red 12484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℝ)
90	88, 89	ltnled 11312	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵))))
91	87, 90	mpbid 231	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)))
92		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ∈ ℤ)
93		nprmdvds1 16594	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1)
94	93	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ 1)
95		gcdid0 16412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴))
96	66, 95	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 0) = (abs‘𝐴))
97	96	oveq2d 7379	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = ((abs‘𝐴) / (abs‘𝐴)))
98	48	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℂ)
99	98, 62	dividd 11939	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (abs‘𝐴)) = 1)
100	97, 99	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = 1)
101	100	breq2d 5123	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) ↔ 𝑝 ∥ 1))
102	94, 101	mtbird 325	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)))
103		oveq2 7371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 = 0 → (𝐴 gcd 𝐵) = (𝐴 gcd 0))
104	103	oveq2d 7379	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 = 0 → ((abs‘𝐴) / (𝐴 gcd 𝐵)) = ((abs‘𝐴) / (𝐴 gcd 0)))
105	104	breq2d 5123	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 0 → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0))))
106	73, 105	syl5ibcom 244	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐵 = 0 → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0))))
107	106	necon3bd 2954	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) → 𝐵 ≠ 0))
108	102, 107	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ≠ 0)
109		pczcl 16732	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℕ₀)
110	59, 92, 108, 109	syl12anc 836	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈ ℕ₀)
111	110	nn0red 12484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈ ℝ)
112		lemin 13122	. . . . . . . . . . . . . 14 ⊢ (((𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐵) ∈ ℝ) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
113	89, 89, 111, 112	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
114		pcgcd 16762	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)))
115	59, 66, 92, 114	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)))
116	115	breq2d 5123	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)) ↔ (𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))))
117	89	leidd 11731	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴))
118	117	biantrurd 534	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
119	113, 116, 118	3bitr4rd 312	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵))))
120	91, 119	mtbird 325	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
121	120	expr 458	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
122	121	reximdva 3162	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
123		rexnal 3100	. . . . . . . . 9 ⊢ (∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
124	122, 123	syl6ib 251	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
125	58, 124	syl5 34	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2) → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
126	57, 125	orim12d 964	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)) → (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
127	43, 126	mpd 15	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
128	127	ord 863	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (¬ 𝐴 ∥ 𝐵 → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
129	128	con4d 115	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵))
130		2prm 16580	. . . . . 6 ⊢ 2 ∈ ℙ
131	130	ne0ii 4303	. . . . 5 ⊢ ℙ ≠ ∅
132		r19.2z 4458	. . . . 5 ⊢ ((ℙ ≠ ∅ ∧ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))
133	131, 132	mpan 689	. . . 4 ⊢ (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))
134		id 22	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
135		zq 12889	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℚ)
136	135	adantl 483	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℚ)
137		pcxcl 16745	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℙ ∧ 𝐵 ∈ ℚ) → (𝑝 pCnt 𝐵) ∈ ℝ^*)
138	134, 136, 137	syl2anr 598	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ∈ ℝ^*)
139		pnfge 13061	. . . . . . . . . 10 ⊢ ((𝑝 pCnt 𝐵) ∈ ℝ^* → (𝑝 pCnt 𝐵) ≤ +∞)
140	138, 139	syl 17	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ≤ +∞)
141	140	biantrurd 534	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (+∞ ≤ (𝑝 pCnt 𝐵) ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
142		pc0 16738	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → (𝑝 pCnt 0) = +∞)
143	142	adantl 483	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 0) = +∞)
144	143	breq1d 5121	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ +∞ ≤ (𝑝 pCnt 𝐵)))
145		pnfxr 11219	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
146		xrletri3 13084	. . . . . . . . 9 ⊢ (((𝑝 pCnt 𝐵) ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
147	138, 145, 146	sylancl 587	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
148	141, 144, 147	3bitr4d 311	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 𝐵) = +∞))
149		pnfnre 11206	. . . . . . . . . 10 ⊢ +∞ ∉ ℝ
150	149	neli 3048	. . . . . . . . 9 ⊢ ¬ +∞ ∈ ℝ
151		eleq1 2821	. . . . . . . . 9 ⊢ ((𝑝 pCnt 𝐵) = +∞ → ((𝑝 pCnt 𝐵) ∈ ℝ ↔ +∞ ∈ ℝ))
152	150, 151	mtbiri 327	. . . . . . . 8 ⊢ ((𝑝 pCnt 𝐵) = +∞ → ¬ (𝑝 pCnt 𝐵) ∈ ℝ)
153	109	nn0red 12484	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
154	153	adantll 713	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℙ) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
155	154	an4s 659	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑝 ∈ ℙ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
156	155	expr 458	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝐵 ≠ 0 → (𝑝 pCnt 𝐵) ∈ ℝ))
157	156	necon1bd 2958	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (¬ (𝑝 pCnt 𝐵) ∈ ℝ → 𝐵 = 0))
158	152, 157	syl5 34	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ → 𝐵 = 0))
159	148, 158	sylbid 239	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0))
160	159	rexlimdva 3149	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0))
161		0dvds 16171	. . . . . 6 ⊢ (𝐵 ∈ ℤ → (0 ∥ 𝐵 ↔ 𝐵 = 0))
162	161	adantl 483	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ∥ 𝐵 ↔ 𝐵 = 0))
163	160, 162	sylibrd 259	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵))
164	133, 163	syl5 34	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵))
165	9, 129, 164	pm2.61ne 3027	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵))
166	4, 165	impbid 211	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ∅c0 4288 ifcif 4492 class class class wbr 5111 ‘cfv 6502 (class class class)co 7363 ℂcc 11059 ℝcr 11060 0cc0 11061 1c1 11062 · cmul 11066 +∞cpnf 11196 ℝ^*cxr 11198 < clt 11199 ≤ cle 11200 − cmin 11395 / cdiv 11822 ℕcn 12163 2c2 12218 ℕ₀cn0 12423 ℤcz 12509 ℤ_≥cuz 12773 ℚcq 12883 abscabs 15132 ∥ cdvds 16148 gcd cgcd 16386 ℙcprime 16559 pCnt cpc 16720

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2703 ax-sep 5262 ax-nul 5269 ax-pow 5326 ax-pr 5390 ax-un 7678 ax-cnex 11117 ax-resscn 11118 ax-1cn 11119 ax-icn 11120 ax-addcl 11121 ax-addrcl 11122 ax-mulcl 11123 ax-mulrcl 11124 ax-mulcom 11125 ax-addass 11126 ax-mulass 11127 ax-distr 11128 ax-i2m1 11129 ax-1ne0 11130 ax-1rid 11131 ax-rnegex 11132 ax-rrecex 11133 ax-cnre 11134 ax-pre-lttri 11135 ax-pre-lttrn 11136 ax-pre-ltadd 11137 ax-pre-mulgt0 11138 ax-pre-sup 11139

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3352 df-reu 3353 df-rab 3407 df-v 3449 df-sbc 3744 df-csb 3860 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3933 df-nul 4289 df-if 4493 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4872 df-iun 4962 df-br 5112 df-opab 5174 df-mpt 5195 df-tr 5229 df-id 5537 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5594 df-we 5596 df-xp 5645 df-rel 5646 df-cnv 5647 df-co 5648 df-dm 5649 df-rn 5650 df-res 5651 df-ima 5652 df-pred 6259 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-riota 7319 df-ov 7366 df-oprab 7367 df-mpo 7368 df-om 7809 df-1st 7927 df-2nd 7928 df-frecs 8218 df-wrecs 8249 df-recs 8323 df-rdg 8362 df-1o 8418 df-2o 8419 df-er 8656 df-en 8892 df-dom 8893 df-sdom 8894 df-fin 8895 df-sup 9388 df-inf 9389 df-pnf 11201 df-mnf 11202 df-xr 11203 df-ltxr 11204 df-le 11205 df-sub 11397 df-neg 11398 df-div 11823 df-nn 12164 df-2 12226 df-3 12227 df-n0 12424 df-z 12510 df-uz 12774 df-q 12884 df-rp 12926 df-fz 13436 df-fl 13708 df-mod 13786 df-seq 13918 df-exp 13979 df-cj 14997 df-re 14998 df-im 14999 df-sqrt 15133 df-abs 15134 df-dvds 16149 df-gcd 16387 df-prm 16560 df-pc 16721

This theorem is referenced by: pc11 16764 pcz 16765 pcprmpw2 16766 pockthg 16790 pgpfi 19402 fislw 19422 gexexlem 19645 ablfac1c 19865 sqff1o 26569 chtublem 26597 bposlem6 26675 aks4d1p7d1 40613 aks4d1p8d2 40616

W3C validator