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 16498

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 7263	. . . 4 ⊢ (𝑁 = 0 → (𝑃 pCnt 𝑁) = (𝑃 pCnt 0))
2	1	breq2d 5082	. . 3 ⊢ (𝑁 = 0 → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ 𝐴 ≤ (𝑃 pCnt 0)))
3		breq2 5074	. . 3 ⊢ (𝑁 = 0 → ((𝑃↑𝐴) ∥ 𝑁 ↔ (𝑃↑𝐴) ∥ 0))
4	2, 3	bibi12d 345	. 2 ⊢ (𝑁 = 0 → ((𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁) ↔ (𝐴 ≤ (𝑃 pCnt 0) ↔ (𝑃↑𝐴) ∥ 0)))
5		simpl3 1191	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℕ₀)
6	5	nn0zd 12353	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ)
7		simpl1 1189	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑃 ∈ ℙ)
8		simpl2 1190	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℤ)
9		simpr 484	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0)
10		pczcl 16477	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℕ₀)
11	7, 8, 9, 10	syl12anc 833	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃 pCnt 𝑁) ∈ ℕ₀)
12	11	nn0zd 12353	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃 pCnt 𝑁) ∈ ℤ)
13		eluz 12525	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ (𝑃 pCnt 𝑁) ∈ ℤ) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) ↔ 𝐴 ≤ (𝑃 pCnt 𝑁)))
14	6, 12, 13	syl2anc 583	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) ↔ 𝐴 ≤ (𝑃 pCnt 𝑁)))
15		prmnn 16307	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
16	7, 15	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑃 ∈ ℕ)
17	16	nnzd 12354	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑃 ∈ ℤ)
18		dvdsexp 15965	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ₀ ∧ (𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴)) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)))
19	18	3expia 1119	. . . . . 6 ⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))))
20	17, 5, 19	syl2anc 583	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))))
21	14, 20	sylbird 259	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ≤ (𝑃 pCnt 𝑁) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))))
22		pczdvds 16492	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
23	7, 8, 9, 22	syl12anc 833	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
24		nnexpcl 13723	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℕ)
25	15, 24	sylan 579	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℕ)
26	25	3adant2 1129	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℕ)
27	26	nnzd 12354	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℤ)
28	27	adantr 480	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑𝐴) ∈ ℤ)
29	16, 11	nnexpcld 13888	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℕ)
30	29	nnzd 12354	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℤ)
31		dvdstr 15931	. . . . . 6 ⊢ (((𝑃↑𝐴) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) → (𝑃↑𝐴) ∥ 𝑁))
32	28, 30, 8, 31	syl3anc 1369	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) → (𝑃↑𝐴) ∥ 𝑁))
33	23, 32	mpan2d 690	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) → (𝑃↑𝐴) ∥ 𝑁))
34	21, 33	syld 47	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ≤ (𝑃 pCnt 𝑁) → (𝑃↑𝐴) ∥ 𝑁))
35		nn0re 12172	. . . . . . 7 ⊢ ((𝑃 pCnt 𝑁) ∈ ℕ₀ → (𝑃 pCnt 𝑁) ∈ ℝ)
36		nn0re 12172	. . . . . . 7 ⊢ (𝐴 ∈ ℕ₀ → 𝐴 ∈ ℝ)
37		ltnle 10985	. . . . . . 7 ⊢ (((𝑃 pCnt 𝑁) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ¬ 𝐴 ≤ (𝑃 pCnt 𝑁)))
38	35, 36, 37	syl2an 595	. . . . . 6 ⊢ (((𝑃 pCnt 𝑁) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ₀) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ¬ 𝐴 ≤ (𝑃 pCnt 𝑁)))
39		nn0ltp1le 12308	. . . . . 6 ⊢ (((𝑃 pCnt 𝑁) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ₀) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
40	38, 39	bitr3d 280	. . . . 5 ⊢ (((𝑃 pCnt 𝑁) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ₀) → (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
41	11, 5, 40	syl2anc 583	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
42		peano2nn0 12203	. . . . . . . . 9 ⊢ ((𝑃 pCnt 𝑁) ∈ ℕ₀ → ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀)
43	11, 42	syl 17	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀)
44	43	nn0zd 12353	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) + 1) ∈ ℤ)
45		eluz 12525	. . . . . . 7 ⊢ ((((𝑃 pCnt 𝑁) + 1) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
46	44, 6, 45	syl2anc 583	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
47		dvdsexp 15965	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀ ∧ 𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1))) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴))
48	47	3expia 1119	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)))
49	17, 43, 48	syl2anc 583	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)))
50	46, 49	sylbird 259	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃 pCnt 𝑁) + 1) ≤ 𝐴 → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)))
51		pczndvds 16494	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
52	7, 8, 9, 51	syl12anc 833	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
53	16, 43	nnexpcld 13888	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℕ)
54	53	nnzd 12354	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℤ)
55		dvdstr 15931	. . . . . . . 8 ⊢ (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℤ ∧ (𝑃↑𝐴) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁))
56	54, 28, 8, 55	syl3anc 1369	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁))
57	52, 56	mtod 197	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ¬ ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁))
58		imnan 399	. . . . . 6 ⊢ (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) → ¬ (𝑃↑𝐴) ∥ 𝑁) ↔ ¬ ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁))
59	57, 58	sylibr 233	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) → ¬ (𝑃↑𝐴) ∥ 𝑁))
60	50, 59	syld 47	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃 pCnt 𝑁) + 1) ≤ 𝐴 → ¬ (𝑃↑𝐴) ∥ 𝑁))
61	41, 60	sylbid 239	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) → ¬ (𝑃↑𝐴) ∥ 𝑁))
62	34, 61	impcon4bid 226	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))
63	36	3ad2ant3 1133	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ∈ ℝ)
64	63	rexrd 10956	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ∈ ℝ^*)
65		pnfge 12795	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
66	64, 65	syl 17	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ≤ +∞)
67		pc0 16483	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) = +∞)
68	67	3ad2ant1 1131	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃 pCnt 0) = +∞)
69	66, 68	breqtrrd 5098	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ≤ (𝑃 pCnt 0))
70		dvds0 15909	. . . 4 ⊢ ((𝑃↑𝐴) ∈ ℤ → (𝑃↑𝐴) ∥ 0)
71	27, 70	syl 17	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∥ 0)
72	69, 71	2thd 264	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝐴 ≤ (𝑃 pCnt 0) ↔ (𝑃↑𝐴) ∥ 0))
73	4, 62, 72	pm2.61ne 3029	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 +∞cpnf 10937 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 ℕcn 11903 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 ↑cexp 13710 ∥ cdvds 15891 ℙcprime 16304 pCnt cpc 16465

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-q 12618 df-rp 12660 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-dvds 15892 df-gcd 16130 df-prm 16305 df-pc 16466

This theorem is referenced by: pcelnn 16499 pcidlem 16501 pcdvdstr 16505 pcgcd1 16506 pcfac 16528 pockthlem 16534 pockthg 16535 prmreclem2 16546 sylow1lem1 19118 sylow1lem3 19120 sylow1lem5 19122 ablfac1c 19589 ablfac1eu 19591 issqf 26190 vmasum 26269

W3C validator