Step |
Hyp |
Ref |
Expression |
1 |
|
id |
⊢ ( 𝑎 = 0 → 𝑎 = 0 ) |
2 |
|
oveq2 |
⊢ ( 𝑎 = 0 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 0 ) ) |
3 |
1 2
|
breq12d |
⊢ ( 𝑎 = 0 → ( 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 0 ≤ ( 𝐴 Yrm 0 ) ) ) |
4 |
3
|
imbi2d |
⊢ ( 𝑎 = 0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ ( 𝐴 Yrm 0 ) ) ) ) |
5 |
|
id |
⊢ ( 𝑎 = 𝑏 → 𝑎 = 𝑏 ) |
6 |
|
oveq2 |
⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) ) |
7 |
5 6
|
breq12d |
⊢ ( 𝑎 = 𝑏 → ( 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) ) |
8 |
7
|
imbi2d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) ) ) |
9 |
|
id |
⊢ ( 𝑎 = ( 𝑏 + 1 ) → 𝑎 = ( 𝑏 + 1 ) ) |
10 |
|
oveq2 |
⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) |
11 |
9 10
|
breq12d |
⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ↔ ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) |
12 |
11
|
imbi2d |
⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) ) |
13 |
|
id |
⊢ ( 𝑎 = 𝑁 → 𝑎 = 𝑁 ) |
14 |
|
oveq2 |
⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑁 ) ) |
15 |
13 14
|
breq12d |
⊢ ( 𝑎 = 𝑁 → ( 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ↔ 𝑁 ≤ ( 𝐴 Yrm 𝑁 ) ) ) |
16 |
15
|
imbi2d |
⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑎 ≤ ( 𝐴 Yrm 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( 𝐴 Yrm 𝑁 ) ) ) ) |
17 |
|
0le0 |
⊢ 0 ≤ 0 |
18 |
|
rmy0 |
⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 ) |
19 |
17 18
|
breqtrrid |
⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ ( 𝐴 Yrm 0 ) ) |
20 |
|
nn0z |
⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ ) |
21 |
20
|
3ad2ant1 |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝑏 ∈ ℤ ) |
22 |
21
|
peano2zd |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 + 1 ) ∈ ℤ ) |
23 |
22
|
zred |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 + 1 ) ∈ ℝ ) |
24 |
|
simp2 |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) |
25 |
|
frmy |
⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ |
26 |
25
|
fovcl |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ ) |
27 |
24 21 26
|
syl2anc |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ ) |
28 |
27
|
peano2zd |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( ( 𝐴 Yrm 𝑏 ) + 1 ) ∈ ℤ ) |
29 |
28
|
zred |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( ( 𝐴 Yrm 𝑏 ) + 1 ) ∈ ℝ ) |
30 |
25
|
fovcl |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℤ ) |
31 |
24 22 30
|
syl2anc |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℤ ) |
32 |
31
|
zred |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ ) |
33 |
|
nn0re |
⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℝ ) |
34 |
33
|
3ad2ant1 |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝑏 ∈ ℝ ) |
35 |
27
|
zred |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm 𝑏 ) ∈ ℝ ) |
36 |
|
1red |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 1 ∈ ℝ ) |
37 |
|
simp3 |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) |
38 |
34 35 36 37
|
leadd1dd |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 + 1 ) ≤ ( ( 𝐴 Yrm 𝑏 ) + 1 ) ) |
39 |
34
|
ltp1d |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → 𝑏 < ( 𝑏 + 1 ) ) |
40 |
|
ltrmy |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝑏 < ( 𝑏 + 1 ) ↔ ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) |
41 |
24 21 22 40
|
syl3anc |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 < ( 𝑏 + 1 ) ↔ ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) |
42 |
39 41
|
mpbid |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) |
43 |
|
zltp1le |
⊢ ( ( ( 𝐴 Yrm 𝑏 ) ∈ ℤ ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℤ ) → ( ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) ↔ ( ( 𝐴 Yrm 𝑏 ) + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) |
44 |
27 31 43
|
syl2anc |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( ( 𝐴 Yrm 𝑏 ) < ( 𝐴 Yrm ( 𝑏 + 1 ) ) ↔ ( ( 𝐴 Yrm 𝑏 ) + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) |
45 |
42 44
|
mpbid |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( ( 𝐴 Yrm 𝑏 ) + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) |
46 |
23 29 32 38 45
|
letrd |
⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) |
47 |
46
|
3exp |
⊢ ( 𝑏 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) → ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) ) |
48 |
47
|
a2d |
⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑏 ≤ ( 𝐴 Yrm 𝑏 ) ) → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑏 + 1 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) ) |
49 |
4 8 12 16 19 48
|
nn0ind |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( 𝐴 Yrm 𝑁 ) ) ) |
50 |
49
|
impcom |
⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ≤ ( 𝐴 Yrm 𝑁 ) ) |