Step | Hyp | Ref
| Expression |
1 | | chtcl 26258 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ →
(θ‘𝐵) ∈
ℝ) |
2 | 1 | 3ad2ant2 1133 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐵) ∈ ℝ) |
3 | 2 | recnd 11003 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐵) ∈ ℂ) |
4 | | chtcl 26258 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) ∈
ℝ) |
5 | 4 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐴) ∈ ℝ) |
6 | 5 | recnd 11003 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘𝐴) ∈ ℂ) |
7 | | efsub 15809 |
. . . . 5
⊢
(((θ‘𝐵)
∈ ℂ ∧ (θ‘𝐴) ∈ ℂ) →
(exp‘((θ‘𝐵) − (θ‘𝐴))) = ((exp‘(θ‘𝐵)) /
(exp‘(θ‘𝐴)))) |
8 | 3, 6, 7 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘((θ‘𝐵) − (θ‘𝐴))) =
((exp‘(θ‘𝐵)) / (exp‘(θ‘𝐴)))) |
9 | | chtfl 26298 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ →
(θ‘(⌊‘𝐵)) = (θ‘𝐵)) |
10 | 9 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘(⌊‘𝐵)) = (θ‘𝐵)) |
11 | | chtfl 26298 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(θ‘(⌊‘𝐴)) = (θ‘𝐴)) |
12 | 11 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (θ‘(⌊‘𝐴)) = (θ‘𝐴)) |
13 | 10, 12 | oveq12d 7293 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) →
((θ‘(⌊‘𝐵)) −
(θ‘(⌊‘𝐴))) = ((θ‘𝐵) − (θ‘𝐴))) |
14 | | flword2 13533 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐵) ∈
(ℤ≥‘(⌊‘𝐴))) |
15 | | chtdif 26307 |
. . . . . . . 8
⊢
((⌊‘𝐵)
∈ (ℤ≥‘(⌊‘𝐴)) →
((θ‘(⌊‘𝐵)) −
(θ‘(⌊‘𝐴))) = Σ𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)(log‘𝑝)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) →
((θ‘(⌊‘𝐵)) −
(θ‘(⌊‘𝐴))) = Σ𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)(log‘𝑝)) |
17 | 13, 16 | eqtr3d 2780 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((θ‘𝐵) − (θ‘𝐴)) = Σ𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)(log‘𝑝)) |
18 | | ssrab2 4013 |
. . . . . . . . 9
⊢ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} ⊆ ℝ |
19 | | ax-resscn 10928 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
20 | 18, 19 | sstri 3930 |
. . . . . . . 8
⊢ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} ⊆ ℂ |
21 | 20 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ⊆
ℂ) |
22 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (exp‘𝑥) = (exp‘𝑦)) |
23 | 22 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((exp‘𝑥) ∈ ℕ ↔ (exp‘𝑦) ∈
ℕ)) |
24 | 23 | elrab 3624 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔ (𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ)) |
25 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (exp‘𝑥) = (exp‘𝑧)) |
26 | 25 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((exp‘𝑥) ∈ ℕ ↔ (exp‘𝑧) ∈
ℕ)) |
27 | 26 | elrab 3624 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔ (𝑧 ∈ ℝ ∧
(exp‘𝑧) ∈
ℕ)) |
28 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 + 𝑧) → (exp‘𝑥) = (exp‘(𝑦 + 𝑧))) |
29 | 28 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 + 𝑧) → ((exp‘𝑥) ∈ ℕ ↔ (exp‘(𝑦 + 𝑧)) ∈ ℕ)) |
30 | | simpll 764 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑦
∈ ℝ) |
31 | | simprl 768 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑧
∈ ℝ) |
32 | 30, 31 | readdcld 11004 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (𝑦
+ 𝑧) ∈
ℝ) |
33 | 30 | recnd 11003 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑦
∈ ℂ) |
34 | 31 | recnd 11003 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑧
∈ ℂ) |
35 | | efadd 15803 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑦 + 𝑧)) = ((exp‘𝑦) · (exp‘𝑧))) |
36 | 33, 34, 35 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (exp‘(𝑦 + 𝑧)) = ((exp‘𝑦) · (exp‘𝑧))) |
37 | | nnmulcl 11997 |
. . . . . . . . . . . 12
⊢
(((exp‘𝑦)
∈ ℕ ∧ (exp‘𝑧) ∈ ℕ) → ((exp‘𝑦) · (exp‘𝑧)) ∈
ℕ) |
38 | 37 | ad2ant2l 743 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → ((exp‘𝑦) · (exp‘𝑧)) ∈ ℕ) |
39 | 36, 38 | eqeltrd 2839 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (exp‘(𝑦 + 𝑧)) ∈ ℕ) |
40 | 29, 32, 39 | elrabd 3626 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (𝑦
+ 𝑧) ∈ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ}) |
41 | 24, 27, 40 | syl2anb 598 |
. . . . . . . 8
⊢ ((𝑦 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ∧ 𝑧 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ}) → (𝑦 + 𝑧) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
42 | 41 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ∧ 𝑧 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ})) →
(𝑦 + 𝑧) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
43 | | fzfid 13693 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∈ Fin) |
44 | | inss1 4162 |
. . . . . . . 8
⊢
((((⌊‘𝐴)
+ 1)...(⌊‘𝐵))
∩ ℙ) ⊆ (((⌊‘𝐴) + 1)...(⌊‘𝐵)) |
45 | | ssfi 8956 |
. . . . . . . 8
⊢
(((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∈ Fin ∧ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ) ⊆
(((⌊‘𝐴) +
1)...(⌊‘𝐵)))
→ ((((⌊‘𝐴)
+ 1)...(⌊‘𝐵))
∩ ℙ) ∈ Fin) |
46 | 43, 44, 45 | sylancl 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ) ∈
Fin) |
47 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑥 = (log‘𝑝) → (exp‘𝑥) = (exp‘(log‘𝑝))) |
48 | 47 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑥 = (log‘𝑝) → ((exp‘𝑥) ∈ ℕ ↔
(exp‘(log‘𝑝))
∈ ℕ)) |
49 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) |
50 | 49 | elin2d 4133 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → 𝑝 ∈ ℙ) |
51 | | prmnn 16379 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → 𝑝 ∈ ℕ) |
53 | 52 | nnrpd 12770 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
54 | 53 | relogcld 25778 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
55 | 53 | reeflogd 25779 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) →
(exp‘(log‘𝑝)) =
𝑝) |
56 | 55, 52 | eqeltrd 2839 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) →
(exp‘(log‘𝑝))
∈ ℕ) |
57 | 48, 54, 56 | elrabd 3626 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)) → (log‘𝑝) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
58 | | 0re 10977 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
59 | | 1nn 11984 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
60 | | fveq2 6774 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (exp‘𝑥) =
(exp‘0)) |
61 | | ef0 15800 |
. . . . . . . . . . . 12
⊢
(exp‘0) = 1 |
62 | 60, 61 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (exp‘𝑥) = 1) |
63 | 62 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → ((exp‘𝑥) ∈ ℕ ↔ 1 ∈
ℕ)) |
64 | 63 | elrab 3624 |
. . . . . . . . 9
⊢ (0 ∈
{𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} ↔ (0 ∈ ℝ ∧ 1 ∈ ℕ)) |
65 | 58, 59, 64 | mpbir2an 708 |
. . . . . . . 8
⊢ 0 ∈
{𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} |
66 | 65 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 0 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
67 | 21, 42, 46, 57, 66 | fsumcllem 15444 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → Σ𝑝 ∈ ((((⌊‘𝐴) + 1)...(⌊‘𝐵)) ∩ ℙ)(log‘𝑝) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
68 | 17, 67 | eqeltrd 2839 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((θ‘𝐵) − (θ‘𝐴)) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
69 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑥 = ((θ‘𝐵) − (θ‘𝐴)) → (exp‘𝑥) =
(exp‘((θ‘𝐵) − (θ‘𝐴)))) |
70 | 69 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑥 = ((θ‘𝐵) − (θ‘𝐴)) → ((exp‘𝑥) ∈ ℕ ↔
(exp‘((θ‘𝐵) − (θ‘𝐴))) ∈ ℕ)) |
71 | 70 | elrab 3624 |
. . . . . 6
⊢
(((θ‘𝐵)
− (θ‘𝐴))
∈ {𝑥 ∈ ℝ
∣ (exp‘𝑥)
∈ ℕ} ↔ (((θ‘𝐵) − (θ‘𝐴)) ∈ ℝ ∧
(exp‘((θ‘𝐵) − (θ‘𝐴))) ∈ ℕ)) |
72 | 71 | simprbi 497 |
. . . . 5
⊢
(((θ‘𝐵)
− (θ‘𝐴))
∈ {𝑥 ∈ ℝ
∣ (exp‘𝑥)
∈ ℕ} → (exp‘((θ‘𝐵) − (θ‘𝐴))) ∈ ℕ) |
73 | 68, 72 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘((θ‘𝐵) − (θ‘𝐴))) ∈
ℕ) |
74 | 8, 73 | eqeltrrd 2840 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((exp‘(θ‘𝐵)) /
(exp‘(θ‘𝐴))) ∈ ℕ) |
75 | 74 | nnzd 12425 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((exp‘(θ‘𝐵)) /
(exp‘(θ‘𝐴))) ∈ ℤ) |
76 | | efchtcl 26260 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(exp‘(θ‘𝐴)) ∈ ℕ) |
77 | 76 | 3ad2ant1 1132 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∈
ℕ) |
78 | 77 | nnzd 12425 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∈
ℤ) |
79 | 77 | nnne0d 12023 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ≠ 0) |
80 | | efchtcl 26260 |
. . . . 5
⊢ (𝐵 ∈ ℝ →
(exp‘(θ‘𝐵)) ∈ ℕ) |
81 | 80 | 3ad2ant2 1133 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐵)) ∈
ℕ) |
82 | 81 | nnzd 12425 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐵)) ∈
ℤ) |
83 | | dvdsval2 15966 |
. . 3
⊢
(((exp‘(θ‘𝐴)) ∈ ℤ ∧
(exp‘(θ‘𝐴)) ≠ 0 ∧
(exp‘(θ‘𝐵)) ∈ ℤ) →
((exp‘(θ‘𝐴)) ∥ (exp‘(θ‘𝐵)) ↔
((exp‘(θ‘𝐵)) / (exp‘(θ‘𝐴))) ∈
ℤ)) |
84 | 78, 79, 82, 83 | syl3anc 1370 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → ((exp‘(θ‘𝐴)) ∥
(exp‘(θ‘𝐵)) ↔ ((exp‘(θ‘𝐵)) /
(exp‘(θ‘𝐴))) ∈ ℤ)) |
85 | 75, 84 | mpbird 256 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (exp‘(θ‘𝐴)) ∥
(exp‘(θ‘𝐵))) |