Proof of Theorem seqf1olem1
Step | Hyp | Ref
| Expression |
1 | | seqf1olem.7 |
. 2
⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
2 | | fvex 6113 |
. . 3
⊢ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ V |
3 | 2 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ V) |
4 | | fvex 6113 |
. . . 4
⊢ (◡𝐹‘𝑥) ∈ V |
5 | | ovex 6577 |
. . . 4
⊢ ((◡𝐹‘𝑥) − 1) ∈ V |
6 | 4, 5 | ifex 4106 |
. . 3
⊢ if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ∈ V |
7 | 6 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ∈ V) |
8 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘) |
9 | 8 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘)) |
10 | 9 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘))) |
11 | 10 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘))) |
12 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 = (𝐹‘𝑘)) |
13 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ) |
14 | 13 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ) |
15 | 14 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ ℝ) |
16 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 < 𝐾) |
17 | 15, 16 | gtned 10051 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐾 ≠ 𝑘) |
18 | | seqf1olem.5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
19 | | f1of 6050 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
21 | 20 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
22 | | fzssp1 12255 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) |
23 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...𝑁)) |
24 | 22, 23 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
25 | 21, 24 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1))) |
26 | | seqf1o.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
27 | | elfzp1 12261 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))) |
29 | 28 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))) |
30 | 25, 29 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1))) |
31 | 30 | ord 391 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → (𝐹‘𝑘) = (𝑁 + 1))) |
32 | 18 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
33 | | f1ocnvfv 6434 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = 𝑘)) |
34 | 32, 24, 33 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = 𝑘)) |
35 | | seqf1olem.8 |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (◡𝐹‘(𝑁 + 1)) |
36 | 35 | eqeq1i 2615 |
. . . . . . . . . . . . 13
⊢ (𝐾 = 𝑘 ↔ (◡𝐹‘(𝑁 + 1)) = 𝑘) |
37 | 34, 36 | syl6ibr 241 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → 𝐾 = 𝑘)) |
38 | 31, 37 | syld 46 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘)) |
39 | 38 | necon1ad 2799 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐾 ≠ 𝑘 → (𝐹‘𝑘) ∈ (𝑀...𝑁))) |
40 | 17, 39 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...𝑁)) |
41 | 12, 40 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 ∈ (𝑀...𝑁)) |
42 | 12 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) = 𝑥) |
43 | | f1ocnvfv 6434 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = 𝑥 → (◡𝐹‘𝑥) = 𝑘)) |
44 | 32, 24, 43 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = 𝑥 → (◡𝐹‘𝑥) = 𝑘)) |
45 | 42, 44 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (◡𝐹‘𝑥) = 𝑘) |
46 | 45, 16 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (◡𝐹‘𝑥) < 𝐾) |
47 | | iftrue 4042 |
. . . . . . . . . 10
⊢ ((◡𝐹‘𝑥) < 𝐾 → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = (◡𝐹‘𝑥)) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = (◡𝐹‘𝑥)) |
49 | 48, 45 | eqtr2d 2645 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))) |
50 | 41, 49 | jca 553 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)))) |
51 | 50 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘𝑘) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
52 | 11, 51 | sylbid 229 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
53 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1)) |
54 | 53 | fveq2d 6107 |
. . . . . . . 8
⊢ (¬
𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
55 | 54 | eqeq2d 2620 |
. . . . . . 7
⊢ (¬
𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1)))) |
56 | 55 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1)))) |
57 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 = (𝐹‘(𝑘 + 1))) |
58 | | f1ocnv 6062 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
59 | 18, 58 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
60 | | f1of1 6049 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1))) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1))) |
62 | | f1f 6014 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
64 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
65 | 26, 64 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
66 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
68 | 63, 67 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1))) |
69 | 35, 68 | syl5eqel 2692 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ (𝑀...(𝑁 + 1))) |
70 | | elfzelz 12213 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℤ) |
72 | 71 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℝ) |
73 | 72 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ) |
74 | 14 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ) |
75 | | peano2re 10088 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ) |
77 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾) |
78 | 73, 74 | lenltd 10062 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾 ≤ 𝑘 ↔ ¬ 𝑘 < 𝐾)) |
79 | 77, 78 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≤ 𝑘) |
80 | 74 | ltp1d 10833 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1)) |
81 | 73, 74, 76, 79, 80 | lelttrd 10074 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1)) |
82 | 73, 81 | ltned 10052 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1)) |
83 | 20 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
84 | | fzp1elp1 12264 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) |
85 | 84 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) |
86 | 83, 85 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1))) |
87 | | elfzp1 12261 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))) |
88 | 26, 87 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))) |
89 | 88 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))) |
90 | 86, 89 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))) |
91 | 90 | ord 391 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1))) |
92 | 18 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
93 | | f1ocnvfv 6434 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = (𝑘 + 1))) |
94 | 92, 85, 93 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = (𝑘 + 1))) |
95 | 35 | eqeq1i 2615 |
. . . . . . . . . . . . 13
⊢ (𝐾 = (𝑘 + 1) ↔ (◡𝐹‘(𝑁 + 1)) = (𝑘 + 1)) |
96 | 94, 95 | syl6ibr 241 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → 𝐾 = (𝑘 + 1))) |
97 | 91, 96 | syld 46 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1))) |
98 | 97 | necon1ad 2799 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))) |
99 | 82, 98 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁)) |
100 | 57, 99 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁)) |
101 | 57 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥) |
102 | | f1ocnvfv 6434 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (◡𝐹‘𝑥) = (𝑘 + 1))) |
103 | 92, 85, 102 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (◡𝐹‘𝑥) = (𝑘 + 1))) |
104 | 101, 103 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (◡𝐹‘𝑥) = (𝑘 + 1)) |
105 | 104 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((◡𝐹‘𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾)) |
106 | | lttr 9993 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾)) |
107 | 74, 76, 73, 106 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾)) |
108 | 80, 107 | mpand 707 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾 → 𝑘 < 𝐾)) |
109 | 105, 108 | sylbid 229 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((◡𝐹‘𝑥) < 𝐾 → 𝑘 < 𝐾)) |
110 | 77, 109 | mtod 188 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (◡𝐹‘𝑥) < 𝐾) |
111 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
(◡𝐹‘𝑥) < 𝐾 → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = ((◡𝐹‘𝑥) − 1)) |
112 | 110, 111 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = ((◡𝐹‘𝑥) − 1)) |
113 | 104 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((◡𝐹‘𝑥) − 1) = ((𝑘 + 1) − 1)) |
114 | 74 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ) |
115 | | ax-1cn 9873 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
116 | | pncan 10166 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
117 | 114, 115,
116 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘) |
118 | 112, 113,
117 | 3eqtrrd 2649 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))) |
119 | 100, 118 | jca 553 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)))) |
120 | 119 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
121 | 56, 120 | sylbid 229 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
122 | 52, 121 | pm2.61dan 828 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
123 | 122 | expimpd 627 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
124 | 47 | eqeq2d 2620 |
. . . . . . 7
⊢ ((◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (◡𝐹‘𝑥))) |
125 | 124 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (◡𝐹‘𝑥))) |
126 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 = (◡𝐹‘𝑥)) |
127 | 63 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
128 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...𝑁)) |
129 | 22, 128 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
130 | 127, 129 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1))) |
131 | 126, 130 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
132 | | elfzle1 12215 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝑘) |
133 | 131, 132 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑀 ≤ 𝑘) |
134 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
135 | 131, 134 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ ℤ) |
136 | 135 | zred 11358 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ ℝ) |
137 | 72 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝐾 ∈ ℝ) |
138 | | eluzelz 11573 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
139 | 26, 138 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
140 | 139 | peano2zd 11361 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
141 | 140 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) |
142 | 141 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑁 + 1) ∈ ℝ) |
143 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (◡𝐹‘𝑥) < 𝐾) |
144 | 126, 143 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 < 𝐾) |
145 | | elfzle2 12216 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1)) |
146 | 69, 145 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ≤ (𝑁 + 1)) |
147 | 146 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝐾 ≤ (𝑁 + 1)) |
148 | 136, 137,
142, 144, 147 | ltletrd 10076 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 < (𝑁 + 1)) |
149 | 139 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑁 ∈ ℤ) |
150 | | zleltp1 11305 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1))) |
151 | 135, 149,
150 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1))) |
152 | 148, 151 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ≤ 𝑁) |
153 | | eluzel2 11568 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
154 | 26, 153 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
155 | 154 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑀 ∈ ℤ) |
156 | | elfz 12203 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
157 | 135, 155,
149, 156 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
158 | 133, 152,
157 | mpbir2and 959 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...𝑁)) |
159 | 144, 9 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘)) |
160 | 126 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝐹‘𝑘) = (𝐹‘(◡𝐹‘𝑥))) |
161 | 18 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
162 | | f1ocnvfv2 6433 |
. . . . . . . . . 10
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
163 | 161, 129,
162 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
164 | 159, 160,
163 | 3eqtrrd 2649 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
165 | 158, 164 | jca 553 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))) |
166 | 165 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = (◡𝐹‘𝑥) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
167 | 125, 166 | sylbid 229 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
168 | 111 | eqeq2d 2620 |
. . . . . . 7
⊢ (¬
(◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((◡𝐹‘𝑥) − 1))) |
169 | 168 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((◡𝐹‘𝑥) − 1))) |
170 | 154 | zred 11358 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
171 | 170 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℝ) |
172 | 72 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℝ) |
173 | | simprr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 = ((◡𝐹‘𝑥) − 1)) |
174 | 63 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
175 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...𝑁)) |
176 | 22, 175 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
177 | 174, 176 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1))) |
178 | | elfzelz 12213 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) → (◡𝐹‘𝑥) ∈ ℤ) |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ ℤ) |
180 | | peano2zm 11297 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹‘𝑥) ∈ ℤ → ((◡𝐹‘𝑥) − 1) ∈ ℤ) |
181 | 179, 180 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘𝑥) − 1) ∈ ℤ) |
182 | 173, 181 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℤ) |
183 | 182 | zred 11358 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℝ) |
184 | | elfzle1 12215 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝐾) |
185 | 69, 184 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≤ 𝐾) |
186 | 185 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝐾) |
187 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ¬ (◡𝐹‘𝑥) < 𝐾) |
188 | 179 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ ℝ) |
189 | 172, 188 | lenltd 10062 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐾 ≤ (◡𝐹‘𝑥) ↔ ¬ (◡𝐹‘𝑥) < 𝐾)) |
190 | 187, 189 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≤ (◡𝐹‘𝑥)) |
191 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ) |
192 | 191 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ) |
193 | 192 | zred 11358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ) |
194 | 139 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℝ) |
195 | 194 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ) |
196 | 141 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ) |
197 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ≤ 𝑁) |
198 | 197 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝑁) |
199 | 195 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1)) |
200 | 193, 195,
196, 198, 199 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1)) |
201 | 193, 200 | gtned 10051 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ≠ 𝑥) |
202 | 201 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ≠ 𝑥) |
203 | 61 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1))) |
204 | 67 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
205 | | f1fveq 6420 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((◡𝐹‘(𝑁 + 1)) = (◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥)) |
206 | 203, 204,
176, 205 | syl12anc 1316 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘(𝑁 + 1)) = (◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥)) |
207 | 206 | necon3bid 2826 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘(𝑁 + 1)) ≠ (◡𝐹‘𝑥) ↔ (𝑁 + 1) ≠ 𝑥)) |
208 | 202, 207 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘(𝑁 + 1)) ≠ (◡𝐹‘𝑥)) |
209 | 35 | neeq1i 2846 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ≠ (◡𝐹‘𝑥) ↔ (◡𝐹‘(𝑁 + 1)) ≠ (◡𝐹‘𝑥)) |
210 | 208, 209 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≠ (◡𝐹‘𝑥)) |
211 | 210 | necomd 2837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ≠ 𝐾) |
212 | 172, 188 | ltlend 10061 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐾 < (◡𝐹‘𝑥) ↔ (𝐾 ≤ (◡𝐹‘𝑥) ∧ (◡𝐹‘𝑥) ≠ 𝐾))) |
213 | 190, 211,
212 | mpbir2and 959 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 < (◡𝐹‘𝑥)) |
214 | 71 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℤ) |
215 | | zltlem1 11307 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ (◡𝐹‘𝑥) ∈ ℤ) → (𝐾 < (◡𝐹‘𝑥) ↔ 𝐾 ≤ ((◡𝐹‘𝑥) − 1))) |
216 | 214, 179,
215 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐾 < (◡𝐹‘𝑥) ↔ 𝐾 ≤ ((◡𝐹‘𝑥) − 1))) |
217 | 213, 216 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≤ ((◡𝐹‘𝑥) − 1)) |
218 | 217, 173 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≤ 𝑘) |
219 | 171, 172,
183, 186, 218 | letrd 10073 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝑘) |
220 | | elfzle2 12216 |
. . . . . . . . . . . 12
⊢ ((◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) → (◡𝐹‘𝑥) ≤ (𝑁 + 1)) |
221 | 177, 220 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ≤ (𝑁 + 1)) |
222 | 194 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℝ) |
223 | | 1re 9918 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
224 | | lesubadd 10379 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧
𝑁 ∈ ℝ) →
(((◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (◡𝐹‘𝑥) ≤ (𝑁 + 1))) |
225 | 223, 224 | mp3an2 1404 |
. . . . . . . . . . . 12
⊢ (((◡𝐹‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (◡𝐹‘𝑥) ≤ (𝑁 + 1))) |
226 | 188, 222,
225 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (((◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (◡𝐹‘𝑥) ≤ (𝑁 + 1))) |
227 | 221, 226 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘𝑥) − 1) ≤ 𝑁) |
228 | 173, 227 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ≤ 𝑁) |
229 | 154 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℤ) |
230 | 139 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℤ) |
231 | 182, 229,
230, 156 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
232 | 219, 228,
231 | mpbir2and 959 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁)) |
233 | 172, 183 | lenltd 10062 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐾 ≤ 𝑘 ↔ ¬ 𝑘 < 𝐾)) |
234 | 218, 233 | mpbid 221 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ¬ 𝑘 < 𝐾) |
235 | 234, 54 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
236 | 173 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (((◡𝐹‘𝑥) − 1) + 1)) |
237 | 179 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ ℂ) |
238 | | npcan 10169 |
. . . . . . . . . . . 12
⊢ (((◡𝐹‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((◡𝐹‘𝑥) − 1) + 1) = (◡𝐹‘𝑥)) |
239 | 237, 115,
238 | sylancl 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (((◡𝐹‘𝑥) − 1) + 1) = (◡𝐹‘𝑥)) |
240 | 236, 239 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (◡𝐹‘𝑥)) |
241 | 240 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐹‘(𝑘 + 1)) = (𝐹‘(◡𝐹‘𝑥))) |
242 | 18 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
243 | 242, 176,
162 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
244 | 235, 241,
243 | 3eqtrrd 2649 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
245 | 232, 244 | jca 553 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))) |
246 | 245 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = ((◡𝐹‘𝑥) − 1) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
247 | 169, 246 | sylbid 229 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
248 | 167, 247 | pm2.61dan 828 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
249 | 248 | expimpd 627 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
250 | 123, 249 | impbid 201 |
. 2
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
251 | 1, 3, 7, 250 | f1od 6783 |
1
⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |