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 
|- Q = ( CCfld |`s QQ )
qabsabv.a 
|- A = ( AbsVal ` Q )
ostthlem1.1 
|- ( ph -> F e. A )
ostthlem1.2 
|- ( ph -> G e. A )
ostthlem1.3 
|- ( ( ph /\ n e. ( ZZ>= ` 2 ) ) -> ( F ` n ) = ( G ` n ) )
Assertion ostthlem1 
|- ( ph -> F = G )

Proof

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