pcadd

Description: An inequality for the prime count of a sum. This is the source of the ultrametric inequality for the p-adic metric. (Contributed by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Hypotheses	pcadd.1	$⊢ φ \to P \in ℙ$
	pcadd.2	$⊢ φ \to A \in ℚ$
	pcadd.3	$⊢ φ \to B \in ℚ$
	pcadd.4	$⊢ φ \to P pCnt A \leq P pCnt B$
Assertion	pcadd	$⊢ φ \to P pCnt A \leq P pCnt (A + B)$

Proof

Step	Hyp	Ref	Expression
1		pcadd.1	$⊢ φ \to P \in ℙ$
2		pcadd.2	$⊢ φ \to A \in ℚ$
3		pcadd.3	$⊢ φ \to B \in ℚ$
4		pcadd.4	$⊢ φ \to P pCnt A \leq P pCnt B$
5		elq	$⊢ A \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y}$
6	2 5	sylib	$⊢ φ \to \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y}$
7		elq	$⊢ B \in ℚ \leftrightarrow \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w}$
8	3 7	sylib	$⊢ φ \to \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w}$
9		pcxcl	$⊢ (P \in ℙ \land A \in ℚ) \to P pCnt A \in ℝ^{*}$
10	1 2 9	syl2anc	$⊢ φ \to P pCnt A \in ℝ^{*}$
11	10	xrleidd	$⊢ φ \to P pCnt A \leq P pCnt A$
12	11	adantr	$⊢ (φ \land B = 0) \to P pCnt A \leq P pCnt A$
13		oveq2	$⊢ B = 0 \to A + B = A + 0$
14		qcn	$⊢ A \in ℚ \to A \in ℂ$
15	2 14	syl	$⊢ φ \to A \in ℂ$
16	15	addridd	$⊢ φ \to A + 0 = A$
17	13 16	sylan9eqr	$⊢ (φ \land B = 0) \to A + B = A$
18	17	oveq2d	$⊢ (φ \land B = 0) \to P pCnt (A + B) = P pCnt A$
19	12 18	breqtrrd	$⊢ (φ \land B = 0) \to P pCnt A \leq P pCnt (A + B)$
20	19	a1d	$⊢ (φ \land B = 0) \to ((\exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \land \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w}) \to P pCnt A \leq P pCnt (A + B))$
21		reeanv	$⊢ \exists x \in ℤ \exists z \in ℤ (\exists y \in ℕ A = \frac{x}{y} \land \exists w \in ℕ B = \frac{z}{w}) \leftrightarrow (\exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \land \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w})$
22		reeanv	$⊢ \exists y \in ℕ \exists w \in ℕ (A = \frac{x}{y} \land B = \frac{z}{w}) \leftrightarrow (\exists y \in ℕ A = \frac{x}{y} \land \exists w \in ℕ B = \frac{z}{w})$
23	1	ad3antrrr	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P \in ℙ$
24		prmnn	$⊢ P \in ℙ \to P \in ℕ$
25	23 24	syl	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P \in ℕ$
26		simplrl	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to x \in ℤ$
27		simprrl	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to A = \frac{x}{y}$
28		pc0	$⊢ P \in ℙ \to P pCnt 0 = +∞$
29	23 28	syl	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt 0 = +∞$
30	3	ad3antrrr	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to B \in ℚ$
31		simpllr	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to B \neq 0$
32		pcqcl	$⊢ (P \in ℙ \land (B \in ℚ \land B \neq 0)) \to P pCnt B \in ℤ$
33	23 30 31 32	syl12anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt B \in ℤ$
34	33	zred	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt B \in ℝ$
35		ltpnf	$⊢ P pCnt B \in ℝ \to P pCnt B < +∞$
36		rexr	$⊢ P pCnt B \in ℝ \to P pCnt B \in ℝ^{*}$
37		pnfxr	$⊢ +∞ \in ℝ^{*}$
38		xrltnle	$⊢ (P pCnt B \in ℝ^{} \land +∞ \in ℝ^{}) \to (P pCnt B < +∞ \leftrightarrow \neg +∞ \leq P pCnt B)$
39	36 37 38	sylancl	$⊢ P pCnt B \in ℝ \to (P pCnt B < +∞ \leftrightarrow \neg +∞ \leq P pCnt B)$
40	35 39	mpbid	$⊢ P pCnt B \in ℝ \to \neg +∞ \leq P pCnt B$
41	34 40	syl	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \neg +∞ \leq P pCnt B$
42	29 41	eqnbrtrd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \neg P pCnt 0 \leq P pCnt B$
43	4	ad3antrrr	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt A \leq P pCnt B$
44		oveq2	$⊢ A = 0 \to P pCnt A = P pCnt 0$
45	44	breq1d	$⊢ A = 0 \to (P pCnt A \leq P pCnt B \leftrightarrow P pCnt 0 \leq P pCnt B)$
46	43 45	syl5ibcom	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (A = 0 \to P pCnt 0 \leq P pCnt B)$
47	46	necon3bd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (\neg P pCnt 0 \leq P pCnt B \to A \neq 0)$
48	42 47	mpd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to A \neq 0$
49	27 48	eqnetrrd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{x}{y} \neq 0$
50		simprll	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to y \in ℕ$
51	50	nncnd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to y \in ℂ$
52	50	nnne0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to y \neq 0$
53	51 52	div0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{0}{y} = 0$
54		oveq1	$⊢ x = 0 \to \frac{x}{y} = \frac{0}{y}$
55	54	eqeq1d	$⊢ x = 0 \to (\frac{x}{y} = 0 \leftrightarrow \frac{0}{y} = 0)$
56	53 55	syl5ibrcom	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (x = 0 \to \frac{x}{y} = 0)$
57	56	necon3d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (\frac{x}{y} \neq 0 \to x \neq 0)$
58	49 57	mpd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to x \neq 0$
59		pczcl	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0)) \to P pCnt x \in ℕ_{0}$
60	23 26 58 59	syl12anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt x \in ℕ_{0}$
61	25 60	nnexpcld	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt x} \in ℕ$
62	61	nncnd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt x} \in ℂ$
63	62 51	mulcomd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt x} y = y P^{P pCnt x}$
64	63	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{x P^{P pCnt y}}{P^{P pCnt x} y} = \frac{x P^{P pCnt y}}{y P^{P pCnt x}}$
65	26	zcnd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to x \in ℂ$
66	23 50	pccld	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt y \in ℕ_{0}$
67	25 66	nnexpcld	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt y} \in ℕ$
68	67	nncnd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt y} \in ℂ$
69	61	nnne0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt x} \neq 0$
70	67	nnne0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt y} \neq 0$
71	65 62 51 68 69 70 52	divdivdivd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{\frac{x}{P^{P pCnt x}}}{\frac{y}{P^{P pCnt y}}} = \frac{x P^{P pCnt y}}{P^{P pCnt x} y}$
72	27	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt A = P pCnt (\frac{x}{y})$
73		pcdiv	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0) \land y \in ℕ) \to P pCnt (\frac{x}{y}) = (P pCnt x) - (P pCnt y)$
74	23 26 58 50 73	syl121anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt (\frac{x}{y}) = (P pCnt x) - (P pCnt y)$
75	72 74	eqtrd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt A = (P pCnt x) - (P pCnt y)$
76	75	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt A} = P^{(P pCnt x) - (P pCnt y)}$
77	25	nncnd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P \in ℂ$
78	25	nnne0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P \neq 0$
79	66	nn0zd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt y \in ℤ$
80	60	nn0zd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt x \in ℤ$
81	77 78 79 80	expsubd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{(P pCnt x) - (P pCnt y)} = \frac{P^{P pCnt x}}{P^{P pCnt y}}$
82	76 81	eqtrd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt A} = \frac{P^{P pCnt x}}{P^{P pCnt y}}$
83	82	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{A}{P^{P pCnt A}} = \frac{A}{\frac{P^{P pCnt x}}{P^{P pCnt y}}}$
84	27	oveq1d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{A}{\frac{P^{P pCnt x}}{P^{P pCnt y}}} = \frac{\frac{x}{y}}{\frac{P^{P pCnt x}}{P^{P pCnt y}}}$
85	65 51 62 68 52 70 69	divdivdivd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{\frac{x}{y}}{\frac{P^{P pCnt x}}{P^{P pCnt y}}} = \frac{x P^{P pCnt y}}{y P^{P pCnt x}}$
86	83 84 85	3eqtrd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{A}{P^{P pCnt A}} = \frac{x P^{P pCnt y}}{y P^{P pCnt x}}$
87	64 71 86	3eqtr4d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{\frac{x}{P^{P pCnt x}}}{\frac{y}{P^{P pCnt y}}} = \frac{A}{P^{P pCnt A}}$
88	87	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt A} (\frac{\frac{x}{P^{P pCnt x}}}{\frac{y}{P^{P pCnt y}}}) = P^{P pCnt A} (\frac{A}{P^{P pCnt A}})$
89	2	ad3antrrr	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to A \in ℚ$
90	89 14	syl	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to A \in ℂ$
91		pcqcl	$⊢ (P \in ℙ \land (A \in ℚ \land A \neq 0)) \to P pCnt A \in ℤ$
92	23 89 48 91	syl12anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt A \in ℤ$
93	77 78 92	expclzd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt A} \in ℂ$
94	77 78 92	expne0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt A} \neq 0$
95	90 93 94	divcan2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt A} (\frac{A}{P^{P pCnt A}}) = A$
96	88 95	eqtr2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to A = P^{P pCnt A} (\frac{\frac{x}{P^{P pCnt x}}}{\frac{y}{P^{P pCnt y}}})$
97		simplrr	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to z \in ℤ$
98		simprrr	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to B = \frac{z}{w}$
99	98 31	eqnetrrd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{z}{w} \neq 0$
100		simprlr	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to w \in ℕ$
101	100	nncnd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to w \in ℂ$
102	100	nnne0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to w \neq 0$
103	101 102	div0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{0}{w} = 0$
104		oveq1	$⊢ z = 0 \to \frac{z}{w} = \frac{0}{w}$
105	104	eqeq1d	$⊢ z = 0 \to (\frac{z}{w} = 0 \leftrightarrow \frac{0}{w} = 0)$
106	103 105	syl5ibrcom	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (z = 0 \to \frac{z}{w} = 0)$
107	106	necon3d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (\frac{z}{w} \neq 0 \to z \neq 0)$
108	99 107	mpd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to z \neq 0$
109		pczcl	$⊢ (P \in ℙ \land (z \in ℤ \land z \neq 0)) \to P pCnt z \in ℕ_{0}$
110	23 97 108 109	syl12anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt z \in ℕ_{0}$
111	25 110	nnexpcld	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt z} \in ℕ$
112	111	nncnd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt z} \in ℂ$
113	112 101	mulcomd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt z} w = w P^{P pCnt z}$
114	113	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{z P^{P pCnt w}}{P^{P pCnt z} w} = \frac{z P^{P pCnt w}}{w P^{P pCnt z}}$
115	97	zcnd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to z \in ℂ$
116	23 100	pccld	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt w \in ℕ_{0}$
117	25 116	nnexpcld	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt w} \in ℕ$
118	117	nncnd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt w} \in ℂ$
119	111	nnne0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt z} \neq 0$
120	117	nnne0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt w} \neq 0$
121	115 112 101 118 119 120 102	divdivdivd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{\frac{z}{P^{P pCnt z}}}{\frac{w}{P^{P pCnt w}}} = \frac{z P^{P pCnt w}}{P^{P pCnt z} w}$
122	98	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt B = P pCnt (\frac{z}{w})$
123		pcdiv	$⊢ (P \in ℙ \land (z \in ℤ \land z \neq 0) \land w \in ℕ) \to P pCnt (\frac{z}{w}) = (P pCnt z) - (P pCnt w)$
124	23 97 108 100 123	syl121anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt (\frac{z}{w}) = (P pCnt z) - (P pCnt w)$
125	122 124	eqtrd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt B = (P pCnt z) - (P pCnt w)$
126	125	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt B} = P^{(P pCnt z) - (P pCnt w)}$
127	116	nn0zd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt w \in ℤ$
128	110	nn0zd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt z \in ℤ$
129	77 78 127 128	expsubd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{(P pCnt z) - (P pCnt w)} = \frac{P^{P pCnt z}}{P^{P pCnt w}}$
130	126 129	eqtrd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt B} = \frac{P^{P pCnt z}}{P^{P pCnt w}}$
131	130	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{B}{P^{P pCnt B}} = \frac{B}{\frac{P^{P pCnt z}}{P^{P pCnt w}}}$
132	98	oveq1d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{B}{\frac{P^{P pCnt z}}{P^{P pCnt w}}} = \frac{\frac{z}{w}}{\frac{P^{P pCnt z}}{P^{P pCnt w}}}$
133	115 101 112 118 102 120 119	divdivdivd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{\frac{z}{w}}{\frac{P^{P pCnt z}}{P^{P pCnt w}}} = \frac{z P^{P pCnt w}}{w P^{P pCnt z}}$
134	131 132 133	3eqtrd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{B}{P^{P pCnt B}} = \frac{z P^{P pCnt w}}{w P^{P pCnt z}}$
135	114 121 134	3eqtr4d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{\frac{z}{P^{P pCnt z}}}{\frac{w}{P^{P pCnt w}}} = \frac{B}{P^{P pCnt B}}$
136	135	oveq2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt B} (\frac{\frac{z}{P^{P pCnt z}}}{\frac{w}{P^{P pCnt w}}}) = P^{P pCnt B} (\frac{B}{P^{P pCnt B}})$
137		qcn	$⊢ B \in ℚ \to B \in ℂ$
138	30 137	syl	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to B \in ℂ$
139	77 78 33	expclzd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt B} \in ℂ$
140	77 78 33	expne0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt B} \neq 0$
141	138 139 140	divcan2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt B} (\frac{B}{P^{P pCnt B}}) = B$
142	136 141	eqtr2d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to B = P^{P pCnt B} (\frac{\frac{z}{P^{P pCnt z}}}{\frac{w}{P^{P pCnt w}}})$
143		eluz	$⊢ (P pCnt A \in ℤ \land P pCnt B \in ℤ) \to (P pCnt B \in ℤ_{\geq (P pCnt A)} \leftrightarrow P pCnt A \leq P pCnt B)$
144	92 33 143	syl2anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (P pCnt B \in ℤ_{\geq (P pCnt A)} \leftrightarrow P pCnt A \leq P pCnt B)$
145	43 144	mpbird	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt B \in ℤ_{\geq (P pCnt A)}$
146		pczdvds	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0)) \to P^{P pCnt x} ∥ x$
147	23 26 58 146	syl12anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt x} ∥ x$
148	61	nnzd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt x} \in ℤ$
149		dvdsval2	$⊢ (P^{P pCnt x} \in ℤ \land P^{P pCnt x} \neq 0 \land x \in ℤ) \to (P^{P pCnt x} ∥ x \leftrightarrow \frac{x}{P^{P pCnt x}} \in ℤ)$
150	148 69 26 149	syl3anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (P^{P pCnt x} ∥ x \leftrightarrow \frac{x}{P^{P pCnt x}} \in ℤ)$
151	147 150	mpbid	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{x}{P^{P pCnt x}} \in ℤ$
152		pczndvds2	$⊢ (P \in ℙ \land (x \in ℤ \land x \neq 0)) \to \neg P ∥ (\frac{x}{P^{P pCnt x}})$
153	23 26 58 152	syl12anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \neg P ∥ (\frac{x}{P^{P pCnt x}})$
154	151 153	jca	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (\frac{x}{P^{P pCnt x}} \in ℤ \land \neg P ∥ (\frac{x}{P^{P pCnt x}}))$
155		pcdvds	$⊢ (P \in ℙ \land y \in ℕ) \to P^{P pCnt y} ∥ y$
156	23 50 155	syl2anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt y} ∥ y$
157	67	nnzd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt y} \in ℤ$
158	50	nnzd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to y \in ℤ$
159		dvdsval2	$⊢ (P^{P pCnt y} \in ℤ \land P^{P pCnt y} \neq 0 \land y \in ℤ) \to (P^{P pCnt y} ∥ y \leftrightarrow \frac{y}{P^{P pCnt y}} \in ℤ)$
160	157 70 158 159	syl3anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (P^{P pCnt y} ∥ y \leftrightarrow \frac{y}{P^{P pCnt y}} \in ℤ)$
161	156 160	mpbid	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{y}{P^{P pCnt y}} \in ℤ$
162	50	nnred	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to y \in ℝ$
163	67	nnred	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt y} \in ℝ$
164	50	nngt0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to 0 < y$
165	67	nngt0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to 0 < P^{P pCnt y}$
166	162 163 164 165	divgt0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to 0 < \frac{y}{P^{P pCnt y}}$
167		elnnz	$⊢ \frac{y}{P^{P pCnt y}} \in ℕ \leftrightarrow (\frac{y}{P^{P pCnt y}} \in ℤ \land 0 < \frac{y}{P^{P pCnt y}})$
168	161 166 167	sylanbrc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{y}{P^{P pCnt y}} \in ℕ$
169		pcndvds2	$⊢ (P \in ℙ \land y \in ℕ) \to \neg P ∥ (\frac{y}{P^{P pCnt y}})$
170	23 50 169	syl2anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \neg P ∥ (\frac{y}{P^{P pCnt y}})$
171	168 170	jca	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (\frac{y}{P^{P pCnt y}} \in ℕ \land \neg P ∥ (\frac{y}{P^{P pCnt y}}))$
172		pczdvds	$⊢ (P \in ℙ \land (z \in ℤ \land z \neq 0)) \to P^{P pCnt z} ∥ z$
173	23 97 108 172	syl12anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt z} ∥ z$
174	111	nnzd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt z} \in ℤ$
175		dvdsval2	$⊢ (P^{P pCnt z} \in ℤ \land P^{P pCnt z} \neq 0 \land z \in ℤ) \to (P^{P pCnt z} ∥ z \leftrightarrow \frac{z}{P^{P pCnt z}} \in ℤ)$
176	174 119 97 175	syl3anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (P^{P pCnt z} ∥ z \leftrightarrow \frac{z}{P^{P pCnt z}} \in ℤ)$
177	173 176	mpbid	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{z}{P^{P pCnt z}} \in ℤ$
178		pczndvds2	$⊢ (P \in ℙ \land (z \in ℤ \land z \neq 0)) \to \neg P ∥ (\frac{z}{P^{P pCnt z}})$
179	23 97 108 178	syl12anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \neg P ∥ (\frac{z}{P^{P pCnt z}})$
180	177 179	jca	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (\frac{z}{P^{P pCnt z}} \in ℤ \land \neg P ∥ (\frac{z}{P^{P pCnt z}}))$
181		pcdvds	$⊢ (P \in ℙ \land w \in ℕ) \to P^{P pCnt w} ∥ w$
182	23 100 181	syl2anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt w} ∥ w$
183	117	nnzd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt w} \in ℤ$
184	100	nnzd	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to w \in ℤ$
185		dvdsval2	$⊢ (P^{P pCnt w} \in ℤ \land P^{P pCnt w} \neq 0 \land w \in ℤ) \to (P^{P pCnt w} ∥ w \leftrightarrow \frac{w}{P^{P pCnt w}} \in ℤ)$
186	183 120 184 185	syl3anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (P^{P pCnt w} ∥ w \leftrightarrow \frac{w}{P^{P pCnt w}} \in ℤ)$
187	182 186	mpbid	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{w}{P^{P pCnt w}} \in ℤ$
188	100	nnred	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to w \in ℝ$
189	117	nnred	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P^{P pCnt w} \in ℝ$
190	100	nngt0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to 0 < w$
191	117	nngt0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to 0 < P^{P pCnt w}$
192	188 189 190 191	divgt0d	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to 0 < \frac{w}{P^{P pCnt w}}$
193		elnnz	$⊢ \frac{w}{P^{P pCnt w}} \in ℕ \leftrightarrow (\frac{w}{P^{P pCnt w}} \in ℤ \land 0 < \frac{w}{P^{P pCnt w}})$
194	187 192 193	sylanbrc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \frac{w}{P^{P pCnt w}} \in ℕ$
195		pcndvds2	$⊢ (P \in ℙ \land w \in ℕ) \to \neg P ∥ (\frac{w}{P^{P pCnt w}})$
196	23 100 195	syl2anc	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to \neg P ∥ (\frac{w}{P^{P pCnt w}})$
197	194 196	jca	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to (\frac{w}{P^{P pCnt w}} \in ℕ \land \neg P ∥ (\frac{w}{P^{P pCnt w}}))$
198	23 96 142 145 154 171 180 197	pcaddlem	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land ((y \in ℕ \land w \in ℕ) \land (A = \frac{x}{y} \land B = \frac{z}{w}))) \to P pCnt A \leq P pCnt (A + B)$
199	198	expr	$⊢ (((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \land (y \in ℕ \land w \in ℕ)) \to ((A = \frac{x}{y} \land B = \frac{z}{w}) \to P pCnt A \leq P pCnt (A + B))$
200	199	rexlimdvva	$⊢ ((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \to (\exists y \in ℕ \exists w \in ℕ (A = \frac{x}{y} \land B = \frac{z}{w}) \to P pCnt A \leq P pCnt (A + B))$
201	22 200	biimtrrid	$⊢ ((φ \land B \neq 0) \land (x \in ℤ \land z \in ℤ)) \to ((\exists y \in ℕ A = \frac{x}{y} \land \exists w \in ℕ B = \frac{z}{w}) \to P pCnt A \leq P pCnt (A + B))$
202	201	rexlimdvva	$⊢ (φ \land B \neq 0) \to (\exists x \in ℤ \exists z \in ℤ (\exists y \in ℕ A = \frac{x}{y} \land \exists w \in ℕ B = \frac{z}{w}) \to P pCnt A \leq P pCnt (A + B))$
203	21 202	biimtrrid	$⊢ (φ \land B \neq 0) \to ((\exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \land \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w}) \to P pCnt A \leq P pCnt (A + B))$
204	20 203	pm2.61dane	$⊢ φ \to ((\exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \land \exists z \in ℤ \exists w \in ℕ B = \frac{z}{w}) \to P pCnt A \leq P pCnt (A + B))$
205	6 8 204	mp2and	$⊢ φ \to P pCnt A \leq P pCnt (A + B)$

Metamath Proof Explorer

Theorem pcadd

Proof