Proof of Theorem seqf1olem1
Step | Hyp | Ref
| Expression |
1 | | seqf1olem.7 |
. 2
⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
2 | | fvexd 6553 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ V) |
3 | | fvex 6551 |
. . . 4
⊢ (◡𝐹‘𝑥) ∈ V |
4 | | ovex 7048 |
. . . 4
⊢ ((◡𝐹‘𝑥) − 1) ∈ V |
5 | 3, 4 | ifex 4429 |
. . 3
⊢ if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ∈ V |
6 | 5 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ∈ V) |
7 | | iftrue 4387 |
. . . . . . . . 9
⊢ (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘) |
8 | 7 | fveq2d 6542 |
. . . . . . . 8
⊢ (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘)) |
9 | 8 | eqeq2d 2805 |
. . . . . . 7
⊢ (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘))) |
10 | 9 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘))) |
11 | | simprr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 = (𝐹‘𝑘)) |
12 | | elfzelz 12758 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ) |
13 | 12 | zred 11936 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ) |
14 | 13 | ad2antlr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ ℝ) |
15 | | simprl 767 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 < 𝐾) |
16 | 14, 15 | gtned 10622 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐾 ≠ 𝑘) |
17 | | seqf1olem.5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
18 | | f1of 6483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
20 | 19 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
21 | | fzssp1 12800 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) |
22 | | simplr 765 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...𝑁)) |
23 | 21, 22 | sseldi 3887 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
24 | 20, 23 | ffvelrnd 6717 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1))) |
25 | | seqf1o.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
26 | | elfzp1 12807 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))) |
28 | 27 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))) |
29 | 24, 28 | mpbid 233 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1))) |
30 | 29 | ord 859 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → (𝐹‘𝑘) = (𝑁 + 1))) |
31 | 17 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
32 | | f1ocnvfv 6900 |
. . . . . . . . . . . . . 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 2800 |
. . . . . . . . . . . . 13
⊢ (𝐾 = 𝑘 ↔ (◡𝐹‘(𝑁 + 1)) = 𝑘) |
36 | 33, 35 | syl6ibr 253 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → 𝐾 = 𝑘)) |
37 | 30, 36 | syld 47 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘)) |
38 | 37 | necon1ad 3001 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐾 ≠ 𝑘 → (𝐹‘𝑘) ∈ (𝑀...𝑁))) |
39 | 16, 38 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...𝑁)) |
40 | 11, 39 | eqeltrd 2883 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 ∈ (𝑀...𝑁)) |
41 | 11 | eqcomd 2801 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) = 𝑥) |
42 | | f1ocnvfv 6900 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = 𝑥 → (◡𝐹‘𝑥) = 𝑘)) |
43 | 31, 23, 42 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = 𝑥 → (◡𝐹‘𝑥) = 𝑘)) |
44 | 41, 43 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (◡𝐹‘𝑥) = 𝑘) |
45 | 44, 15 | eqbrtrd 4984 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (◡𝐹‘𝑥) < 𝐾) |
46 | | iftrue 4387 |
. . . . . . . . . 10
⊢ ((◡𝐹‘𝑥) < 𝐾 → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = (◡𝐹‘𝑥)) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = (◡𝐹‘𝑥)) |
48 | 47, 44 | eqtr2d 2832 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))) |
49 | 40, 48 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)))) |
50 | 49 | expr 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘𝑘) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
51 | 10, 50 | sylbid 241 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
52 | | iffalse 4390 |
. . . . . . . . 9
⊢ (¬
𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1)) |
53 | 52 | fveq2d 6542 |
. . . . . . . 8
⊢ (¬
𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
54 | 53 | eqeq2d 2805 |
. . . . . . 7
⊢ (¬
𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1)))) |
55 | 54 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1)))) |
56 | | simprr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 = (𝐹‘(𝑘 + 1))) |
57 | | f1ocnv 6495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
58 | 17, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
59 | | f1of1 6482 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1))) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1))) |
61 | | f1f 6443 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
63 | | peano2uz 12150 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
64 | 25, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
65 | | eluzfz2 12765 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
67 | 62, 66 | ffvelrnd 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1))) |
68 | 34, 67 | syl5eqel 2887 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ (𝑀...(𝑁 + 1))) |
69 | | elfzelz 12758 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℤ) |
71 | 70 | zred 11936 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℝ) |
72 | 71 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ) |
73 | 13 | ad2antlr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ) |
74 | | peano2re 10660 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ) |
76 | | simprl 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾) |
77 | 72, 73, 76 | nltled 10637 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≤ 𝑘) |
78 | 73 | ltp1d 11418 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1)) |
79 | 72, 73, 75, 77, 78 | lelttrd 10645 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1)) |
80 | 72, 79 | ltned 10623 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1)) |
81 | 19 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
82 | | fzp1elp1 12810 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) |
83 | 82 | ad2antlr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) |
84 | 81, 83 | ffvelrnd 6717 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1))) |
85 | | elfzp1 12807 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))) |
86 | 25, 85 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))) |
87 | 86 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))) |
88 | 84, 87 | mpbid 233 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))) |
89 | 88 | ord 859 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1))) |
90 | 17 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
91 | | f1ocnvfv 6900 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = (𝑘 + 1))) |
92 | 90, 83, 91 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (◡𝐹‘(𝑁 + 1)) = (𝑘 + 1))) |
93 | 34 | eqeq1i 2800 |
. . . . . . . . . . . . 13
⊢ (𝐾 = (𝑘 + 1) ↔ (◡𝐹‘(𝑁 + 1)) = (𝑘 + 1)) |
94 | 92, 93 | syl6ibr 253 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → 𝐾 = (𝑘 + 1))) |
95 | 89, 94 | syld 47 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1))) |
96 | 95 | necon1ad 3001 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))) |
97 | 80, 96 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁)) |
98 | 56, 97 | eqeltrd 2883 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁)) |
99 | 56 | eqcomd 2801 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥) |
100 | | f1ocnvfv 6900 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (◡𝐹‘𝑥) = (𝑘 + 1))) |
101 | 90, 83, 100 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (◡𝐹‘𝑥) = (𝑘 + 1))) |
102 | 99, 101 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (◡𝐹‘𝑥) = (𝑘 + 1)) |
103 | 102 | breq1d 4972 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((◡𝐹‘𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾)) |
104 | | lttr 10564 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾)) |
105 | 73, 75, 72, 104 | syl3anc 1364 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾)) |
106 | 78, 105 | mpand 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾 → 𝑘 < 𝐾)) |
107 | 103, 106 | sylbid 241 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((◡𝐹‘𝑥) < 𝐾 → 𝑘 < 𝐾)) |
108 | 76, 107 | mtod 199 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (◡𝐹‘𝑥) < 𝐾) |
109 | | iffalse 4390 |
. . . . . . . . . 10
⊢ (¬
(◡𝐹‘𝑥) < 𝐾 → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = ((◡𝐹‘𝑥) − 1)) |
110 | 108, 109 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) = ((◡𝐹‘𝑥) − 1)) |
111 | 102 | oveq1d 7031 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((◡𝐹‘𝑥) − 1) = ((𝑘 + 1) − 1)) |
112 | 73 | recnd 10515 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ) |
113 | | ax-1cn 10441 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
114 | | pncan 10739 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
115 | 112, 113,
114 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘) |
116 | 110, 111,
115 | 3eqtrrd 2836 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))) |
117 | 98, 116 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)))) |
118 | 117 | expr 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
119 | 55, 118 | sylbid 241 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
120 | 51, 119 | pm2.61dan 809 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
121 | 120 | expimpd 454 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
122 | 46 | eqeq2d 2805 |
. . . . . . 7
⊢ ((◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (◡𝐹‘𝑥))) |
123 | 122 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (◡𝐹‘𝑥))) |
124 | | simprr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 = (◡𝐹‘𝑥)) |
125 | 62 | ad2antrr 722 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
126 | | simplr 765 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...𝑁)) |
127 | 21, 126 | sseldi 3887 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
128 | 125, 127 | ffvelrnd 6717 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1))) |
129 | 124, 128 | eqeltrd 2883 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
130 | | elfzle1 12760 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝑘) |
131 | 129, 130 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑀 ≤ 𝑘) |
132 | | elfzelz 12758 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
133 | 129, 132 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ ℤ) |
134 | 133 | zred 11936 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ ℝ) |
135 | 71 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝐾 ∈ ℝ) |
136 | | eluzelz 12103 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
137 | 25, 136 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
138 | 137 | peano2zd 11939 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
139 | 138 | zred 11936 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) |
140 | 139 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑁 + 1) ∈ ℝ) |
141 | | simprl 767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (◡𝐹‘𝑥) < 𝐾) |
142 | 124, 141 | eqbrtrd 4984 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 < 𝐾) |
143 | | elfzle2 12761 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1)) |
144 | 68, 143 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ≤ (𝑁 + 1)) |
145 | 144 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝐾 ≤ (𝑁 + 1)) |
146 | 134, 135,
140, 142, 145 | ltletrd 10647 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 < (𝑁 + 1)) |
147 | 137 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑁 ∈ ℤ) |
148 | | zleltp1 11882 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1))) |
149 | 133, 147,
148 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1))) |
150 | 146, 149 | mpbird 258 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ≤ 𝑁) |
151 | | eluzel2 12098 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
152 | 25, 151 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
153 | 152 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑀 ∈ ℤ) |
154 | | elfz 12748 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
155 | 133, 153,
147, 154 | syl3anc 1364 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
156 | 131, 150,
155 | mpbir2and 709 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...𝑁)) |
157 | 142, 8 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘)) |
158 | 124 | fveq2d 6542 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝐹‘𝑘) = (𝐹‘(◡𝐹‘𝑥))) |
159 | 17 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
160 | | f1ocnvfv2 6899 |
. . . . . . . . . 10
⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
161 | 159, 127,
160 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
162 | 157, 158,
161 | 3eqtrrd 2836 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
163 | 156, 162 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (◡𝐹‘𝑥))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))) |
164 | 163 | expr 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = (◡𝐹‘𝑥) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
165 | 123, 164 | sylbid 241 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
166 | 109 | eqeq2d 2805 |
. . . . . . 7
⊢ (¬
(◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((◡𝐹‘𝑥) − 1))) |
167 | 166 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((◡𝐹‘𝑥) − 1))) |
168 | 152 | zred 11936 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
169 | 168 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℝ) |
170 | 71 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℝ) |
171 | | simprr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 = ((◡𝐹‘𝑥) − 1)) |
172 | 62 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) |
173 | | simplr 765 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...𝑁)) |
174 | 21, 173 | sseldi 3887 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1))) |
175 | 172, 174 | ffvelrnd 6717 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1))) |
176 | | elfzelz 12758 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) → (◡𝐹‘𝑥) ∈ ℤ) |
177 | 175, 176 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ ℤ) |
178 | | peano2zm 11874 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹‘𝑥) ∈ ℤ → ((◡𝐹‘𝑥) − 1) ∈ ℤ) |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘𝑥) − 1) ∈ ℤ) |
180 | 171, 179 | eqeltrd 2883 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℤ) |
181 | 180 | zred 11936 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℝ) |
182 | | elfzle1 12760 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝐾) |
183 | 68, 182 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≤ 𝐾) |
184 | 183 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝐾) |
185 | 177 | zred 11936 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ ℝ) |
186 | | simprl 767 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ¬ (◡𝐹‘𝑥) < 𝐾) |
187 | 170, 185,
186 | nltled 10637 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≤ (◡𝐹‘𝑥)) |
188 | | elfzelz 12758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ) |
189 | 188 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ) |
190 | 189 | zred 11936 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ) |
191 | 137 | zred 11936 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℝ) |
192 | 191 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ) |
193 | 139 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ) |
194 | | elfzle2 12761 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ≤ 𝑁) |
195 | 194 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝑁) |
196 | 192 | ltp1d 11418 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1)) |
197 | 190, 192,
193, 195, 196 | lelttrd 10645 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1)) |
198 | 190, 197 | gtned 10622 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ≠ 𝑥) |
199 | 198 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ≠ 𝑥) |
200 | 60 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1))) |
201 | 66 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
202 | | f1fveq 6885 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((◡𝐹‘(𝑁 + 1)) = (◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥)) |
203 | 200, 201,
174, 202 | syl12anc 833 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘(𝑁 + 1)) = (◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥)) |
204 | 203 | necon3bid 3028 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘(𝑁 + 1)) ≠ (◡𝐹‘𝑥) ↔ (𝑁 + 1) ≠ 𝑥)) |
205 | 199, 204 | mpbird 258 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘(𝑁 + 1)) ≠ (◡𝐹‘𝑥)) |
206 | 34 | neeq1i 3048 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ≠ (◡𝐹‘𝑥) ↔ (◡𝐹‘(𝑁 + 1)) ≠ (◡𝐹‘𝑥)) |
207 | 205, 206 | sylibr 235 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≠ (◡𝐹‘𝑥)) |
208 | 207 | necomd 3039 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ≠ 𝐾) |
209 | 170, 185,
187, 208 | leneltd 10641 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 < (◡𝐹‘𝑥)) |
210 | 70 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℤ) |
211 | | zltlem1 11884 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ (◡𝐹‘𝑥) ∈ ℤ) → (𝐾 < (◡𝐹‘𝑥) ↔ 𝐾 ≤ ((◡𝐹‘𝑥) − 1))) |
212 | 210, 177,
211 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐾 < (◡𝐹‘𝑥) ↔ 𝐾 ≤ ((◡𝐹‘𝑥) − 1))) |
213 | 209, 212 | mpbid 233 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≤ ((◡𝐹‘𝑥) − 1)) |
214 | 213, 171 | breqtrrd 4990 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐾 ≤ 𝑘) |
215 | 169, 170,
181, 184, 214 | letrd 10644 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝑘) |
216 | | elfzle2 12761 |
. . . . . . . . . . . 12
⊢ ((◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) → (◡𝐹‘𝑥) ≤ (𝑁 + 1)) |
217 | 175, 216 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ≤ (𝑁 + 1)) |
218 | 191 | ad2antrr 722 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℝ) |
219 | | 1re 10487 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
220 | | lesubadd 10960 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧
𝑁 ∈ ℝ) →
(((◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (◡𝐹‘𝑥) ≤ (𝑁 + 1))) |
221 | 219, 220 | mp3an2 1441 |
. . . . . . . . . . . 12
⊢ (((◡𝐹‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (◡𝐹‘𝑥) ≤ (𝑁 + 1))) |
222 | 185, 218,
221 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (((◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (◡𝐹‘𝑥) ≤ (𝑁 + 1))) |
223 | 217, 222 | mpbird 258 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ((◡𝐹‘𝑥) − 1) ≤ 𝑁) |
224 | 171, 223 | eqbrtrd 4984 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ≤ 𝑁) |
225 | 152 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℤ) |
226 | 137 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℤ) |
227 | 180, 225,
226, 154 | syl3anc 1364 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
228 | 215, 224,
227 | mpbir2and 709 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁)) |
229 | 170, 181,
214 | lensymd 10638 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → ¬ 𝑘 < 𝐾) |
230 | 229, 53 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
231 | 171 | oveq1d 7031 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (((◡𝐹‘𝑥) − 1) + 1)) |
232 | 177 | zcnd 11937 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (◡𝐹‘𝑥) ∈ ℂ) |
233 | | npcan 10743 |
. . . . . . . . . . . 12
⊢ (((◡𝐹‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((◡𝐹‘𝑥) − 1) + 1) = (◡𝐹‘𝑥)) |
234 | 232, 113,
233 | sylancl 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (((◡𝐹‘𝑥) − 1) + 1) = (◡𝐹‘𝑥)) |
235 | 231, 234 | eqtrd 2831 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (◡𝐹‘𝑥)) |
236 | 235 | fveq2d 6542 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐹‘(𝑘 + 1)) = (𝐹‘(◡𝐹‘𝑥))) |
237 | 17 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) |
238 | 237, 174,
160 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
239 | 230, 236,
238 | 3eqtrrd 2836 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) |
240 | 228, 239 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))) |
241 | 240 | expr 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = ((◡𝐹‘𝑥) − 1) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
242 | 167, 241 | sylbid 241 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
243 | 165, 242 | pm2.61dan 809 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
244 | 243 | expimpd 454 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))) |
245 | 121, 244 | impbid 213 |
. 2
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((◡𝐹‘𝑥) < 𝐾, (◡𝐹‘𝑥), ((◡𝐹‘𝑥) − 1))))) |
246 | 1, 2, 6, 245 | f1od 7255 |
1
⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |