pcpremul

Description: Multiplicative property of the prime count pre-function. Note that the primality of P is essential for this property; ( 4 pCnt 2 ) = 0 but ( 4 pCnt ( 2 x. 2 ) ) = 1 =/= 2 x. ( 4 pCnt 2 ) = 0 . Since this is needed to show uniqueness for the real prime count function (over QQ ), we don't bother to define it off the primes. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Hypotheses	pcpremul.1	$⊢ S = sup (\{n \in ℕ_{0} \| P^{n} ∥ M\} ℝ <)$
	pcpremul.2	$⊢ T = sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)$
	pcpremul.3	$⊢ U = sup (\{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} ℝ <)$
Assertion	pcpremul	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T = U$

Proof

Step	Hyp	Ref	Expression
1		pcpremul.1	$⊢ S = sup (\{n \in ℕ_{0} \| P^{n} ∥ M\} ℝ <)$
2		pcpremul.2	$⊢ T = sup (\{n \in ℕ_{0} \| P^{n} ∥ N\} ℝ <)$
3		pcpremul.3	$⊢ U = sup (\{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} ℝ <)$
4		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
5	4	3ad2ant1	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P \in ℤ_{\geq 2}$
6		zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
7	6	ad2ant2r	$⊢ ((M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \cdot N \in ℤ$
8	7	3adant1	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \cdot N \in ℤ$
9		zcn	$⊢ M \in ℤ \to M \in ℂ$
10	9	anim1i	$⊢ (M \in ℤ \land M \neq 0) \to (M \in ℂ \land M \neq 0)$
11		zcn	$⊢ N \in ℤ \to N \in ℂ$
12	11	anim1i	$⊢ (N \in ℤ \land N \neq 0) \to (N \in ℂ \land N \neq 0)$
13		mulne0	$⊢ ((M \in ℂ \land M \neq 0) \land (N \in ℂ \land N \neq 0)) \to M \cdot N \neq 0$
14	10 12 13	syl2an	$⊢ ((M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \cdot N \neq 0$
15	14	3adant1	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \cdot N \neq 0$
16		eqid	$⊢ \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} = \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\}$
17	16	pclem	$⊢ (P \in ℤ_{\geq 2} \land (M \cdot N \in ℤ \land M \cdot N \neq 0)) \to (\{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} \subseteq ℤ \land \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} \neq \emptyset \land \exists x \in ℤ \forall y \in \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} y \leq x)$
18	5 8 15 17	syl12anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (\{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} \subseteq ℤ \land \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} \neq \emptyset \land \exists x \in ℤ \forall y \in \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} y \leq x)$
19	18	simp1d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} \subseteq ℤ$
20	18	simp3d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \exists x \in ℤ \forall y \in \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} y \leq x$
21		oveq2	$⊢ x = S + T \to P^{x} = P^{S + T}$
22	21	breq1d	$⊢ x = S + T \to (P^{x} ∥ M \cdot N \leftrightarrow P^{S + T} ∥ M \cdot N)$
23		simp2l	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \in ℤ$
24		simp2r	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \neq 0$
25		eqid	$⊢ \{n \in ℕ_{0} \| P^{n} ∥ M\} = \{n \in ℕ_{0} \| P^{n} ∥ M\}$
26	25 1	pcprecl	$⊢ (P \in ℤ_{\geq 2} \land (M \in ℤ \land M \neq 0)) \to (S \in ℕ_{0} \land P^{S} ∥ M)$
27	5 23 24 26	syl12anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (S \in ℕ_{0} \land P^{S} ∥ M)$
28	27	simpld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S \in ℕ_{0}$
29		simp3l	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to N \in ℤ$
30		simp3r	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to N \neq 0$
31		eqid	$⊢ \{n \in ℕ_{0} \| P^{n} ∥ N\} = \{n \in ℕ_{0} \| P^{n} ∥ N\}$
32	31 2	pcprecl	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to (T \in ℕ_{0} \land P^{T} ∥ N)$
33	5 29 30 32	syl12anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (T \in ℕ_{0} \land P^{T} ∥ N)$
34	33	simpld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to T \in ℕ_{0}$
35	28 34	nn0addcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T \in ℕ_{0}$
36		prmnn	$⊢ P \in ℙ \to P \in ℕ$
37	36	3ad2ant1	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P \in ℕ$
38	37	nncnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P \in ℂ$
39	38 34 28	expaddd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} = P^{S} P^{T}$
40	27	simprd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} ∥ M$
41	37 28	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} \in ℕ$
42	41	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} \in ℤ$
43	37 34	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} \in ℕ$
44	43	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} \in ℤ$
45		dvdsmulc	$⊢ (P^{S} \in ℤ \land M \in ℤ \land P^{T} \in ℤ) \to (P^{S} ∥ M \to P^{S} P^{T} ∥ M P^{T})$
46	42 23 44 45	syl3anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (P^{S} ∥ M \to P^{S} P^{T} ∥ M P^{T})$
47	40 46	mpd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} P^{T} ∥ M P^{T}$
48	39 47	eqbrtrd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} ∥ M P^{T}$
49	33	simprd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} ∥ N$
50		dvdscmul	$⊢ (P^{T} \in ℤ \land N \in ℤ \land M \in ℤ) \to (P^{T} ∥ N \to M P^{T} ∥ M \cdot N)$
51	44 29 23 50	syl3anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (P^{T} ∥ N \to M P^{T} ∥ M \cdot N)$
52	49 51	mpd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M P^{T} ∥ M \cdot N$
53	37 35	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} \in ℕ$
54	53	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} \in ℤ$
55	23 44	zmulcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M P^{T} \in ℤ$
56		dvdstr	$⊢ (P^{S + T} \in ℤ \land M P^{T} \in ℤ \land M \cdot N \in ℤ) \to ((P^{S + T} ∥ M P^{T} \land M P^{T} ∥ M \cdot N) \to P^{S + T} ∥ M \cdot N)$
57	54 55 8 56	syl3anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to ((P^{S + T} ∥ M P^{T} \land M P^{T} ∥ M \cdot N) \to P^{S + T} ∥ M \cdot N)$
58	48 52 57	mp2and	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} ∥ M \cdot N$
59	22 35 58	elrabd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T \in \{x \in ℕ_{0} \| P^{x} ∥ M \cdot N\}$
60		oveq2	$⊢ x = n \to P^{x} = P^{n}$
61	60	breq1d	$⊢ x = n \to (P^{x} ∥ M \cdot N \leftrightarrow P^{n} ∥ M \cdot N)$
62	61	cbvrabv	$⊢ \{x \in ℕ_{0} \| P^{x} ∥ M \cdot N\} = \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\}$
63	59 62	eleqtrdi	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T \in \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\}$
64		suprzub	$⊢ (\{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} \subseteq ℤ \land \exists x \in ℤ \forall y \in \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} y \leq x \land S + T \in \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\}) \to S + T \leq sup (\{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} ℝ <)$
65	19 20 63 64	syl3anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T \leq sup (\{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\} ℝ <)$
66	65 3	breqtrrdi	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T \leq U$
67	25 1	pcprendvds2	$⊢ (P \in ℤ_{\geq 2} \land (M \in ℤ \land M \neq 0)) \to \neg P ∥ (\frac{M}{P^{S}})$
68	5 23 24 67	syl12anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \neg P ∥ (\frac{M}{P^{S}})$
69	31 2	pcprendvds2	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \neg P ∥ (\frac{N}{P^{T}})$
70	5 29 30 69	syl12anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \neg P ∥ (\frac{N}{P^{T}})$
71		ioran	$⊢ \neg (P ∥ (\frac{M}{P^{S}}) \lor P ∥ (\frac{N}{P^{T}})) \leftrightarrow (\neg P ∥ (\frac{M}{P^{S}}) \land \neg P ∥ (\frac{N}{P^{T}}))$
72	68 70 71	sylanbrc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \neg (P ∥ (\frac{M}{P^{S}}) \lor P ∥ (\frac{N}{P^{T}}))$
73		simp1	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P \in ℙ$
74	41	nnne0d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} \neq 0$
75		dvdsval2	$⊢ (P^{S} \in ℤ \land P^{S} \neq 0 \land M \in ℤ) \to (P^{S} ∥ M \leftrightarrow \frac{M}{P^{S}} \in ℤ)$
76	42 74 23 75	syl3anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (P^{S} ∥ M \leftrightarrow \frac{M}{P^{S}} \in ℤ)$
77	40 76	mpbid	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \frac{M}{P^{S}} \in ℤ$
78	43	nnne0d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} \neq 0$
79		dvdsval2	$⊢ (P^{T} \in ℤ \land P^{T} \neq 0 \land N \in ℤ) \to (P^{T} ∥ N \leftrightarrow \frac{N}{P^{T}} \in ℤ)$
80	44 78 29 79	syl3anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (P^{T} ∥ N \leftrightarrow \frac{N}{P^{T}} \in ℤ)$
81	49 80	mpbid	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \frac{N}{P^{T}} \in ℤ$
82		euclemma	$⊢ (P \in ℙ \land \frac{M}{P^{S}} \in ℤ \land \frac{N}{P^{T}} \in ℤ) \to (P ∥ (\frac{M}{P^{S}}) (\frac{N}{P^{T}}) \leftrightarrow (P ∥ (\frac{M}{P^{S}}) \lor P ∥ (\frac{N}{P^{T}})))$
83	73 77 81 82	syl3anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (P ∥ (\frac{M}{P^{S}}) (\frac{N}{P^{T}}) \leftrightarrow (P ∥ (\frac{M}{P^{S}}) \lor P ∥ (\frac{N}{P^{T}})))$
84	72 83	mtbird	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \neg P ∥ (\frac{M}{P^{S}}) (\frac{N}{P^{T}})$
85	16 3	pcprecl	$⊢ (P \in ℤ_{\geq 2} \land (M \cdot N \in ℤ \land M \cdot N \neq 0)) \to (U \in ℕ_{0} \land P^{U} ∥ M \cdot N)$
86	5 8 15 85	syl12anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (U \in ℕ_{0} \land P^{U} ∥ M \cdot N)$
87	86	simpld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to U \in ℕ_{0}$
88		nn0ltp1le	$⊢ (S + T \in ℕ_{0} \land U \in ℕ_{0}) \to (S + T < U \leftrightarrow S + T + 1 \leq U)$
89	35 87 88	syl2anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (S + T < U \leftrightarrow S + T + 1 \leq U)$
90	37	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P \in ℤ$
91		peano2nn0	$⊢ S + T \in ℕ_{0} \to S + T + 1 \in ℕ_{0}$
92	35 91	syl	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T + 1 \in ℕ_{0}$
93		dvdsexp	$⊢ (P \in ℤ \land S + T + 1 \in ℕ_{0} \land U \in ℤ_{\geq (S + T + 1)}) \to P^{S + T + 1} ∥ P^{U}$
94	93	3expia	$⊢ (P \in ℤ \land S + T + 1 \in ℕ_{0}) \to (U \in ℤ_{\geq (S + T + 1)} \to P^{S + T + 1} ∥ P^{U})$
95	90 92 94	syl2anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (U \in ℤ_{\geq (S + T + 1)} \to P^{S + T + 1} ∥ P^{U})$
96	86	simprd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{U} ∥ M \cdot N$
97	37 92	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T + 1} \in ℕ$
98	97	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T + 1} \in ℤ$
99	37 87	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{U} \in ℕ$
100	99	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{U} \in ℤ$
101		dvdstr	$⊢ (P^{S + T + 1} \in ℤ \land P^{U} \in ℤ \land M \cdot N \in ℤ) \to ((P^{S + T + 1} ∥ P^{U} \land P^{U} ∥ M \cdot N) \to P^{S + T + 1} ∥ M \cdot N)$
102	98 100 8 101	syl3anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to ((P^{S + T + 1} ∥ P^{U} \land P^{U} ∥ M \cdot N) \to P^{S + T + 1} ∥ M \cdot N)$
103	96 102	mpan2d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (P^{S + T + 1} ∥ P^{U} \to P^{S + T + 1} ∥ M \cdot N)$
104	95 103	syld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (U \in ℤ_{\geq (S + T + 1)} \to P^{S + T + 1} ∥ M \cdot N)$
105	92	nn0zd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T + 1 \in ℤ$
106	87	nn0zd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to U \in ℤ$
107		eluz	$⊢ (S + T + 1 \in ℤ \land U \in ℤ) \to (U \in ℤ_{\geq (S + T + 1)} \leftrightarrow S + T + 1 \leq U)$
108	105 106 107	syl2anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (U \in ℤ_{\geq (S + T + 1)} \leftrightarrow S + T + 1 \leq U)$
109	38 35	expp1d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T + 1} = P^{S + T} P$
110	23	zcnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \in ℂ$
111	29	zcnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to N \in ℂ$
112	110 111	mulcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \cdot N \in ℂ$
113	53	nncnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} \in ℂ$
114	53	nnne0d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} \neq 0$
115	112 113 114	divcan2d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} (\frac{M \cdot N}{P^{S + T}}) = M \cdot N$
116	39	oveq2d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \frac{M \cdot N}{P^{S + T}} = \frac{M \cdot N}{P^{S} P^{T}}$
117	41	nncnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} \in ℂ$
118	43	nncnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} \in ℂ$
119	110 117 111 118 74 78	divmuldivd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (\frac{M}{P^{S}}) (\frac{N}{P^{T}}) = \frac{M \cdot N}{P^{S} P^{T}}$
120	116 119	eqtr4d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \frac{M \cdot N}{P^{S + T}} = (\frac{M}{P^{S}}) (\frac{N}{P^{T}})$
121	120	oveq2d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} (\frac{M \cdot N}{P^{S + T}}) = P^{S + T} (\frac{M}{P^{S}}) (\frac{N}{P^{T}})$
122	115 121	eqtr3d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \cdot N = P^{S + T} (\frac{M}{P^{S}}) (\frac{N}{P^{T}})$
123	109 122	breq12d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (P^{S + T + 1} ∥ M \cdot N \leftrightarrow P^{S + T} P ∥ P^{S + T} (\frac{M}{P^{S}}) (\frac{N}{P^{T}}))$
124	77 81	zmulcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (\frac{M}{P^{S}}) (\frac{N}{P^{T}}) \in ℤ$
125		dvdscmulr	$⊢ (P \in ℤ \land (\frac{M}{P^{S}}) (\frac{N}{P^{T}}) \in ℤ \land (P^{S + T} \in ℤ \land P^{S + T} \neq 0)) \to (P^{S + T} P ∥ P^{S + T} (\frac{M}{P^{S}}) (\frac{N}{P^{T}}) \leftrightarrow P ∥ (\frac{M}{P^{S}}) (\frac{N}{P^{T}}))$
126	90 124 54 114 125	syl112anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (P^{S + T} P ∥ P^{S + T} (\frac{M}{P^{S}}) (\frac{N}{P^{T}}) \leftrightarrow P ∥ (\frac{M}{P^{S}}) (\frac{N}{P^{T}}))$
127	123 126	bitrd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (P^{S + T + 1} ∥ M \cdot N \leftrightarrow P ∥ (\frac{M}{P^{S}}) (\frac{N}{P^{T}}))$
128	104 108 127	3imtr3d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (S + T + 1 \leq U \to P ∥ (\frac{M}{P^{S}}) (\frac{N}{P^{T}}))$
129	89 128	sylbid	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (S + T < U \to P ∥ (\frac{M}{P^{S}}) (\frac{N}{P^{T}}))$
130	84 129	mtod	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \neg S + T < U$
131	35	nn0red	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T \in ℝ$
132	87	nn0red	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to U \in ℝ$
133	131 132	eqleltd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to (S + T = U \leftrightarrow (S + T \leq U \land \neg S + T < U))$
134	66 130 133	mpbir2and	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T = U$

Metamath Proof Explorer

Theorem pcpremul

Proof