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 16785

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 7362	. . . 4 ⊢ (𝑁 = 0 → (𝑃 pCnt 𝑁) = (𝑃 pCnt 0))
2	1	breq2d 5107	. . 3 ⊢ (𝑁 = 0 → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ 𝐴 ≤ (𝑃 pCnt 0)))
3		breq2 5099	. . 3 ⊢ (𝑁 = 0 → ((𝑃↑𝐴) ∥ 𝑁 ↔ (𝑃↑𝐴) ∥ 0))
4	2, 3	bibi12d 345	. 2 ⊢ (𝑁 = 0 → ((𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁) ↔ (𝐴 ≤ (𝑃 pCnt 0) ↔ (𝑃↑𝐴) ∥ 0)))
5		simpl3 1194	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℕ₀)
6	5	nn0zd 12502	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝐴 ∈ ℤ)
7		simpl1 1192	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑃 ∈ ℙ)
8		simpl2 1193	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑁 ∈ ℤ)
9		simpr 484	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑁 ≠ 0)
10		pczcl 16764	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℕ₀)
11	7, 8, 9, 10	syl12anc 836	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃 pCnt 𝑁) ∈ ℕ₀)
12	11	nn0zd 12502	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃 pCnt 𝑁) ∈ ℤ)
13		eluz 12754	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ (𝑃 pCnt 𝑁) ∈ ℤ) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) ↔ 𝐴 ≤ (𝑃 pCnt 𝑁)))
14	6, 12, 13	syl2anc 584	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) ↔ 𝐴 ≤ (𝑃 pCnt 𝑁)))
15		prmnn 16589	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
16	7, 15	syl 17	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑃 ∈ ℕ)
17	16	nnzd 12503	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → 𝑃 ∈ ℤ)
18		dvdsexp 16243	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ₀ ∧ (𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴)) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)))
19	18	3expia 1121	. . . . . 6 ⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))))
20	17, 5, 19	syl2anc 584	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) ∈ (ℤ_≥‘𝐴) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))))
21	14, 20	sylbird 260	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ≤ (𝑃 pCnt 𝑁) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))))
22		pczdvds 16779	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
23	7, 8, 9, 22	syl12anc 836	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
24		nnexpcl 13985	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℕ)
25	15, 24	sylan 580	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℕ)
26	25	3adant2 1131	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℕ)
27	26	nnzd 12503	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∈ ℤ)
28	27	adantr 480	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑𝐴) ∈ ℤ)
29	16, 11	nnexpcld 14156	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℕ)
30	29	nnzd 12503	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℤ)
31		dvdstr 16209	. . . . . 6 ⊢ (((𝑃↑𝐴) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) → (𝑃↑𝐴) ∥ 𝑁))
32	28, 30, 8, 31	syl3anc 1373	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) → (𝑃↑𝐴) ∥ 𝑁))
33	23, 32	mpan2d 694	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) → (𝑃↑𝐴) ∥ 𝑁))
34	21, 33	syld 47	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ≤ (𝑃 pCnt 𝑁) → (𝑃↑𝐴) ∥ 𝑁))
35		nn0re 12399	. . . . . . 7 ⊢ ((𝑃 pCnt 𝑁) ∈ ℕ₀ → (𝑃 pCnt 𝑁) ∈ ℝ)
36		nn0re 12399	. . . . . . 7 ⊢ (𝐴 ∈ ℕ₀ → 𝐴 ∈ ℝ)
37		ltnle 11201	. . . . . . 7 ⊢ (((𝑃 pCnt 𝑁) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ¬ 𝐴 ≤ (𝑃 pCnt 𝑁)))
38	35, 36, 37	syl2an 596	. . . . . 6 ⊢ (((𝑃 pCnt 𝑁) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ₀) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ¬ 𝐴 ≤ (𝑃 pCnt 𝑁)))
39		nn0ltp1le 12539	. . . . . 6 ⊢ (((𝑃 pCnt 𝑁) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ₀) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
40	38, 39	bitr3d 281	. . . . 5 ⊢ (((𝑃 pCnt 𝑁) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ₀) → (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
41	11, 5, 40	syl2anc 584	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
42		peano2nn0 12430	. . . . . . . . 9 ⊢ ((𝑃 pCnt 𝑁) ∈ ℕ₀ → ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀)
43	11, 42	syl 17	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀)
44	43	nn0zd 12502	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃 pCnt 𝑁) + 1) ∈ ℤ)
45		eluz 12754	. . . . . . 7 ⊢ ((((𝑃 pCnt 𝑁) + 1) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
46	44, 6, 45	syl2anc 584	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴))
47		dvdsexp 16243	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀ ∧ 𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1))) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴))
48	47	3expia 1121	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 pCnt 𝑁) + 1) ∈ ℕ₀) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)))
49	17, 43, 48	syl2anc 584	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ∈ (ℤ_≥‘((𝑃 pCnt 𝑁) + 1)) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)))
50	46, 49	sylbird 260	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃 pCnt 𝑁) + 1) ≤ 𝐴 → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)))
51		pczndvds 16781	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
52	7, 8, 9, 51	syl12anc 836	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
53	16, 43	nnexpcld 14156	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℕ)
54	53	nnzd 12503	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℤ)
55		dvdstr 16209	. . . . . . . 8 ⊢ (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℤ ∧ (𝑃↑𝐴) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁))
56	54, 28, 8, 55	syl3anc 1373	. . . . . . 7 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁))
57	52, 56	mtod 198	. . . . . 6 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ¬ ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁))
58		imnan 399	. . . . . 6 ⊢ (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) → ¬ (𝑃↑𝐴) ∥ 𝑁) ↔ ¬ ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁))
59	57, 58	sylibr 234	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) → ¬ (𝑃↑𝐴) ∥ 𝑁))
60	50, 59	syld 47	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (((𝑃 pCnt 𝑁) + 1) ≤ 𝐴 → ¬ (𝑃↑𝐴) ∥ 𝑁))
61	41, 60	sylbid 240	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) → ¬ (𝑃↑𝐴) ∥ 𝑁))
62	34, 61	impcon4bid 227	. 2 ⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) ∧ 𝑁 ≠ 0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))
63	36	3ad2ant3 1135	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ∈ ℝ)
64	63	rexrd 11171	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ∈ ℝ^*)
65		pnfge 13033	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
66	64, 65	syl 17	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ≤ +∞)
67		pc0 16770	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) = +∞)
68	67	3ad2ant1 1133	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃 pCnt 0) = +∞)
69	66, 68	breqtrrd 5123	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → 𝐴 ≤ (𝑃 pCnt 0))
70		dvds0 16186	. . . 4 ⊢ ((𝑃↑𝐴) ∈ ℤ → (𝑃↑𝐴) ∥ 0)
71	27, 70	syl 17	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝑃↑𝐴) ∥ 0)
72	69, 71	2thd 265	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝐴 ≤ (𝑃 pCnt 0) ↔ (𝑃↑𝐴) ∥ 0))
73	4, 62, 72	pm2.61ne 3014	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 class class class wbr 5095 ‘cfv 6488 (class class class)co 7354 ℝcr 11014 0cc0 11015 1c1 11016 + caddc 11018 +∞cpnf 11152 ℝ^*cxr 11154 < clt 11155 ≤ cle 11156 ℕcn 12134 ℕ₀cn0 12390 ℤcz 12477 ℤ_≥cuz 12740 ↑cexp 13972 ∥ cdvds 16167 ℙcprime 16586 pCnt cpc 16752

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7676 ax-cnex 11071 ax-resscn 11072 ax-1cn 11073 ax-icn 11074 ax-addcl 11075 ax-addrcl 11076 ax-mulcl 11077 ax-mulrcl 11078 ax-mulcom 11079 ax-addass 11080 ax-mulass 11081 ax-distr 11082 ax-i2m1 11083 ax-1ne0 11084 ax-1rid 11085 ax-rnegex 11086 ax-rrecex 11087 ax-cnre 11088 ax-pre-lttri 11089 ax-pre-lttrn 11090 ax-pre-ltadd 11091 ax-pre-mulgt0 11092 ax-pre-sup 11093

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-riota 7311 df-ov 7357 df-oprab 7358 df-mpo 7359 df-om 7805 df-1st 7929 df-2nd 7930 df-frecs 8219 df-wrecs 8250 df-recs 8299 df-rdg 8337 df-1o 8393 df-2o 8394 df-er 8630 df-en 8878 df-dom 8879 df-sdom 8880 df-fin 8881 df-sup 9335 df-inf 9336 df-pnf 11157 df-mnf 11158 df-xr 11159 df-ltxr 11160 df-le 11161 df-sub 11355 df-neg 11356 df-div 11784 df-nn 12135 df-2 12197 df-3 12198 df-n0 12391 df-z 12478 df-uz 12741 df-q 12851 df-rp 12895 df-fl 13700 df-mod 13778 df-seq 13913 df-exp 13973 df-cj 15010 df-re 15011 df-im 15012 df-sqrt 15146 df-abs 15147 df-dvds 16168 df-gcd 16410 df-prm 16587 df-pc 16753

This theorem is referenced by: pcelnn 16786 pcidlem 16788 pcdvdstr 16792 pcgcd1 16793 pcfac 16815 pockthlem 16821 pockthg 16822 prmreclem2 16833 sylow1lem1 19514 sylow1lem3 19516 sylow1lem5 19518 ablfac1c 19989 ablfac1eu 19991 issqf 27076 vmasum 27157

W3C validator