Theorem pceulem

Description: Lemma for pceu . (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Hypotheses	pcval.1	$$⊢S=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel x\right\},ℝ,<\right)$$
	pcval.2	$$⊢T=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel y\right\},ℝ,<\right)$$
	pceu.3	$$⊢U=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel s\right\},ℝ,<\right)$$
	pceu.4	$$⊢V=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel t\right\},ℝ,<\right)$$
	pceu.5	$$⊢\phi \to P\in \mathbb{P}$$
	pceu.6	$$⊢\phi \to N\ne 0$$
	pceu.7	$$⊢\phi \to \left(x\in \mathbb{Z}\wedge y\in \mathbb{N}\right)$$
	pceu.8	$$⊢\phi \to N=\frac{x}{y}$$
	pceu.9	$$⊢\phi \to \left(s\in \mathbb{Z}\wedge t\in \mathbb{N}\right)$$
	pceu.10	$$⊢\phi \to N=\frac{s}{t}$$
Assertion	pceulem	$$⊢\phi \to S-T=U-V$$

Proof

Step	Hyp	Ref	Expression
1		pcval.1	$$⊢S=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel x\right\},ℝ,<\right)$$
2		pcval.2	$$⊢T=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel y\right\},ℝ,<\right)$$
3		pceu.3	$$⊢U=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel s\right\},ℝ,<\right)$$
4		pceu.4	$$⊢V=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel t\right\},ℝ,<\right)$$
5		pceu.5	$$⊢\phi \to P\in \mathbb{P}$$
6		pceu.6	$$⊢\phi \to N\ne 0$$
7		pceu.7	$$⊢\phi \to \left(x\in \mathbb{Z}\wedge y\in \mathbb{N}\right)$$
8		pceu.8	$$⊢\phi \to N=\frac{x}{y}$$
9		pceu.9	$$⊢\phi \to \left(s\in \mathbb{Z}\wedge t\in \mathbb{N}\right)$$
10		pceu.10	$$⊢\phi \to N=\frac{s}{t}$$
11	7	simprd	$$⊢\phi \to y\in \mathbb{N}$$
12	11	nncnd	$$⊢\phi \to y\in ℂ$$
13	9	simpld	$$⊢\phi \to s\in \mathbb{Z}$$
14	13	zcnd	$$⊢\phi \to s\in ℂ$$
15	12 14	mulcomd	$$⊢\phi \to ys=sy$$
16	10 8	eqtr3d	$$⊢\phi \to \frac{s}{t}=\frac{x}{y}$$
17	9	simprd	$$⊢\phi \to t\in \mathbb{N}$$
18	17	nncnd	$$⊢\phi \to t\in ℂ$$
19	7	simpld	$$⊢\phi \to x\in \mathbb{Z}$$
20	19	zcnd	$$⊢\phi \to x\in ℂ$$
21	17	nnne0d	$$⊢\phi \to t\ne 0$$
22	11	nnne0d	$$⊢\phi \to y\ne 0$$
23	14 18 20 12 21 22	divmuleqd	$$⊢\phi \to \left(\frac{s}{t}=\frac{x}{y}\leftrightarrow sy=xt\right)$$
24	16 23	mpbid	$$⊢\phi \to sy=xt$$
25	15 24	eqtrd	$$⊢\phi \to ys=xt$$
26	25	breq2d	$$⊢\phi \to \left(P^z\parallel ys\leftrightarrow P^z\parallel xt\right)$$
27	26	rabbidv	$$⊢\phi \to \left\{z\in {\mathbb{N}}_0|P^z\parallel ys\right\}=\left\{z\in {\mathbb{N}}_0|P^z\parallel xt\right\}$$
28		oveq2	$$⊢n=z\to P^n=P^z$$
29	28	breq1d	$$⊢n=z\to \left(P^n\parallel ys\leftrightarrow P^z\parallel ys\right)$$
30	29	cbvrabv	$$⊢\left\{n\in {\mathbb{N}}_0|P^n\parallel ys\right\}=\left\{z\in {\mathbb{N}}_0|P^z\parallel ys\right\}$$
31	28	breq1d	$$⊢n=z\to \left(P^n\parallel xt\leftrightarrow P^z\parallel xt\right)$$
32	31	cbvrabv	$$⊢\left\{n\in {\mathbb{N}}_0|P^n\parallel xt\right\}=\left\{z\in {\mathbb{N}}_0|P^z\parallel xt\right\}$$
33	27 30 32	3eqtr4g	$$⊢\phi \to \left\{n\in {\mathbb{N}}_0|P^n\parallel ys\right\}=\left\{n\in {\mathbb{N}}_0|P^n\parallel xt\right\}$$
34	33	supeq1d	$$⊢\phi \to sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel ys\right\},ℝ,<\right)=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel xt\right\},ℝ,<\right)$$
35	11	nnzd	$$⊢\phi \to y\in \mathbb{Z}$$
36	18 21	div0d	$$⊢\phi \to \frac{0}{t}=0$$
37		oveq1	$$⊢s=0\to \frac{s}{t}=\frac{0}{t}$$
38	37	eqeq1d	$$⊢s=0\to \left(\frac{s}{t}=0\leftrightarrow \frac{0}{t}=0\right)$$
39	36 38	syl5ibrcom	$$⊢\phi \to \left(s=0\to \frac{s}{t}=0\right)$$
40	10	eqeq1d	$$⊢\phi \to \left(N=0\leftrightarrow \frac{s}{t}=0\right)$$
41	39 40	sylibrd	$$⊢\phi \to \left(s=0\to N=0\right)$$
42	41	necon3d	$$⊢\phi \to \left(N\ne 0\to s\ne 0\right)$$
43	6 42	mpd	$$⊢\phi \to s\ne 0$$
44		eqid	$$⊢sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel ys\right\},ℝ,<\right)=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel ys\right\},ℝ,<\right)$$
45	2 3 44	pcpremul	$$⊢\left(P\in \mathbb{P}\wedge \left(y\in \mathbb{Z}\wedge y\ne 0\right)\wedge \left(s\in \mathbb{Z}\wedge s\ne 0\right)\right)\to T+U=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel ys\right\},ℝ,<\right)$$
46	5 35 22 13 43 45	syl122anc	$$⊢\phi \to T+U=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel ys\right\},ℝ,<\right)$$
47	12 22	div0d	$$⊢\phi \to \frac{0}{y}=0$$
48		oveq1	$$⊢x=0\to \frac{x}{y}=\frac{0}{y}$$
49	48	eqeq1d	$$⊢x=0\to \left(\frac{x}{y}=0\leftrightarrow \frac{0}{y}=0\right)$$
50	47 49	syl5ibrcom	$$⊢\phi \to \left(x=0\to \frac{x}{y}=0\right)$$
51	8	eqeq1d	$$⊢\phi \to \left(N=0\leftrightarrow \frac{x}{y}=0\right)$$
52	50 51	sylibrd	$$⊢\phi \to \left(x=0\to N=0\right)$$
53	52	necon3d	$$⊢\phi \to \left(N\ne 0\to x\ne 0\right)$$
54	6 53	mpd	$$⊢\phi \to x\ne 0$$
55	17	nnzd	$$⊢\phi \to t\in \mathbb{Z}$$
56		eqid	$$⊢sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel xt\right\},ℝ,<\right)=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel xt\right\},ℝ,<\right)$$
57	1 4 56	pcpremul	$$⊢\left(P\in \mathbb{P}\wedge \left(x\in \mathbb{Z}\wedge x\ne 0\right)\wedge \left(t\in \mathbb{Z}\wedge t\ne 0\right)\right)\to S+V=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel xt\right\},ℝ,<\right)$$
58	5 19 54 55 21 57	syl122anc	$$⊢\phi \to S+V=sup\left(\left\{n\in {\mathbb{N}}_0|P^n\parallel xt\right\},ℝ,<\right)$$
59	34 46 58	3eqtr4d	$$⊢\phi \to T+U=S+V$$
60		prmuz2	$$⊢P\in \mathbb{P}\to P\in {\mathbb{Z}}_{\ge 2}$$
61	5 60	syl	$$⊢\phi \to P\in {\mathbb{Z}}_{\ge 2}$$
62		eqid	$$⊢\left\{n\in {\mathbb{N}}_0|P^n\parallel y\right\}=\left\{n\in {\mathbb{N}}_0|P^n\parallel y\right\}$$
63	62 2	pcprecl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(y\in \mathbb{Z}\wedge y\ne 0\right)\right)\to \left(T\in {\mathbb{N}}_0\wedge P^T\parallel y\right)$$
64	63	simpld	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(y\in \mathbb{Z}\wedge y\ne 0\right)\right)\to T\in {\mathbb{N}}_0$$
65	61 35 22 64	syl12anc	$$⊢\phi \to T\in {\mathbb{N}}_0$$
66	65	nn0cnd	$$⊢\phi \to T\in ℂ$$
67		eqid	$$⊢\left\{n\in {\mathbb{N}}_0|P^n\parallel s\right\}=\left\{n\in {\mathbb{N}}_0|P^n\parallel s\right\}$$
68	67 3	pcprecl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(s\in \mathbb{Z}\wedge s\ne 0\right)\right)\to \left(U\in {\mathbb{N}}_0\wedge P^U\parallel s\right)$$
69	68	simpld	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(s\in \mathbb{Z}\wedge s\ne 0\right)\right)\to U\in {\mathbb{N}}_0$$
70	61 13 43 69	syl12anc	$$⊢\phi \to U\in {\mathbb{N}}_0$$
71	70	nn0cnd	$$⊢\phi \to U\in ℂ$$
72		eqid	$$⊢\left\{n\in {\mathbb{N}}_0|P^n\parallel x\right\}=\left\{n\in {\mathbb{N}}_0|P^n\parallel x\right\}$$
73	72 1	pcprecl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(x\in \mathbb{Z}\wedge x\ne 0\right)\right)\to \left(S\in {\mathbb{N}}_0\wedge P^S\parallel x\right)$$
74	73	simpld	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(x\in \mathbb{Z}\wedge x\ne 0\right)\right)\to S\in {\mathbb{N}}_0$$
75	61 19 54 74	syl12anc	$$⊢\phi \to S\in {\mathbb{N}}_0$$
76	75	nn0cnd	$$⊢\phi \to S\in ℂ$$
77		eqid	$$⊢\left\{n\in {\mathbb{N}}_0|P^n\parallel t\right\}=\left\{n\in {\mathbb{N}}_0|P^n\parallel t\right\}$$
78	77 4	pcprecl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(t\in \mathbb{Z}\wedge t\ne 0\right)\right)\to \left(V\in {\mathbb{N}}_0\wedge P^V\parallel t\right)$$
79	78	simpld	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(t\in \mathbb{Z}\wedge t\ne 0\right)\right)\to V\in {\mathbb{N}}_0$$
80	61 55 21 79	syl12anc	$$⊢\phi \to V\in {\mathbb{N}}_0$$
81	80	nn0cnd	$$⊢\phi \to V\in ℂ$$
82	66 71 76 81	addsubeq4d	$$⊢\phi \to \left(T+U=S+V\leftrightarrow S-T=U-V\right)$$
83	59 82	mpbid	$$⊢\phi \to S-T=U-V$$