Proof of Theorem ivthinclemur
Step | Hyp | Ref
| Expression |
1 | | ivth.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | ad2antrr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) → 𝐴 ∈ ℝ) |
3 | | ivth.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | 3 | ad2antrr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) → 𝐵 ∈ ℝ) |
5 | | ivth.3 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ ℝ) |
6 | 5 | ad2antrr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) → 𝑈 ∈ ℝ) |
7 | | ivth.4 |
. . . . . 6
⊢ (𝜑 → 𝐴 < 𝐵) |
8 | 7 | ad2antrr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) → 𝐴 < 𝐵) |
9 | | ivth.5 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) |
10 | 9 | ad2antrr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) → (𝐴[,]𝐵) ⊆ 𝐷) |
11 | | ivth.7 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) |
12 | 11 | ad2antrr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) → 𝐹 ∈ (𝐷–cn→ℂ)) |
13 | | ivth.8 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
14 | 13 | adantlr 474 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
15 | 14 | adantlr 474 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
16 | | ivth.9 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) |
17 | 16 | ad2antrr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) |
18 | | ivthinc.i |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦)) |
19 | 18 | adantllr 478 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦)) |
20 | 19 | adantllr 478 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦)) |
21 | | ivthinclem.l |
. . . . 5
⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈} |
22 | | ivthinclem.r |
. . . . 5
⊢ 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹‘𝑤)} |
23 | | simpr 109 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) → 𝑟 ∈ 𝑅) |
24 | 2, 4, 6, 8, 10, 12, 15, 17, 20, 21, 22, 23 | ivthinclemuopn 13375 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑟 ∈ 𝑅) → ∃𝑞 ∈ 𝑅 𝑞 < 𝑟) |
25 | 24 | ex 114 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) → (𝑟 ∈ 𝑅 → ∃𝑞 ∈ 𝑅 𝑞 < 𝑟)) |
26 | | simpllr 529 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → 𝑟 ∈ (𝐴[,]𝐵)) |
27 | 5 | ad3antrrr 489 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → 𝑈 ∈ ℝ) |
28 | | fveq2 5494 |
. . . . . . . 8
⊢ (𝑥 = 𝑞 → (𝐹‘𝑥) = (𝐹‘𝑞)) |
29 | 28 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑥 = 𝑞 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑞) ∈ ℝ)) |
30 | 13 | ralrimiva 2543 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
31 | 30 | ad3antrrr 489 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
32 | | fveq2 5494 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑞 → (𝐹‘𝑤) = (𝐹‘𝑞)) |
33 | 32 | breq2d 3999 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑞 → (𝑈 < (𝐹‘𝑤) ↔ 𝑈 < (𝐹‘𝑞))) |
34 | 33, 22 | elrab2 2889 |
. . . . . . . . 9
⊢ (𝑞 ∈ 𝑅 ↔ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑈 < (𝐹‘𝑞))) |
35 | 34 | simplbi 272 |
. . . . . . . 8
⊢ (𝑞 ∈ 𝑅 → 𝑞 ∈ (𝐴[,]𝐵)) |
36 | 35 | ad2antlr 486 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → 𝑞 ∈ (𝐴[,]𝐵)) |
37 | 29, 31, 36 | rspcdva 2839 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → (𝐹‘𝑞) ∈ ℝ) |
38 | | fveq2 5494 |
. . . . . . . 8
⊢ (𝑥 = 𝑟 → (𝐹‘𝑥) = (𝐹‘𝑟)) |
39 | 38 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑥 = 𝑟 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑟) ∈ ℝ)) |
40 | 39, 31, 26 | rspcdva 2839 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → (𝐹‘𝑟) ∈ ℝ) |
41 | 34 | simprbi 273 |
. . . . . . 7
⊢ (𝑞 ∈ 𝑅 → 𝑈 < (𝐹‘𝑞)) |
42 | 41 | ad2antlr 486 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → 𝑈 < (𝐹‘𝑞)) |
43 | | simpr 109 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → 𝑞 < 𝑟) |
44 | | breq2 3991 |
. . . . . . . . 9
⊢ (𝑦 = 𝑟 → (𝑞 < 𝑦 ↔ 𝑞 < 𝑟)) |
45 | | fveq2 5494 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑟 → (𝐹‘𝑦) = (𝐹‘𝑟)) |
46 | 45 | breq2d 3999 |
. . . . . . . . 9
⊢ (𝑦 = 𝑟 → ((𝐹‘𝑞) < (𝐹‘𝑦) ↔ (𝐹‘𝑞) < (𝐹‘𝑟))) |
47 | 44, 46 | imbi12d 233 |
. . . . . . . 8
⊢ (𝑦 = 𝑟 → ((𝑞 < 𝑦 → (𝐹‘𝑞) < (𝐹‘𝑦)) ↔ (𝑞 < 𝑟 → (𝐹‘𝑞) < (𝐹‘𝑟)))) |
48 | | breq1 3990 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑞 → (𝑥 < 𝑦 ↔ 𝑞 < 𝑦)) |
49 | 28 | breq1d 3997 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑞 → ((𝐹‘𝑥) < (𝐹‘𝑦) ↔ (𝐹‘𝑞) < (𝐹‘𝑦))) |
50 | 48, 49 | imbi12d 233 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑞 → ((𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦)) ↔ (𝑞 < 𝑦 → (𝐹‘𝑞) < (𝐹‘𝑦)))) |
51 | 50 | ralbidv 2470 |
. . . . . . . . 9
⊢ (𝑥 = 𝑞 → (∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦)) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑞 < 𝑦 → (𝐹‘𝑞) < (𝐹‘𝑦)))) |
52 | 18 | expr 373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
53 | 52 | ralrimiva 2543 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
54 | 53 | ralrimiva 2543 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
55 | 54 | ad3antrrr 489 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
56 | 51, 55, 36 | rspcdva 2839 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑞 < 𝑦 → (𝐹‘𝑞) < (𝐹‘𝑦))) |
57 | 47, 56, 26 | rspcdva 2839 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → (𝑞 < 𝑟 → (𝐹‘𝑞) < (𝐹‘𝑟))) |
58 | 43, 57 | mpd 13 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → (𝐹‘𝑞) < (𝐹‘𝑟)) |
59 | 27, 37, 40, 42, 58 | lttrd 8038 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → 𝑈 < (𝐹‘𝑟)) |
60 | | fveq2 5494 |
. . . . . . 7
⊢ (𝑤 = 𝑟 → (𝐹‘𝑤) = (𝐹‘𝑟)) |
61 | 60 | breq2d 3999 |
. . . . . 6
⊢ (𝑤 = 𝑟 → (𝑈 < (𝐹‘𝑤) ↔ 𝑈 < (𝐹‘𝑟))) |
62 | 61, 22 | elrab2 2889 |
. . . . 5
⊢ (𝑟 ∈ 𝑅 ↔ (𝑟 ∈ (𝐴[,]𝐵) ∧ 𝑈 < (𝐹‘𝑟))) |
63 | 26, 59, 62 | sylanbrc 415 |
. . . 4
⊢ ((((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ 𝑞 ∈ 𝑅) ∧ 𝑞 < 𝑟) → 𝑟 ∈ 𝑅) |
64 | 63 | rexlimdva2 2590 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) → (∃𝑞 ∈ 𝑅 𝑞 < 𝑟 → 𝑟 ∈ 𝑅)) |
65 | 25, 64 | impbid 128 |
. 2
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) → (𝑟 ∈ 𝑅 ↔ ∃𝑞 ∈ 𝑅 𝑞 < 𝑟)) |
66 | 65 | ralrimiva 2543 |
1
⊢ (𝜑 → ∀𝑟 ∈ (𝐴[,]𝐵)(𝑟 ∈ 𝑅 ↔ ∃𝑞 ∈ 𝑅 𝑞 < 𝑟)) |