Proof of Theorem ivthinclemloc
Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑞 < 𝑟) |
2 | | breq2 3969 |
. . . . . . . 8
⊢ (𝑦 = 𝑟 → (𝑞 < 𝑦 ↔ 𝑞 < 𝑟)) |
3 | | fveq2 5468 |
. . . . . . . . 9
⊢ (𝑦 = 𝑟 → (𝐹‘𝑦) = (𝐹‘𝑟)) |
4 | 3 | breq2d 3977 |
. . . . . . . 8
⊢ (𝑦 = 𝑟 → ((𝐹‘𝑞) < (𝐹‘𝑦) ↔ (𝐹‘𝑞) < (𝐹‘𝑟))) |
5 | 2, 4 | imbi12d 233 |
. . . . . . 7
⊢ (𝑦 = 𝑟 → ((𝑞 < 𝑦 → (𝐹‘𝑞) < (𝐹‘𝑦)) ↔ (𝑞 < 𝑟 → (𝐹‘𝑞) < (𝐹‘𝑟)))) |
6 | | breq1 3968 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑞 → (𝑥 < 𝑦 ↔ 𝑞 < 𝑦)) |
7 | | fveq2 5468 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑞 → (𝐹‘𝑥) = (𝐹‘𝑞)) |
8 | 7 | breq1d 3975 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑞 → ((𝐹‘𝑥) < (𝐹‘𝑦) ↔ (𝐹‘𝑞) < (𝐹‘𝑦))) |
9 | 6, 8 | imbi12d 233 |
. . . . . . . . 9
⊢ (𝑥 = 𝑞 → ((𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦)) ↔ (𝑞 < 𝑦 → (𝐹‘𝑞) < (𝐹‘𝑦)))) |
10 | 9 | ralbidv 2457 |
. . . . . . . 8
⊢ (𝑥 = 𝑞 → (∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦)) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑞 < 𝑦 → (𝐹‘𝑞) < (𝐹‘𝑦)))) |
11 | | ivthinc.i |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦)) |
12 | 11 | expr 373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
13 | 12 | ralrimiva 2530 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
14 | 13 | ralrimiva 2530 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
15 | 14 | ad2antrr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
16 | | simplrl 525 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑞 ∈ (𝐴[,]𝐵)) |
17 | 10, 15, 16 | rspcdva 2821 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑞 < 𝑦 → (𝐹‘𝑞) < (𝐹‘𝑦))) |
18 | | simplrr 526 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑟 ∈ (𝐴[,]𝐵)) |
19 | 5, 17, 18 | rspcdva 2821 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝑞 < 𝑟 → (𝐹‘𝑞) < (𝐹‘𝑟))) |
20 | 1, 19 | mpd 13 |
. . . . 5
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝐹‘𝑞) < (𝐹‘𝑟)) |
21 | 7 | eleq1d 2226 |
. . . . . . 7
⊢ (𝑥 = 𝑞 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑞) ∈ ℝ)) |
22 | | ivth.8 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
23 | 22 | ralrimiva 2530 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
24 | 23 | ad2antrr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
25 | 21, 24, 16 | rspcdva 2821 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝐹‘𝑞) ∈ ℝ) |
26 | | fveq2 5468 |
. . . . . . . 8
⊢ (𝑥 = 𝑟 → (𝐹‘𝑥) = (𝐹‘𝑟)) |
27 | 26 | eleq1d 2226 |
. . . . . . 7
⊢ (𝑥 = 𝑟 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑟) ∈ ℝ)) |
28 | 27, 24, 18 | rspcdva 2821 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝐹‘𝑟) ∈ ℝ) |
29 | | ivth.3 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ ℝ) |
30 | 29 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑈 ∈ ℝ) |
31 | | axltwlin 7945 |
. . . . . 6
⊢ (((𝐹‘𝑞) ∈ ℝ ∧ (𝐹‘𝑟) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝑞) < (𝐹‘𝑟) → ((𝐹‘𝑞) < 𝑈 ∨ 𝑈 < (𝐹‘𝑟)))) |
32 | 25, 28, 30, 31 | syl3anc 1220 |
. . . . 5
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ((𝐹‘𝑞) < (𝐹‘𝑟) → ((𝐹‘𝑞) < 𝑈 ∨ 𝑈 < (𝐹‘𝑟)))) |
33 | 20, 32 | mpd 13 |
. . . 4
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ((𝐹‘𝑞) < 𝑈 ∨ 𝑈 < (𝐹‘𝑟))) |
34 | 16 | adantr 274 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ (𝐹‘𝑞) < 𝑈) → 𝑞 ∈ (𝐴[,]𝐵)) |
35 | | simpr 109 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ (𝐹‘𝑞) < 𝑈) → (𝐹‘𝑞) < 𝑈) |
36 | | fveq2 5468 |
. . . . . . . . 9
⊢ (𝑤 = 𝑞 → (𝐹‘𝑤) = (𝐹‘𝑞)) |
37 | 36 | breq1d 3975 |
. . . . . . . 8
⊢ (𝑤 = 𝑞 → ((𝐹‘𝑤) < 𝑈 ↔ (𝐹‘𝑞) < 𝑈)) |
38 | | ivthinclem.l |
. . . . . . . 8
⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈} |
39 | 37, 38 | elrab2 2871 |
. . . . . . 7
⊢ (𝑞 ∈ 𝐿 ↔ (𝑞 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑞) < 𝑈)) |
40 | 34, 35, 39 | sylanbrc 414 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ (𝐹‘𝑞) < 𝑈) → 𝑞 ∈ 𝐿) |
41 | 40 | ex 114 |
. . . . 5
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ((𝐹‘𝑞) < 𝑈 → 𝑞 ∈ 𝐿)) |
42 | 18 | adantr 274 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ 𝑈 < (𝐹‘𝑟)) → 𝑟 ∈ (𝐴[,]𝐵)) |
43 | | simpr 109 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ 𝑈 < (𝐹‘𝑟)) → 𝑈 < (𝐹‘𝑟)) |
44 | | fveq2 5468 |
. . . . . . . . 9
⊢ (𝑤 = 𝑟 → (𝐹‘𝑤) = (𝐹‘𝑟)) |
45 | 44 | breq2d 3977 |
. . . . . . . 8
⊢ (𝑤 = 𝑟 → (𝑈 < (𝐹‘𝑤) ↔ 𝑈 < (𝐹‘𝑟))) |
46 | | ivthinclem.r |
. . . . . . . 8
⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)} |
47 | 45, 46 | elrab2 2871 |
. . . . . . 7
⊢ (𝑟 ∈ 𝑅 ↔ (𝑟 ∈ (𝐴[,]𝐵) ∧ 𝑈 < (𝐹‘𝑟))) |
48 | 42, 43, 47 | sylanbrc 414 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ 𝑈 < (𝐹‘𝑟)) → 𝑟 ∈ 𝑅) |
49 | 48 | ex 114 |
. . . . 5
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝑈 < (𝐹‘𝑟) → 𝑟 ∈ 𝑅)) |
50 | 41, 49 | orim12d 776 |
. . . 4
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (((𝐹‘𝑞) < 𝑈 ∨ 𝑈 < (𝐹‘𝑟)) → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑅))) |
51 | 33, 50 | mpd 13 |
. . 3
⊢ (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑅)) |
52 | 51 | ex 114 |
. 2
⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) → (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑅))) |
53 | 52 | ralrimivva 2539 |
1
⊢ (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑅))) |