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 17058

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 17055	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
2	1	ancoms 464	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
3	2	ralrimiva 3154	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
4	3	3expia 1139	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
5		oveq2 7428	. . . . . 6 ⊢ (𝐴 = 0 → (𝑝 pCnt 𝐴) = (𝑝 pCnt 0))
6	5	breq1d 5112	. . . . 5 ⊢ (𝐴 = 0 → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)))
7	6	ralbidv 3185	. . . 4 ⊢ (𝐴 = 0 → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)))
8		breq1 5105	. . . 4 ⊢ (𝐴 = 0 → (𝐴 ∥ 𝐵 ↔ 0 ∥ 𝐵))
9	7, 8	imbi12d 347	. . 3 ⊢ (𝐴 = 0 → ((∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵) ↔ (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵)))
10		gcddvds 16674	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
11	10	simpld 500	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐴)
12		gcdcl 16677	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
13	12	nn0zd 12719	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ)
14		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈ ℤ)
15		dvdsabsb 16446	. . . . . . . . . . . 12 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴)))
16	13, 14, 15	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴)))
17	11, 16	mpbid 235	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴))
18	17	adantr 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴))
19		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → 𝐴 = 0)
20	19	necon3ai 2980	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 0 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
21		gcdn0cl 16673	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
22	20, 21	sylan2 605	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℕ)
23	22	nnzd 12720	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℤ)
24	22	nnne0d 12389	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ≠ 0)
25		nnabscl 15494	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
26	25	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
27	26	nnzd 12720	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℤ)
28		dvdsval2 16426	. . . . . . . . . 10 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ (abs‘𝐴) ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ))
29	23, 24, 27, 28	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ))
30	18, 29	mpbid 235	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ)
31		nnre 12343	. . . . . . . . . . 11 ⊢ ((abs‘𝐴) ∈ ℕ → (abs‘𝐴) ∈ ℝ)
32		nngt0 12370	. . . . . . . . . . 11 ⊢ ((abs‘𝐴) ∈ ℕ → 0 < (abs‘𝐴))
33	31, 32	jca 521	. . . . . . . . . 10 ⊢ ((abs‘𝐴) ∈ ℕ → ((abs‘𝐴) ∈ ℝ ∧ 0 < (abs‘𝐴)))
34		nnre 12343	. . . . . . . . . . 11 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → (𝐴 gcd 𝐵) ∈ ℝ)
35		nngt0 12370	. . . . . . . . . . 11 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → 0 < (𝐴 gcd 𝐵))
36	34, 35	jca 521	. . . . . . . . . 10 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵)))
37		divgt0 12186	. . . . . . . . . 10 ⊢ ((((abs‘𝐴) ∈ ℝ ∧ 0 < (abs‘𝐴)) ∧ ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵))) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
38	33, 36, 37	syl2an 608	. . . . . . . . 9 ⊢ (((abs‘𝐴) ∈ ℕ ∧ (𝐴 gcd 𝐵) ∈ ℕ) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
39	26, 22, 38	syl2anc 596	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
40		elnnz 12704	. . . . . . . 8 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ ↔ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ ∧ 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵))))
41	30, 39, 40	sylanbrc 595	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ)
42		elnn1uz2 13053	. . . . . . 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 501	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐵)
45	44	adantr 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ 𝐵)
46		breq1 5105	. . . . . . . . 9 ⊢ ((𝐴 gcd 𝐵) = (abs‘𝐴) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
47	45, 46	syl5ibcom 248	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) = (abs‘𝐴) → (abs‘𝐴) ∥ 𝐵))
48	26	nncnd 12352	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℂ)
49	22	nncnd 12352	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℂ)
50		1cnd 11303	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 1 ∈ ℂ)
51	48, 49, 50, 24	divmuld 12116	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ ((𝐴 gcd 𝐵) · 1) = (abs‘𝐴)))
52	49	mulridd 11327	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) · 1) = (𝐴 gcd 𝐵))
53	52	eqeq1d 2762	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((𝐴 gcd 𝐵) · 1) = (abs‘𝐴) ↔ (𝐴 gcd 𝐵) = (abs‘𝐴)))
54	51, 53	bitrd 282	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ (𝐴 gcd 𝐵) = (abs‘𝐴)))
55		absdvdsb 16445	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
56	55	adantr 486	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
57	47, 54, 56	3imtr4d 297	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 → 𝐴 ∥ 𝐵))
58		exprmfct 16881	. . . . . . . 8 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))
59		simprl 783	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∈ ℙ)
60	26	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℕ)
61	60	nnzd 12720	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℤ)
62	60	nnne0d 12389	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ≠ 0)
63	22	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 𝐵) ∈ ℕ)
64		pcdiv 17031	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ ((abs‘𝐴) ∈ ℤ ∧ (abs‘𝐴) ≠ 0) ∧ (𝐴 gcd 𝐵) ∈ ℕ) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))))
65	59, 61, 62, 63, 64	syl121anc 1402	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))))
66		simplll 787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℤ)
67		zq 13082	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
68	66, 67	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℚ)
69		pcabs 17054	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴))
70	59, 68, 69	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴))
71	70	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))))
72	65, 71	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))))
73		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))
74	41	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ)
75		pcelnn 17049	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ) → ((𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵))))
76	59, 74, 75	syl2anc 596	. . . . . . . . . . . . . . . 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 2861	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ)
79	59, 63	pccld 17029	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℕ₀)
80	79	nn0zd 12719	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ)
81		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ≠ 0)
82		pczcl 17027	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑝 pCnt 𝐴) ∈ ℕ₀)
83	59, 66, 81, 82	syl12anc 850	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℕ₀)
84	83	nn0zd 12719	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℤ)
85		znnsub 12743	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝑝 pCnt 𝐴) ∈ ℤ) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ))
86	80, 84, 85	syl2anc 596	. . . . . . . . . . . . . 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 12669	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℝ)
89	83	nn0red 12669	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℝ)
90	88, 89	ltnled 11458	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵))))
91	87, 90	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)))
92		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ∈ ℤ)
93		nprmdvds1 16883	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1)
94	93	ad2antrl 741	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ 1)
95		gcdid0 16693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴))
96	66, 95	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 0) = (abs‘𝐴))
97	96	oveq2d 7436	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = ((abs‘𝐴) / (abs‘𝐴)))
98	48	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℂ)
99	98, 62	dividd 12092	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (abs‘𝐴)) = 1)
100	97, 99	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = 1)
101	100	breq2d 5114	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) ↔ 𝑝 ∥ 1))
102	94, 101	mtbird 328	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)))
103		oveq2 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 = 0 → (𝐴 gcd 𝐵) = (𝐴 gcd 0))
104	103	oveq2d 7436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 = 0 → ((abs‘𝐴) / (𝐴 gcd 𝐵)) = ((abs‘𝐴) / (𝐴 gcd 0)))
105	104	breq2d 5114	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 0 → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0))))
106	73, 105	syl5ibcom 248	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐵 = 0 → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0))))
107	106	necon3bd 2969	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) → 𝐵 ≠ 0))
108	102, 107	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ≠ 0)
109		pczcl 17027	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℕ₀)
110	59, 92, 108, 109	syl12anc 850	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈ ℕ₀)
111	110	nn0red 12669	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈ ℝ)
112		lemin 13323	. . . . . . . . . . . . . 14 ⊢ (((𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐵) ∈ ℝ) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
113	89, 89, 111, 112	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
114		pcgcd 17057	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)))
115	59, 66, 92, 114	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)))
116	115	breq2d 5114	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)) ↔ (𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))))
117	89	leidd 11883	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴))
118	117	biantrurd 542	. . . . . . . . . . . . 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 462	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
122	121	reximdva 3175	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
123		rexnal 3114	. . . . . . . . 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 979	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)) → (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
127	43, 126	mpd 16	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
128	127	ord 878	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (¬ 𝐴 ∥ 𝐵 → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
129	128	con4d 116	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵))
130		2prm 16868	. . . . . 6 ⊢ 2 ∈ ℙ
131	130	ne0ii 4289	. . . . 5 ⊢ ℙ ≠ ∅
132		r19.2z 4454	. . . . 5 ⊢ ((ℙ ≠ ∅ ∧ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))
133	131, 132	mpan 703	. . . 4 ⊢ (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))
134		id 23	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
135		zq 13082	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℚ)
136	135	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℚ)
137		pcxcl 17040	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℙ ∧ 𝐵 ∈ ℚ) → (𝑝 pCnt 𝐵) ∈ ℝ^*)
138	134, 136, 137	syl2anr 609	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ∈ ℝ^*)
139		pnfge 13260	. . . . . . . . . 10 ⊢ ((𝑝 pCnt 𝐵) ∈ ℝ^* → (𝑝 pCnt 𝐵) ≤ +∞)
140	138, 139	syl 18	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ≤ +∞)
141	140	biantrurd 542	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (+∞ ≤ (𝑝 pCnt 𝐵) ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
142		pc0 17033	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → (𝑝 pCnt 0) = +∞)
143	142	adantl 487	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 0) = +∞)
144	143	breq1d 5112	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ +∞ ≤ (𝑝 pCnt 𝐵)))
145		pnfxr 11364	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
146		xrletri3 13284	. . . . . . . . 9 ⊢ (((𝑝 pCnt 𝐵) ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
147	138, 145, 146	sylancl 598	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
148	141, 144, 147	3bitr4d 314	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 𝐵) = +∞))
149		pnfnre 11351	. . . . . . . . . 10 ⊢ +∞ ∉ ℝ
150	149	neli 3063	. . . . . . . . 9 ⊢ ¬ +∞ ∈ ℝ
151		eleq1 2848	. . . . . . . . 9 ⊢ ((𝑝 pCnt 𝐵) = +∞ → ((𝑝 pCnt 𝐵) ∈ ℝ ↔ +∞ ∈ ℝ))
152	150, 151	mtbiri 330	. . . . . . . 8 ⊢ ((𝑝 pCnt 𝐵) = +∞ → ¬ (𝑝 pCnt 𝐵) ∈ ℝ)
153	109	nn0red 12669	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
154	153	adantll 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℙ) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
155	154	an4s 673	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑝 ∈ ℙ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
156	155	expr 462	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝐵 ≠ 0 → (𝑝 pCnt 𝐵) ∈ ℝ))
157	156	necon1bd 2973	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (¬ (𝑝 pCnt 𝐵) ∈ ℝ → 𝐵 = 0))
158	152, 157	syl5 35	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ → 𝐵 = 0))
159	148, 158	sylbid 243	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0))
160	159	rexlimdva 3163	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0))
161		0dvds 16447	. . . . . 6 ⊢ (𝐵 ∈ ℤ → (0 ∥ 𝐵 ↔ 𝐵 = 0))
162	161	adantl 487	. . . . 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 3040	. 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 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 ∅c0 4278 ifcif 4481 class class class wbr 5102 ‘cfv 6538 (class class class)co 7420 ℂcc 11199 ℝcr 11200 0cc0 11201 1c1 11202 · cmul 11206 +∞cpnf 11341 ℝ^*cxr 11343 < clt 11344 ≤ cle 11345 − cmin 11542 / cdiv 11974 ℕcn 12336 2c2 12398 ℕ₀cn0 12607 ℤcz 12694 ℤ_≥cuz 12966 ℚcq 13076 abscabs 15402 ∥ cdvds 16423 gcd cgcd 16665 ℙcprime 16847 pCnt cpc 17015

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278 ax-pre-sup 11279

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-2o 8478 df-er 8718 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-sup 9435 df-inf 9436 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-div 11975 df-nn 12337 df-2 12406 df-3 12407 df-n0 12608 df-z 12695 df-uz 12967 df-q 13077 df-rp 13122 df-fz 13641 df-fl 13933 df-mod 14011 df-seq 14146 df-exp 14206 df-cj 15267 df-re 15268 df-im 15269 df-sqrt 15403 df-abs 15404 df-dvds 16424 df-gcd 16666 df-prm 16848 df-pc 17016

This theorem is used by: pc11 17059 pcz 17060 pcprmpw2 17061 pockthg 17085 pgpfi 19820 fislw 19840 gexexlem 20067 ablfac1c 20288 sqff1o 27510 chtublem 27539 bposlem6 27617 aks4d1p7d1 43208 aks4d1p8d2 43211

W3C validator