pceu

Description: Uniqueness for the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Hypotheses	pcval.1	$⊢ S = sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <)$
	pcval.2	$⊢ T = sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <)$
Assertion	pceu	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to \exists! z \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T)$

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		simprl	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to N \in ℚ$
4		elq	$⊢ N \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ N = \frac{x}{y}$
5	3 4	sylib	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to \exists x \in ℤ \exists y \in ℕ N = \frac{x}{y}$
6		ovex	$⊢ S - T \in V$
7		biidd	$⊢ z = S - T \to (N = \frac{x}{y} \leftrightarrow N = \frac{x}{y})$
8	6 7	ceqsexv	$⊢ \exists z (z = S - T \land N = \frac{x}{y}) \leftrightarrow N = \frac{x}{y}$
9		exancom	$⊢ \exists z (z = S - T \land N = \frac{x}{y}) \leftrightarrow \exists z (N = \frac{x}{y} \land z = S - T)$
10	8 9	bitr3i	$⊢ N = \frac{x}{y} \leftrightarrow \exists z (N = \frac{x}{y} \land z = S - T)$
11	10	rexbii	$⊢ \exists y \in ℕ N = \frac{x}{y} \leftrightarrow \exists y \in ℕ \exists z (N = \frac{x}{y} \land z = S - T)$
12		rexcom4	$⊢ \exists y \in ℕ \exists z (N = \frac{x}{y} \land z = S - T) \leftrightarrow \exists z \exists y \in ℕ (N = \frac{x}{y} \land z = S - T)$
13	11 12	bitri	$⊢ \exists y \in ℕ N = \frac{x}{y} \leftrightarrow \exists z \exists y \in ℕ (N = \frac{x}{y} \land z = S - T)$
14	13	rexbii	$⊢ \exists x \in ℤ \exists y \in ℕ N = \frac{x}{y} \leftrightarrow \exists x \in ℤ \exists z \exists y \in ℕ (N = \frac{x}{y} \land z = S - T)$
15		rexcom4	$⊢ \exists x \in ℤ \exists z \exists y \in ℕ (N = \frac{x}{y} \land z = S - T) \leftrightarrow \exists z \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T)$
16	14 15	bitri	$⊢ \exists x \in ℤ \exists y \in ℕ N = \frac{x}{y} \leftrightarrow \exists z \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T)$
17	5 16	sylib	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to \exists z \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T)$
18		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <)$
19		eqid	$⊢ sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)$
20		simp11l	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to P \in ℙ$
21		simp11r	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to N \neq 0$
22		simp12	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to (x \in ℤ \land y \in ℕ)$
23		simp13l	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to N = \frac{x}{y}$
24		simp2	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to (s \in ℤ \land t \in ℕ)$
25		simp3l	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to N = \frac{s}{t}$
26	1 2 18 19 20 21 22 23 24 25	pceulem	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to S - T = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)$
27		simp13r	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to z = S - T$
28		simp3r	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)$
29	26 27 28	3eqtr4d	$⊢ (((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \land (s \in ℤ \land t \in ℕ) \land (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to z = w$
30	29	3exp	$⊢ ((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \to ((s \in ℤ \land t \in ℕ) \to ((N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)) \to z = w))$
31	30	rexlimdvv	$⊢ ((P \in ℙ \land N \neq 0) \land (x \in ℤ \land y \in ℕ) \land (N = \frac{x}{y} \land z = S - T)) \to (\exists s \in ℤ \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)) \to z = w)$
32	31	3exp	$⊢ (P \in ℙ \land N \neq 0) \to ((x \in ℤ \land y \in ℕ) \to ((N = \frac{x}{y} \land z = S - T) \to (\exists s \in ℤ \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)) \to z = w)))$
33	32	adantrl	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to ((x \in ℤ \land y \in ℕ) \to ((N = \frac{x}{y} \land z = S - T) \to (\exists s \in ℤ \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)) \to z = w)))$
34	33	rexlimdvv	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to (\exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T) \to (\exists s \in ℤ \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)) \to z = w))$
35	34	impd	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to ((\exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T) \land \exists s \in ℤ \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to z = w)$
36	35	alrimivv	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to \forall z \forall w ((\exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T) \land \exists s \in ℤ \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to z = w)$
37		eqeq1	$⊢ z = w \to (z = S - T \leftrightarrow w = S - T)$
38	37	anbi2d	$⊢ z = w \to ((N = \frac{x}{y} \land z = S - T) \leftrightarrow (N = \frac{x}{y} \land w = S - T))$
39	38	2rexbidv	$⊢ z = w \to (\exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T) \leftrightarrow \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land w = S - T))$
40		oveq1	$⊢ x = s \to \frac{x}{y} = \frac{s}{y}$
41	40	eqeq2d	$⊢ x = s \to (N = \frac{x}{y} \leftrightarrow N = \frac{s}{y})$
42		breq2	$⊢ x = s \to (P^{n} ∥ x \leftrightarrow P^{n} ∥ s)$
43	42	rabbidv	$⊢ x = s \to \{n \in ℕ_{0} \| P^{n} ∥ x\} = \{n \in ℕ_{0} \| P^{n} ∥ s\}$
44	43	supeq1d	$⊢ x = s \to sup (\{n \in ℕ_{0} \| P^{n} ∥ x\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <)$
45	1 44	syl5eq	$⊢ x = s \to S = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <)$
46	45	oveq1d	$⊢ x = s \to S - T = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - T$
47	46	eqeq2d	$⊢ x = s \to (w = S - T \leftrightarrow w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - T)$
48	41 47	anbi12d	$⊢ x = s \to ((N = \frac{x}{y} \land w = S - T) \leftrightarrow (N = \frac{s}{y} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - T))$
49	48	rexbidv	$⊢ x = s \to (\exists y \in ℕ (N = \frac{x}{y} \land w = S - T) \leftrightarrow \exists y \in ℕ (N = \frac{s}{y} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - T))$
50		oveq2	$⊢ y = t \to \frac{s}{y} = \frac{s}{t}$
51	50	eqeq2d	$⊢ y = t \to (N = \frac{s}{y} \leftrightarrow N = \frac{s}{t})$
52		breq2	$⊢ y = t \to (P^{n} ∥ y \leftrightarrow P^{n} ∥ t)$
53	52	rabbidv	$⊢ y = t \to \{n \in ℕ_{0} \| P^{n} ∥ y\} = \{n \in ℕ_{0} \| P^{n} ∥ t\}$
54	53	supeq1d	$⊢ y = t \to sup (\{n \in ℕ_{0} \| P^{n} ∥ y\} ℝ <) = sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)$
55	2 54	syl5eq	$⊢ y = t \to T = sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)$
56	55	oveq2d	$⊢ y = t \to sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - T = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)$
57	56	eqeq2d	$⊢ y = t \to (w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - T \leftrightarrow w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))$
58	51 57	anbi12d	$⊢ y = t \to ((N = \frac{s}{y} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - T) \leftrightarrow (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)))$
59	58	cbvrexvw	$⊢ \exists y \in ℕ (N = \frac{s}{y} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - T) \leftrightarrow \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))$
60	49 59	bitrdi	$⊢ x = s \to (\exists y \in ℕ (N = \frac{x}{y} \land w = S - T) \leftrightarrow \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)))$
61	60	cbvrexvw	$⊢ \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land w = S - T) \leftrightarrow \exists s \in ℤ \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))$
62	39 61	bitrdi	$⊢ z = w \to (\exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T) \leftrightarrow \exists s \in ℤ \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <)))$
63	62	eu4	$⊢ \exists! z \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T) \leftrightarrow (\exists z \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T) \land \forall z \forall w ((\exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T) \land \exists s \in ℤ \exists t \in ℕ (N = \frac{s}{t} \land w = sup (\{n \in ℕ_{0} \| P^{n} ∥ s\} ℝ <) - sup (\{n \in ℕ_{0} \| P^{n} ∥ t\} ℝ <))) \to z = w))$
64	17 36 63	sylanbrc	$⊢ (P \in ℙ \land (N \in ℚ \land N \neq 0)) \to \exists! z \exists x \in ℤ \exists y \in ℕ (N = \frac{x}{y} \land z = S - T)$

Metamath Proof Explorer

Theorem pceu

Proof