Step | Hyp | Ref
| Expression |
1 | | ostthlem1.1 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
2 | | qabsabv.a |
. . . 4
⊢ 𝐴 = (AbsVal‘𝑄) |
3 | | qrng.q |
. . . . 5
⊢ 𝑄 = (ℂfld
↾s ℚ) |
4 | 3 | qrngbas 26355 |
. . . 4
⊢ ℚ =
(Base‘𝑄) |
5 | 2, 4 | abvf 19713 |
. . 3
⊢ (𝐹 ∈ 𝐴 → 𝐹:ℚ⟶ℝ) |
6 | | ffn 6504 |
. . 3
⊢ (𝐹:ℚ⟶ℝ →
𝐹 Fn
ℚ) |
7 | 1, 5, 6 | 3syl 18 |
. 2
⊢ (𝜑 → 𝐹 Fn ℚ) |
8 | | ostthlem1.2 |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝐴) |
9 | 2, 4 | abvf 19713 |
. . 3
⊢ (𝐺 ∈ 𝐴 → 𝐺:ℚ⟶ℝ) |
10 | | ffn 6504 |
. . 3
⊢ (𝐺:ℚ⟶ℝ →
𝐺 Fn
ℚ) |
11 | 8, 9, 10 | 3syl 18 |
. 2
⊢ (𝜑 → 𝐺 Fn ℚ) |
12 | | elq 12432 |
. . . 4
⊢ (𝑦 ∈ ℚ ↔
∃𝑘 ∈ ℤ
∃𝑛 ∈ ℕ
𝑦 = (𝑘 / 𝑛)) |
13 | 3 | qdrng 26356 |
. . . . . . . . . 10
⊢ 𝑄 ∈ DivRing |
14 | 13 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → 𝑄 ∈ DivRing) |
15 | 1 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → 𝐹 ∈ 𝐴) |
16 | | zq 12436 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℚ) |
17 | 16 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → 𝑘 ∈ ℚ) |
18 | | nnq 12444 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℚ) |
19 | 18 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → 𝑛 ∈ ℚ) |
20 | | nnne0 11750 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
21 | 20 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → 𝑛 ≠ 0) |
22 | 3 | qrng0 26357 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑄) |
23 | | eqid 2738 |
. . . . . . . . . 10
⊢
(/r‘𝑄) = (/r‘𝑄) |
24 | 2, 4, 22, 23 | abvdiv 19727 |
. . . . . . . . 9
⊢ (((𝑄 ∈ DivRing ∧ 𝐹 ∈ 𝐴) ∧ (𝑘 ∈ ℚ ∧ 𝑛 ∈ ℚ ∧ 𝑛 ≠ 0)) → (𝐹‘(𝑘(/r‘𝑄)𝑛)) = ((𝐹‘𝑘) / (𝐹‘𝑛))) |
25 | 14, 15, 17, 19, 21, 24 | syl23anc 1378 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝐹‘(𝑘(/r‘𝑄)𝑛)) = ((𝐹‘𝑘) / (𝐹‘𝑛))) |
26 | 8 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → 𝐺 ∈ 𝐴) |
27 | 2, 4, 22, 23 | abvdiv 19727 |
. . . . . . . . . 10
⊢ (((𝑄 ∈ DivRing ∧ 𝐺 ∈ 𝐴) ∧ (𝑘 ∈ ℚ ∧ 𝑛 ∈ ℚ ∧ 𝑛 ≠ 0)) → (𝐺‘(𝑘(/r‘𝑄)𝑛)) = ((𝐺‘𝑘) / (𝐺‘𝑛))) |
28 | 14, 26, 17, 19, 21, 27 | syl23anc 1378 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝐺‘(𝑘(/r‘𝑄)𝑛)) = ((𝐺‘𝑘) / (𝐺‘𝑛))) |
29 | 2, 22 | abv0 19721 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) = 0) |
30 | 1, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹‘0) = 0) |
31 | 2, 22 | abv0 19721 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ 𝐴 → (𝐺‘0) = 0) |
32 | 8, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺‘0) = 0) |
33 | 30, 32 | eqtr4d 2776 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘0) = (𝐺‘0)) |
34 | | fveq2 6674 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → (𝐹‘𝑘) = (𝐹‘0)) |
35 | | fveq2 6674 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → (𝐺‘𝑘) = (𝐺‘0)) |
36 | 34, 35 | eqeq12d 2754 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → ((𝐹‘𝑘) = (𝐺‘𝑘) ↔ (𝐹‘0) = (𝐺‘0))) |
37 | 33, 36 | syl5ibrcom 250 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 = 0 → (𝐹‘𝑘) = (𝐺‘𝑘))) |
38 | 37 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 = 0 → (𝐹‘𝑘) = (𝐺‘𝑘))) |
39 | 38 | imp 410 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → (𝐹‘𝑘) = (𝐺‘𝑘)) |
40 | | elnn1uz2 12407 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ ↔ (𝑛 = 1 ∨ 𝑛 ∈
(ℤ≥‘2))) |
41 | 3 | qrng1 26358 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 =
(1r‘𝑄) |
42 | 2, 41 | abv1 19723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ DivRing ∧ 𝐹 ∈ 𝐴) → (𝐹‘1) = 1) |
43 | 13, 1, 42 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹‘1) = 1) |
44 | 2, 41 | abv1 19723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ DivRing ∧ 𝐺 ∈ 𝐴) → (𝐺‘1) = 1) |
45 | 13, 8, 44 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺‘1) = 1) |
46 | 43, 45 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐹‘1) = (𝐺‘1)) |
47 | | fveq2 6674 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → (𝐹‘𝑛) = (𝐹‘1)) |
48 | | fveq2 6674 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 1 → (𝐺‘𝑛) = (𝐺‘1)) |
49 | 47, 48 | eqeq12d 2754 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → ((𝐹‘𝑛) = (𝐺‘𝑛) ↔ (𝐹‘1) = (𝐺‘1))) |
50 | 46, 49 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑛 = 1 → (𝐹‘𝑛) = (𝐺‘𝑛))) |
51 | 50 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 = 1) → (𝐹‘𝑛) = (𝐺‘𝑛)) |
52 | | ostthlem1.3 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘2))
→ (𝐹‘𝑛) = (𝐺‘𝑛)) |
53 | 51, 52 | jaodan 957 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑛 = 1 ∨ 𝑛 ∈ (ℤ≥‘2)))
→ (𝐹‘𝑛) = (𝐺‘𝑛)) |
54 | 40, 53 | sylan2b 597 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (𝐺‘𝑛)) |
55 | 54 | ralrimiva 3096 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐹‘𝑛) = (𝐺‘𝑛)) |
56 | 55 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) = (𝐺‘𝑛)) |
57 | | fveq2 6674 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
58 | | fveq2 6674 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) |
59 | 57, 58 | eqeq12d 2754 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛) = (𝐺‘𝑛) ↔ (𝐹‘𝑘) = (𝐺‘𝑘))) |
60 | 59 | rspccva 3525 |
. . . . . . . . . . . . 13
⊢
((∀𝑛 ∈
ℕ (𝐹‘𝑛) = (𝐺‘𝑛) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐺‘𝑘)) |
61 | 56, 60 | sylan 583 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐺‘𝑘)) |
62 | | fveq2 6674 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = ((invg‘𝑄)‘𝑘) → (𝐹‘𝑛) = (𝐹‘((invg‘𝑄)‘𝑘))) |
63 | | fveq2 6674 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = ((invg‘𝑄)‘𝑘) → (𝐺‘𝑛) = (𝐺‘((invg‘𝑄)‘𝑘))) |
64 | 62, 63 | eqeq12d 2754 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = ((invg‘𝑄)‘𝑘) → ((𝐹‘𝑛) = (𝐺‘𝑛) ↔ (𝐹‘((invg‘𝑄)‘𝑘)) = (𝐺‘((invg‘𝑄)‘𝑘)))) |
65 | 55 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ -𝑘 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) = (𝐺‘𝑛)) |
66 | 16 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℚ) |
67 | 3 | qrngneg 26359 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℚ →
((invg‘𝑄)‘𝑘) = -𝑘) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) →
((invg‘𝑄)‘𝑘) = -𝑘) |
69 | 68 | eleq1d 2817 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) →
(((invg‘𝑄)‘𝑘) ∈ ℕ ↔ -𝑘 ∈ ℕ)) |
70 | 69 | biimpar 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ -𝑘 ∈ ℕ) →
((invg‘𝑄)‘𝑘) ∈ ℕ) |
71 | 64, 65, 70 | rspcdva 3528 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ -𝑘 ∈ ℕ) → (𝐹‘((invg‘𝑄)‘𝑘)) = (𝐺‘((invg‘𝑄)‘𝑘))) |
72 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ -𝑘 ∈ ℕ) → 𝐹 ∈ 𝐴) |
73 | 16 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ -𝑘 ∈ ℕ) → 𝑘 ∈ ℚ) |
74 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(invg‘𝑄) = (invg‘𝑄) |
75 | 2, 4, 74 | abvneg 19724 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑘 ∈ ℚ) → (𝐹‘((invg‘𝑄)‘𝑘)) = (𝐹‘𝑘)) |
76 | 72, 73, 75 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ -𝑘 ∈ ℕ) → (𝐹‘((invg‘𝑄)‘𝑘)) = (𝐹‘𝑘)) |
77 | 8 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ -𝑘 ∈ ℕ) → 𝐺 ∈ 𝐴) |
78 | 2, 4, 74 | abvneg 19724 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ 𝐴 ∧ 𝑘 ∈ ℚ) → (𝐺‘((invg‘𝑄)‘𝑘)) = (𝐺‘𝑘)) |
79 | 77, 73, 78 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ -𝑘 ∈ ℕ) → (𝐺‘((invg‘𝑄)‘𝑘)) = (𝐺‘𝑘)) |
80 | 71, 76, 79 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ -𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐺‘𝑘)) |
81 | | elz 12064 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ ↔ (𝑘 ∈ ℝ ∧ (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ))) |
82 | 81 | simprbi 500 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ)) |
83 | 82 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ)) |
84 | 39, 61, 80, 83 | mpjao3dan 1432 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = (𝐺‘𝑘)) |
85 | 84 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝐹‘𝑘) = (𝐺‘𝑘)) |
86 | 54 | adantrl 716 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝐹‘𝑛) = (𝐺‘𝑛)) |
87 | 85, 86 | oveq12d 7188 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → ((𝐹‘𝑘) / (𝐹‘𝑛)) = ((𝐺‘𝑘) / (𝐺‘𝑛))) |
88 | 28, 87 | eqtr4d 2776 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝐺‘(𝑘(/r‘𝑄)𝑛)) = ((𝐹‘𝑘) / (𝐹‘𝑛))) |
89 | 25, 88 | eqtr4d 2776 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝐹‘(𝑘(/r‘𝑄)𝑛)) = (𝐺‘(𝑘(/r‘𝑄)𝑛))) |
90 | 3 | qrngdiv 26360 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℚ ∧ 𝑛 ∈ ℚ ∧ 𝑛 ≠ 0) → (𝑘(/r‘𝑄)𝑛) = (𝑘 / 𝑛)) |
91 | 17, 19, 21, 90 | syl3anc 1372 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝑘(/r‘𝑄)𝑛) = (𝑘 / 𝑛)) |
92 | 91 | fveq2d 6678 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝐹‘(𝑘(/r‘𝑄)𝑛)) = (𝐹‘(𝑘 / 𝑛))) |
93 | 91 | fveq2d 6678 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝐺‘(𝑘(/r‘𝑄)𝑛)) = (𝐺‘(𝑘 / 𝑛))) |
94 | 89, 92, 93 | 3eqtr3d 2781 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝐹‘(𝑘 / 𝑛)) = (𝐺‘(𝑘 / 𝑛))) |
95 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑦 = (𝑘 / 𝑛) → (𝐹‘𝑦) = (𝐹‘(𝑘 / 𝑛))) |
96 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑦 = (𝑘 / 𝑛) → (𝐺‘𝑦) = (𝐺‘(𝑘 / 𝑛))) |
97 | 95, 96 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑦 = (𝑘 / 𝑛) → ((𝐹‘𝑦) = (𝐺‘𝑦) ↔ (𝐹‘(𝑘 / 𝑛)) = (𝐺‘(𝑘 / 𝑛)))) |
98 | 94, 97 | syl5ibrcom 250 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ)) → (𝑦 = (𝑘 / 𝑛) → (𝐹‘𝑦) = (𝐺‘𝑦))) |
99 | 98 | rexlimdvva 3204 |
. . . 4
⊢ (𝜑 → (∃𝑘 ∈ ℤ ∃𝑛 ∈ ℕ 𝑦 = (𝑘 / 𝑛) → (𝐹‘𝑦) = (𝐺‘𝑦))) |
100 | 12, 99 | syl5bi 245 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℚ → (𝐹‘𝑦) = (𝐺‘𝑦))) |
101 | 100 | imp 410 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℚ) → (𝐹‘𝑦) = (𝐺‘𝑦)) |
102 | 7, 11, 101 | eqfnfvd 6812 |
1
⊢ (𝜑 → 𝐹 = 𝐺) |