Step | Hyp | Ref
| Expression |
1 | | ssdec.1 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzel2 11568 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | | eluzelz 11573 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
6 | 3, 5 | jca 553 |
. . 3
⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
7 | | eluzle 11576 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
8 | 1, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
9 | 5 | zred 11358 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
10 | 9 | leidd 10473 |
. . . 4
⊢ (𝜑 → 𝑁 ≤ 𝑁) |
11 | 5, 8, 10 | 3jca 1235 |
. . 3
⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁)) |
12 | 6, 11 | jca 553 |
. 2
⊢ (𝜑 → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
13 | | fveq2 6103 |
. . . . 5
⊢ (𝑛 = 𝑀 → (𝐹‘𝑛) = (𝐹‘𝑀)) |
14 | 13 | sseq1d 3595 |
. . . 4
⊢ (𝑛 = 𝑀 → ((𝐹‘𝑛) ⊆ (𝐹‘𝑀) ↔ (𝐹‘𝑀) ⊆ (𝐹‘𝑀))) |
15 | 14 | imbi2d 329 |
. . 3
⊢ (𝑛 = 𝑀 → ((𝜑 → (𝐹‘𝑛) ⊆ (𝐹‘𝑀)) ↔ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑀)))) |
16 | | fveq2 6103 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
17 | 16 | sseq1d 3595 |
. . . 4
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛) ⊆ (𝐹‘𝑀) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑀))) |
18 | 17 | imbi2d 329 |
. . 3
⊢ (𝑛 = 𝑚 → ((𝜑 → (𝐹‘𝑛) ⊆ (𝐹‘𝑀)) ↔ (𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)))) |
19 | | fveq2 6103 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑚 + 1))) |
20 | 19 | sseq1d 3595 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → ((𝐹‘𝑛) ⊆ (𝐹‘𝑀) ↔ (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑀))) |
21 | 20 | imbi2d 329 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐹‘𝑛) ⊆ (𝐹‘𝑀)) ↔ (𝜑 → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑀)))) |
22 | | fveq2 6103 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝐹‘𝑛) = (𝐹‘𝑁)) |
23 | 22 | sseq1d 3595 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝐹‘𝑛) ⊆ (𝐹‘𝑀) ↔ (𝐹‘𝑁) ⊆ (𝐹‘𝑀))) |
24 | 23 | imbi2d 329 |
. . 3
⊢ (𝑛 = 𝑁 → ((𝜑 → (𝐹‘𝑛) ⊆ (𝐹‘𝑀)) ↔ (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀)))) |
25 | | ssid 3587 |
. . . . 5
⊢ (𝐹‘𝑀) ⊆ (𝐹‘𝑀) |
26 | 25 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑀)) |
27 | 26 | a1i 11 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑀))) |
28 | | simpr 476 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝜑) |
29 | | simplll 794 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑀 ∈ ℤ) |
30 | | simplr1 1096 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑚 ∈ ℤ) |
31 | | simplr2 1097 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑀 ≤ 𝑚) |
32 | 29, 30, 31 | 3jca 1235 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → (𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚)) |
33 | | eluz2 11569 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚)) |
34 | 32, 33 | sylibr 223 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑚 ∈ (ℤ≥‘𝑀)) |
35 | | simpllr 795 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑁 ∈ ℤ) |
36 | | simplr3 1098 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑚 < 𝑁) |
37 | 34, 35, 36 | 3jca 1235 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → (𝑚 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑚 < 𝑁)) |
38 | | elfzo2 12342 |
. . . . . . . 8
⊢ (𝑚 ∈ (𝑀..^𝑁) ↔ (𝑚 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑚 < 𝑁)) |
39 | 37, 38 | sylibr 223 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → 𝑚 ∈ (𝑀..^𝑁)) |
40 | | ssdec.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚)) |
41 | 28, 39, 40 | syl2anc 691 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ 𝜑) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚)) |
42 | 41 | 3adant2 1073 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ (𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) ∧ 𝜑) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚)) |
43 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) ∧ 𝜑) → 𝜑) |
44 | | simpl 472 |
. . . . . . 7
⊢ (((𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) ∧ 𝜑) → (𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀))) |
45 | | pm3.35 609 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀))) → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) |
46 | 43, 44, 45 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) ∧ 𝜑) → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) |
47 | 46 | 3adant1 1072 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ (𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) ∧ 𝜑) → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) |
48 | 42, 47 | sstrd 3578 |
. . . 4
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) ∧ (𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) ∧ 𝜑) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑀)) |
49 | 48 | 3exp 1256 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁)) → ((𝜑 → (𝐹‘𝑚) ⊆ (𝐹‘𝑀)) → (𝜑 → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑀)))) |
50 | 15, 18, 21, 24, 27, 49 | fzind 11351 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁)) → (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀))) |
51 | 12, 50 | mpcom 37 |
1
⊢ (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀)) |