Step | Hyp | Ref
| Expression |
1 | | eluz2nn 9456 |
. . . . 5
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈ ℕ) |
2 | 1 | nnrpd 9579 |
. . . 4
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈
ℝ+) |
3 | 2 | 3ad2ant2 1004 |
. . 3
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)
∧ (𝑋 gcd 𝐵) = 1) → 𝐵 ∈
ℝ+) |
4 | | 1red 7872 |
. . . . 5
⊢ (𝐵 ∈
(ℤ≥‘2) → 1 ∈ ℝ) |
5 | | eluzelre 9428 |
. . . . 5
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈ ℝ) |
6 | | eluz2gt1 9491 |
. . . . 5
⊢ (𝐵 ∈
(ℤ≥‘2) → 1 < 𝐵) |
7 | 4, 5, 6 | gtapd 8491 |
. . . 4
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 # 1) |
8 | 7 | 3ad2ant2 1004 |
. . 3
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)
∧ (𝑋 gcd 𝐵) = 1) → 𝐵 # 1) |
9 | | eluz2nn 9456 |
. . . . 5
⊢ (𝑋 ∈
(ℤ≥‘2) → 𝑋 ∈ ℕ) |
10 | 9 | nnrpd 9579 |
. . . 4
⊢ (𝑋 ∈
(ℤ≥‘2) → 𝑋 ∈
ℝ+) |
11 | 10 | 3ad2ant1 1003 |
. . 3
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)
∧ (𝑋 gcd 𝐵) = 1) → 𝑋 ∈
ℝ+) |
12 | | rplogbcl 13202 |
. . 3
⊢ ((𝐵 ∈ ℝ+
∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+)
→ (𝐵 logb
𝑋) ∈
ℝ) |
13 | 3, 8, 11, 12 | syl3anc 1217 |
. 2
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)
∧ (𝑋 gcd 𝐵) = 1) → (𝐵 logb 𝑋) ∈ ℝ) |
14 | | eluz2gt1 9491 |
. . . . . . . . . 10
⊢ (𝑋 ∈
(ℤ≥‘2) → 1 < 𝑋) |
15 | 14 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 1 < 𝑋) |
16 | 9 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 𝑋 ∈
ℕ) |
17 | 16 | nnrpd 9579 |
. . . . . . . . . 10
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 𝑋 ∈
ℝ+) |
18 | 1 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 𝐵 ∈
ℕ) |
19 | 18 | nnrpd 9579 |
. . . . . . . . . 10
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 𝐵 ∈
ℝ+) |
20 | 6 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 1 < 𝐵) |
21 | | logbgt0b 13222 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℝ+
∧ (𝐵 ∈
ℝ+ ∧ 1 < 𝐵)) → (0 < (𝐵 logb 𝑋) ↔ 1 < 𝑋)) |
22 | 17, 19, 20, 21 | syl12anc 1215 |
. . . . . . . . 9
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (0 < (𝐵
logb 𝑋) ↔ 1
< 𝑋)) |
23 | 15, 22 | mpbird 166 |
. . . . . . . 8
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 0 < (𝐵
logb 𝑋)) |
24 | 23 | anim1ci 339 |
. . . . . . 7
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝐵 logb
𝑋) ∈ ℚ) →
((𝐵 logb 𝑋) ∈ ℚ ∧ 0 <
(𝐵 logb 𝑋))) |
25 | | elpq 9535 |
. . . . . . 7
⊢ (((𝐵 logb 𝑋) ∈ ℚ ∧ 0 <
(𝐵 logb 𝑋)) → ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (𝐵 logb 𝑋) = (𝑚 / 𝑛)) |
26 | 24, 25 | syl 14 |
. . . . . 6
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝐵 logb
𝑋) ∈ ℚ) →
∃𝑚 ∈ ℕ
∃𝑛 ∈ ℕ
(𝐵 logb 𝑋) = (𝑚 / 𝑛)) |
27 | 26 | ex 114 |
. . . . 5
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ ((𝐵 logb
𝑋) ∈ ℚ →
∃𝑚 ∈ ℕ
∃𝑛 ∈ ℕ
(𝐵 logb 𝑋) = (𝑚 / 𝑛))) |
28 | | oveq2 5822 |
. . . . . . . . . 10
⊢ ((𝑚 / 𝑛) = (𝐵 logb 𝑋) → (𝐵↑𝑐(𝑚 / 𝑛)) = (𝐵↑𝑐(𝐵 logb 𝑋))) |
29 | 28 | eqcoms 2157 |
. . . . . . . . 9
⊢ ((𝐵 logb 𝑋) = (𝑚 / 𝑛) → (𝐵↑𝑐(𝑚 / 𝑛)) = (𝐵↑𝑐(𝐵 logb 𝑋))) |
30 | 7 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 𝐵 #
1) |
31 | | rpcxplogb 13220 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ+
∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+)
→ (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋) |
32 | 19, 30, 17, 31 | syl3anc 1217 |
. . . . . . . . . 10
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋) |
33 | 32 | adantr 274 |
. . . . . . . . 9
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋) |
34 | 29, 33 | sylan9eqr 2209 |
. . . . . . . 8
⊢ ((((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
∧ (𝐵 logb
𝑋) = (𝑚 / 𝑛)) → (𝐵↑𝑐(𝑚 / 𝑛)) = 𝑋) |
35 | 34 | ex 114 |
. . . . . . 7
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝐵 logb
𝑋) = (𝑚 / 𝑛) → (𝐵↑𝑐(𝑚 / 𝑛)) = 𝑋)) |
36 | | oveq1 5821 |
. . . . . . . 8
⊢ ((𝐵↑𝑐(𝑚 / 𝑛)) = 𝑋 → ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛) = (𝑋↑𝑛)) |
37 | 19 | adantr 274 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ 𝐵 ∈
ℝ+) |
38 | | nnrp 9548 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
39 | 38 | ad2antrl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ 𝑚 ∈
ℝ+) |
40 | | nnrp 9548 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
41 | 40 | ad2antll 483 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ 𝑛 ∈
ℝ+) |
42 | 39, 41 | rpdivcld 9599 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (𝑚 / 𝑛) ∈
ℝ+) |
43 | 42 | rpred 9581 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (𝑚 / 𝑛) ∈
ℝ) |
44 | | nncn 8820 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
45 | 44 | ad2antll 483 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ 𝑛 ∈
ℂ) |
46 | 37, 43, 45 | cxpmuld 13195 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (𝐵↑𝑐((𝑚 / 𝑛) · 𝑛)) = ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑐𝑛)) |
47 | 39 | rpcnd 9583 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ 𝑚 ∈
ℂ) |
48 | 41 | rpap0d 9587 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ 𝑛 #
0) |
49 | 47, 45, 48 | divcanap1d 8643 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝑚 / 𝑛) · 𝑛) = 𝑚) |
50 | 49 | oveq2d 5830 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (𝐵↑𝑐((𝑚 / 𝑛) · 𝑛)) = (𝐵↑𝑐𝑚)) |
51 | 1 | ad2antlr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ 𝐵 ∈
ℕ) |
52 | | nnz 9165 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
53 | 52 | ad2antrl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ 𝑚 ∈
ℤ) |
54 | | cxpexpnn 13156 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (𝐵↑𝑐𝑚) = (𝐵↑𝑚)) |
55 | 51, 53, 54 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (𝐵↑𝑐𝑚) = (𝐵↑𝑚)) |
56 | 50, 55 | eqtrd 2187 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (𝐵↑𝑐((𝑚 / 𝑛) · 𝑛)) = (𝐵↑𝑚)) |
57 | 37, 43 | rpcxpcld 13191 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (𝐵↑𝑐(𝑚 / 𝑛)) ∈
ℝ+) |
58 | | nnz 9165 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
59 | 58 | ad2antll 483 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ 𝑛 ∈
ℤ) |
60 | | cxpexprp 13155 |
. . . . . . . . . . . 12
⊢ (((𝐵↑𝑐(𝑚 / 𝑛)) ∈ ℝ+ ∧ 𝑛 ∈ ℤ) → ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑐𝑛) = ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛)) |
61 | 57, 59, 60 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑐𝑛) = ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛)) |
62 | 46, 56, 61 | 3eqtr3rd 2196 |
. . . . . . . . . 10
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛) = (𝐵↑𝑚)) |
63 | 62 | eqeq1d 2163 |
. . . . . . . . 9
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛) = (𝑋↑𝑛) ↔ (𝐵↑𝑚) = (𝑋↑𝑛))) |
64 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℕ) |
65 | | rplpwr 11882 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ) → ((𝑋 gcd 𝐵) = 1 → ((𝑋↑𝑛) gcd 𝐵) = 1)) |
66 | 16, 18, 64, 65 | syl2an3an 1277 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝑋 gcd 𝐵) = 1 → ((𝑋↑𝑛) gcd 𝐵) = 1)) |
67 | | oveq1 5821 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋↑𝑛) = (𝐵↑𝑚) → ((𝑋↑𝑛) gcd 𝐵) = ((𝐵↑𝑚) gcd 𝐵)) |
68 | 67 | eqeq1d 2163 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋↑𝑛) = (𝐵↑𝑚) → (((𝑋↑𝑛) gcd 𝐵) = 1 ↔ ((𝐵↑𝑚) gcd 𝐵) = 1)) |
69 | 68 | eqcoms 2157 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵↑𝑚) = (𝑋↑𝑛) → (((𝑋↑𝑛) gcd 𝐵) = 1 ↔ ((𝐵↑𝑚) gcd 𝐵) = 1)) |
70 | 69 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
∧ (𝐵↑𝑚) = (𝑋↑𝑛)) → (((𝑋↑𝑛) gcd 𝐵) = 1 ↔ ((𝐵↑𝑚) gcd 𝐵) = 1)) |
71 | | eluzelz 9427 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈ ℤ) |
72 | 71 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ 𝐵 ∈
ℤ) |
73 | | simpl 108 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝑚 ∈
ℕ) |
74 | | rpexp 11998 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑚 ∈ ℕ) → (((𝐵↑𝑚) gcd 𝐵) = 1 ↔ (𝐵 gcd 𝐵) = 1)) |
75 | 72, 72, 73, 74 | syl2an3an 1277 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (((𝐵↑𝑚) gcd 𝐵) = 1 ↔ (𝐵 gcd 𝐵) = 1)) |
76 | | gcdid 11841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 ∈ ℤ → (𝐵 gcd 𝐵) = (abs‘𝐵)) |
77 | 71, 76 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈
(ℤ≥‘2) → (𝐵 gcd 𝐵) = (abs‘𝐵)) |
78 | | nnnn0 9076 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℕ0) |
79 | | nn0ge0 9094 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 ∈ ℕ0
→ 0 ≤ 𝐵) |
80 | 1, 78, 79 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 ∈
(ℤ≥‘2) → 0 ≤ 𝐵) |
81 | 5, 80 | absidd 11044 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈
(ℤ≥‘2) → (abs‘𝐵) = 𝐵) |
82 | 77, 81 | eqtrd 2187 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈
(ℤ≥‘2) → (𝐵 gcd 𝐵) = 𝐵) |
83 | 82 | eqeq1d 2163 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈
(ℤ≥‘2) → ((𝐵 gcd 𝐵) = 1 ↔ 𝐵 = 1)) |
84 | 83 | ad2antlr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝐵 gcd 𝐵) = 1 ↔ 𝐵 = 1)) |
85 | 4, 6 | gtned 7968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ≠ 1) |
86 | | eqneqall 2334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 = 1 → (𝐵 ≠ 1 → ⊥)) |
87 | 85, 86 | syl5com 29 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈
(ℤ≥‘2) → (𝐵 = 1 → ⊥)) |
88 | 87 | ad2antlr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (𝐵 = 1 →
⊥)) |
89 | 84, 88 | sylbid 149 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝐵 gcd 𝐵) = 1 →
⊥)) |
90 | 75, 89 | sylbid 149 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (((𝐵↑𝑚) gcd 𝐵) = 1 → ⊥)) |
91 | 90 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
∧ (𝐵↑𝑚) = (𝑋↑𝑛)) → (((𝐵↑𝑚) gcd 𝐵) = 1 → ⊥)) |
92 | 70, 91 | sylbid 149 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
∧ (𝐵↑𝑚) = (𝑋↑𝑛)) → (((𝑋↑𝑛) gcd 𝐵) = 1 → ⊥)) |
93 | 92 | ex 114 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝐵↑𝑚) = (𝑋↑𝑛) → (((𝑋↑𝑛) gcd 𝐵) = 1 → ⊥))) |
94 | 93 | com23 78 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (((𝑋↑𝑛) gcd 𝐵) = 1 → ((𝐵↑𝑚) = (𝑋↑𝑛) → ⊥))) |
95 | 66, 94 | syld 45 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝑋 gcd 𝐵) = 1 → ((𝐵↑𝑚) = (𝑋↑𝑛) → ⊥))) |
96 | | dfnot 1350 |
. . . . . . . . . . 11
⊢ (¬
(𝐵↑𝑚) = (𝑋↑𝑛) ↔ ((𝐵↑𝑚) = (𝑋↑𝑛) → ⊥)) |
97 | 95, 96 | syl6ibr 161 |
. . . . . . . . . 10
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝑋 gcd 𝐵) = 1 → ¬ (𝐵↑𝑚) = (𝑋↑𝑛))) |
98 | 97 | con2d 614 |
. . . . . . . . 9
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝐵↑𝑚) = (𝑋↑𝑛) → ¬ (𝑋 gcd 𝐵) = 1)) |
99 | 63, 98 | sylbid 149 |
. . . . . . . 8
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ (((𝐵↑𝑐(𝑚 / 𝑛))↑𝑛) = (𝑋↑𝑛) → ¬ (𝑋 gcd 𝐵) = 1)) |
100 | 36, 99 | syl5 32 |
. . . . . . 7
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝐵↑𝑐(𝑚 / 𝑛)) = 𝑋 → ¬ (𝑋 gcd 𝐵) = 1)) |
101 | 35, 100 | syld 45 |
. . . . . 6
⊢ (((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
∧ (𝑚 ∈ ℕ
∧ 𝑛 ∈ ℕ))
→ ((𝐵 logb
𝑋) = (𝑚 / 𝑛) → ¬ (𝑋 gcd 𝐵) = 1)) |
102 | 101 | rexlimdvva 2579 |
. . . . 5
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ (∃𝑚 ∈
ℕ ∃𝑛 ∈
ℕ (𝐵 logb
𝑋) = (𝑚 / 𝑛) → ¬ (𝑋 gcd 𝐵) = 1)) |
103 | 27, 102 | syld 45 |
. . . 4
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ ((𝐵 logb
𝑋) ∈ ℚ →
¬ (𝑋 gcd 𝐵) = 1)) |
104 | 103 | con2d 614 |
. . 3
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2))
→ ((𝑋 gcd 𝐵) = 1 → ¬ (𝐵 logb 𝑋) ∈
ℚ)) |
105 | 104 | 3impia 1179 |
. 2
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)
∧ (𝑋 gcd 𝐵) = 1) → ¬ (𝐵 logb 𝑋) ∈
ℚ) |
106 | 13, 105 | eldifd 3108 |
1
⊢ ((𝑋 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)
∧ (𝑋 gcd 𝐵) = 1) → (𝐵 logb 𝑋) ∈ (ℝ ∖
ℚ)) |