| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 0 → (𝐹‘𝑘) = (𝐹‘0)) | 
| 2 |  | id 22 | . . . . 5
⊢ (𝑘 = 0 → 𝑘 = 0) | 
| 3 | 1, 2 | breq12d 5156 | . . . 4
⊢ (𝑘 = 0 → ((𝐹‘𝑘) ≤ 𝑘 ↔ (𝐹‘0) ≤ 0)) | 
| 4 | 3 | imbi2d 340 | . . 3
⊢ (𝑘 = 0 → ((𝐹 ∈ 𝐴 → (𝐹‘𝑘) ≤ 𝑘) ↔ (𝐹 ∈ 𝐴 → (𝐹‘0) ≤ 0))) | 
| 5 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) | 
| 6 |  | id 22 | . . . . 5
⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛) | 
| 7 | 5, 6 | breq12d 5156 | . . . 4
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ≤ 𝑘 ↔ (𝐹‘𝑛) ≤ 𝑛)) | 
| 8 | 7 | imbi2d 340 | . . 3
⊢ (𝑘 = 𝑛 → ((𝐹 ∈ 𝐴 → (𝐹‘𝑘) ≤ 𝑘) ↔ (𝐹 ∈ 𝐴 → (𝐹‘𝑛) ≤ 𝑛))) | 
| 9 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) | 
| 10 |  | id 22 | . . . . 5
⊢ (𝑘 = (𝑛 + 1) → 𝑘 = (𝑛 + 1)) | 
| 11 | 9, 10 | breq12d 5156 | . . . 4
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ≤ 𝑘 ↔ (𝐹‘(𝑛 + 1)) ≤ (𝑛 + 1))) | 
| 12 | 11 | imbi2d 340 | . . 3
⊢ (𝑘 = (𝑛 + 1) → ((𝐹 ∈ 𝐴 → (𝐹‘𝑘) ≤ 𝑘) ↔ (𝐹 ∈ 𝐴 → (𝐹‘(𝑛 + 1)) ≤ (𝑛 + 1)))) | 
| 13 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁)) | 
| 14 |  | id 22 | . . . . 5
⊢ (𝑘 = 𝑁 → 𝑘 = 𝑁) | 
| 15 | 13, 14 | breq12d 5156 | . . . 4
⊢ (𝑘 = 𝑁 → ((𝐹‘𝑘) ≤ 𝑘 ↔ (𝐹‘𝑁) ≤ 𝑁)) | 
| 16 | 15 | imbi2d 340 | . . 3
⊢ (𝑘 = 𝑁 → ((𝐹 ∈ 𝐴 → (𝐹‘𝑘) ≤ 𝑘) ↔ (𝐹 ∈ 𝐴 → (𝐹‘𝑁) ≤ 𝑁))) | 
| 17 |  | qabsabv.a | . . . . 5
⊢ 𝐴 = (AbsVal‘𝑄) | 
| 18 |  | qrng.q | . . . . . 6
⊢ 𝑄 = (ℂfld
↾s ℚ) | 
| 19 | 18 | qrng0 27665 | . . . . 5
⊢ 0 =
(0g‘𝑄) | 
| 20 | 17, 19 | abv0 20824 | . . . 4
⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) = 0) | 
| 21 |  | 0le0 12367 | . . . 4
⊢ 0 ≤
0 | 
| 22 | 20, 21 | eqbrtrdi 5182 | . . 3
⊢ (𝐹 ∈ 𝐴 → (𝐹‘0) ≤ 0) | 
| 23 |  | nn0p1nn 12565 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) | 
| 24 | 23 | ad2antrl 728 | . . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝑛 + 1) ∈ ℕ) | 
| 25 |  | nnq 13004 | . . . . . . . . 9
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ∈
ℚ) | 
| 26 | 24, 25 | syl 17 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝑛 + 1) ∈ ℚ) | 
| 27 | 18 | qrngbas 27663 | . . . . . . . . 9
⊢ ℚ =
(Base‘𝑄) | 
| 28 | 17, 27 | abvcl 20817 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 + 1) ∈ ℚ) → (𝐹‘(𝑛 + 1)) ∈ ℝ) | 
| 29 | 26, 28 | syldan 591 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝐹‘(𝑛 + 1)) ∈ ℝ) | 
| 30 |  | nn0z 12638 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) | 
| 31 | 30 | ad2antrl 728 | . . . . . . . . . 10
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → 𝑛 ∈ ℤ) | 
| 32 |  | zq 12996 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℚ) | 
| 33 | 31, 32 | syl 17 | . . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → 𝑛 ∈ ℚ) | 
| 34 | 17, 27 | abvcl 20817 | . . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℚ) → (𝐹‘𝑛) ∈ ℝ) | 
| 35 | 33, 34 | syldan 591 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝐹‘𝑛) ∈ ℝ) | 
| 36 |  | peano2re 11434 | . . . . . . . 8
⊢ ((𝐹‘𝑛) ∈ ℝ → ((𝐹‘𝑛) + 1) ∈ ℝ) | 
| 37 | 35, 36 | syl 17 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → ((𝐹‘𝑛) + 1) ∈ ℝ) | 
| 38 | 31 | zred 12722 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → 𝑛 ∈ ℝ) | 
| 39 |  | peano2re 11434 | . . . . . . . 8
⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈
ℝ) | 
| 40 | 38, 39 | syl 17 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝑛 + 1) ∈ ℝ) | 
| 41 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → 𝐹 ∈ 𝐴) | 
| 42 |  | 1z 12647 | . . . . . . . . . 10
⊢ 1 ∈
ℤ | 
| 43 |  | zq 12996 | . . . . . . . . . 10
⊢ (1 ∈
ℤ → 1 ∈ ℚ) | 
| 44 | 42, 43 | mp1i 13 | . . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → 1 ∈ ℚ) | 
| 45 |  | qex 13003 | . . . . . . . . . . 11
⊢ ℚ
∈ V | 
| 46 |  | cnfldadd 21370 | . . . . . . . . . . . 12
⊢  + =
(+g‘ℂfld) | 
| 47 | 18, 46 | ressplusg 17334 | . . . . . . . . . . 11
⊢ (ℚ
∈ V → + = (+g‘𝑄)) | 
| 48 | 45, 47 | ax-mp 5 | . . . . . . . . . 10
⊢  + =
(+g‘𝑄) | 
| 49 | 17, 27, 48 | abvtri 20823 | . . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℚ ∧ 1 ∈ ℚ)
→ (𝐹‘(𝑛 + 1)) ≤ ((𝐹‘𝑛) + (𝐹‘1))) | 
| 50 | 41, 33, 44, 49 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝐹‘(𝑛 + 1)) ≤ ((𝐹‘𝑛) + (𝐹‘1))) | 
| 51 |  | ax-1ne0 11224 | . . . . . . . . . . 11
⊢ 1 ≠
0 | 
| 52 | 18 | qrng1 27666 | . . . . . . . . . . . 12
⊢ 1 =
(1r‘𝑄) | 
| 53 | 17, 52, 19 | abv1z 20825 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ 𝐴 ∧ 1 ≠ 0) → (𝐹‘1) = 1) | 
| 54 | 51, 53 | mpan2 691 | . . . . . . . . . 10
⊢ (𝐹 ∈ 𝐴 → (𝐹‘1) = 1) | 
| 55 | 54 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝐹‘1) = 1) | 
| 56 | 55 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → ((𝐹‘𝑛) + (𝐹‘1)) = ((𝐹‘𝑛) + 1)) | 
| 57 | 50, 56 | breqtrd 5169 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝐹‘(𝑛 + 1)) ≤ ((𝐹‘𝑛) + 1)) | 
| 58 |  | 1red 11262 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → 1 ∈ ℝ) | 
| 59 |  | simprr 773 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝐹‘𝑛) ≤ 𝑛) | 
| 60 | 35, 38, 58, 59 | leadd1dd 11877 | . . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → ((𝐹‘𝑛) + 1) ≤ (𝑛 + 1)) | 
| 61 | 29, 37, 40, 57, 60 | letrd 11418 | . . . . . 6
⊢ ((𝐹 ∈ 𝐴 ∧ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≤ 𝑛)) → (𝐹‘(𝑛 + 1)) ≤ (𝑛 + 1)) | 
| 62 | 61 | expr 456 | . . . . 5
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℕ0) → ((𝐹‘𝑛) ≤ 𝑛 → (𝐹‘(𝑛 + 1)) ≤ (𝑛 + 1))) | 
| 63 | 62 | expcom 413 | . . . 4
⊢ (𝑛 ∈ ℕ0
→ (𝐹 ∈ 𝐴 → ((𝐹‘𝑛) ≤ 𝑛 → (𝐹‘(𝑛 + 1)) ≤ (𝑛 + 1)))) | 
| 64 | 63 | a2d 29 | . . 3
⊢ (𝑛 ∈ ℕ0
→ ((𝐹 ∈ 𝐴 → (𝐹‘𝑛) ≤ 𝑛) → (𝐹 ∈ 𝐴 → (𝐹‘(𝑛 + 1)) ≤ (𝑛 + 1)))) | 
| 65 | 4, 8, 12, 16, 22, 64 | nn0ind 12713 | . 2
⊢ (𝑁 ∈ ℕ0
→ (𝐹 ∈ 𝐴 → (𝐹‘𝑁) ≤ 𝑁)) | 
| 66 | 65 | impcom 407 | 1
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0) → (𝐹‘𝑁) ≤ 𝑁) |