Proof of Theorem dvle
Step | Hyp | Ref
| Expression |
1 | | dvle.r |
. . . 4
⊢ (𝑥 = 𝑌 → 𝐴 = 𝑅) |
2 | 1 | eleq1d 2825 |
. . 3
⊢ (𝑥 = 𝑌 → (𝐴 ∈ ℝ ↔ 𝑅 ∈ ℝ)) |
3 | | dvle.a |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
4 | | cncff 24054 |
. . . . 5
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
6 | | eqid 2740 |
. . . . 5
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) |
7 | 6 | fmpt 6981 |
. . . 4
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
8 | 5, 7 | sylibr 233 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ) |
9 | | dvle.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝑀[,]𝑁)) |
10 | 2, 8, 9 | rspcdva 3563 |
. 2
⊢ (𝜑 → 𝑅 ∈ ℝ) |
11 | | dvle.s |
. . . . 5
⊢ (𝑥 = 𝑌 → 𝐶 = 𝑆) |
12 | 11 | eleq1d 2825 |
. . . 4
⊢ (𝑥 = 𝑌 → (𝐶 ∈ ℝ ↔ 𝑆 ∈ ℝ)) |
13 | | dvle.c |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
14 | | cncff 24054 |
. . . . . 6
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶):(𝑀[,]𝑁)⟶ℝ) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶):(𝑀[,]𝑁)⟶ℝ) |
16 | | eqid 2740 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶) |
17 | 16 | fmpt 6981 |
. . . . 5
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐶 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐶):(𝑀[,]𝑁)⟶ℝ) |
18 | 15, 17 | sylibr 233 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐶 ∈ ℝ) |
19 | 12, 18, 9 | rspcdva 3563 |
. . 3
⊢ (𝜑 → 𝑆 ∈ ℝ) |
20 | | dvle.q |
. . . . 5
⊢ (𝑥 = 𝑋 → 𝐶 = 𝑄) |
21 | 20 | eleq1d 2825 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝐶 ∈ ℝ ↔ 𝑄 ∈ ℝ)) |
22 | | dvle.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝑀[,]𝑁)) |
23 | 21, 18, 22 | rspcdva 3563 |
. . 3
⊢ (𝜑 → 𝑄 ∈ ℝ) |
24 | 19, 23 | resubcld 11403 |
. 2
⊢ (𝜑 → (𝑆 − 𝑄) ∈ ℝ) |
25 | | dvle.p |
. . . 4
⊢ (𝑥 = 𝑋 → 𝐴 = 𝑃) |
26 | 25 | eleq1d 2825 |
. . 3
⊢ (𝑥 = 𝑋 → (𝐴 ∈ ℝ ↔ 𝑃 ∈ ℝ)) |
27 | 26, 8, 22 | rspcdva 3563 |
. 2
⊢ (𝜑 → 𝑃 ∈ ℝ) |
28 | 10 | recnd 11004 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ ℂ) |
29 | 23 | recnd 11004 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ ℂ) |
30 | 19 | recnd 11004 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℂ) |
31 | 29, 30 | subcld 11332 |
. . . . 5
⊢ (𝜑 → (𝑄 − 𝑆) ∈ ℂ) |
32 | 28, 31 | addcomd 11177 |
. . . 4
⊢ (𝜑 → (𝑅 + (𝑄 − 𝑆)) = ((𝑄 − 𝑆) + 𝑅)) |
33 | 28, 30, 29 | subsub2d 11361 |
. . . 4
⊢ (𝜑 → (𝑅 − (𝑆 − 𝑄)) = (𝑅 + (𝑄 − 𝑆))) |
34 | 29, 30, 28 | subsubd 11360 |
. . . 4
⊢ (𝜑 → (𝑄 − (𝑆 − 𝑅)) = ((𝑄 − 𝑆) + 𝑅)) |
35 | 32, 33, 34 | 3eqtr4d 2790 |
. . 3
⊢ (𝜑 → (𝑅 − (𝑆 − 𝑄)) = (𝑄 − (𝑆 − 𝑅))) |
36 | 19, 10 | resubcld 11403 |
. . . 4
⊢ (𝜑 → (𝑆 − 𝑅) ∈ ℝ) |
37 | | dvle.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
38 | | dvle.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
39 | | eqid 2740 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
40 | 39 | subcn 24027 |
. . . . . . 7
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
41 | | ax-resscn 10929 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
42 | | resubcl 11285 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℝ) |
43 | 39, 40, 13, 3, 41, 42 | cncfmpt2ss 24077 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
44 | 41 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ⊆
ℂ) |
45 | | iccssre 13160 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀[,]𝑁) ⊆ ℝ) |
46 | 37, 38, 45 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
47 | 15 | fvmptelrn 6984 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℝ) |
48 | 5 | fvmptelrn 6984 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) |
49 | 47, 48 | resubcld 11403 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝐶 − 𝐴) ∈ ℝ) |
50 | 49 | recnd 11004 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → (𝐶 − 𝐴) ∈ ℂ) |
51 | 39 | tgioo2 23964 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
52 | | iccntr 23982 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
53 | 37, 38, 52 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝑀[,]𝑁)) = (𝑀(,)𝑁)) |
54 | 44, 46, 50, 51, 39, 53 | dvmptntr 25133 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))) = (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐶 − 𝐴)))) |
55 | | reelprrecn 10964 |
. . . . . . . . . 10
⊢ ℝ
∈ {ℝ, ℂ} |
56 | 55 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
57 | | ioossicc 13164 |
. . . . . . . . . . 11
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
58 | 57 | sseli 3922 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁)) |
59 | 47 | recnd 11004 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐶 ∈ ℂ) |
60 | 58, 59 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℂ) |
61 | | dvle.f |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ≤ 𝐷) |
62 | | lerel 11040 |
. . . . . . . . . . 11
⊢ Rel
≤ |
63 | 62 | brrelex2i 5645 |
. . . . . . . . . 10
⊢ (𝐵 ≤ 𝐷 → 𝐷 ∈ V) |
64 | 61, 63 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐷 ∈ V) |
65 | | dvle.d |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷)) |
66 | 48 | recnd 11004 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℂ) |
67 | 58, 66 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℂ) |
68 | 62 | brrelex1i 5644 |
. . . . . . . . . 10
⊢ (𝐵 ≤ 𝐷 → 𝐵 ∈ V) |
69 | 61, 68 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ V) |
70 | | dvle.b |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
71 | 56, 60, 64, 65, 67, 69, 70 | dvmptsub 25129 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐶 − 𝐴))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐷 − 𝐵))) |
72 | 54, 71 | eqtrd 2780 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))) = (𝑥 ∈ (𝑀(,)𝑁) ↦ (𝐷 − 𝐵))) |
73 | 58, 47 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐶 ∈ ℝ) |
74 | 73 | fmpttd 6986 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℝ) |
75 | | ioossre 13139 |
. . . . . . . . . . . 12
⊢ (𝑀(,)𝑁) ⊆ ℝ |
76 | | dvfre 25113 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶))⟶ℝ) |
77 | 74, 75, 76 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶))⟶ℝ) |
78 | 65 | dmeqd 5813 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷)) |
79 | 64 | ralrimiva 3110 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ (𝑀(,)𝑁)𝐷 ∈ V) |
80 | | dmmptg 6144 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐷 ∈ V → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷) = (𝑀(,)𝑁)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷) = (𝑀(,)𝑁)) |
82 | 78, 81 | eqtrd 2780 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)) = (𝑀(,)𝑁)) |
83 | 65, 82 | feq12d 6586 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐶))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷):(𝑀(,)𝑁)⟶ℝ)) |
84 | 77, 83 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐷):(𝑀(,)𝑁)⟶ℝ) |
85 | 84 | fvmptelrn 6984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐷 ∈ ℝ) |
86 | 58, 48 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ) |
87 | 86 | fmpttd 6986 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ) |
88 | | dvfre 25113 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) |
89 | 87, 75, 88 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) |
90 | 70 | dmeqd 5813 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
91 | 69 | ralrimiva 3110 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ V) |
92 | | dmmptg 6144 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ V → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) |
94 | 90, 93 | eqtrd 2780 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑀(,)𝑁)) |
95 | 70, 94 | feq12d 6586 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)) |
96 | 89, 95 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) |
97 | 96 | fvmptelrn 6984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ ℝ) |
98 | 85, 97 | resubcld 11403 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝐷 − 𝐵) ∈ ℝ) |
99 | 85, 97 | subge0d 11565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (0 ≤ (𝐷 − 𝐵) ↔ 𝐵 ≤ 𝐷)) |
100 | 61, 99 | mpbird 256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 0 ≤ (𝐷 − 𝐵)) |
101 | | elrege0 13185 |
. . . . . . . 8
⊢ ((𝐷 − 𝐵) ∈ (0[,)+∞) ↔ ((𝐷 − 𝐵) ∈ ℝ ∧ 0 ≤ (𝐷 − 𝐵))) |
102 | 98, 100, 101 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → (𝐷 − 𝐵) ∈ (0[,)+∞)) |
103 | 72, 102 | fmpt3d 6987 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))):(𝑀(,)𝑁)⟶(0[,)+∞)) |
104 | | dvle.l |
. . . . . 6
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
105 | 37, 38, 43, 103, 22, 9, 104 | dvge0 25168 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑋) ≤ ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑌)) |
106 | 20, 25 | oveq12d 7289 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐶 − 𝐴) = (𝑄 − 𝑃)) |
107 | | eqid 2740 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴)) = (𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴)) |
108 | | ovex 7304 |
. . . . . . 7
⊢ (𝐶 − 𝐴) ∈ V |
109 | 106, 107,
108 | fvmpt3i 6877 |
. . . . . 6
⊢ (𝑋 ∈ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑋) = (𝑄 − 𝑃)) |
110 | 22, 109 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑋) = (𝑄 − 𝑃)) |
111 | 11, 1 | oveq12d 7289 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (𝐶 − 𝐴) = (𝑆 − 𝑅)) |
112 | 111, 107,
108 | fvmpt3i 6877 |
. . . . . 6
⊢ (𝑌 ∈ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑌) = (𝑆 − 𝑅)) |
113 | 9, 112 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝑀[,]𝑁) ↦ (𝐶 − 𝐴))‘𝑌) = (𝑆 − 𝑅)) |
114 | 105, 110,
113 | 3brtr3d 5110 |
. . . 4
⊢ (𝜑 → (𝑄 − 𝑃) ≤ (𝑆 − 𝑅)) |
115 | 23, 27, 36, 114 | subled 11578 |
. . 3
⊢ (𝜑 → (𝑄 − (𝑆 − 𝑅)) ≤ 𝑃) |
116 | 35, 115 | eqbrtrd 5101 |
. 2
⊢ (𝜑 → (𝑅 − (𝑆 − 𝑄)) ≤ 𝑃) |
117 | 10, 24, 27, 116 | subled 11578 |
1
⊢ (𝜑 → (𝑅 − 𝑃) ≤ (𝑆 − 𝑄)) |