Proof of Theorem expnbnd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1nn 12277 | . . 3
⊢ 1 ∈
ℕ | 
| 2 |  | 1re 11261 | . . . . . . . 8
⊢ 1 ∈
ℝ | 
| 3 |  | lttr 11337 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝐵 ∈
ℝ) → ((𝐴 < 1
∧ 1 < 𝐵) →
𝐴 < 𝐵)) | 
| 4 | 2, 3 | mp3an2 1451 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 1 ∧ 1 < 𝐵) → 𝐴 < 𝐵)) | 
| 5 | 4 | exp4b 430 | . . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 1 → (1 < 𝐵 → 𝐴 < 𝐵)))) | 
| 6 | 5 | com34 91 | . . . . 5
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 <
𝐵 → (𝐴 < 1 → 𝐴 < 𝐵)))) | 
| 7 | 6 | 3imp1 1348 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → 𝐴 < 𝐵) | 
| 8 |  | recn 11245 | . . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) | 
| 9 |  | exp1 14108 | . . . . . . 7
⊢ (𝐵 ∈ ℂ → (𝐵↑1) = 𝐵) | 
| 10 | 8, 9 | syl 17 | . . . . . 6
⊢ (𝐵 ∈ ℝ → (𝐵↑1) = 𝐵) | 
| 11 | 10 | 3ad2ant2 1135 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵↑1) = 𝐵) | 
| 12 | 11 | adantr 480 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → (𝐵↑1) = 𝐵) | 
| 13 | 7, 12 | breqtrrd 5171 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → 𝐴 < (𝐵↑1)) | 
| 14 |  | oveq2 7439 | . . . . 5
⊢ (𝑘 = 1 → (𝐵↑𝑘) = (𝐵↑1)) | 
| 15 | 14 | breq2d 5155 | . . . 4
⊢ (𝑘 = 1 → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑1))) | 
| 16 | 15 | rspcev 3622 | . . 3
⊢ ((1
∈ ℕ ∧ 𝐴 <
(𝐵↑1)) →
∃𝑘 ∈ ℕ
𝐴 < (𝐵↑𝑘)) | 
| 17 | 1, 13, 16 | sylancr 587 | . 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝐴 < 1) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) | 
| 18 |  | peano2rem 11576 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ∈
ℝ) | 
| 19 | 18 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → (𝐴 − 1) ∈
ℝ) | 
| 20 |  | peano2rem 11576 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈
ℝ) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵 − 1) ∈
ℝ) | 
| 22 | 21 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → (𝐵 − 1) ∈
ℝ) | 
| 23 |  | posdif 11756 | . . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1))) | 
| 24 | 2, 23 | mpan 690 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ → (1 <
𝐵 ↔ 0 < (𝐵 − 1))) | 
| 25 | 24 | biimpa 476 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 < (𝐵 − 1)) | 
| 26 | 25 | gt0ne0d 11827 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵 − 1) ≠
0) | 
| 27 | 26 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → (𝐵 − 1) ≠
0) | 
| 28 | 19, 22, 27 | redivcld 12095 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 <
𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈
ℝ) | 
| 29 | 28 | adantll 714 | . . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈
ℝ) | 
| 30 | 18 | adantl 481 | . . . . . . . . . 10
⊢ ((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) → (𝐴 − 1) ∈ ℝ) | 
| 31 |  | subge0 11776 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (0 ≤ (𝐴
− 1) ↔ 1 ≤ 𝐴)) | 
| 32 | 2, 31 | mpan2 691 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (0 ≤
(𝐴 − 1) ↔ 1 ≤
𝐴)) | 
| 33 | 32 | biimparc 479 | . . . . . . . . . 10
⊢ ((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) → 0 ≤ (𝐴 − 1)) | 
| 34 | 30, 33 | jca 511 | . . . . . . . . 9
⊢ ((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) → ((𝐴 − 1) ∈ ℝ ∧ 0 ≤
(𝐴 −
1))) | 
| 35 | 21, 25 | jca 511 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → ((𝐵 − 1) ∈ ℝ ∧
0 < (𝐵 −
1))) | 
| 36 |  | divge0 12137 | . . . . . . . . 9
⊢ ((((𝐴 − 1) ∈ ℝ ∧
0 ≤ (𝐴 − 1)) ∧
((𝐵 − 1) ∈
ℝ ∧ 0 < (𝐵
− 1))) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1))) | 
| 37 | 34, 35, 36 | syl2an 596 | . . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1))) | 
| 38 |  | flge0nn0 13860 | . . . . . . . 8
⊢ ((((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ ∧ 0 ≤
((𝐴 − 1) / (𝐵 − 1))) →
(⌊‘((𝐴 −
1) / (𝐵 − 1))) ∈
ℕ0) | 
| 39 | 29, 37, 38 | syl2anc 584 | . . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈
ℕ0) | 
| 40 |  | nn0p1nn 12565 | . . . . . . 7
⊢
((⌊‘((𝐴
− 1) / (𝐵 −
1))) ∈ ℕ0 → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈
ℕ) | 
| 41 | 39, 40 | syl 17 | . . . . . 6
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) →
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ) | 
| 42 |  | simplr 769 | . . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 ∈ ℝ) | 
| 43 | 21 | adantl 481 | . . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵 − 1) ∈ ℝ) | 
| 44 |  | peano2nn0 12566 | . . . . . . . . . . 11
⊢
((⌊‘((𝐴
− 1) / (𝐵 −
1))) ∈ ℕ0 → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈
ℕ0) | 
| 45 | 39, 44 | syl 17 | . . . . . . . . . 10
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) →
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ0) | 
| 46 | 45 | nn0red 12588 | . . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) →
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℝ) | 
| 47 | 43, 46 | remulcld 11291 | . . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈
ℝ) | 
| 48 |  | peano2re 11434 | . . . . . . . 8
⊢ (((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
∈ ℝ → (((𝐵
− 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ∈
ℝ) | 
| 49 | 47, 48 | syl 17 | . . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ∈
ℝ) | 
| 50 |  | simprl 771 | . . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐵 ∈ ℝ) | 
| 51 |  | reexpcl 14119 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ0) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈
ℝ) | 
| 52 | 50, 45, 51 | syl2anc 584 | . . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈
ℝ) | 
| 53 |  | flltp1 13840 | . . . . . . . . . 10
⊢ (((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ → ((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) | 
| 54 | 29, 53 | syl 17 | . . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) | 
| 55 | 30 | adantr 480 | . . . . . . . . . 10
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) ∈ ℝ) | 
| 56 | 25 | adantl 481 | . . . . . . . . . 10
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 < (𝐵 − 1)) | 
| 57 |  | ltdivmul 12143 | . . . . . . . . . 10
⊢ (((𝐴 − 1) ∈ ℝ ∧
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℝ ∧ ((𝐵
− 1) ∈ ℝ ∧ 0 < (𝐵 − 1))) → (((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ↔ (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))) | 
| 58 | 55, 46, 43, 56, 57 | syl112anc 1376 | . . . . . . . . 9
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ↔ (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))) | 
| 59 | 54, 58 | mpbid 232 | . . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) | 
| 60 |  | ltsubadd 11733 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ ((𝐵 −
1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ) →
((𝐴 − 1) < ((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
↔ 𝐴 < (((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
+ 1))) | 
| 61 | 2, 60 | mp3an2 1451 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝐵 − 1) ·
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1))
∈ ℝ) → ((𝐴
− 1) < ((𝐵 −
1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1))) | 
| 62 | 42, 47, 61 | syl2anc 584 | . . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1))) | 
| 63 | 59, 62 | mpbid 232 | . . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1)) | 
| 64 |  | 0lt1 11785 | . . . . . . . . . . . 12
⊢ 0 <
1 | 
| 65 |  | 0re 11263 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℝ | 
| 66 |  | lttr 11337 | . . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 1 ∧ 1
< 𝐵) → 0 < 𝐵)) | 
| 67 | 65, 2, 66 | mp3an12 1453 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → ((0 <
1 ∧ 1 < 𝐵) → 0
< 𝐵)) | 
| 68 | 64, 67 | mpani 696 | . . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (1 <
𝐵 → 0 < 𝐵)) | 
| 69 |  | ltle 11349 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → (0 < 𝐵 → 0 ≤ 𝐵)) | 
| 70 | 65, 69 | mpan 690 | . . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (0 <
𝐵 → 0 ≤ 𝐵)) | 
| 71 | 68, 70 | syld 47 | . . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → (1 <
𝐵 → 0 ≤ 𝐵)) | 
| 72 | 71 | imp 406 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 ≤ 𝐵) | 
| 73 | 72 | adantl 481 | . . . . . . . 8
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 ≤ 𝐵) | 
| 74 |  | bernneq2 14269 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧
((⌊‘((𝐴 −
1) / (𝐵 − 1))) + 1)
∈ ℕ0 ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) | 
| 75 | 50, 45, 73, 74 | syl3anc 1373 | . . . . . . 7
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) | 
| 76 | 42, 49, 52, 63, 75 | ltletrd 11421 | . . . . . 6
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) | 
| 77 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐵↑𝑘) = (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) | 
| 78 | 77 | breq2d 5155 | . . . . . . 7
⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))) | 
| 79 | 78 | rspcev 3622 | . . . . . 6
⊢
((((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ ∧
𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) | 
| 80 | 41, 76, 79 | syl2anc 584 | . . . . 5
⊢ (((1 ≤
𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) | 
| 81 | 80 | exp43 436 | . . . 4
⊢ (1 ≤
𝐴 → (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 < 𝐵 → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))))) | 
| 82 | 81 | com4l 92 | . . 3
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 <
𝐵 → (1 ≤ 𝐴 → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))))) | 
| 83 | 82 | 3imp1 1348 | . 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 1 ≤ 𝐴) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) | 
| 84 |  | simp1 1137 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐴 ∈ ℝ) | 
| 85 |  | 1red 11262 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 1 ∈
ℝ) | 
| 86 | 17, 83, 84, 85 | ltlecasei 11369 | 1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |