Proof of Theorem seqf1olem1
Step | Hyp | Ref
| Expression |
1 | | seqf1olem.7 |
. 2
⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
2 | | fvexd 6789 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ V) |
3 | | fvex 6787 |
. . . 4
⊢ (◡𝐹‘𝑥) ∈ V |
4 | | ovex 7308 |
. . . 4
⊢ ((◡𝐹‘𝑥) − 1) ∈ V |
5 | 3, 4 | ifex 4509 |
. . 3
⊢ if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ∈ V |
6 | 5 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ∈ V) |
7 | | iftrue 4465 |
. . . . . . . . 9
⊢ (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘) |
8 | 7 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘)) |
9 | 8 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘))) |
10 | 9 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘))) |
11 | | simprr 770 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 = (𝐹‘𝑘)) |
12 | | elfzelz 13256 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ) |
13 | 12 | zred 12426 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ) |
14 | 13 | ad2antlr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ ℝ) |
15 | | simprl 768 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 < 𝐾) |
16 | 14, 15 | gtned 11110 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐾 ≠ 𝑘) |
17 | | seqf1olem.5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
18 | | f1of 6716 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
20 | 19 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
21 | | fzssp1 13299 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) |
22 | | simplr 766 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...𝑁)) |
23 | 21, 22 | sselid 3919 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
24 | 20, 23 | ffvelrnd 6962 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1))) |
25 | | seqf1o.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
26 | | elfzp1 13306 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))) |
28 | 27 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))) |
29 | 24, 28 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1))) |
30 | 29 | ord 861 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → (𝐹‘𝑘) = (𝑁 + 1))) |
31 | 17 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
32 | | f1ocnvfv 7150 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = 𝑘)) |
33 | 31, 23, 32 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = 𝑘)) |
34 | | seqf1olem.8 |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (◡𝐹‘(𝑁 + 1)) |
35 | 34 | eqeq1i 2743 |
. . . . . . . . . . . . 13
⊢ (𝐾 = 𝑘 ↔ (◡𝐹‘(𝑁 + 1)) = 𝑘) |
36 | 33, 35 | syl6ibr 251 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → 𝐾 = 𝑘)) |
37 | 30, 36 | syld 47 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘)) |
38 | 37 | necon1ad 2960 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐾 ≠ 𝑘 → (𝐹‘𝑘) ∈ (𝑀...𝑁))) |
39 | 16, 38 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...𝑁)) |
40 | 11, 39 | eqeltrd 2839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 ∈ (𝑀...𝑁)) |
41 | 11 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) = 𝑥) |
42 | | f1ocnvfv 7150 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = 𝑥 → (◡𝐹‘𝑥) = 𝑘)) |
43 | 31, 23, 42 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = 𝑥 → (◡𝐹‘𝑥) = 𝑘)) |
44 | 41, 43 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (◡𝐹‘𝑥) = 𝑘) |
45 | 44, 15 | eqbrtrd 5096 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (◡𝐹‘𝑥) < 𝐾) |
46 | | iftrue 4465 |
. . . . . . . . . 10
⊢ ((◡𝐹‘𝑥) < 𝐾 → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = (◡𝐹‘𝑥)) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = (◡𝐹‘𝑥)) |
48 | 47, 44 | eqtr2d 2779 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))) |
49 | 40, 48 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)))) |
50 | 49 | expr 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘𝑘) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
51 | 10, 50 | sylbid 239 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
52 | | iffalse 4468 |
. . . . . . . . 9
⊢ (¬
𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1)) |
53 | 52 | fveq2d 6778 |
. . . . . . . 8
⊢ (¬
𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
54 | 53 | eqeq2d 2749 |
. . . . . . 7
⊢ (¬
𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1)))) |
55 | 54 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1)))) |
56 | | simprr 770 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 = (𝐹‘(𝑘 + 1))) |
57 | | f1ocnv 6728 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
58 | 17, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
59 | | f1of1 6715 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1))) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1))) |
61 | | f1f 6670 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
63 | | peano2uz 12641 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
64 | 25, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
65 | | eluzfz2 13264 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
67 | 62, 66 | ffvelrnd 6962 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1))) |
68 | 34, 67 | eqeltrid 2843 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ (𝑀...(𝑁 + 1))) |
69 | 68 | elfzelzd 13257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℤ) |
70 | 69 | zred 12426 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℝ) |
71 | 70 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ) |
72 | 13 | ad2antlr 724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ) |
73 | | peano2re 11148 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ) |
75 | | simprl 768 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾) |
76 | 71, 72, 75 | nltled 11125 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≤ 𝑘) |
77 | 72 | ltp1d 11905 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1)) |
78 | 71, 72, 74, 76, 77 | lelttrd 11133 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1)) |
79 | 71, 78 | ltned 11111 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1)) |
80 | 19 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
81 | | fzp1elp1 13309 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) |
82 | 81 | ad2antlr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) |
83 | 80, 82 | ffvelrnd 6962 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1))) |
84 | | elfzp1 13306 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))) |
85 | 25, 84 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))) |
86 | 85 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))) |
87 | 83, 86 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))) |
88 | 87 | ord 861 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1))) |
89 | 17 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
90 | | f1ocnvfv 7150 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = (𝑘 + 1))) |
91 | 89, 82, 90 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = (𝑘 + 1))) |
92 | 34 | eqeq1i 2743 |
. . . . . . . . . . . . 13
⊢ (𝐾 = (𝑘 + 1) ↔ (◡𝐹‘(𝑁 + 1)) = (𝑘 + 1)) |
93 | 91, 92 | syl6ibr 251 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → 𝐾 = (𝑘 + 1))) |
94 | 88, 93 | syld 47 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1))) |
95 | 94 | necon1ad 2960 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))) |
96 | 79, 95 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁)) |
97 | 56, 96 | eqeltrd 2839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁)) |
98 | 56 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥) |
99 | | f1ocnvfv 7150 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (◡𝐹‘𝑥) = (𝑘 + 1))) |
100 | 89, 82, 99 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (◡𝐹‘𝑥) = (𝑘 + 1))) |
101 | 98, 100 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (◡𝐹‘𝑥) = (𝑘 + 1)) |
102 | 101 | breq1d 5084 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((◡𝐹‘𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾)) |
103 | | lttr 11051 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾)) |
104 | 72, 74, 71, 103 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾)) |
105 | 77, 104 | mpand 692 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾 → 𝑘 < 𝐾)) |
106 | 102, 105 | sylbid 239 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((◡𝐹‘𝑥) < 𝐾 → 𝑘 < 𝐾)) |
107 | 75, 106 | mtod 197 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (◡𝐹‘𝑥) < 𝐾) |
108 | | iffalse 4468 |
. . . . . . . . . 10
⊢ (¬
(◡𝐹‘𝑥) < 𝐾 → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = ((◡𝐹‘𝑥) − 1)) |
109 | 107, 108 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = ((◡𝐹‘𝑥) − 1)) |
110 | 101 | oveq1d 7290 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((◡𝐹‘𝑥) − 1) = ((𝑘 + 1) − 1)) |
111 | 72 | recnd 11003 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ) |
112 | | ax-1cn 10929 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
113 | | pncan 11227 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
114 | 111, 112,
113 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘) |
115 | 109, 110,
114 | 3eqtrrd 2783 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))) |
116 | 97, 115 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)))) |
117 | 116 | expr 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
118 | 55, 117 | sylbid 239 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
119 | 51, 118 | pm2.61dan 810 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
120 | 119 | expimpd 454 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
121 | 46 | eqeq2d 2749 |
. . . . . . 7
⊢ ((◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (◡𝐹‘𝑥))) |
122 | 121 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (◡𝐹‘𝑥))) |
123 | | eluzel2 12587 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
124 | 25, 123 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
125 | 124 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑀 ∈ ℤ) |
126 | | eluzelz 12592 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
127 | 25, 126 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
128 | 127 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑁 ∈ ℤ) |
129 | | simprr 770 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 = (◡𝐹‘𝑥)) |
130 | 62 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
131 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...𝑁)) |
132 | 21, 131 | sselid 3919 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
133 | 130, 132 | ffvelrnd 6962 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1))) |
134 | 129, 133 | eqeltrd 2839 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
135 | 134 | elfzelzd 13257 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ ℤ) |
136 | | elfzle1 13259 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝑘) |
137 | 134, 136 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑀 ≤ 𝑘) |
138 | 135 | zred 12426 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ ℝ) |
139 | 70 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝐾 ∈ ℝ) |
140 | 127 | peano2zd 12429 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
141 | 140 | zred 12426 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) |
142 | 141 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑁 + 1) ∈ ℝ) |
143 | | simprl 768 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (◡𝐹‘𝑥) < 𝐾) |
144 | 129, 143 | eqbrtrd 5096 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 < 𝐾) |
145 | | elfzle2 13260 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1)) |
146 | 68, 145 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ≤ (𝑁 + 1)) |
147 | 146 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝐾 ≤ (𝑁 + 1)) |
148 | 138, 139,
142, 144, 147 | ltletrd 11135 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 < (𝑁 + 1)) |
149 | | zleltp1 12371 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1))) |
150 | 135, 128,
149 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1))) |
151 | 148, 150 | mpbird 256 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ≤ 𝑁) |
152 | 125, 128,
135, 137, 151 | elfzd 13247 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...𝑁)) |
153 | 144, 8 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘)) |
154 | 129 | fveq2d 6778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝐹‘𝑘) = (𝐹‘(◡𝐹‘𝑥))) |
155 | 17 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
156 | | f1ocnvfv2 7149 |
. . . . . . . . . 10
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
157 | 155, 132,
156 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
158 | 153, 154,
157 | 3eqtrrd 2783 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
159 | 152, 158 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))) |
160 | 159 | expr 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = (◡𝐹‘𝑥) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
161 | 122, 160 | sylbid 239 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
162 | 108 | eqeq2d 2749 |
. . . . . . 7
⊢ (¬
(◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((◡𝐹‘𝑥) − 1))) |
163 | 162 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((◡𝐹‘𝑥) − 1))) |
164 | 124 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℤ) |
165 | 127 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℤ) |
166 | | simprr 770 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 = ((◡𝐹‘𝑥) − 1)) |
167 | 62 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
168 | | simplr 766 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...𝑁)) |
169 | 21, 168 | sselid 3919 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
170 | 167, 169 | ffvelrnd 6962 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1))) |
171 | 170 | elfzelzd 13257 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ ℤ) |
172 | | peano2zm 12363 |
. . . . . . . . . . 11
⊢ ((◡𝐹‘𝑥) ∈ ℤ → ((◡𝐹‘𝑥) − 1) ∈ ℤ) |
173 | 171, 172 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘𝑥) − 1) ∈ ℤ) |
174 | 166, 173 | eqeltrd 2839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℤ) |
175 | 124 | zred 12426 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
176 | 175 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℝ) |
177 | 70 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℝ) |
178 | 174 | zred 12426 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℝ) |
179 | | elfzle1 13259 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝐾) |
180 | 68, 179 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≤ 𝐾) |
181 | 180 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝐾) |
182 | 171 | zred 12426 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ ℝ) |
183 | | simprl 768 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ¬ (◡𝐹‘𝑥) < 𝐾) |
184 | 177, 182,
183 | nltled 11125 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≤ (◡𝐹‘𝑥)) |
185 | | elfzelz 13256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ) |
186 | 185 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ) |
187 | 186 | zred 12426 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ) |
188 | 127 | zred 12426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℝ) |
189 | 188 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ) |
190 | 141 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ) |
191 | | elfzle2 13260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ≤ 𝑁) |
192 | 191 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝑁) |
193 | 189 | ltp1d 11905 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1)) |
194 | 187, 189,
190, 192, 193 | lelttrd 11133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1)) |
195 | 187, 194 | gtned 11110 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ≠ 𝑥) |
196 | 195 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ≠ 𝑥) |
197 | 60 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1))) |
198 | 66 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
199 | | f1fveq 7135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((◡𝐹‘(𝑁 + 1)) = (◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥)) |
200 | 197, 198,
169, 199 | syl12anc 834 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘(𝑁 + 1)) = (◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥)) |
201 | 200 | necon3bid 2988 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘(𝑁 + 1)) ≠ (◡𝐹‘𝑥) ↔ (𝑁 + 1) ≠ 𝑥)) |
202 | 196, 201 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘(𝑁 + 1)) ≠ (◡𝐹‘𝑥)) |
203 | 34 | neeq1i 3008 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ≠ (◡𝐹‘𝑥) ↔ (◡𝐹‘(𝑁 + 1)) ≠ (◡𝐹‘𝑥)) |
204 | 202, 203 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≠ (◡𝐹‘𝑥)) |
205 | 204 | necomd 2999 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ≠ 𝐾) |
206 | 177, 182,
184, 205 | leneltd 11129 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 < (◡𝐹‘𝑥)) |
207 | 69 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℤ) |
208 | | zltlem1 12373 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ (◡𝐹‘𝑥) ∈ ℤ) → (𝐾 < (◡𝐹‘𝑥) ↔ 𝐾 ≤ ((◡𝐹‘𝑥) − 1))) |
209 | 207, 171,
208 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐾 < (◡𝐹‘𝑥) ↔ 𝐾 ≤ ((◡𝐹‘𝑥) − 1))) |
210 | 206, 209 | mpbid 231 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≤ ((◡𝐹‘𝑥) − 1)) |
211 | 210, 166 | breqtrrd 5102 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≤ 𝑘) |
212 | 176, 177,
178, 181, 211 | letrd 11132 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝑘) |
213 | | elfzle2 13260 |
. . . . . . . . . . . 12
⊢ ((◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) → (◡𝐹‘𝑥) ≤ (𝑁 + 1)) |
214 | 170, 213 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ≤ (𝑁 + 1)) |
215 | 188 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℝ) |
216 | | 1re 10975 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
217 | | lesubadd 11447 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧
𝑁 ∈ ℝ) →
(((◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (◡𝐹‘𝑥) ≤ (𝑁 + 1))) |
218 | 216, 217 | mp3an2 1448 |
. . . . . . . . . . . 12
⊢ (((◡𝐹‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (◡𝐹‘𝑥) ≤ (𝑁 + 1))) |
219 | 182, 215,
218 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (((◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (◡𝐹‘𝑥) ≤ (𝑁 + 1))) |
220 | 214, 219 | mpbird 256 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘𝑥) − 1) ≤ 𝑁) |
221 | 166, 220 | eqbrtrd 5096 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ≤ 𝑁) |
222 | 164, 165,
174, 212, 221 | elfzd 13247 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁)) |
223 | 177, 178,
211 | lensymd 11126 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ¬ 𝑘 < 𝐾) |
224 | 223, 53 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
225 | 166 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (((◡𝐹‘𝑥) − 1) + 1)) |
226 | 171 | zcnd 12427 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ ℂ) |
227 | | npcan 11230 |
. . . . . . . . . . . 12
⊢ (((◡𝐹‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((◡𝐹‘𝑥) − 1) + 1) = (◡𝐹‘𝑥)) |
228 | 226, 112,
227 | sylancl 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (((◡𝐹‘𝑥) − 1) + 1) = (◡𝐹‘𝑥)) |
229 | 225, 228 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (◡𝐹‘𝑥)) |
230 | 229 | fveq2d 6778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐹‘(𝑘 + 1)) = (𝐹‘(◡𝐹‘𝑥))) |
231 | 17 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
232 | 231, 169,
156 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
233 | 224, 230,
232 | 3eqtrrd 2783 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
234 | 222, 233 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))) |
235 | 234 | expr 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = ((◡𝐹‘𝑥) − 1) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
236 | 163, 235 | sylbid 239 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
237 | 161, 236 | pm2.61dan 810 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
238 | 237 | expimpd 454 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
239 | 120, 238 | impbid 211 |
. 2
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
240 | 1, 2, 6, 239 | f1od 7521 |
1
⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |