Metamath Proof Explorer

Theorem ostth2lem4

Description: Lemma for ostth2 . (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses qrng.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
qabsabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
padic.j ⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
ostth.k ⊢ 𝐾 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , 1 ) )
ostth.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
ostth2.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
ostth2.3 ⊢ ( 𝜑 → 1 < ( 𝐹 ‘ 𝑁 ) )
ostth2.4 ⊢ 𝑅 = ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) )
ostth2.5 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
ostth2.6 ⊢ 𝑆 = ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) )
ostth2.7 ⊢ 𝑇 = if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) )
ostth2.8 ⊢ 𝑈 = ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) )
Assertion ostth2lem4 ( 𝜑 → ( 1 < ( 𝐹 ‘ 𝑀 ) ∧ 𝑅 ≤ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 qrng.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
2 qabsabv.a ⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3 padic.j ⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
4 ostth.k ⊢ 𝐾 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , 1 ) )
5 ostth.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
6 ostth2.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
7 ostth2.3 ⊢ ( 𝜑 → 1 < ( 𝐹 ‘ 𝑁 ) )
8 ostth2.4 ⊢ 𝑅 = ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) )
9 ostth2.5 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
10 ostth2.6 ⊢ 𝑆 = ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) )
11 ostth2.7 ⊢ 𝑇 = if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) )
12 ostth2.8 ⊢ 𝑈 = ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) )
13 1re ⊢ 1 ∈ ℝ
14 eluz2b2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
15 6 14 sylib ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
16 15 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
17 nnq ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℚ )
18 16 17 syl ⊢ ( 𝜑 → 𝑁 ∈ ℚ )
19 1 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
20 2 19 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
21 5 18 20 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
22 ltnle ⊢ ( ( 1 ∈ ℝ ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℝ ) → ( 1 < ( 𝐹 ‘ 𝑁 ) ↔ ¬ ( 𝐹 ‘ 𝑁 ) ≤ 1 ) )
23 13 21 22 sylancr ⊢ ( 𝜑 → ( 1 < ( 𝐹 ‘ 𝑁 ) ↔ ¬ ( 𝐹 ‘ 𝑁 ) ≤ 1 ) )
24 7 23 mpbid ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑁 ) ≤ 1 )
25 eluz2b2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑀 ∈ ℕ ∧ 1 < 𝑀 ) )
26 9 25 sylib ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 1 < 𝑀 ) )
27 26 simpld ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
28 nnq ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℚ )
29 27 28 syl ⊢ ( 𝜑 → 𝑀 ∈ ℚ )
30 2 19 abvcl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ) → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
31 5 29 30 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
32 ifcl ⊢ ( ( 1 ∈ ℝ ∧ ( 𝐹 ‘ 𝑀 ) ∈ ℝ ) → if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) ∈ ℝ )
33 13 31 32 sylancr ⊢ ( 𝜑 → if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) ∈ ℝ )
34 11 33 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
35 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
36 13 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
37 0lt1 ⊢ 0 < 1
38 37 a1i ⊢ ( 𝜑 → 0 < 1 )
39 max2 ⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ ∧ 1 ∈ ℝ ) → 1 ≤ if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) )
40 31 13 39 sylancl ⊢ ( 𝜑 → 1 ≤ if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) )
41 40 11 breqtrrdi ⊢ ( 𝜑 → 1 ≤ 𝑇 )
42 35 36 34 38 41 ltletrd ⊢ ( 𝜑 → 0 < 𝑇 )
43 34 42 elrpd ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
44 16 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
45 44 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
46 27 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
47 26 simprd ⊢ ( 𝜑 → 1 < 𝑀 )
48 46 47 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑀 ) ∈ ℝ+ )
49 45 48 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) ) ∈ ℝ )
50 12 49 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
51 43 50 rpcxpcld ⊢ ( 𝜑 → ( 𝑇 ↑𝑐 𝑈 ) ∈ ℝ+ )
52 21 51 rerpdivcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) / ( 𝑇 ↑𝑐 𝑈 ) ) ∈ ℝ )
53 46 34 remulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑇 ) ∈ ℝ )
54 peano2re ⊢ ( 𝑈 ∈ ℝ → ( 𝑈 + 1 ) ∈ ℝ )
55 50 54 syl ⊢ ( 𝜑 → ( 𝑈 + 1 ) ∈ ℝ )
56 53 55 remulcld ⊢ ( 𝜑 → ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ∈ ℝ )
57 1 2 3 4 5 6 7 8 9 10 11 12 ostth2lem3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑁 ) / ( 𝑇 ↑𝑐 𝑈 ) ) ↑ 𝑛 ) ≤ ( 𝑛 · ( ( 𝑀 · 𝑇 ) · ( 𝑈 + 1 ) ) ) )
58 52 56 57 ostth2lem1 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) / ( 𝑇 ↑𝑐 𝑈 ) ) ≤ 1 )
59 21 36 51 ledivmuld ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑁 ) / ( 𝑇 ↑𝑐 𝑈 ) ) ≤ 1 ↔ ( 𝐹 ‘ 𝑁 ) ≤ ( ( 𝑇 ↑𝑐 𝑈 ) · 1 ) ) )
60 58 59 mpbid ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ ( ( 𝑇 ↑𝑐 𝑈 ) · 1 ) )
61 51 rpcnd ⊢ ( 𝜑 → ( 𝑇 ↑𝑐 𝑈 ) ∈ ℂ )
62 61 mulridd ⊢ ( 𝜑 → ( ( 𝑇 ↑𝑐 𝑈 ) · 1 ) = ( 𝑇 ↑𝑐 𝑈 ) )
63 60 62 breqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ ( 𝑇 ↑𝑐 𝑈 ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑀 ) ≤ 1 ) → ( 𝐹 ‘ 𝑁 ) ≤ ( 𝑇 ↑𝑐 𝑈 ) )
65 iftrue ⊢ ( ( 𝐹 ‘ 𝑀 ) ≤ 1 → if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) = 1 )
66 11 65 eqtrid ⊢ ( ( 𝐹 ‘ 𝑀 ) ≤ 1 → 𝑇 = 1 )
67 66 oveq1d ⊢ ( ( 𝐹 ‘ 𝑀 ) ≤ 1 → ( 𝑇 ↑𝑐 𝑈 ) = ( 1 ↑𝑐 𝑈 ) )
68 50 recnd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
69 68 1cxpd ⊢ ( 𝜑 → ( 1 ↑𝑐 𝑈 ) = 1 )
70 67 69 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑀 ) ≤ 1 ) → ( 𝑇 ↑𝑐 𝑈 ) = 1 )
71 64 70 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑀 ) ≤ 1 ) → ( 𝐹 ‘ 𝑁 ) ≤ 1 )
72 24 71 mtand ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑀 ) ≤ 1 )
73 ltnle ⊢ ( ( 1 ∈ ℝ ∧ ( 𝐹 ‘ 𝑀 ) ∈ ℝ ) → ( 1 < ( 𝐹 ‘ 𝑀 ) ↔ ¬ ( 𝐹 ‘ 𝑀 ) ≤ 1 ) )
74 13 31 73 sylancr ⊢ ( 𝜑 → ( 1 < ( 𝐹 ‘ 𝑀 ) ↔ ¬ ( 𝐹 ‘ 𝑀 ) ≤ 1 ) )
75 72 74 mpbird ⊢ ( 𝜑 → 1 < ( 𝐹 ‘ 𝑀 ) )
76 35 36 21 38 7 lttrd ⊢ ( 𝜑 → 0 < ( 𝐹 ‘ 𝑁 ) )
77 21 76 elrpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ+ )
78 77 reeflogd ⊢ ( 𝜑 → ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( 𝐹 ‘ 𝑁 ) )
79 iffalse ⊢ ( ¬ ( 𝐹 ‘ 𝑀 ) ≤ 1 → if ( ( 𝐹 ‘ 𝑀 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑀 ) ) = ( 𝐹 ‘ 𝑀 ) )
80 11 79 eqtrid ⊢ ( ¬ ( 𝐹 ‘ 𝑀 ) ≤ 1 → 𝑇 = ( 𝐹 ‘ 𝑀 ) )
81 72 80 syl ⊢ ( 𝜑 → 𝑇 = ( 𝐹 ‘ 𝑀 ) )
82 81 oveq1d ⊢ ( 𝜑 → ( 𝑇 ↑𝑐 𝑈 ) = ( ( 𝐹 ‘ 𝑀 ) ↑𝑐 𝑈 ) )
83 31 recnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℂ )
84 35 36 31 38 75 lttrd ⊢ ( 𝜑 → 0 < ( 𝐹 ‘ 𝑀 ) )
85 31 84 elrpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ+ )
86 85 rpne0d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ≠ 0 )
87 83 86 68 cxpefd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) ↑𝑐 𝑈 ) = ( exp ‘ ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) ) )
88 82 87 eqtr2d ⊢ ( 𝜑 → ( exp ‘ ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) ) = ( 𝑇 ↑𝑐 𝑈 ) )
89 63 78 88 3brtr4d ⊢ ( 𝜑 → ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) ) )
90 77 relogcld ⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
91 85 relogcld ⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ∈ ℝ )
92 50 91 remulcld ⊢ ( 𝜑 → ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) ∈ ℝ )
93 efle ⊢ ( ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) ∈ ℝ ) → ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) ↔ ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) ) ) )
94 90 92 93 syl2anc ⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) ↔ ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) ) ) )
95 89 94 mpbird ⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) )
96 45 recnd ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℂ )
97 91 recnd ⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ∈ ℂ )
98 48 rpcnd ⊢ ( 𝜑 → ( log ‘ 𝑀 ) ∈ ℂ )
99 48 rpne0d ⊢ ( 𝜑 → ( log ‘ 𝑀 ) ≠ 0 )
100 96 97 98 99 div12d ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) ) ) = ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) · ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) ) ) )
101 12 oveq2i ⊢ ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) · 𝑈 ) = ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) · ( ( log ‘ 𝑁 ) / ( log ‘ 𝑀 ) ) )
102 100 101 eqtr4di ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) ) ) = ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) · 𝑈 ) )
103 97 68 mulcomd ⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) · 𝑈 ) = ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) )
104 102 103 eqtrd ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) ) ) = ( 𝑈 · ( log ‘ ( 𝐹 ‘ 𝑀 ) ) ) )
105 95 104 breqtrrd ⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( ( log ‘ 𝑁 ) · ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) ) ) )
106 91 48 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) ) ∈ ℝ )
107 16 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
108 15 simprd ⊢ ( 𝜑 → 1 < 𝑁 )
109 107 108 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ+ )
110 90 106 109 ledivmuld ⊢ ( 𝜑 → ( ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) ) ≤ ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) ) ↔ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( ( log ‘ 𝑁 ) · ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) ) ) ) )
111 105 110 mpbird ⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) ) ≤ ( ( log ‘ ( 𝐹 ‘ 𝑀 ) ) / ( log ‘ 𝑀 ) ) )
112 111 8 10 3brtr4g ⊢ ( 𝜑 → 𝑅 ≤ 𝑆 )
113 75 112 jca ⊢ ( 𝜑 → ( 1 < ( 𝐹 ‘ 𝑀 ) ∧ 𝑅 ≤ 𝑆 ) )