pcdvdsb - Metamath Proof Explorer

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

Theorem pcdvdsb 16917

Description: 𝑃↑𝐴 divides 𝑁 if and only if 𝐴 is at most the count of 𝑃. (Contributed by Mario Carneiro, 3-Oct-2014.)

**Assertion**
Ref	Expression
pcdvdsb	⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))

**Proof of Theorem pcdvdsb**
Step	Hyp	Ref	Expression
1		oveq2 7408	. . . 4 ⊢ (𝑁 = 0 → (𝑃 pCnt 𝑁) = (𝑃 pCnt 0))
2	1	breq2d 5116	. . 3 ⊢ (𝑁 = 0 → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ 𝐴 ≤ (𝑃 pCnt 0)))
3		breq2 5108	. . 3 ⊢ (𝑁 = 0 → ((𝑃↑𝐴) ∥ 𝑁 ↔ (𝑃↑𝐴) ∥ 0))
4	2, 3	bibi12d 348	. 2 ⊢ (𝑁 = 0 → ((𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁) ↔ (𝐴 ≤ (𝑃 pCnt 0) ↔ (𝑃↑𝐴) ∥ 0)))
5		simpl3 1210	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℕ₀)
6	5	nn0zd 12604	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ)
7		simpl1 1208	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑃 ∈ ℙ)
8		simpl2 1209	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℤ)
9		simpr 489	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0)
10		pczcl 16896	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℕ₀)
11	7, 8, 9, 10	syl12anc 849	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃 pCnt 𝑁) ∈ ℕ₀)
12	11	nn0zd 12604	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃 pCnt 𝑁) ∈ ℤ)
13		eluz 12864	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ (𝑃 pCnt 𝑁) ∈ ℤ) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) ↔ 𝐴 ≤ (𝑃 pCnt 𝑁)))
14	6, 12, 13	syl2anc 595	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) ↔ 𝐴 ≤ (𝑃 pCnt 𝑁)))
15		prmnn 16720	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
16	7, 15	syl 18	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑃 ∈ ℕ)
17	16	nnzd 12605	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑃 ∈ ℤ)
18		dvdsexp 16374	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ₀ ∧ (𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴)) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)))
19	18	3expia 1137	. . . . . 6 ⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))))
20	17, 5, 19	syl2anc 595	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))))
21	14, 20	sylbird 263	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ≤ (𝑃 pCnt 𝑁) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))))
22		pczdvds 16911	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
23	7, 8, 9, 22	syl12anc 849	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
24		nnexpcl 14098	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℕ)
25	15, 24	sylan 591	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℕ)
26	25	3adant2 1147	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℕ)
27	26	nnzd 12605	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℤ)
28	27	adantr 485	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑𝐴) ∈ ℤ)
29	16, 11	nnexpcld 14269	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℕ)
30	29	nnzd 12605	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℤ)
31		dvdstr 16340	. . . . . 6 ⊢ (((𝑃↑𝐴) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) → (𝑃↑𝐴) ∥ 𝑁))
32	28, 30, 8, 31	syl3anc 1394	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) → (𝑃↑𝐴) ∥ 𝑁))
33	23, 32	mpan2d 706	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) → (𝑃↑𝐴) ∥ 𝑁))
34	21, 33	syld 48	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ≤ (𝑃 pCnt 𝑁) → (𝑃↑𝐴) ∥ 𝑁))
35		nn0re 12501	. . . . . . 7 ⊢ ((𝑃 pCnt 𝑁) ∈ ℕ₀ → (𝑃 pCnt 𝑁) ∈ ℝ)
36		nn0re 12501	. . . . . . 7 ⊢ (𝐴 ∈ ℕ₀ → 𝐴 ∈ ℝ)
37		ltnle 11277	. . . . . . 7 ⊢ (((𝑃 pCnt 𝑁) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ¬ 𝐴 ≤ (𝑃 pCnt 𝑁)))
38	35, 36, 37	syl2an 607	. . . . . 6 ⊢ (((𝑃 pCnt 𝑁) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ₀) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ¬ 𝐴 ≤ (𝑃 pCnt 𝑁)))
39		nn0ltp1le 12642	. . . . . 6 ⊢ (((𝑃 pCnt 𝑁) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ₀) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
40	38, 39	bitr3d 284	. . . . 5 ⊢ (((𝑃 pCnt 𝑁) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ₀) → (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
41	11, 5, 40	syl2anc 595	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
42		peano2nn0 12532	. . . . . . . . 9 ⊢ ((𝑃 pCnt 𝑁) ∈ ℕ₀ → ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀)
43	11, 42	syl 18	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀)
44	43	nn0zd 12604	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) + 1) ∈ ℤ)
45		eluz 12864	. . . . . . 7 ⊢ ((((𝑃 pCnt 𝑁) + 1) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
46	44, 6, 45	syl2anc 595	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
47		dvdsexp 16374	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀ ∧ 𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1))) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴))
48	47	3expia 1137	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)))
49	17, 43, 48	syl2anc 595	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)))
50	46, 49	sylbird 263	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃 pCnt 𝑁) + 1) ≤ 𝐴 → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)))
51		pczndvds 16913	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
52	7, 8, 9, 51	syl12anc 849	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
53	16, 43	nnexpcld 14269	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℕ)
54	53	nnzd 12605	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℤ)
55		dvdstr 16340	. . . . . . . 8 ⊢ (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℤ ∧ (𝑃↑𝐴) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁))
56	54, 28, 8, 55	syl3anc 1394	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁))
57	52, 56	mtod 201	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ¬ ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁))
58		imnan 404	. . . . . 6 ⊢ (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) → ¬ (𝑃↑𝐴) ∥ 𝑁) ↔ ¬ ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁))
59	57, 58	sylibr 237	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) → ¬ (𝑃↑𝐴) ∥ 𝑁))
60	50, 59	syld 48	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃 pCnt 𝑁) + 1) ≤ 𝐴 → ¬ (𝑃↑𝐴) ∥ 𝑁))
61	41, 60	sylbid 243	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) → ¬ (𝑃↑𝐴) ∥ 𝑁))
62	34, 61	impcon4bid 230	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))
63	36	3ad2ant3 1151	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ∈ ℝ)
64	63	rexrd 11247	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ∈ ℝ^*)
65		pnfge 13143	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
66	64, 65	syl 18	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ≤ +∞)
67		pc0 16902	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) = +∞)
68	67	3ad2ant1 1149	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃 pCnt 0) = +∞)
69	66, 68	breqtrrd 5132	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ≤ (𝑃 pCnt 0))
70		dvds0 16317	. . . 4 ⊢ ((𝑃↑𝐴) ∈ ℤ → (𝑃↑𝐴) ∥ 0)
71	27, 70	syl 18	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∥ 0)
72	69, 71	2thd 268	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝐴 ≤ (𝑃 pCnt 0) ↔ (𝑃↑𝐴) ∥ 0))
73	4, 62, 72	pm2.61ne 3045	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 class class class wbr 5104 ‘cfv 6525 (class class class)co 7400 ℝcr 11087 0cc0 11088 1c1 11089 + caddc 11091 +∞cpnf 11228 ℝ^*cxr 11230 < clt 11231 ≤ cle 11232 ℕcn 12221 ℕ₀cn0 12492 ℤcz 12579 ℤ_≥cuz 12850 ↑cexp 14085 ∥ cdvds 16298 ℙcprime 16717 pCnt cpc 16884

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-sup 9390 df-inf 9391 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12222 df-2 12291 df-3 12292 df-n0 12493 df-z 12580 df-uz 12851 df-q 12961 df-rp 13005 df-fl 13813 df-mod 13891 df-seq 14026 df-exp 14086 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-dvds 16299 df-gcd 16541 df-prm 16718 df-pc 16885

This theorem is referenced by: pcelnn 16918 pcidlem 16920 pcdvdstr 16924 pcgcd1 16925 pcfac 16947 pockthlem 16953 pockthg 16954 prmreclem2 16965 sylow1lem1 19656 sylow1lem3 19658 sylow1lem5 19660 ablfac1c 20131 ablfac1eu 20133 issqf 27254 vmasum 27334

W3C validator