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 35	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} \in ℕ$
39	38	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} \in ℤ$
40	37 34	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} \in ℕ$
41	40	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} \in ℤ$
42	23 41	zmulcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M P^{T} \in ℤ$
43	37	nncnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P \in ℂ$
44	43 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}$
45	27	simprd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} ∥ M$
46	37 28	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} \in ℕ$
47	46	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} \in ℤ$
48		dvdsmulc	$⊢ (P^{S} \in ℤ \land M \in ℤ \land P^{T} \in ℤ) \to (P^{S} ∥ M \to P^{S} P^{T} ∥ M P^{T})$
49	47 23 41 48	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})$
50	45 49	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}$
51	44 50	eqbrtrd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} ∥ M P^{T}$
52	33	simprd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} ∥ N$
53		dvdscmul	$⊢ (P^{T} \in ℤ \land N \in ℤ \land M \in ℤ) \to (P^{T} ∥ N \to M P^{T} ∥ M \cdot N)$
54	41 29 23 53	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)$
55	52 54	mpd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M P^{T} ∥ M \cdot N$
56	39 42 8 51 55	dvdstrd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} ∥ M \cdot N$
57	22 35 56	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\}$
58		oveq2	$⊢ x = n \to P^{x} = P^{n}$
59	58	breq1d	$⊢ x = n \to (P^{x} ∥ M \cdot N \leftrightarrow P^{n} ∥ M \cdot N)$
60	59	cbvrabv	$⊢ \{x \in ℕ_{0} \| P^{x} ∥ M \cdot N\} = \{n \in ℕ_{0} \| P^{n} ∥ M \cdot N\}$
61	57 60	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\}$
62		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\} ℝ <)$
63	19 20 61 62	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\} ℝ <)$
64	63 3	breqtrrdi	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T \leq U$
65	25 1	pcprendvds2	$⊢ (P \in ℤ_{\geq 2} \land (M \in ℤ \land M \neq 0)) \to \neg P ∥ (\frac{M}{P^{S}})$
66	5 23 24 65	syl12anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \neg P ∥ (\frac{M}{P^{S}})$
67	31 2	pcprendvds2	$⊢ (P \in ℤ_{\geq 2} \land (N \in ℤ \land N \neq 0)) \to \neg P ∥ (\frac{N}{P^{T}})$
68	5 29 30 67	syl12anc	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \neg P ∥ (\frac{N}{P^{T}})$
69		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}}))$
70	66 68 69	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}}))$
71		simp1	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P \in ℙ$
72	46	nnne0d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} \neq 0$
73		dvdsval2	$⊢ (P^{S} \in ℤ \land P^{S} \neq 0 \land M \in ℤ) \to (P^{S} ∥ M \leftrightarrow \frac{M}{P^{S}} \in ℤ)$
74	47 72 23 73	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 ℤ)$
75	45 74	mpbid	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \frac{M}{P^{S}} \in ℤ$
76	40	nnne0d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} \neq 0$
77		dvdsval2	$⊢ (P^{T} \in ℤ \land P^{T} \neq 0 \land N \in ℤ) \to (P^{T} ∥ N \leftrightarrow \frac{N}{P^{T}} \in ℤ)$
78	41 76 29 77	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 ℤ)$
79	52 78	mpbid	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \frac{N}{P^{T}} \in ℤ$
80		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}})))$
81	71 75 79 80	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}})))$
82	70 81	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}})$
83	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)$
84	5 8 15 83	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)$
85	84	simpld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to U \in ℕ_{0}$
86		nn0ltp1le	$⊢ (S + T \in ℕ_{0} \land U \in ℕ_{0}) \to (S + T < U \leftrightarrow S + T + 1 \leq U)$
87	35 85 86	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)$
88	37	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P \in ℤ$
89		peano2nn0	$⊢ S + T \in ℕ_{0} \to S + T + 1 \in ℕ_{0}$
90	35 89	syl	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T + 1 \in ℕ_{0}$
91		dvdsexp	$⊢ (P \in ℤ \land S + T + 1 \in ℕ_{0} \land U \in ℤ_{\geq (S + T + 1)}) \to P^{S + T + 1} ∥ P^{U}$
92	91	3expia	$⊢ (P \in ℤ \land S + T + 1 \in ℕ_{0}) \to (U \in ℤ_{\geq (S + T + 1)} \to P^{S + T + 1} ∥ P^{U})$
93	88 90 92	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})$
94	84	simprd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{U} ∥ M \cdot N$
95	37 90	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T + 1} \in ℕ$
96	95	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T + 1} \in ℤ$
97	37 85	nnexpcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{U} \in ℕ$
98	97	nnzd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{U} \in ℤ$
99		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)$
100	96 98 8 99	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)$
101	94 100	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)$
102	93 101	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)$
103	90	nn0zd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T + 1 \in ℤ$
104	85	nn0zd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to U \in ℤ$
105		eluz	$⊢ (S + T + 1 \in ℤ \land U \in ℤ) \to (U \in ℤ_{\geq (S + T + 1)} \leftrightarrow S + T + 1 \leq U)$
106	103 104 105	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)$
107	43 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$
108	23	zcnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \in ℂ$
109	29	zcnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to N \in ℂ$
110	108 109	mulcld	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to M \cdot N \in ℂ$
111	38	nncnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} \in ℂ$
112	38	nnne0d	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S + T} \neq 0$
113	110 111 112	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$
114	44	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}}$
115	46	nncnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{S} \in ℂ$
116	40	nncnd	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to P^{T} \in ℂ$
117	108 115 109 116 72 76	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}}$
118	114 117	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}})$
119	118	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}})$
120	113 119	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}})$
121	107 120	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}}))$
122	75 79	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 ℤ$
123		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}}))$
124	88 122 39 112 123	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}}))$
125	121 124	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}}))$
126	102 106 125	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}}))$
127	87 126	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}}))$
128	82 127	mtod	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to \neg S + T < U$
129	35	nn0red	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to S + T \in ℝ$
130	85	nn0red	$⊢ (P \in ℙ \land (M \in ℤ \land M \neq 0) \land (N \in ℤ \land N \neq 0)) \to U \in ℝ$
131	129 130	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))$
132	64 128 131	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