pcqmul - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > pcqmul		GIF version

Theorem pcqmul 12231

Description: Multiplication property of the prime power function. (Contributed by Mario Carneiro, 9-Sep-2014.)

**Assertion**
Ref	Expression
pcqmul	⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)))

Proof of Theorem pcqmul Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp2l 1013	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐴 ∈ ℚ)
2		elq 9556	. . 3 ⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
3	1, 2	sylib 121	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
4		simp3l 1015	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐵 ∈ ℚ)
5		elq 9556	. . 3 ⊢ (𝐵 ∈ ℚ ↔ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤))
6	4, 5	sylib 121	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤))
7		reeanv 2634	. . 3 ⊢ (∃𝑥 ∈ ℤ ∃𝑧 ∈ ℤ (∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) ↔ (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)))
8		reeanv 2634	. . . . 5 ⊢ (∃𝑦 ∈ ℕ ∃𝑤 ∈ ℕ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) ↔ (∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)))
9		simp2r 1014	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐴 ≠ 0)
10		simp3r 1016	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝐵 ≠ 0)
11	9, 10	jca 304	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝐴 ≠ 0 ∧ 𝐵 ≠ 0))
12	11	ad2antrr 480	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (𝐴 ≠ 0 ∧ 𝐵 ≠ 0))
13		simp1 987	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → 𝑃 ∈ ℙ)
14		simprl 521	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → 𝑦 ∈ ℕ)
15	14	nncnd 8867	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → 𝑦 ∈ ℂ)
16	14	nnap0d 8899	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → 𝑦 # 0)
17	15, 16	div0apd 8679	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (0 / 𝑦) = 0)
18		oveq1 5848	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → (𝑥 / 𝑦) = (0 / 𝑦))
19	18	eqeq1d 2174	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → ((𝑥 / 𝑦) = 0 ↔ (0 / 𝑦) = 0))
20	17, 19	syl5ibrcom 156	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (𝑥 = 0 → (𝑥 / 𝑦) = 0))
21	20	necon3d 2379	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝑥 / 𝑦) ≠ 0 → 𝑥 ≠ 0))
22		simprr 522	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → 𝑤 ∈ ℕ)
23	22	nncnd 8867	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → 𝑤 ∈ ℂ)
24	22	nnap0d 8899	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → 𝑤 # 0)
25	23, 24	div0apd 8679	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (0 / 𝑤) = 0)
26		oveq1 5848	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → (𝑧 / 𝑤) = (0 / 𝑤))
27	26	eqeq1d 2174	. . . . . . . . . . . 12 ⊢ (𝑧 = 0 → ((𝑧 / 𝑤) = 0 ↔ (0 / 𝑤) = 0))
28	25, 27	syl5ibrcom 156	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (𝑧 = 0 → (𝑧 / 𝑤) = 0))
29	28	necon3d 2379	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝑧 / 𝑤) ≠ 0 → 𝑧 ≠ 0))
30		simpll 519	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑃 ∈ ℙ)
31		simplrl 525	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑥 ∈ ℤ)
32		simplrr 526	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑧 ∈ ℤ)
33	31, 32	zmulcld 9315	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑥 · 𝑧) ∈ ℤ)
34	31	zcnd 9310	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑥 ∈ ℂ)
35	32	zcnd 9310	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑧 ∈ ℂ)
36		simprrl 529	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑥 ≠ 0)
37		0zd 9199	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 0 ∈ ℤ)
38		zapne 9261	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 0 ∈ ℤ) → (𝑥 # 0 ↔ 𝑥 ≠ 0))
39	31, 37, 38	syl2anc 409	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑥 # 0 ↔ 𝑥 ≠ 0))
40	36, 39	mpbird 166	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑥 # 0)
41		simprrr 530	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑧 ≠ 0)
42		zapne 9261	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ ℤ ∧ 0 ∈ ℤ) → (𝑧 # 0 ↔ 𝑧 ≠ 0))
43	32, 37, 42	syl2anc 409	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑧 # 0 ↔ 𝑧 ≠ 0))
44	41, 43	mpbird 166	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑧 # 0)
45	34, 35, 40, 44	mulap0d 8551	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑥 · 𝑧) # 0)
46		zapne 9261	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 · 𝑧) ∈ ℤ ∧ 0 ∈ ℤ) → ((𝑥 · 𝑧) # 0 ↔ (𝑥 · 𝑧) ≠ 0))
47	33, 37, 46	syl2anc 409	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → ((𝑥 · 𝑧) # 0 ↔ (𝑥 · 𝑧) ≠ 0))
48	45, 47	mpbid 146	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑥 · 𝑧) ≠ 0)
49	14	adantrr 471	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑦 ∈ ℕ)
50	22	adantrr 471	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑤 ∈ ℕ)
51	49, 50	nnmulcld 8902	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑦 · 𝑤) ∈ ℕ)
52		pcdiv 12230	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ ((𝑥 · 𝑧) ∈ ℤ ∧ (𝑥 · 𝑧) ≠ 0) ∧ (𝑦 · 𝑤) ∈ ℕ) → (𝑃 pCnt ((𝑥 · 𝑧) / (𝑦 · 𝑤))) = ((𝑃 pCnt (𝑥 · 𝑧)) − (𝑃 pCnt (𝑦 · 𝑤))))
53	30, 33, 48, 51, 52	syl121anc 1233	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt ((𝑥 · 𝑧) / (𝑦 · 𝑤))) = ((𝑃 pCnt (𝑥 · 𝑧)) − (𝑃 pCnt (𝑦 · 𝑤))))
54		pcmul 12229	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt (𝑥 · 𝑧)) = ((𝑃 pCnt 𝑥) + (𝑃 pCnt 𝑧)))
55	30, 31, 36, 32, 41, 54	syl122anc 1237	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt (𝑥 · 𝑧)) = ((𝑃 pCnt 𝑥) + (𝑃 pCnt 𝑧)))
56	49	nnzd 9308	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑦 ∈ ℤ)
57	14	nnne0d 8898	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → 𝑦 ≠ 0)
58	57	adantrr 471	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑦 ≠ 0)
59	50	nnzd 9308	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑤 ∈ ℤ)
60	22	nnne0d 8898	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → 𝑤 ≠ 0)
61	60	adantrr 471	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑤 ≠ 0)
62		pcmul 12229	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0) ∧ (𝑤 ∈ ℤ ∧ 𝑤 ≠ 0)) → (𝑃 pCnt (𝑦 · 𝑤)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑤)))
63	30, 56, 58, 59, 61, 62	syl122anc 1237	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt (𝑦 · 𝑤)) = ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑤)))
64	55, 63	oveq12d 5859	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → ((𝑃 pCnt (𝑥 · 𝑧)) − (𝑃 pCnt (𝑦 · 𝑤))) = (((𝑃 pCnt 𝑥) + (𝑃 pCnt 𝑧)) − ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑤))))
65		pczcl 12226	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℕ₀)
66	30, 31, 36, 65	syl12anc 1226	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt 𝑥) ∈ ℕ₀)
67	66	nn0cnd 9165	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt 𝑥) ∈ ℂ)
68		pczcl 12226	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0)) → (𝑃 pCnt 𝑧) ∈ ℕ₀)
69	30, 32, 41, 68	syl12anc 1226	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt 𝑧) ∈ ℕ₀)
70	69	nn0cnd 9165	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt 𝑧) ∈ ℂ)
71	30, 49	pccld 12228	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt 𝑦) ∈ ℕ₀)
72	71	nn0cnd 9165	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt 𝑦) ∈ ℂ)
73	30, 50	pccld 12228	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt 𝑤) ∈ ℕ₀)
74	73	nn0cnd 9165	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt 𝑤) ∈ ℂ)
75	67, 70, 72, 74	addsub4d 8252	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (((𝑃 pCnt 𝑥) + (𝑃 pCnt 𝑧)) − ((𝑃 pCnt 𝑦) + (𝑃 pCnt 𝑤))) = (((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)) + ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤))))
76	53, 64, 75	3eqtrd 2202	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt ((𝑥 · 𝑧) / (𝑦 · 𝑤))) = (((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)) + ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤))))
77	15	adantrr 471	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑦 ∈ ℂ)
78	23	adantrr 471	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑤 ∈ ℂ)
79	16	adantrr 471	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑦 # 0)
80	24	adantrr 471	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → 𝑤 # 0)
81	34, 77, 35, 78, 79, 80	divmuldivapd 8724	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → ((𝑥 / 𝑦) · (𝑧 / 𝑤)) = ((𝑥 · 𝑧) / (𝑦 · 𝑤)))
82	81	oveq2d 5857	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt ((𝑥 / 𝑦) · (𝑧 / 𝑤))) = (𝑃 pCnt ((𝑥 · 𝑧) / (𝑦 · 𝑤))))
83		pcdiv 12230	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)))
84	30, 31, 36, 49, 83	syl121anc 1233	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)))
85		pcdiv 12230	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ (𝑧 ∈ ℤ ∧ 𝑧 ≠ 0) ∧ 𝑤 ∈ ℕ) → (𝑃 pCnt (𝑧 / 𝑤)) = ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤)))
86	30, 32, 41, 50, 85	syl121anc 1233	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt (𝑧 / 𝑤)) = ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤)))
87	84, 86	oveq12d 5859	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → ((𝑃 pCnt (𝑥 / 𝑦)) + (𝑃 pCnt (𝑧 / 𝑤))) = (((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)) + ((𝑃 pCnt 𝑧) − (𝑃 pCnt 𝑤))))
88	76, 82, 87	3eqtr4d 2208	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑧 ≠ 0))) → (𝑃 pCnt ((𝑥 / 𝑦) · (𝑧 / 𝑤))) = ((𝑃 pCnt (𝑥 / 𝑦)) + (𝑃 pCnt (𝑧 / 𝑤))))
89	88	expr 373	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝑥 ≠ 0 ∧ 𝑧 ≠ 0) → (𝑃 pCnt ((𝑥 / 𝑦) · (𝑧 / 𝑤))) = ((𝑃 pCnt (𝑥 / 𝑦)) + (𝑃 pCnt (𝑧 / 𝑤)))))
90	21, 29, 89	syl2and 293	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (((𝑥 / 𝑦) ≠ 0 ∧ (𝑧 / 𝑤) ≠ 0) → (𝑃 pCnt ((𝑥 / 𝑦) · (𝑧 / 𝑤))) = ((𝑃 pCnt (𝑥 / 𝑦)) + (𝑃 pCnt (𝑧 / 𝑤)))))
91		neeq1 2348	. . . . . . . . . . 11 ⊢ (𝐴 = (𝑥 / 𝑦) → (𝐴 ≠ 0 ↔ (𝑥 / 𝑦) ≠ 0))
92		neeq1 2348	. . . . . . . . . . 11 ⊢ (𝐵 = (𝑧 / 𝑤) → (𝐵 ≠ 0 ↔ (𝑧 / 𝑤) ≠ 0))
93	91, 92	bi2anan9 596	. . . . . . . . . 10 ⊢ ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ ((𝑥 / 𝑦) ≠ 0 ∧ (𝑧 / 𝑤) ≠ 0)))
94		oveq12 5850	. . . . . . . . . . . 12 ⊢ ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝐴 · 𝐵) = ((𝑥 / 𝑦) · (𝑧 / 𝑤)))
95	94	oveq2d 5857	. . . . . . . . . . 11 ⊢ ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt (𝐴 · 𝐵)) = (𝑃 pCnt ((𝑥 / 𝑦) · (𝑧 / 𝑤))))
96		oveq2 5849	. . . . . . . . . . . 12 ⊢ (𝐴 = (𝑥 / 𝑦) → (𝑃 pCnt 𝐴) = (𝑃 pCnt (𝑥 / 𝑦)))
97		oveq2 5849	. . . . . . . . . . . 12 ⊢ (𝐵 = (𝑧 / 𝑤) → (𝑃 pCnt 𝐵) = (𝑃 pCnt (𝑧 / 𝑤)))
98	96, 97	oveqan12d 5860	. . . . . . . . . . 11 ⊢ ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)) = ((𝑃 pCnt (𝑥 / 𝑦)) + (𝑃 pCnt (𝑧 / 𝑤))))
99	95, 98	eqeq12d 2180	. . . . . . . . . 10 ⊢ ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → ((𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)) ↔ (𝑃 pCnt ((𝑥 / 𝑦) · (𝑧 / 𝑤))) = ((𝑃 pCnt (𝑥 / 𝑦)) + (𝑃 pCnt (𝑧 / 𝑤)))))
100	93, 99	imbi12d 233	. . . . . . . . 9 ⊢ ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))) ↔ (((𝑥 / 𝑦) ≠ 0 ∧ (𝑧 / 𝑤) ≠ 0) → (𝑃 pCnt ((𝑥 / 𝑦) · (𝑧 / 𝑤))) = ((𝑃 pCnt (𝑥 / 𝑦)) + (𝑃 pCnt (𝑧 / 𝑤))))))
101	90, 100	syl5ibrcom 156	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)))))
102	13, 101	sylanl1 400	. . . . . . 7 ⊢ ((((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)))))
103	12, 102	mpid 42	. . . . . 6 ⊢ ((((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))))
104	103	rexlimdvva 2590	. . . . 5 ⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → (∃𝑦 ∈ ℕ ∃𝑤 ∈ ℕ (𝐴 = (𝑥 / 𝑦) ∧ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))))
105	8, 104	syl5bir 152	. . . 4 ⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) ∧ (𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ)) → ((∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))))
106	105	rexlimdvva 2590	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (∃𝑥 ∈ ℤ ∃𝑧 ∈ ℤ (∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))))
107	7, 106	syl5bir 152	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ((∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ 𝐵 = (𝑧 / 𝑤)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))))
108	3, 6, 107	mp2and 430	1 ⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 968 = wceq 1343 ∈ wcel 2136 ≠ wne 2335 ∃wrex 2444 class class class wbr 3981 (class class class)co 5841 ℂcc 7747 0cc0 7749 + caddc 7752 · cmul 7754 − cmin 8065 # cap 8475 / cdiv 8564 ℕcn 8853 ℕ₀cn0 9110 ℤcz 9187 ℚcq 9553 ℙcprime 12035 pCnt cpc 12212

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4096 ax-sep 4099 ax-nul 4107 ax-pow 4152 ax-pr 4186 ax-un 4410 ax-setind 4513 ax-iinf 4564 ax-cnex 7840 ax-resscn 7841 ax-1cn 7842 ax-1re 7843 ax-icn 7844 ax-addcl 7845 ax-addrcl 7846 ax-mulcl 7847 ax-mulrcl 7848 ax-addcom 7849 ax-mulcom 7850 ax-addass 7851 ax-mulass 7852 ax-distr 7853 ax-i2m1 7854 ax-0lt1 7855 ax-1rid 7856 ax-0id 7857 ax-rnegex 7858 ax-precex 7859 ax-cnre 7860 ax-pre-ltirr 7861 ax-pre-ltwlin 7862 ax-pre-lttrn 7863 ax-pre-apti 7864 ax-pre-ltadd 7865 ax-pre-mulgt0 7866 ax-pre-mulext 7867 ax-arch 7868 ax-caucvg 7869

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2296 df-ne 2336 df-nel 2431 df-ral 2448 df-rex 2449 df-reu 2450 df-rmo 2451 df-rab 2452 df-v 2727 df-sbc 2951 df-csb 3045 df-dif 3117 df-un 3119 df-in 3121 df-ss 3128 df-nul 3409 df-if 3520 df-pw 3560 df-sn 3581 df-pr 3582 df-op 3584 df-uni 3789 df-int 3824 df-iun 3867 df-br 3982 df-opab 4043 df-mpt 4044 df-tr 4080 df-id 4270 df-po 4273 df-iso 4274 df-iord 4343 df-on 4345 df-ilim 4346 df-suc 4348 df-iom 4567 df-xp 4609 df-rel 4610 df-cnv 4611 df-co 4612 df-dm 4613 df-rn 4614 df-res 4615 df-ima 4616 df-iota 5152 df-fun 5189 df-fn 5190 df-f 5191 df-f1 5192 df-fo 5193 df-f1o 5194 df-fv 5195 df-isom 5196 df-riota 5797 df-ov 5844 df-oprab 5845 df-mpo 5846 df-1st 6105 df-2nd 6106 df-recs 6269 df-frec 6355 df-1o 6380 df-2o 6381 df-er 6497 df-en 6703 df-sup 6945 df-inf 6946 df-pnf 7931 df-mnf 7932 df-xr 7933 df-ltxr 7934 df-le 7935 df-sub 8067 df-neg 8068 df-reap 8469 df-ap 8476 df-div 8565 df-inn 8854 df-2 8912 df-3 8913 df-4 8914 df-n0 9111 df-z 9188 df-uz 9463 df-q 9554 df-rp 9586 df-fz 9941 df-fzo 10074 df-fl 10201 df-mod 10254 df-seqfrec 10377 df-exp 10451 df-cj 10780 df-re 10781 df-im 10782 df-rsqrt 10936 df-abs 10937 df-dvds 11724 df-gcd 11872 df-prm 12036 df-pc 12213

This theorem is referenced by: pcqdiv 12235 pcexp 12237 pcaddlem 12266

W3C validator