Proof of Theorem logbgcd1irraplemexp
Step | Hyp | Ref
| Expression |
1 | | logbgcd1irraplem.rp |
. . . . . . . 8
⊢ (𝜑 → (𝑋 gcd 𝐵) = 1) |
2 | | logbgcd1irraplem.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈
(ℤ≥‘2)) |
3 | | eluz2nn 9456 |
. . . . . . . . . 10
⊢ (𝑋 ∈
(ℤ≥‘2) → 𝑋 ∈ ℕ) |
4 | 2, 3 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℕ) |
5 | | logbgcd1irraplem.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
(ℤ≥‘2)) |
6 | | eluz2nn 9456 |
. . . . . . . . . 10
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈ ℕ) |
7 | 5, 6 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℕ) |
8 | | logbgcd1irraplem.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
9 | | rplpwr 11882 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑋 gcd 𝐵) = 1 → ((𝑋↑𝑁) gcd 𝐵) = 1)) |
10 | 4, 7, 8, 9 | syl3anc 1217 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 gcd 𝐵) = 1 → ((𝑋↑𝑁) gcd 𝐵) = 1)) |
11 | 1, 10 | mpd 13 |
. . . . . . 7
⊢ (𝜑 → ((𝑋↑𝑁) gcd 𝐵) = 1) |
12 | 11 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ (𝐵↑𝑀) = (𝑋↑𝑁)) → ((𝑋↑𝑁) gcd 𝐵) = 1) |
13 | | 1red 7872 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ) |
14 | | eluz2gt1 9491 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈
(ℤ≥‘2) → 1 < 𝐵) |
15 | 5, 14 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < 𝐵) |
16 | 13, 15 | gtned 7968 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ≠ 1) |
17 | 16 | neneqd 2345 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝐵 = 1) |
18 | 7 | nnzd 9264 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ ℤ) |
19 | | gcdid 11841 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℤ → (𝐵 gcd 𝐵) = (abs‘𝐵)) |
20 | 18, 19 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 gcd 𝐵) = (abs‘𝐵)) |
21 | 7 | nnred 8825 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ ℝ) |
22 | 7 | nnnn0d 9122 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
23 | 22 | nn0ge0d 9125 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ 𝐵) |
24 | 21, 23 | absidd 11044 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘𝐵) = 𝐵) |
25 | 20, 24 | eqtrd 2187 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 gcd 𝐵) = 𝐵) |
26 | 25 | eqeq1d 2163 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 gcd 𝐵) = 1 ↔ 𝐵 = 1)) |
27 | 17, 26 | mtbird 663 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐵 gcd 𝐵) = 1) |
28 | 27 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ¬ (𝐵 gcd 𝐵) = 1) |
29 | 18 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝐵 ∈ ℤ) |
30 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ ℕ) |
31 | | rpexp 11998 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((𝐵↑𝑀) gcd 𝐵) = 1 ↔ (𝐵 gcd 𝐵) = 1)) |
32 | 29, 29, 30, 31 | syl3anc 1217 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (((𝐵↑𝑀) gcd 𝐵) = 1 ↔ (𝐵 gcd 𝐵) = 1)) |
33 | 28, 32 | mtbird 663 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ¬ ((𝐵↑𝑀) gcd 𝐵) = 1) |
34 | 33 | adantr 274 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ (𝐵↑𝑀) = (𝑋↑𝑁)) → ¬ ((𝐵↑𝑀) gcd 𝐵) = 1) |
35 | | oveq1 5821 |
. . . . . . . . . 10
⊢ ((𝑋↑𝑁) = (𝐵↑𝑀) → ((𝑋↑𝑁) gcd 𝐵) = ((𝐵↑𝑀) gcd 𝐵)) |
36 | 35 | eqeq1d 2163 |
. . . . . . . . 9
⊢ ((𝑋↑𝑁) = (𝐵↑𝑀) → (((𝑋↑𝑁) gcd 𝐵) = 1 ↔ ((𝐵↑𝑀) gcd 𝐵) = 1)) |
37 | 36 | eqcoms 2157 |
. . . . . . . 8
⊢ ((𝐵↑𝑀) = (𝑋↑𝑁) → (((𝑋↑𝑁) gcd 𝐵) = 1 ↔ ((𝐵↑𝑀) gcd 𝐵) = 1)) |
38 | 37 | adantl 275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ (𝐵↑𝑀) = (𝑋↑𝑁)) → (((𝑋↑𝑁) gcd 𝐵) = 1 ↔ ((𝐵↑𝑀) gcd 𝐵) = 1)) |
39 | 34, 38 | mtbird 663 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 ∈ ℕ) ∧ (𝐵↑𝑀) = (𝑋↑𝑁)) → ¬ ((𝑋↑𝑁) gcd 𝐵) = 1) |
40 | 12, 39 | pm2.65da 651 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ¬ (𝐵↑𝑀) = (𝑋↑𝑁)) |
41 | 40 | neqcomd 2159 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ¬ (𝑋↑𝑁) = (𝐵↑𝑀)) |
42 | 41 | neqned 2331 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑋↑𝑁) ≠ (𝐵↑𝑀)) |
43 | 4 | nnzd 9264 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℤ) |
44 | 43 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑋 ∈ ℤ) |
45 | 8 | nnnn0d 9122 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
46 | 45 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑁 ∈
ℕ0) |
47 | | zexpcl 10412 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝑋↑𝑁) ∈
ℤ) |
48 | 44, 46, 47 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑋↑𝑁) ∈ ℤ) |
49 | 30 | nnnn0d 9122 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑀 ∈
ℕ0) |
50 | | zexpcl 10412 |
. . . . 5
⊢ ((𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝐵↑𝑀) ∈
ℤ) |
51 | 29, 49, 50 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝐵↑𝑀) ∈ ℤ) |
52 | | zapne 9217 |
. . . 4
⊢ (((𝑋↑𝑁) ∈ ℤ ∧ (𝐵↑𝑀) ∈ ℤ) → ((𝑋↑𝑁) # (𝐵↑𝑀) ↔ (𝑋↑𝑁) ≠ (𝐵↑𝑀))) |
53 | 48, 51, 52 | syl2anc 409 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ((𝑋↑𝑁) # (𝐵↑𝑀) ↔ (𝑋↑𝑁) ≠ (𝐵↑𝑀))) |
54 | 42, 53 | mpbird 166 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑋↑𝑁) # (𝐵↑𝑀)) |
55 | 7 | nnrpd 9579 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
56 | 55 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝐵 ∈
ℝ+) |
57 | | logbgcd1irraplem.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
58 | 57 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝑀 ∈
ℤ) |
59 | 56, 58 | rpexpcld 10552 |
. . . 4
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) ∈
ℝ+) |
60 | 59 | rpred 9581 |
. . 3
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) ∈ ℝ) |
61 | 4 | nnred 8825 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℝ) |
62 | 61, 45 | reexpcld 10545 |
. . . 4
⊢ (𝜑 → (𝑋↑𝑁) ∈ ℝ) |
63 | 62 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝑋↑𝑁) ∈ ℝ) |
64 | | 1red 7872 |
. . . 4
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ∈
ℝ) |
65 | | 1rp 9542 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
66 | 65 | a1i 9 |
. . . . . 6
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ∈
ℝ+) |
67 | 21 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝐵 ∈
ℝ) |
68 | | simpr 109 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → -𝑀 ∈
ℕ0) |
69 | 7 | nnge1d 8855 |
. . . . . . . . 9
⊢ (𝜑 → 1 ≤ 𝐵) |
70 | 69 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ≤
𝐵) |
71 | 67, 68, 70 | expge1d 10547 |
. . . . . . 7
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ≤
(𝐵↑-𝑀)) |
72 | 67 | recnd 7885 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝐵 ∈
ℂ) |
73 | 7 | nnap0d 8858 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 # 0) |
74 | 73 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 𝐵 # 0) |
75 | 72, 74, 58 | expnegapd 10535 |
. . . . . . 7
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑-𝑀) = (1 / (𝐵↑𝑀))) |
76 | 71, 75 | breqtrd 3986 |
. . . . . 6
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 ≤
(1 / (𝐵↑𝑀))) |
77 | 66, 59, 76 | lerec2d 9603 |
. . . . 5
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) ≤ (1 / 1)) |
78 | | 1div1e1 8556 |
. . . . 5
⊢ (1 / 1) =
1 |
79 | 77, 78 | breqtrdi 4001 |
. . . 4
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) ≤ 1) |
80 | | eluz2gt1 9491 |
. . . . . . 7
⊢ (𝑋 ∈
(ℤ≥‘2) → 1 < 𝑋) |
81 | 2, 80 | syl 14 |
. . . . . 6
⊢ (𝜑 → 1 < 𝑋) |
82 | | expgt1 10435 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 <
𝑋) → 1 < (𝑋↑𝑁)) |
83 | 61, 8, 81, 82 | syl3anc 1217 |
. . . . 5
⊢ (𝜑 → 1 < (𝑋↑𝑁)) |
84 | 83 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → 1 <
(𝑋↑𝑁)) |
85 | 60, 64, 63, 79, 84 | lelttrd 7979 |
. . 3
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝐵↑𝑀) < (𝑋↑𝑁)) |
86 | 60, 63, 85 | gtapd 8491 |
. 2
⊢ ((𝜑 ∧ -𝑀 ∈ ℕ0) → (𝑋↑𝑁) # (𝐵↑𝑀)) |
87 | | elznn 9162 |
. . . 4
⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ ∨ -𝑀 ∈
ℕ0))) |
88 | 57, 87 | sylib 121 |
. . 3
⊢ (𝜑 → (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ ∨ -𝑀 ∈
ℕ0))) |
89 | 88 | simprd 113 |
. 2
⊢ (𝜑 → (𝑀 ∈ ℕ ∨ -𝑀 ∈
ℕ0)) |
90 | 54, 86, 89 | mpjaodan 788 |
1
⊢ (𝜑 → (𝑋↑𝑁) # (𝐵↑𝑀)) |