ostthlem1

Description: Lemma for ostth . If two absolute values agree on the positive integers greater than one, then they agree for all rational numbers and thus are equal as functions. (Contributed by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Hypotheses	qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	qabsabv.a	$⊢ A = AbsVal (Q)$
	ostthlem1.1	$⊢ φ \to F \in A$
	ostthlem1.2	$⊢ φ \to G \in A$
	ostthlem1.3	$⊢ (φ \land n \in ℤ_{\geq 2}) \to F (n) = G (n)$
Assertion	ostthlem1	$⊢ φ \to F = G$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
2		qabsabv.a	$⊢ A = AbsVal (Q)$
3		ostthlem1.1	$⊢ φ \to F \in A$
4		ostthlem1.2	$⊢ φ \to G \in A$
5		ostthlem1.3	$⊢ (φ \land n \in ℤ_{\geq 2}) \to F (n) = G (n)$
6	1	qrngbas	$⊢ ℚ = {Base}_{Q}$
7	2 6	abvf	$⊢ F \in A \to F : ℚ ⟶ ℝ$
8		ffn	$⊢ F : ℚ ⟶ ℝ \to F Fn ℚ$
9	3 7 8	3syl	$⊢ φ \to F Fn ℚ$
10	2 6	abvf	$⊢ G \in A \to G : ℚ ⟶ ℝ$
11		ffn	$⊢ G : ℚ ⟶ ℝ \to G Fn ℚ$
12	4 10 11	3syl	$⊢ φ \to G Fn ℚ$
13		elq	$⊢ y \in ℚ \leftrightarrow \exists k \in ℤ \exists n \in ℕ y = \frac{k}{n}$
14	1	qdrng	$⊢ Q \in DivRing$
15	14	a1i	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to Q \in DivRing$
16	3	adantr	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to F \in A$
17		zq	$⊢ k \in ℤ \to k \in ℚ$
18	17	ad2antrl	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to k \in ℚ$
19		nnq	$⊢ n \in ℕ \to n \in ℚ$
20	19	ad2antll	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to n \in ℚ$
21		nnne0	$⊢ n \in ℕ \to n \neq 0$
22	21	ad2antll	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to n \neq 0$
23	1	qrng0	$⊢ 0 = 0_{Q}$
24		eqid	$⊢ /_{r} (Q) = /_{r} (Q)$
25	2 6 23 24	abvdiv	$⊢ ((Q \in DivRing \land F \in A) \land (k \in ℚ \land n \in ℚ \land n \neq 0)) \to F (k /_{r} (Q) n) = \frac{F (k)}{F (n)}$
26	15 16 18 20 22 25	syl23anc	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to F (k /_{r} (Q) n) = \frac{F (k)}{F (n)}$
27	4	adantr	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to G \in A$
28	2 6 23 24	abvdiv	$⊢ ((Q \in DivRing \land G \in A) \land (k \in ℚ \land n \in ℚ \land n \neq 0)) \to G (k /_{r} (Q) n) = \frac{G (k)}{G (n)}$
29	15 27 18 20 22 28	syl23anc	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to G (k /_{r} (Q) n) = \frac{G (k)}{G (n)}$
30	2 23	abv0	$⊢ F \in A \to F (0) = 0$
31	3 30	syl	$⊢ φ \to F (0) = 0$
32	2 23	abv0	$⊢ G \in A \to G (0) = 0$
33	4 32	syl	$⊢ φ \to G (0) = 0$
34	31 33	eqtr4d	$⊢ φ \to F (0) = G (0)$
35		fveq2	$⊢ k = 0 \to F (k) = F (0)$
36		fveq2	$⊢ k = 0 \to G (k) = G (0)$
37	35 36	eqeq12d	$⊢ k = 0 \to (F (k) = G (k) \leftrightarrow F (0) = G (0))$
38	34 37	syl5ibrcom	$⊢ φ \to (k = 0 \to F (k) = G (k))$
39	38	adantr	$⊢ (φ \land k \in ℤ) \to (k = 0 \to F (k) = G (k))$
40	39	imp	$⊢ ((φ \land k \in ℤ) \land k = 0) \to F (k) = G (k)$
41		elnn1uz2	$⊢ n \in ℕ \leftrightarrow (n = 1 \lor n \in ℤ_{\geq 2})$
42	1	qrng1	$⊢ 1 = 1_{Q}$
43	2 42	abv1	$⊢ (Q \in DivRing \land F \in A) \to F (1) = 1$
44	14 3 43	sylancr	$⊢ φ \to F (1) = 1$
45	2 42	abv1	$⊢ (Q \in DivRing \land G \in A) \to G (1) = 1$
46	14 4 45	sylancr	$⊢ φ \to G (1) = 1$
47	44 46	eqtr4d	$⊢ φ \to F (1) = G (1)$
48		fveq2	$⊢ n = 1 \to F (n) = F (1)$
49		fveq2	$⊢ n = 1 \to G (n) = G (1)$
50	48 49	eqeq12d	$⊢ n = 1 \to (F (n) = G (n) \leftrightarrow F (1) = G (1))$
51	47 50	syl5ibrcom	$⊢ φ \to (n = 1 \to F (n) = G (n))$
52	51	imp	$⊢ (φ \land n = 1) \to F (n) = G (n)$
53	52 5	jaodan	$⊢ (φ \land (n = 1 \lor n \in ℤ_{\geq 2})) \to F (n) = G (n)$
54	41 53	sylan2b	$⊢ (φ \land n \in ℕ) \to F (n) = G (n)$
55	54	ralrimiva	$⊢ φ \to \forall n \in ℕ F (n) = G (n)$
56	55	adantr	$⊢ (φ \land k \in ℤ) \to \forall n \in ℕ F (n) = G (n)$
57		fveq2	$⊢ n = k \to F (n) = F (k)$
58		fveq2	$⊢ n = k \to G (n) = G (k)$
59	57 58	eqeq12d	$⊢ n = k \to (F (n) = G (n) \leftrightarrow F (k) = G (k))$
60	59	rspccva	$⊢ (\forall n \in ℕ F (n) = G (n) \land k \in ℕ) \to F (k) = G (k)$
61	56 60	sylan	$⊢ ((φ \land k \in ℤ) \land k \in ℕ) \to F (k) = G (k)$
62		fveq2	$⊢ n = {inv}_{g} (Q) (k) \to F (n) = F ({inv}_{g} (Q) (k))$
63		fveq2	$⊢ n = {inv}_{g} (Q) (k) \to G (n) = G ({inv}_{g} (Q) (k))$
64	62 63	eqeq12d	$⊢ n = {inv}_{g} (Q) (k) \to (F (n) = G (n) \leftrightarrow F ({inv}_{g} (Q) (k)) = G ({inv}_{g} (Q) (k)))$
65	55	ad2antrr	$⊢ ((φ \land k \in ℤ) \land - k \in ℕ) \to \forall n \in ℕ F (n) = G (n)$
66	17	adantl	$⊢ (φ \land k \in ℤ) \to k \in ℚ$
67	1	qrngneg	$⊢ k \in ℚ \to {inv}_{g} (Q) (k) = - k$
68	66 67	syl	$⊢ (φ \land k \in ℤ) \to {inv}_{g} (Q) (k) = - k$
69	68	eleq1d	$⊢ (φ \land k \in ℤ) \to ({inv}_{g} (Q) (k) \in ℕ \leftrightarrow - k \in ℕ)$
70	69	biimpar	$⊢ ((φ \land k \in ℤ) \land - k \in ℕ) \to {inv}_{g} (Q) (k) \in ℕ$
71	64 65 70	rspcdva	$⊢ ((φ \land k \in ℤ) \land - k \in ℕ) \to F ({inv}_{g} (Q) (k)) = G ({inv}_{g} (Q) (k))$
72	3	ad2antrr	$⊢ ((φ \land k \in ℤ) \land - k \in ℕ) \to F \in A$
73	17	ad2antlr	$⊢ ((φ \land k \in ℤ) \land - k \in ℕ) \to k \in ℚ$
74		eqid	$⊢ {inv}_{g} (Q) = {inv}_{g} (Q)$
75	2 6 74	abvneg	$⊢ (F \in A \land k \in ℚ) \to F ({inv}_{g} (Q) (k)) = F (k)$
76	72 73 75	syl2anc	$⊢ ((φ \land k \in ℤ) \land - k \in ℕ) \to F ({inv}_{g} (Q) (k)) = F (k)$
77	4	ad2antrr	$⊢ ((φ \land k \in ℤ) \land - k \in ℕ) \to G \in A$
78	2 6 74	abvneg	$⊢ (G \in A \land k \in ℚ) \to G ({inv}_{g} (Q) (k)) = G (k)$
79	77 73 78	syl2anc	$⊢ ((φ \land k \in ℤ) \land - k \in ℕ) \to G ({inv}_{g} (Q) (k)) = G (k)$
80	71 76 79	3eqtr3d	$⊢ ((φ \land k \in ℤ) \land - k \in ℕ) \to F (k) = G (k)$
81		elz	$⊢ k \in ℤ \leftrightarrow (k \in ℝ \land (k = 0 \lor k \in ℕ \lor - k \in ℕ))$
82	81	simprbi	$⊢ k \in ℤ \to (k = 0 \lor k \in ℕ \lor - k \in ℕ)$
83	82	adantl	$⊢ (φ \land k \in ℤ) \to (k = 0 \lor k \in ℕ \lor - k \in ℕ)$
84	40 61 80 83	mpjao3dan	$⊢ (φ \land k \in ℤ) \to F (k) = G (k)$
85	84	adantrr	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to F (k) = G (k)$
86	54	adantrl	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to F (n) = G (n)$
87	85 86	oveq12d	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to \frac{F (k)}{F (n)} = \frac{G (k)}{G (n)}$
88	29 87	eqtr4d	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to G (k /_{r} (Q) n) = \frac{F (k)}{F (n)}$
89	26 88	eqtr4d	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to F (k /_{r} (Q) n) = G (k /_{r} (Q) n)$
90	1	qrngdiv	$⊢ (k \in ℚ \land n \in ℚ \land n \neq 0) \to k /_{r} (Q) n = \frac{k}{n}$
91	18 20 22 90	syl3anc	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to k /_{r} (Q) n = \frac{k}{n}$
92	91	fveq2d	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to F (k /_{r} (Q) n) = F (\frac{k}{n})$
93	91	fveq2d	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to G (k /_{r} (Q) n) = G (\frac{k}{n})$
94	89 92 93	3eqtr3d	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to F (\frac{k}{n}) = G (\frac{k}{n})$
95		fveq2	$⊢ y = \frac{k}{n} \to F (y) = F (\frac{k}{n})$
96		fveq2	$⊢ y = \frac{k}{n} \to G (y) = G (\frac{k}{n})$
97	95 96	eqeq12d	$⊢ y = \frac{k}{n} \to (F (y) = G (y) \leftrightarrow F (\frac{k}{n}) = G (\frac{k}{n}))$
98	94 97	syl5ibrcom	$⊢ (φ \land (k \in ℤ \land n \in ℕ)) \to (y = \frac{k}{n} \to F (y) = G (y))$
99	98	rexlimdvva	$⊢ φ \to (\exists k \in ℤ \exists n \in ℕ y = \frac{k}{n} \to F (y) = G (y))$
100	13 99	biimtrid	$⊢ φ \to (y \in ℚ \to F (y) = G (y))$
101	100	imp	$⊢ (φ \land y \in ℚ) \to F (y) = G (y)$
102	9 12 101	eqfnfvd	$⊢ φ \to F = G$

Metamath Proof Explorer

Theorem ostthlem1

Proof