pceulem

	Ref	Expression
Hypotheses	pcval.1	$⊢ S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <)$
	pcval.2	$⊢ T = sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)$
	pceu.3	$⊢ U = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <)$
	pceu.4	$⊢ V = sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)$
	pceu.5	$⊢ φ \to P \in ℙ$
	pceu.6	$⊢ φ \to N \neq 0$
	pceu.7	$⊢ φ \to (x \in ℤ \land y \in ℕ)$
	pceu.8	$⊢ φ \to N = \frac{x}{y}$
	pceu.9	$⊢ φ \to (s \in ℤ \land t \in ℕ)$
	pceu.10	$⊢ φ \to N = \frac{s}{t}$
Assertion	pceulem	$⊢ φ \to S - T = U - V$

Proof

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

Metamath Proof Explorer

Theorem pceulem

Proof