Step |
Hyp |
Ref |
Expression |
1 |
|
nn0re |
⊢ ( 𝐶 ∈ ℕ0 → 𝐶 ∈ ℝ ) |
2 |
1
|
adantl |
⊢ ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℝ ) |
3 |
2
|
adantr |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ∈ ℝ ) |
4 |
|
simpr |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 ) |
5 |
|
simpr |
⊢ ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 ) |
6 |
5
|
adantr |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 ) |
7 |
4 6
|
nn0addcld |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 𝐶 ) ∈ ℕ0 ) |
8 |
7
|
nn0red |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 𝐶 ) ∈ ℝ ) |
9 |
|
nnnn0 |
⊢ ( 𝑌 ∈ ℕ → 𝑌 ∈ ℕ0 ) |
10 |
9
|
ad2antrr |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑌 ∈ ℕ0 ) |
11 |
7 10
|
nn0mulcld |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 𝐶 ) · 𝑌 ) ∈ ℕ0 ) |
12 |
11
|
nn0red |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 𝐶 ) · 𝑌 ) ∈ ℝ ) |
13 |
|
nn0ge0 |
⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 ) |
14 |
13
|
adantl |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝑁 ) |
15 |
6
|
nn0red |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ∈ ℝ ) |
16 |
4
|
nn0red |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ ) |
17 |
15 16
|
addge02d |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 ≤ 𝑁 ↔ 𝐶 ≤ ( 𝑁 + 𝐶 ) ) ) |
18 |
14 17
|
mpbid |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ≤ ( 𝑁 + 𝐶 ) ) |
19 |
|
simpll |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑌 ∈ ℕ ) |
20 |
19
|
nnred |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑌 ∈ ℝ ) |
21 |
7
|
nn0ge0d |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ ( 𝑁 + 𝐶 ) ) |
22 |
|
nnge1 |
⊢ ( 𝑌 ∈ ℕ → 1 ≤ 𝑌 ) |
23 |
22
|
ad2antrr |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 1 ≤ 𝑌 ) |
24 |
8 20 21 23
|
lemulge11d |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 𝐶 ) ≤ ( ( 𝑁 + 𝐶 ) · 𝑌 ) ) |
25 |
3 8 12 18 24
|
letrd |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ≤ ( ( 𝑁 + 𝐶 ) · 𝑌 ) ) |
26 |
|
nn0sub |
⊢ ( ( 𝐶 ∈ ℕ0 ∧ ( ( 𝑁 + 𝐶 ) · 𝑌 ) ∈ ℕ0 ) → ( 𝐶 ≤ ( ( 𝑁 + 𝐶 ) · 𝑌 ) ↔ ( ( ( 𝑁 + 𝐶 ) · 𝑌 ) − 𝐶 ) ∈ ℕ0 ) ) |
27 |
6 11 26
|
syl2anc |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐶 ≤ ( ( 𝑁 + 𝐶 ) · 𝑌 ) ↔ ( ( ( 𝑁 + 𝐶 ) · 𝑌 ) − 𝐶 ) ∈ ℕ0 ) ) |
28 |
25 27
|
mpbid |
⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑁 + 𝐶 ) · 𝑌 ) − 𝐶 ) ∈ ℕ0 ) |