Metamath Proof Explorer

Theorem ostth

Description: Ostrowski's theorem, which classifies all absolute values on QQ . Any such absolute value must either be the trivial absolute value K , a constant exponent 0 < a <_ 1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (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 ) )
Assertion ostth ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )

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 simpl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → 𝐹 ∈ 𝐴 )
6 1re ⊢ 1 ∈ ℝ
7 6 ltnri ⊢ ¬ 1 < 1
8 ax-1ne0 ⊢ 1 ≠ 0
9 1 qrng1 ⊢ 1 = ( 1r ‘ 𝑄 )
10 1 qrng0 ⊢ 0 = ( 0g ‘ 𝑄 )
11 2 9 10 abv1z ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) = 1 )
12 8 11 mpan2 ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 1 ) = 1 )
13 12 breq2d ⊢ ( 𝐹 ∈ 𝐴 → ( 1 < ( 𝐹 ‘ 1 ) ↔ 1 < 1 ) )
14 7 13 mtbiri ⊢ ( 𝐹 ∈ 𝐴 → ¬ 1 < ( 𝐹 ‘ 1 ) )
15 14 adantr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → ¬ 1 < ( 𝐹 ‘ 1 ) )
16 simprr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → 1 < ( 𝐹 ‘ 𝑛 ) )
17 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) )
18 17 breq2d ⊢ ( 𝑛 = 1 → ( 1 < ( 𝐹 ‘ 𝑛 ) ↔ 1 < ( 𝐹 ‘ 1 ) ) )
19 16 18 syl5ibcom ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝑛 = 1 → 1 < ( 𝐹 ‘ 1 ) ) )
20 15 19 mtod ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → ¬ 𝑛 = 1 )
21 simprl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → 𝑛 ∈ ℕ )
22 elnn1uz2 ⊢ ( 𝑛 ∈ ℕ ↔ ( 𝑛 = 1 ∨ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) )
23 21 22 sylib ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝑛 = 1 ∨ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) )
24 23 ord ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → ( ¬ 𝑛 = 1 → 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) )
25 20 24 mpd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 2 ) )
26 eqid ⊢ ( ( log ‘ ( 𝐹 ‘ 𝑛 ) ) / ( log ‘ 𝑛 ) ) = ( ( log ‘ ( 𝐹 ‘ 𝑛 ) ) / ( log ‘ 𝑛 ) )
27 1 2 3 4 5 25 16 26 ostth2 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ ∧ 1 < ( 𝐹 ‘ 𝑛 ) ) ) → ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )
28 27 rexlimdvaa ⊢ ( 𝐹 ∈ 𝐴 → ( ∃ 𝑛 ∈ ℕ 1 < ( 𝐹 ‘ 𝑛 ) → ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
29 3mix2 ⊢ ( ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
30 28 29 syl6 ⊢ ( 𝐹 ∈ 𝐴 → ( ∃ 𝑛 ∈ ℕ 1 < ( 𝐹 ‘ 𝑛 ) → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) ) )
31 ralnex ⊢ ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ↔ ¬ ∃ 𝑛 ∈ ℕ 1 < ( 𝐹 ‘ 𝑛 ) )
32 simpll ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝐹 ∈ 𝐴 )
33 simplr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) )
34 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
35 34 breq2d ⊢ ( 𝑛 = 𝑘 → ( 1 < ( 𝐹 ‘ 𝑛 ) ↔ 1 < ( 𝐹 ‘ 𝑘 ) ) )
36 35 notbid ⊢ ( 𝑛 = 𝑘 → ( ¬ 1 < ( 𝐹 ‘ 𝑛 ) ↔ ¬ 1 < ( 𝐹 ‘ 𝑘 ) ) )
37 36 cbvralvw ⊢ ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ↔ ∀ 𝑘 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑘 ) )
38 33 37 sylib ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ∀ 𝑘 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑘 ) )
39 simprl ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝑝 ∈ ℙ )
40 simprr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( 𝐹 ‘ 𝑝 ) < 1 )
41 eqid ⊢ - ( ( log ‘ ( 𝐹 ‘ 𝑝 ) ) / ( log ‘ 𝑝 ) ) = - ( ( log ‘ ( 𝐹 ‘ 𝑝 ) ) / ( log ‘ 𝑝 ) )
42 eqid ⊢ if ( ( 𝐹 ‘ 𝑝 ) ≤ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑝 ) ) = if ( ( 𝐹 ‘ 𝑝 ) ≤ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑝 ) )
43 1 2 3 4 32 38 39 40 41 42 ostth3 ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )
44 43 expr ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝐹 ‘ 𝑝 ) < 1 → ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
45 44 reximdva ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) → ( ∃ 𝑝 ∈ ℙ ( 𝐹 ‘ 𝑝 ) < 1 → ∃ 𝑝 ∈ ℙ ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
46 1 2 3 padicabvf ⊢ 𝐽 : ℙ ⟶ 𝐴
47 ffn ⊢ ( 𝐽 : ℙ ⟶ 𝐴 → 𝐽 Fn ℙ )
48 fveq1 ⊢ ( 𝑔 = ( 𝐽 ‘ 𝑝 ) → ( 𝑔 ‘ 𝑦 ) = ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) )
49 48 oveq1d ⊢ ( 𝑔 = ( 𝐽 ‘ 𝑝 ) → ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) = ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) )
50 49 mpteq2dv ⊢ ( 𝑔 = ( 𝐽 ‘ 𝑝 ) → ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )
51 50 eqeq2d ⊢ ( 𝑔 = ( 𝐽 ‘ 𝑝 ) → ( 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ↔ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
52 51 rexrn ⊢ ( 𝐽 Fn ℙ → ( ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ↔ ∃ 𝑝 ∈ ℙ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
53 46 47 52 mp2b ⊢ ( ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ↔ ∃ 𝑝 ∈ ℙ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )
54 53 rexbii ⊢ ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ↔ ∃ 𝑎 ∈ ℝ+ ∃ 𝑝 ∈ ℙ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )
55 rexcom ⊢ ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑝 ∈ ℙ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )
56 54 55 bitri ⊢ ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )
57 3mix3 ⊢ ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
58 56 57 sylbir ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑎 ∈ ℝ+ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
59 45 58 syl6 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) → ( ∃ 𝑝 ∈ ℙ ( 𝐹 ‘ 𝑝 ) < 1 → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) ) )
60 ralnex ⊢ ( ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 ↔ ¬ ∃ 𝑝 ∈ ℙ ( 𝐹 ‘ 𝑝 ) < 1 )
61 simpl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ∧ ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝐹 ∈ 𝐴 )
62 simprl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ∧ ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) )
63 62 37 sylib ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ∧ ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ∀ 𝑘 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑘 ) )
64 simprr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ∧ ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 )
65 fveq2 ⊢ ( 𝑝 = 𝑘 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑘 ) )
66 65 breq1d ⊢ ( 𝑝 = 𝑘 → ( ( 𝐹 ‘ 𝑝 ) < 1 ↔ ( 𝐹 ‘ 𝑘 ) < 1 ) )
67 66 notbid ⊢ ( 𝑝 = 𝑘 → ( ¬ ( 𝐹 ‘ 𝑝 ) < 1 ↔ ¬ ( 𝐹 ‘ 𝑘 ) < 1 ) )
68 67 cbvralvw ⊢ ( ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 ↔ ∀ 𝑘 ∈ ℙ ¬ ( 𝐹 ‘ 𝑘 ) < 1 )
69 64 68 sylib ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ∧ ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ∀ 𝑘 ∈ ℙ ¬ ( 𝐹 ‘ 𝑘 ) < 1 )
70 1 2 3 4 61 63 69 ostth1 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ∧ ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → 𝐹 = 𝐾 )
71 70 3mix1d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ∧ ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 ) ) → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
72 71 expr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) → ( ∀ 𝑝 ∈ ℙ ¬ ( 𝐹 ‘ 𝑝 ) < 1 → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) ) )
73 60 72 biimtrrid ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) → ( ¬ ∃ 𝑝 ∈ ℙ ( 𝐹 ‘ 𝑝 ) < 1 → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) ) )
74 59 73 pm2.61d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) ) → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
75 74 ex ⊢ ( 𝐹 ∈ 𝐴 → ( ∀ 𝑛 ∈ ℕ ¬ 1 < ( 𝐹 ‘ 𝑛 ) → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) ) )
76 31 75 biimtrrid ⊢ ( 𝐹 ∈ 𝐴 → ( ¬ ∃ 𝑛 ∈ ℕ 1 < ( 𝐹 ‘ 𝑛 ) → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) ) )
77 30 76 pm2.61d ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )
78 id ⊢ ( 𝐹 = 𝐾 → 𝐹 = 𝐾 )
79 1 qdrng ⊢ 𝑄 ∈ DivRing
80 1 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
81 2 80 10 4 abvtriv ⊢ ( 𝑄 ∈ DivRing → 𝐾 ∈ 𝐴 )
82 79 81 ax-mp ⊢ 𝐾 ∈ 𝐴
83 78 82 eqeltrdi ⊢ ( 𝐹 = 𝐾 → 𝐹 ∈ 𝐴 )
84 1 2 qabsabv ⊢ ( abs ↾ ℚ ) ∈ 𝐴
85 fvres ⊢ ( 𝑦 ∈ ℚ → ( ( abs ↾ ℚ ) ‘ 𝑦 ) = ( abs ‘ 𝑦 ) )
86 85 oveq1d ⊢ ( 𝑦 ∈ ℚ → ( ( ( abs ↾ ℚ ) ‘ 𝑦 ) ↑𝑐 𝑎 ) = ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) )
87 86 mpteq2ia ⊢ ( 𝑦 ∈ ℚ ↦ ( ( ( abs ↾ ℚ ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) )
88 87 eqcomi ⊢ ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) = ( 𝑦 ∈ ℚ ↦ ( ( ( abs ↾ ℚ ) ‘ 𝑦 ) ↑𝑐 𝑎 ) )
89 2 80 88 abvcxp ⊢ ( ( ( abs ↾ ℚ ) ∈ 𝐴 ∧ 𝑎 ∈ ( 0 (,] 1 ) ) → ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∈ 𝐴 )
90 84 89 mpan ⊢ ( 𝑎 ∈ ( 0 (,] 1 ) → ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∈ 𝐴 )
91 eleq1 ⊢ ( 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → ( 𝐹 ∈ 𝐴 ↔ ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∈ 𝐴 ) )
92 90 91 syl5ibrcom ⊢ ( 𝑎 ∈ ( 0 (,] 1 ) → ( 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → 𝐹 ∈ 𝐴 ) )
93 92 rexlimiv ⊢ ( ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → 𝐹 ∈ 𝐴 )
94 1 2 3 padicabvcxp ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑎 ∈ ℝ+ ) → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∈ 𝐴 )
95 94 ancoms ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑝 ∈ ℙ ) → ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∈ 𝐴 )
96 eleq1 ⊢ ( 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → ( 𝐹 ∈ 𝐴 ↔ ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∈ 𝐴 ) )
97 95 96 syl5ibrcom ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑝 ∈ ℙ ) → ( 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → 𝐹 ∈ 𝐴 ) )
98 97 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑝 ∈ ℙ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( ( 𝐽 ‘ 𝑝 ) ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → 𝐹 ∈ 𝐴 )
99 54 98 sylbi ⊢ ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) → 𝐹 ∈ 𝐴 )
100 83 93 99 3jaoi ⊢ ( ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) → 𝐹 ∈ 𝐴 )
101 77 100 impbii ⊢ ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 = 𝐾 ∨ ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ∨ ∃ 𝑎 ∈ ℝ+ ∃ 𝑔 ∈ ran 𝐽 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( 𝑔 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) ) )