Step | Hyp | Ref
| Expression |
1 | | chtcl 24635 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ →
(θ‘𝐵) ∈
ℝ) |
2 | 1 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐵) ∈ ℝ) |
3 | 2 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐵) ∈ ℂ) |
4 | | chtcl 24635 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) ∈
ℝ) |
5 | 4 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐴) ∈ ℝ) |
6 | 5 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐴) ∈ ℂ) |
7 | | efsub 14669 |
. . . . 5
⊢
(((θ‘𝐵)
∈ ℂ ∧ (θ‘𝐴) ∈ ℂ) →
(exp‘((θ‘𝐵) − (θ‘𝐴))) = ((exp‘(θ‘𝐵)) /
(exp‘(θ‘𝐴)))) |
8 | 3, 6, 7 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘((θ‘𝐵) − (θ‘𝐴))) =
((exp‘(θ‘𝐵)) / (exp‘(θ‘𝐴)))) |
9 | | chtfl 24675 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ →
(θ‘(⌊‘𝐵)) = (θ‘𝐵)) |
10 | 9 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘(⌊‘𝐵)) = (θ‘𝐵)) |
11 | | chtfl 24675 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(θ‘(⌊‘𝐴)) = (θ‘𝐴)) |
12 | 11 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘(⌊‘𝐴)) = (θ‘𝐴)) |
13 | 10, 12 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) →
((θ‘(⌊‘𝐵)) −
(θ‘(⌊‘𝐴))) = ((θ‘𝐵) − (θ‘𝐴))) |
14 | | flword2 12476 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐵) ∈
(ℤ≥‘(⌊‘𝐴))) |
15 | | chtdif 24684 |
. . . . . . . 8
⊢
((⌊‘𝐵)
∈ (ℤ≥‘(⌊‘𝐴)) →
((θ‘(⌊‘𝐵)) −
(θ‘(⌊‘𝐴))) = Σ𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)(log‘𝑝)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) →
((θ‘(⌊‘𝐵)) −
(θ‘(⌊‘𝐴))) = Σ𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)(log‘𝑝)) |
17 | 13, 16 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((θ‘𝐵) − (θ‘𝐴)) = Σ𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)(log‘𝑝)) |
18 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} ⊆ ℝ |
19 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
20 | 18, 19 | sstri 3577 |
. . . . . . . 8
⊢ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} ⊆ ℂ |
21 | 20 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ⊆
ℂ) |
22 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (exp‘𝑥) = (exp‘𝑦)) |
23 | 22 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((exp‘𝑥) ∈ ℕ ↔ (exp‘𝑦) ∈
ℕ)) |
24 | 23 | elrab 3331 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔ (𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ)) |
25 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (exp‘𝑥) = (exp‘𝑧)) |
26 | 25 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((exp‘𝑥) ∈ ℕ ↔ (exp‘𝑧) ∈
ℕ)) |
27 | 26 | elrab 3331 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔ (𝑧 ∈ ℝ ∧
(exp‘𝑧) ∈
ℕ)) |
28 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑦
∈ ℝ) |
29 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑧
∈ ℝ) |
30 | 28, 29 | readdcld 9948 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (𝑦
+ 𝑧) ∈
ℝ) |
31 | 28 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑦
∈ ℂ) |
32 | 29 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑧
∈ ℂ) |
33 | | efadd 14663 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑦 + 𝑧)) = ((exp‘𝑦) · (exp‘𝑧))) |
34 | 31, 32, 33 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (exp‘(𝑦 + 𝑧)) = ((exp‘𝑦) · (exp‘𝑧))) |
35 | | nnmulcl 10920 |
. . . . . . . . . . . 12
⊢
(((exp‘𝑦)
∈ ℕ ∧ (exp‘𝑧) ∈ ℕ) → ((exp‘𝑦) · (exp‘𝑧)) ∈
ℕ) |
36 | 35 | ad2ant2l 778 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → ((exp‘𝑦) · (exp‘𝑧)) ∈ ℕ) |
37 | 34, 36 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (exp‘(𝑦 + 𝑧)) ∈ ℕ) |
38 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 + 𝑧) → (exp‘𝑥) = (exp‘(𝑦 + 𝑧))) |
39 | 38 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 + 𝑧) → ((exp‘𝑥) ∈ ℕ ↔ (exp‘(𝑦 + 𝑧)) ∈ ℕ)) |
40 | 39 | elrab 3331 |
. . . . . . . . . 10
⊢ ((𝑦 + 𝑧) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔ ((𝑦 + 𝑧) ∈ ℝ ∧ (exp‘(𝑦 + 𝑧)) ∈ ℕ)) |
41 | 30, 37, 40 | sylanbrc 695 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (𝑦
+ 𝑧) ∈ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ}) |
42 | 24, 27, 41 | syl2anb 495 |
. . . . . . . 8
⊢ ((𝑦 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ∧ 𝑧 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ}) → (𝑦 + 𝑧) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
43 | 42 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ∧ 𝑧 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ})) →
(𝑦 + 𝑧) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
44 | | fzfid 12634 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∈ Fin) |
45 | | inss1 3795 |
. . . . . . . 8
⊢
((((⌊‘𝐴)
+ 1)...(⌊‘𝐵))
∩ ℙ) ⊆ (((⌊‘𝐴) + 1)...(⌊‘𝐵)) |
46 | | ssfi 8065 |
. . . . . . . 8
⊢
(((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∈ Fin ∧ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ) ⊆
(((⌊‘𝐴) +
1)...(⌊‘𝐵)))
→ ((((⌊‘𝐴)
+ 1)...(⌊‘𝐵))
∩ ℙ) ∈ Fin) |
47 | 44, 45, 46 | sylancl 693 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ) ∈
Fin) |
48 | | inss2 3796 |
. . . . . . . . . . . 12
⊢
((((⌊‘𝐴)
+ 1)...(⌊‘𝐵))
∩ ℙ) ⊆ ℙ |
49 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) |
50 | 48, 49 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → 𝑝 ∈ ℙ) |
51 | | prmnn 15226 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → 𝑝 ∈ ℕ) |
53 | 52 | nnrpd 11746 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
54 | 53 | relogcld 24173 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
55 | 53 | reeflogd 24174 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) →
(exp‘(log‘𝑝)) =
𝑝) |
56 | 55, 52 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) →
(exp‘(log‘𝑝))
∈ ℕ) |
57 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = (log‘𝑝) → (exp‘𝑥) = (exp‘(log‘𝑝))) |
58 | 57 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = (log‘𝑝) → ((exp‘𝑥) ∈ ℕ ↔
(exp‘(log‘𝑝))
∈ ℕ)) |
59 | 58 | elrab 3331 |
. . . . . . . 8
⊢
((log‘𝑝)
∈ {𝑥 ∈ ℝ
∣ (exp‘𝑥)
∈ ℕ} ↔ ((log‘𝑝) ∈ ℝ ∧
(exp‘(log‘𝑝))
∈ ℕ)) |
60 | 54, 56, 59 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → (log‘𝑝) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
61 | | 0re 9919 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
62 | | 1nn 10908 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
63 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (exp‘𝑥) =
(exp‘0)) |
64 | | ef0 14660 |
. . . . . . . . . . . 12
⊢
(exp‘0) = 1 |
65 | 63, 64 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (exp‘𝑥) = 1) |
66 | 65 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → ((exp‘𝑥) ∈ ℕ ↔ 1 ∈
ℕ)) |
67 | 66 | elrab 3331 |
. . . . . . . . 9
⊢ (0 ∈
{𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} ↔ (0 ∈ ℝ ∧ 1 ∈ ℕ)) |
68 | 61, 62, 67 | mpbir2an 957 |
. . . . . . . 8
⊢ 0 ∈
{𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} |
69 | 68 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 0 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
70 | 21, 43, 47, 60, 69 | fsumcllem 14310 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → Σ𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)(log‘𝑝) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
71 | 17, 70 | eqeltrd 2688 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((θ‘𝐵) − (θ‘𝐴)) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
72 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = ((θ‘𝐵) − (θ‘𝐴)) → (exp‘𝑥) =
(exp‘((θ‘𝐵) − (θ‘𝐴)))) |
73 | 72 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑥 = ((θ‘𝐵) − (θ‘𝐴)) → ((exp‘𝑥) ∈ ℕ ↔
(exp‘((θ‘𝐵) − (θ‘𝐴))) ∈ ℕ)) |
74 | 73 | elrab 3331 |
. . . . . 6
⊢
(((θ‘𝐵)
− (θ‘𝐴))
∈ {𝑥 ∈ ℝ
∣ (exp‘𝑥)
∈ ℕ} ↔ (((θ‘𝐵) − (θ‘𝐴)) ∈ ℝ ∧
(exp‘((θ‘𝐵) − (θ‘𝐴))) ∈ ℕ)) |
75 | 74 | simprbi 479 |
. . . . 5
⊢
(((θ‘𝐵)
− (θ‘𝐴))
∈ {𝑥 ∈ ℝ
∣ (exp‘𝑥)
∈ ℕ} → (exp‘((θ‘𝐵) − (θ‘𝐴))) ∈ ℕ) |
76 | 71, 75 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘((θ‘𝐵) − (θ‘𝐴))) ∈
ℕ) |
77 | 8, 76 | eqeltrrd 2689 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((exp‘(θ‘𝐵)) /
(exp‘(θ‘𝐴))) ∈ ℕ) |
78 | 77 | nnzd 11357 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((exp‘(θ‘𝐵)) /
(exp‘(θ‘𝐴))) ∈ ℤ) |
79 | | efchtcl 24637 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(exp‘(θ‘𝐴)) ∈ ℕ) |
80 | 79 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∈
ℕ) |
81 | 80 | nnzd 11357 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∈
ℤ) |
82 | 80 | nnne0d 10942 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ≠ 0) |
83 | | efchtcl 24637 |
. . . . 5
⊢ (𝐵 ∈ ℝ →
(exp‘(θ‘𝐵)) ∈ ℕ) |
84 | 83 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐵)) ∈
ℕ) |
85 | 84 | nnzd 11357 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐵)) ∈
ℤ) |
86 | | dvdsval2 14824 |
. . 3
⊢
(((exp‘(θ‘𝐴)) ∈ ℤ ∧
(exp‘(θ‘𝐴)) ≠ 0 ∧
(exp‘(θ‘𝐵)) ∈ ℤ) →
((exp‘(θ‘𝐴)) ∥ (exp‘(θ‘𝐵)) ↔
((exp‘(θ‘𝐵)) / (exp‘(θ‘𝐴))) ∈
ℤ)) |
87 | 81, 82, 85, 86 | syl3anc 1318 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((exp‘(θ‘𝐴)) ∥
(exp‘(θ‘𝐵)) ↔ ((exp‘(θ‘𝐵)) /
(exp‘(θ‘𝐴))) ∈ ℤ)) |
88 | 78, 87 | mpbird 246 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∥
(exp‘(θ‘𝐵))) |