Metamath Proof Explorer

Theorem 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 ⊢ 𝑄 = ( ℂfld ↾s ℚ )
qabsabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
ostthlem1.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
ostthlem1.2 ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
ostthlem1.3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
Assertion ostthlem1 ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 qrng.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
2 qabsabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3 ostthlem1.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
4 ostthlem1.2 ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
5 ostthlem1.3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
6 1 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
7 2 6 abvf ⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : ℚ ⟶ ℝ )
8 ffn ⊢ ( 𝐹 : ℚ ⟶ ℝ → 𝐹 Fn ℚ )
9 3 7 8 3syl ⊢ ( 𝜑 → 𝐹 Fn ℚ )
10 2 6 abvf ⊢ ( 𝐺 ∈ 𝐴 → 𝐺 : ℚ ⟶ ℝ )
11 ffn ⊢ ( 𝐺 : ℚ ⟶ ℝ → 𝐺 Fn ℚ )
12 4 10 11 3syl ⊢ ( 𝜑 → 𝐺 Fn ℚ )
13 elq ⊢ ( 𝑦 ∈ ℚ ↔ ∃ 𝑘 ∈ ℤ ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝑘 / 𝑛 ) )
14 1 qdrng ⊢ 𝑄 ∈ DivRing
15 14 a1i ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → 𝑄 ∈ DivRing )
16 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → 𝐹 ∈ 𝐴 )
17 zq ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℚ )
18 17 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → 𝑘 ∈ ℚ )
19 nnq ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℚ )
20 19 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → 𝑛 ∈ ℚ )
21 nnne0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
22 21 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → 𝑛 ≠ 0 )
23 1 qrng0 ⊢ 0 = ( 0g ‘ 𝑄 )
24 eqid ⊢ ( /r ‘ 𝑄 ) = ( /r ‘ 𝑄 )
25 2 6 23 24 abvdiv ⊢ ( ( ( 𝑄 ∈ DivRing ∧ 𝐹 ∈ 𝐴 ) ∧ ( 𝑘 ∈ ℚ ∧ 𝑛 ∈ ℚ ∧ 𝑛 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) ) = ( ( 𝐹 ‘ 𝑘 ) / ( 𝐹 ‘ 𝑛 ) ) )
26 15 16 18 20 22 25 syl23anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐹 ‘ ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) ) = ( ( 𝐹 ‘ 𝑘 ) / ( 𝐹 ‘ 𝑛 ) ) )
27 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → 𝐺 ∈ 𝐴 )
28 2 6 23 24 abvdiv ⊢ ( ( ( 𝑄 ∈ DivRing ∧ 𝐺 ∈ 𝐴 ) ∧ ( 𝑘 ∈ ℚ ∧ 𝑛 ∈ ℚ ∧ 𝑛 ≠ 0 ) ) → ( 𝐺 ‘ ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) ) = ( ( 𝐺 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑛 ) ) )
29 15 27 18 20 22 28 syl23anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐺 ‘ ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) ) = ( ( 𝐺 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑛 ) ) )
30 2 23 abv0 ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 0 ) = 0 )
31 3 30 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 0 )
32 2 23 abv0 ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ‘ 0 ) = 0 )
33 4 32 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = 0 )
34 31 33 eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) )
35 fveq2 ⊢ ( 𝑘 = 0 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 0 ) )
36 fveq2 ⊢ ( 𝑘 = 0 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 0 ) )
37 35 36 eqeq12d ⊢ ( 𝑘 = 0 → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ) )
38 34 37 syl5ibrcom ⊢ ( 𝜑 → ( 𝑘 = 0 → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 = 0 → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) )
40 39 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑘 = 0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
41 elnn1uz2 ⊢ ( 𝑛 ∈ ℕ ↔ ( 𝑛 = 1 ∨ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) )
42 1 qrng1 ⊢ 1 = ( 1r ‘ 𝑄 )
43 2 42 abv1 ⊢ ( ( 𝑄 ∈ DivRing ∧ 𝐹 ∈ 𝐴 ) → ( 𝐹 ‘ 1 ) = 1 )
44 14 3 43 sylancr ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = 1 )
45 2 42 abv1 ⊢ ( ( 𝑄 ∈ DivRing ∧ 𝐺 ∈ 𝐴 ) → ( 𝐺 ‘ 1 ) = 1 )
46 14 4 45 sylancr ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = 1 )
47 44 46 eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
48 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) )
49 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 1 ) )
50 48 49 eqeq12d ⊢ ( 𝑛 = 1 → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )
51 47 50 syl5ibrcom ⊢ ( 𝜑 → ( 𝑛 = 1 → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) ) )
52 51 imp ⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
53 52 5 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑛 = 1 ∨ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
54 41 53 sylan2b ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
55 54 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
57 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
58 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
59 57 58 eqeq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) )
60 59 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
61 56 60 sylan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
62 fveq2 ⊢ ( 𝑛 = ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) )
63 fveq2 ⊢ ( 𝑛 = ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) )
64 62 63 eqeq12d ⊢ ( 𝑛 = ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) ↔ ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) = ( 𝐺 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) ) )
65 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ - 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
66 17 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℚ )
67 1 qrngneg ⊢ ( 𝑘 ∈ ℚ → ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) = - 𝑘 )
68 66 67 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) = - 𝑘 )
69 68 eleq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ∈ ℕ ↔ - 𝑘 ∈ ℕ ) )
70 69 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ - 𝑘 ∈ ℕ ) → ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ∈ ℕ )
71 64 65 70 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ - 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) = ( 𝐺 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) )
72 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ - 𝑘 ∈ ℕ ) → 𝐹 ∈ 𝐴 )
73 17 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ - 𝑘 ∈ ℕ ) → 𝑘 ∈ ℚ )
74 eqid ⊢ ( invg ‘ 𝑄 ) = ( invg ‘ 𝑄 )
75 2 6 74 abvneg ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑘 ∈ ℚ ) → ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
76 72 73 75 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ - 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
77 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ - 𝑘 ∈ ℕ ) → 𝐺 ∈ 𝐴 )
78 2 6 74 abvneg ⊢ ( ( 𝐺 ∈ 𝐴 ∧ 𝑘 ∈ ℚ ) → ( 𝐺 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) )
79 77 73 78 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ - 𝑘 ∈ ℕ ) → ( 𝐺 ‘ ( ( invg ‘ 𝑄 ) ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) )
80 71 76 79 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ - 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
81 elz ⊢ ( 𝑘 ∈ ℤ ↔ ( 𝑘 ∈ ℝ ∧ ( 𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ - 𝑘 ∈ ℕ ) ) )
82 81 simprbi ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ - 𝑘 ∈ ℕ ) )
83 82 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ - 𝑘 ∈ ℕ ) )
84 40 61 80 83 mpjao3dan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
85 84 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
86 54 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
87 85 86 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑘 ) / ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝐺 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑛 ) ) )
88 29 87 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐺 ‘ ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) ) = ( ( 𝐹 ‘ 𝑘 ) / ( 𝐹 ‘ 𝑛 ) ) )
89 26 88 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐹 ‘ ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) ) = ( 𝐺 ‘ ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) ) )
90 1 qrngdiv ⊢ ( ( 𝑘 ∈ ℚ ∧ 𝑛 ∈ ℚ ∧ 𝑛 ≠ 0 ) → ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) = ( 𝑘 / 𝑛 ) )
91 18 20 22 90 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) = ( 𝑘 / 𝑛 ) )
92 91 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐹 ‘ ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) ) = ( 𝐹 ‘ ( 𝑘 / 𝑛 ) ) )
93 91 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐺 ‘ ( 𝑘 ( /r ‘ 𝑄 ) 𝑛 ) ) = ( 𝐺 ‘ ( 𝑘 / 𝑛 ) ) )
94 89 92 93 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐹 ‘ ( 𝑘 / 𝑛 ) ) = ( 𝐺 ‘ ( 𝑘 / 𝑛 ) ) )
95 fveq2 ⊢ ( 𝑦 = ( 𝑘 / 𝑛 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑘 / 𝑛 ) ) )
96 fveq2 ⊢ ( 𝑦 = ( 𝑘 / 𝑛 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑘 / 𝑛 ) ) )
97 95 96 eqeq12d ⊢ ( 𝑦 = ( 𝑘 / 𝑛 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐹 ‘ ( 𝑘 / 𝑛 ) ) = ( 𝐺 ‘ ( 𝑘 / 𝑛 ) ) ) )
98 94 97 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) ) → ( 𝑦 = ( 𝑘 / 𝑛 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
99 98 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ∃ 𝑛 ∈ ℕ 𝑦 = ( 𝑘 / 𝑛 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
100 13 99 syl5bi ⊢ ( 𝜑 → ( 𝑦 ∈ ℚ → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
101 100 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℚ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
102 9 12 101 eqfnfvd ⊢ ( 𝜑 → 𝐹 = 𝐺 )