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 15421

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 15418	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
2	1	ancoms 468	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
3	2	ralrimiva 2949	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
4	3	3expia 1259	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
5		oveq2 6557	. . . . . 6 ⊢ (𝐴 = 0 → (𝑝 pCnt 𝐴) = (𝑝 pCnt 0))
6	5	breq1d 4593	. . . . 5 ⊢ (𝐴 = 0 → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)))
7	6	ralbidv 2969	. . . 4 ⊢ (𝐴 = 0 → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)))
8		breq1 4586	. . . 4 ⊢ (𝐴 = 0 → (𝐴 ∥ 𝐵 ↔ 0 ∥ 𝐵))
9	7, 8	imbi12d 333	. . 3 ⊢ (𝐴 = 0 → ((∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵) ↔ (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵)))
10		gcddvds 15063	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
11	10	simpld 474	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐴)
12		gcdcl 15066	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℕ₀)
13	12	nn0zd 11356	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ)
14		simpl 472	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈ ℤ)
15		dvdsabsb 14839	. . . . . . . . . . . 12 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴)))
16	13, 14, 15	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴)))
17	11, 16	mpbid 221	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴))
18	17	adantr 480	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴))
19		simpl 472	. . . . . . . . . . . . 13 ⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → 𝐴 = 0)
20	19	necon3ai 2807	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ 0 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
21		gcdn0cl 15062	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ)
22	20, 21	sylan2 490	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℕ)
23	22	nnzd 11357	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℤ)
24	22	nnne0d 10942	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ≠ 0)
25		nnabscl 13913	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
26	25	adantlr 747	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℕ)
27	26	nnzd 11357	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℤ)
28		dvdsval2 14824	. . . . . . . . . 10 ⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ (abs‘𝐴) ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ))
29	23, 24, 27, 28	syl3anc 1318	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ))
30	18, 29	mpbid 221	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ)
31		nnre 10904	. . . . . . . . . . 11 ⊢ ((abs‘𝐴) ∈ ℕ → (abs‘𝐴) ∈ ℝ)
32		nngt0 10926	. . . . . . . . . . 11 ⊢ ((abs‘𝐴) ∈ ℕ → 0 < (abs‘𝐴))
33	31, 32	jca 553	. . . . . . . . . 10 ⊢ ((abs‘𝐴) ∈ ℕ → ((abs‘𝐴) ∈ ℝ ∧ 0 < (abs‘𝐴)))
34		nnre 10904	. . . . . . . . . . 11 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → (𝐴 gcd 𝐵) ∈ ℝ)
35		nngt0 10926	. . . . . . . . . . 11 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → 0 < (𝐴 gcd 𝐵))
36	34, 35	jca 553	. . . . . . . . . 10 ⊢ ((𝐴 gcd 𝐵) ∈ ℕ → ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵)))
37		divgt0 10770	. . . . . . . . . 10 ⊢ ((((abs‘𝐴) ∈ ℝ ∧ 0 < (abs‘𝐴)) ∧ ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵))) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
38	33, 36, 37	syl2an 493	. . . . . . . . 9 ⊢ (((abs‘𝐴) ∈ ℕ ∧ (𝐴 gcd 𝐵) ∈ ℕ) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
39	26, 22, 38	syl2anc 691	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵)))
40		elnnz 11264	. . . . . . . 8 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ ↔ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ ∧ 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵))))
41	30, 39, 40	sylanbrc 695	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ)
42		elnn1uz2 11641	. . . . . . 7 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ ↔ (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)))
43	41, 42	sylib 207	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)))
44	10	simprd 478	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐵)
45	44	adantr 480	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ 𝐵)
46		breq1 4586	. . . . . . . . 9 ⊢ ((𝐴 gcd 𝐵) = (abs‘𝐴) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
47	45, 46	syl5ibcom 234	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) = (abs‘𝐴) → (abs‘𝐴) ∥ 𝐵))
48	26	nncnd 10913	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℂ)
49	22	nncnd 10913	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℂ)
50		1cnd 9935	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 1 ∈ ℂ)
51	48, 49, 50, 24	divmuld 10702	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ ((𝐴 gcd 𝐵) · 1) = (abs‘𝐴)))
52	49	mulid1d 9936	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) · 1) = (𝐴 gcd 𝐵))
53	52	eqeq1d 2612	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((𝐴 gcd 𝐵) · 1) = (abs‘𝐴) ↔ (𝐴 gcd 𝐵) = (abs‘𝐴)))
54	51, 53	bitrd 267	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ (𝐴 gcd 𝐵) = (abs‘𝐴)))
55		absdvdsb 14838	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
56	55	adantr 480	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵))
57	47, 54, 56	3imtr4d 282	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 → 𝐴 ∥ 𝐵))
58		exprmfct 15254	. . . . . . . 8 ⊢ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))
59		simprl 790	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∈ ℙ)
60	26	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℕ)
61	60	nnzd 11357	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℤ)
62	60	nnne0d 10942	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ≠ 0)
63	22	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 𝐵) ∈ ℕ)
64		pcdiv 15395	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ ((abs‘𝐴) ∈ ℤ ∧ (abs‘𝐴) ≠ 0) ∧ (𝐴 gcd 𝐵) ∈ ℕ) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))))
65	59, 61, 62, 63, 64	syl121anc 1323	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))))
66		simplll 794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℤ)
67		zq 11670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)
68	66, 67	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℚ)
69		pcabs 15417	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴))
70	59, 68, 69	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴))
71	70	oveq1d 6564	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))))
72	65, 71	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))))
73		simprr 792	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))
74	41	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ)
75		pcelnn 15412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ) → ((𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵))))
76	59, 74, 75	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵))))
77	73, 76	mpbird 246	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ)
78	72, 77	eqeltrrd 2689	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ)
79	59, 63	pccld 15393	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℕ₀)
80	79	nn0zd 11356	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ)
81		simplr 788	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ≠ 0)
82		pczcl 15391	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑝 pCnt 𝐴) ∈ ℕ₀)
83	59, 66, 81, 82	syl12anc 1316	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℕ₀)
84	83	nn0zd 11356	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℤ)
85		znnsub 11300	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝑝 pCnt 𝐴) ∈ ℤ) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ))
86	80, 84, 85	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ))
87	78, 86	mpbird 246	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴))
88	79	nn0red 11229	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℝ)
89	83	nn0red 11229	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℝ)
90	88, 89	ltnled 10063	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵))))
91	87, 90	mpbid 221	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)))
92		simpllr 795	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ∈ ℤ)
93		nprmdvds1 15256	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1)
94	93	ad2antrl 760	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ 1)
95		gcdid0 15079	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴))
96	66, 95	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 0) = (abs‘𝐴))
97	96	oveq2d 6565	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = ((abs‘𝐴) / (abs‘𝐴)))
98	48	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℂ)
99	98, 62	dividd 10678	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (abs‘𝐴)) = 1)
100	97, 99	eqtrd 2644	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = 1)
101	100	breq2d 4595	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) ↔ 𝑝 ∥ 1))
102	94, 101	mtbird 314	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)))
103		oveq2 6557	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 = 0 → (𝐴 gcd 𝐵) = (𝐴 gcd 0))
104	103	oveq2d 6565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 = 0 → ((abs‘𝐴) / (𝐴 gcd 𝐵)) = ((abs‘𝐴) / (𝐴 gcd 0)))
105	104	breq2d 4595	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 0 → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0))))
106	73, 105	syl5ibcom 234	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐵 = 0 → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0))))
107	106	necon3bd 2796	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) → 𝐵 ≠ 0))
108	102, 107	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ≠ 0)
109		pczcl 15391	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℕ₀)
110	59, 92, 108, 109	syl12anc 1316	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈ ℕ₀)
111	110	nn0red 11229	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈ ℝ)
112		lemin 11897	. . . . . . . . . . . . . 14 ⊢ (((𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐵) ∈ ℝ) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
113	89, 89, 111, 112	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
114		pcgcd 15420	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)))
115	59, 66, 92, 114	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)))
116	115	breq2d 4595	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)) ↔ (𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))))
117	89	leidd 10473	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴))
118	117	biantrurd 528	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
119	113, 116, 118	3bitr4rd 300	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵))))
120	91, 119	mtbird 314	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
121	120	expr 641	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
122	121	reximdva 3000	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
123		rexnal 2978	. . . . . . . . 9 ⊢ (∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))
124	122, 123	syl6ib 240	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
125	58, 124	syl5 33	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2) → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
126	57, 125	orim12d 879	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ_≥‘2)) → (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))))
127	43, 126	mpd 15	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
128	127	ord 391	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (¬ 𝐴 ∥ 𝐵 → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))
129	128	con4d 113	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵))
130		2prm 15243	. . . . . 6 ⊢ 2 ∈ ℙ
131	130	ne0ii 3882	. . . . 5 ⊢ ℙ ≠ ∅
132		r19.2z 4012	. . . . 5 ⊢ ((ℙ ≠ ∅ ∧ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))
133	131, 132	mpan 702	. . . 4 ⊢ (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))
134		id 22	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
135		zq 11670	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ ℚ)
136	135	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℚ)
137		pcxcl 15403	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ ℙ ∧ 𝐵 ∈ ℚ) → (𝑝 pCnt 𝐵) ∈ ℝ^*)
138	134, 136, 137	syl2anr 494	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ∈ ℝ^*)
139		pnfge 11840	. . . . . . . . . 10 ⊢ ((𝑝 pCnt 𝐵) ∈ ℝ^* → (𝑝 pCnt 𝐵) ≤ +∞)
140	138, 139	syl 17	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ≤ +∞)
141	140	biantrurd 528	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (+∞ ≤ (𝑝 pCnt 𝐵) ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
142		pc0 15397	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → (𝑝 pCnt 0) = +∞)
143	142	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 0) = +∞)
144	143	breq1d 4593	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ +∞ ≤ (𝑝 pCnt 𝐵)))
145		pnfxr 9971	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
146		xrletri3 11861	. . . . . . . . 9 ⊢ (((𝑝 pCnt 𝐵) ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
147	138, 145, 146	sylancl 693	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵))))
148	141, 144, 147	3bitr4d 299	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 𝐵) = +∞))
149		pnfnre 9960	. . . . . . . . . 10 ⊢ +∞ ∉ ℝ
150	149	neli 2885	. . . . . . . . 9 ⊢ ¬ +∞ ∈ ℝ
151		eleq1 2676	. . . . . . . . 9 ⊢ ((𝑝 pCnt 𝐵) = +∞ → ((𝑝 pCnt 𝐵) ∈ ℝ ↔ +∞ ∈ ℝ))
152	150, 151	mtbiri 316	. . . . . . . 8 ⊢ ((𝑝 pCnt 𝐵) = +∞ → ¬ (𝑝 pCnt 𝐵) ∈ ℝ)
153	109	nn0red 11229	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
154	153	adantll 746	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℙ) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
155	154	an4s 865	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑝 ∈ ℙ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ)
156	155	expr 641	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝐵 ≠ 0 → (𝑝 pCnt 𝐵) ∈ ℝ))
157	156	necon1bd 2800	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (¬ (𝑝 pCnt 𝐵) ∈ ℝ → 𝐵 = 0))
158	152, 157	syl5 33	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ → 𝐵 = 0))
159	148, 158	sylbid 229	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0))
160	159	rexlimdva 3013	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0))
161		0dvds 14840	. . . . . 6 ⊢ (𝐵 ∈ ℤ → (0 ∥ 𝐵 ↔ 𝐵 = 0))
162	161	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ∥ 𝐵 ↔ 𝐵 = 0))
163	160, 162	sylibrd 248	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵))
164	133, 163	syl5 33	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵))
165	9, 129, 164	pm2.61ne 2867	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵))
166	4, 165	impbid 201	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 ∅c0 3874 ifcif 4036 class class class wbr 4583 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 · cmul 9820 +∞cpnf 9950 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ℚcq 11664 abscabs 13822 ∥ cdvds 14821 gcd cgcd 15054 ℙcprime 15223 pCnt cpc 15379

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-q 11665 df-rp 11709 df-fz 12198 df-fl 12455 df-mod 12531 df-seq 12664 df-exp 12723 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-dvds 14822 df-gcd 15055 df-prm 15224 df-pc 15380

This theorem is referenced by: pc11 15422 pcz 15423 pcprmpw2 15424 pockthg 15448 pgpfi 17843 fislw 17863 gexexlem 18078 ablfac1c 18293 sqff1o 24708 chtublem 24736 bposlem6 24814

W3C validator