Step | Hyp | Ref
| Expression |
1 | | ssinc.1 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzel2 12341 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | | eluzelz 12346 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
6 | 3, 5 | jca 515 |
. . 3
⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
7 | | eluzle 12349 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
8 | 1, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
9 | 5 | zred 12180 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
10 | 9 | leidd 11296 |
. . . 4
⊢ (𝜑 → 𝑁 ≤ 𝑁) |
11 | 5, 8, 10 | 3jca 1129 |
. . 3
⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁)) |
12 | 6, 11 | jca 515 |
. 2
⊢ (𝜑 → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
13 | | id 22 |
. 2
⊢ (𝜑 → 𝜑) |
14 | | fveq2 6686 |
. . . . 5
⊢ (𝑛 = 𝑀 → (𝐹‘𝑛) = (𝐹‘𝑀)) |
15 | 14 | sseq2d 3919 |
. . . 4
⊢ (𝑛 = 𝑀 → ((𝐹‘𝑀) ⊆ (𝐹‘𝑛) ↔ (𝐹‘𝑀) ⊆ (𝐹‘𝑀))) |
16 | 15 | imbi2d 344 |
. . 3
⊢ (𝑛 = 𝑀 → ((𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑛)) ↔ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑀)))) |
17 | | fveq2 6686 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
18 | 17 | sseq2d 3919 |
. . . 4
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑀) ⊆ (𝐹‘𝑛) ↔ (𝐹‘𝑀) ⊆ (𝐹‘𝑚))) |
19 | 18 | imbi2d 344 |
. . 3
⊢ (𝑛 = 𝑚 → ((𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑛)) ↔ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)))) |
20 | | fveq2 6686 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑚 + 1))) |
21 | 20 | sseq2d 3919 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → ((𝐹‘𝑀) ⊆ (𝐹‘𝑛) ↔ (𝐹‘𝑀) ⊆ (𝐹‘(𝑚 + 1)))) |
22 | 21 | imbi2d 344 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑛)) ↔ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘(𝑚 + 1))))) |
23 | | fveq2 6686 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝐹‘𝑛) = (𝐹‘𝑁)) |
24 | 23 | sseq2d 3919 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝐹‘𝑀) ⊆ (𝐹‘𝑛) ↔ (𝐹‘𝑀) ⊆ (𝐹‘𝑁))) |
25 | 24 | imbi2d 344 |
. . 3
⊢ (𝑛 = 𝑁 → ((𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑛)) ↔ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁)))) |
26 | | ssidd 3910 |
. . . 4
⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑀)) |
27 | 26 | a1i 11 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑀))) |
28 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) ∧ 𝜑) → 𝜑) |
29 | | simpl 486 |
. . . . . . 7
⊢ (((𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) ∧ 𝜑) → (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚))) |
30 | | pm3.35 803 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚))) → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) |
31 | 28, 29, 30 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) ∧ 𝜑) → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) |
32 | 31 | 3adant1 1131 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) ∧ 𝜑) → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) |
33 | | simpr 488 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝜑) |
34 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑀 ∈ ℤ) |
35 | | simplr1 1216 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑚 ∈ ℤ) |
36 | | simplr2 1217 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑀 ≤ 𝑚) |
37 | 34, 35, 36 | 3jca 1129 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → (𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚)) |
38 | | eluz2 12342 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚)) |
39 | 37, 38 | sylibr 237 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑚 ∈ (ℤ≥‘𝑀)) |
40 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑁 ∈ ℤ) |
41 | | simplr3 1218 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑚 < 𝑁) |
42 | 39, 40, 41 | 3jca 1129 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → (𝑚 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑚 < 𝑁)) |
43 | | elfzo2 13144 |
. . . . . . . 8
⊢ (𝑚 ∈ (𝑀..^𝑁) ↔ (𝑚 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑚 < 𝑁)) |
44 | 42, 43 | sylibr 237 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑚 ∈ (𝑀..^𝑁)) |
45 | | ssinc.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) |
46 | 33, 44, 45 | syl2anc 587 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) |
47 | 46 | 3adant2 1132 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) ∧ 𝜑) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) |
48 | 32, 47 | sstrd 3897 |
. . . 4
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) ∧ 𝜑) → (𝐹‘𝑀) ⊆ (𝐹‘(𝑚 + 1))) |
49 | 48 | 3exp 1120 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) → ((𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑚)) → (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘(𝑚 + 1))))) |
50 | 16, 19, 22, 25, 27, 49 | fzind 12173 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁)) → (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁))) |
51 | 12, 13, 50 | sylc 65 |
1
⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁)) |