Metamath Proof Explorer

Theorem ostth1

Description: - Lemma for ostth : trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If F is equal to 1 on the primes, then by complete induction and the multiplicative property abvmul of the absolute value, F is equal to 1 on all the integers, and ostthlem1 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses qrng.q 
|- Q = ( CCfld |`s QQ )
qabsabv.a 
|- A = ( AbsVal ` Q )
padic.j 
|- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
ostth.k 
|- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )
ostth.1 
|- ( ph -> F e. A )
ostth1.2 
|- ( ph -> A. n e. NN -. 1 < ( F ` n ) )
ostth1.3 
|- ( ph -> A. n e. Prime -. ( F ` n ) < 1 )
Assertion ostth1 
|- ( ph -> F = K )

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qabsabv.a 
 |-  A = ( AbsVal ` Q )
3 padic.j 
 |-  J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
4 ostth.k 
 |-  K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )
5 ostth.1 
 |-  ( ph -> F e. A )
6 ostth1.2 
 |-  ( ph -> A. n e. NN -. 1 < ( F ` n ) )
7 ostth1.3 
 |-  ( ph -> A. n e. Prime -. ( F ` n ) < 1 )
8 1 qdrng 
 |-  Q e. DivRing
9 1 qrngbas 
 |-  QQ = ( Base ` Q )
10 1 qrng0 
 |-  0 = ( 0g ` Q )
11 2 9 10 4 abvtriv 
 |-  ( Q e. DivRing -> K e. A )
12 8 11 mp1i 
 |-  ( ph -> K e. A )
13 7 r19.21bi 
 |-  ( ( ph /\ n e. Prime ) -> -. ( F ` n ) < 1 )
14 prmnn 
 |-  ( n e. Prime -> n e. NN )
15 6 r19.21bi 
 |-  ( ( ph /\ n e. NN ) -> -. 1 < ( F ` n ) )
16 14 15 sylan2 
 |-  ( ( ph /\ n e. Prime ) -> -. 1 < ( F ` n ) )
17 nnq 
 |-  ( n e. NN -> n e. QQ )
18 14 17 syl 
 |-  ( n e. Prime -> n e. QQ )
19 2 9 abvcl 
 |-  ( ( F e. A /\ n e. QQ ) -> ( F ` n ) e. RR )
20 5 18 19 syl2an 
 |-  ( ( ph /\ n e. Prime ) -> ( F ` n ) e. RR )
21 1re 
 |-  1 e. RR
22 lttri3 
 |-  ( ( ( F ` n ) e. RR /\ 1 e. RR ) -> ( ( F ` n ) = 1 <-> ( -. ( F ` n ) < 1 /\ -. 1 < ( F ` n ) ) ) )
23 20 21 22 sylancl 
 |-  ( ( ph /\ n e. Prime ) -> ( ( F ` n ) = 1 <-> ( -. ( F ` n ) < 1 /\ -. 1 < ( F ` n ) ) ) )
24 13 16 23 mpbir2and 
 |-  ( ( ph /\ n e. Prime ) -> ( F ` n ) = 1 )
25 14 adantl 
 |-  ( ( ph /\ n e. Prime ) -> n e. NN )
26 eqeq1 
 |-  ( x = n -> ( x = 0 <-> n = 0 ) )
27 26 ifbid 
 |-  ( x = n -> if ( x = 0 , 0 , 1 ) = if ( n = 0 , 0 , 1 ) )
28 c0ex 
 |-  0 e. _V
29 1ex 
 |-  1 e. _V
30 28 29 ifex 
 |-  if ( n = 0 , 0 , 1 ) e. _V
31 27 4 30 fvmpt 
 |-  ( n e. QQ -> ( K ` n ) = if ( n = 0 , 0 , 1 ) )
32 17 31 syl 
 |-  ( n e. NN -> ( K ` n ) = if ( n = 0 , 0 , 1 ) )
33 nnne0 
 |-  ( n e. NN -> n =/= 0 )
34 33 neneqd 
 |-  ( n e. NN -> -. n = 0 )
35 34 iffalsed 
 |-  ( n e. NN -> if ( n = 0 , 0 , 1 ) = 1 )
36 32 35 eqtrd 
 |-  ( n e. NN -> ( K ` n ) = 1 )
37 25 36 syl 
 |-  ( ( ph /\ n e. Prime ) -> ( K ` n ) = 1 )
38 24 37 eqtr4d 
 |-  ( ( ph /\ n e. Prime ) -> ( F ` n ) = ( K ` n ) )
39 1 2 5 12 38 ostthlem2 
 |-  ( ph -> F = K )