Step | Hyp | Ref
| Expression |
1 | | breq2 5057 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (1 ≤ 𝑧 ↔ 1 ≤ 𝐴)) |
2 | 1 | elrab 3602 |
. . . . 5
⊢ (𝐴 ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧} ↔ (𝐴 ∈ ℝ ∧ 1 ≤ 𝐴)) |
3 | | ssrab2 3993 |
. . . . . . 7
⊢ {𝑧 ∈ ℝ ∣ 1 ≤
𝑧} ⊆
ℝ |
4 | | ax-resscn 10786 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
5 | 3, 4 | sstri 3910 |
. . . . . 6
⊢ {𝑧 ∈ ℝ ∣ 1 ≤
𝑧} ⊆
ℂ |
6 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (1 ≤ 𝑧 ↔ 1 ≤ 𝑥)) |
7 | 6 | elrab 3602 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧} ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) |
8 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (1 ≤ 𝑧 ↔ 1 ≤ 𝑦)) |
9 | 8 | elrab 3602 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧} ↔ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) |
10 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑧 = (𝑥 · 𝑦) → (1 ≤ 𝑧 ↔ 1 ≤ (𝑥 · 𝑦))) |
11 | | remulcl 10814 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
12 | 11 | ad2ant2r 747 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) → (𝑥 · 𝑦) ∈ ℝ) |
13 | | 1t1e1 11992 |
. . . . . . . . . 10
⊢ (1
· 1) = 1 |
14 | | 1re 10833 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
15 | | 0le1 11355 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
1 |
16 | 14, 15 | pm3.2i 474 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℝ ∧ 0 ≤ 1) |
17 | 16 | jctl 527 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → ((1
∈ ℝ ∧ 0 ≤ 1) ∧ 𝑥 ∈ ℝ)) |
18 | 16 | jctl 527 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → ((1
∈ ℝ ∧ 0 ≤ 1) ∧ 𝑦 ∈ ℝ)) |
19 | | lemul12a 11690 |
. . . . . . . . . . . 12
⊢ ((((1
∈ ℝ ∧ 0 ≤ 1) ∧ 𝑥 ∈ ℝ) ∧ ((1 ∈ ℝ
∧ 0 ≤ 1) ∧ 𝑦
∈ ℝ)) → ((1 ≤ 𝑥 ∧ 1 ≤ 𝑦) → (1 · 1) ≤ (𝑥 · 𝑦))) |
20 | 17, 18, 19 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((1 ≤
𝑥 ∧ 1 ≤ 𝑦) → (1 · 1) ≤
(𝑥 · 𝑦))) |
21 | 20 | imp 410 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (1 ≤
𝑥 ∧ 1 ≤ 𝑦)) → (1 · 1) ≤
(𝑥 · 𝑦)) |
22 | 13, 21 | eqbrtrrid 5089 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (1 ≤
𝑥 ∧ 1 ≤ 𝑦)) → 1 ≤ (𝑥 · 𝑦)) |
23 | 22 | an4s 660 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) → 1 ≤ (𝑥 · 𝑦)) |
24 | 10, 12, 23 | elrabd 3604 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) ∧ (𝑦 ∈ ℝ ∧ 1 ≤
𝑦)) → (𝑥 · 𝑦) ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧}) |
25 | 7, 9, 24 | syl2anb 601 |
. . . . . 6
⊢ ((𝑥 ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧} ∧ 𝑦 ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧}) → (𝑥 · 𝑦) ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧}) |
26 | | 1le1 11460 |
. . . . . . 7
⊢ 1 ≤
1 |
27 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑧 = 1 → (1 ≤ 𝑧 ↔ 1 ≤
1)) |
28 | 27 | elrab 3602 |
. . . . . . 7
⊢ (1 ∈
{𝑧 ∈ ℝ ∣ 1
≤ 𝑧} ↔ (1 ∈
ℝ ∧ 1 ≤ 1)) |
29 | 14, 26, 28 | mpbir2an 711 |
. . . . . 6
⊢ 1 ∈
{𝑧 ∈ ℝ ∣ 1
≤ 𝑧} |
30 | 5, 25, 29 | expcllem 13646 |
. . . . 5
⊢ ((𝐴 ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧} ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧}) |
31 | 2, 30 | sylanbr 585 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧}) |
32 | 31 | 3impa 1112 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴 ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧}) |
33 | 32 | 3com23 1128 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0
∧ 1 ≤ 𝐴) →
(𝐴↑𝑁) ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧}) |
34 | | breq2 5057 |
. . . 4
⊢ (𝑧 = (𝐴↑𝑁) → (1 ≤ 𝑧 ↔ 1 ≤ (𝐴↑𝑁))) |
35 | 34 | elrab 3602 |
. . 3
⊢ ((𝐴↑𝑁) ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧} ↔ ((𝐴↑𝑁) ∈ ℝ ∧ 1 ≤ (𝐴↑𝑁))) |
36 | 35 | simprbi 500 |
. 2
⊢ ((𝐴↑𝑁) ∈ {𝑧 ∈ ℝ ∣ 1 ≤ 𝑧} → 1 ≤ (𝐴↑𝑁)) |
37 | 33, 36 | syl 17 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0
∧ 1 ≤ 𝐴) → 1
≤ (𝐴↑𝑁)) |