Step | Hyp | Ref
| Expression |
1 | | intlewftc.4 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
2 | | cncff 23579 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
4 | | intlewftc.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
5 | | intlewftc.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
6 | 4 | leidd 11229 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≤ 𝐵) |
7 | 4, 5, 6 | 3jca 1126 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵)) |
8 | | intlewftc.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | | elicc2 12829 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵))) |
10 | 8, 4, 9 | syl2anc 588 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵))) |
11 | 7, 10 | mpbird 260 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
12 | 3, 11 | ffvelrnd 6836 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) |
13 | 8 | leidd 11229 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐴) |
14 | 8, 13, 5 | 3jca 1126 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) |
15 | | elicc2 12829 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) |
16 | 8, 4, 15 | syl2anc 588 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) |
17 | 14, 16 | mpbird 260 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
18 | 3, 17 | ffvelrnd 6836 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
19 | 12, 18 | resubcld 11091 |
. . 3
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ) |
20 | | intlewftc.5 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
21 | | cncff 23579 |
. . . . . 6
⊢ (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐺:(𝐴[,]𝐵)⟶ℝ) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℝ) |
23 | 22, 11 | ffvelrnd 6836 |
. . . 4
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℝ) |
24 | 22, 17 | ffvelrnd 6836 |
. . . 4
⊢ (𝜑 → (𝐺‘𝐴) ∈ ℝ) |
25 | 23, 24 | resubcld 11091 |
. . 3
⊢ (𝜑 → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ) |
26 | | intlewftc.10 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
𝐿1) |
27 | | intlewftc.12 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)) |
28 | 27 | eleq1d 2835 |
. . . . . 6
⊢ (𝜑 → (𝐷 ∈ 𝐿1 ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃) ∈
𝐿1)) |
29 | 26, 28 | mpbid 235 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃) ∈
𝐿1) |
30 | | intlewftc.11 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
𝐿1) |
31 | | intlewftc.13 |
. . . . . . 7
⊢ (𝜑 → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)) |
32 | 31 | eleq1d 2835 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∈ 𝐿1 ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄) ∈
𝐿1)) |
33 | 30, 32 | mpbid 235 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄) ∈
𝐿1) |
34 | | intlewftc.8 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
35 | | cncff 23579 |
. . . . . . . 8
⊢ (𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐷:(𝐴(,)𝐵)⟶ℝ) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐷:(𝐴(,)𝐵)⟶ℝ) |
37 | 27 | feq1d 6476 |
. . . . . . 7
⊢ (𝜑 → (𝐷:(𝐴(,)𝐵)⟶ℝ ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃):(𝐴(,)𝐵)⟶ℝ)) |
38 | 36, 37 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃):(𝐴(,)𝐵)⟶ℝ) |
39 | 38 | fvmptelrn 6861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ∈ ℝ) |
40 | | intlewftc.9 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
41 | | cncff 23579 |
. . . . . . . 8
⊢ (𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐸:(𝐴(,)𝐵)⟶ℝ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐸:(𝐴(,)𝐵)⟶ℝ) |
43 | 31 | feq1d 6476 |
. . . . . . 7
⊢ (𝜑 → (𝐸:(𝐴(,)𝐵)⟶ℝ ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄):(𝐴(,)𝐵)⟶ℝ)) |
44 | 42, 43 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄):(𝐴(,)𝐵)⟶ℝ) |
45 | 44 | fvmptelrn 6861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑄 ∈ ℝ) |
46 | | intlewftc.14 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ≤ 𝑄) |
47 | 29, 33, 39, 45, 46 | itgle 24494 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑃 d𝑥 ≤ ∫(𝐴(,)𝐵)𝑄 d𝑥) |
48 | 39 | itgmpt 24467 |
. . . . . 6
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑃 d𝑥 = ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡) d𝑡) |
49 | 27 | fveq1d 6653 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷‘𝑡) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡)) |
50 | 49 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐷‘𝑡) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡)) |
51 | 50 | eqcomd 2765 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡) = (𝐷‘𝑡)) |
52 | 51 | itgeq2dv 24466 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)(𝐷‘𝑡) d𝑡) |
53 | | intlewftc.6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 = (ℝ D 𝐹)) |
54 | 53 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐷 = (ℝ D 𝐹)) |
55 | 54 | fveq1d 6653 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐷‘𝑡) = ((ℝ D 𝐹)‘𝑡)) |
56 | 55 | itgeq2dv 24466 |
. . . . . . . 8
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐷‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
57 | | ax-resscn 10617 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
58 | 57 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ⊆
ℂ) |
59 | | fss 6505 |
. . . . . . . . . . . 12
⊢ ((𝐷:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐷:(𝐴(,)𝐵)⟶ℂ) |
60 | 36, 58, 59 | syl2anc 588 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷:(𝐴(,)𝐵)⟶ℂ) |
61 | | ssidd 3911 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ⊆
ℂ) |
62 | | cncffvrn 23584 |
. . . . . . . . . . . 12
⊢ ((ℂ
⊆ ℂ ∧ 𝐷
∈ ((𝐴(,)𝐵)–cn→ℝ)) → (𝐷 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ 𝐷:(𝐴(,)𝐵)⟶ℂ)) |
63 | 61, 34, 62 | syl2anc 588 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ 𝐷:(𝐴(,)𝐵)⟶ℂ)) |
64 | 60, 63 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
65 | 53 | eleq1d 2835 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))) |
66 | 64, 65 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
67 | 53, 26 | eqeltrrd 2852 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) ∈
𝐿1) |
68 | | fss 6505 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴[,]𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
69 | 3, 58, 68 | syl2anc 588 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
70 | | cncffvrn 23584 |
. . . . . . . . . . 11
⊢ ((ℂ
⊆ ℂ ∧ 𝐹
∈ ((𝐴[,]𝐵)–cn→ℝ)) → (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ 𝐹:(𝐴[,]𝐵)⟶ℂ)) |
71 | 61, 1, 70 | syl2anc 588 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ 𝐹:(𝐴[,]𝐵)⟶ℂ)) |
72 | 69, 71 | mpbird 260 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
73 | 8, 4, 5, 66, 67, 72 | ftc2 24728 |
. . . . . . . 8
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
74 | 56, 73 | eqtrd 2794 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐷‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
75 | 52, 74 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
76 | 48, 75 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑃 d𝑥 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
77 | 45 | itgmpt 24467 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑄 d𝑥 = ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)‘𝑡) d𝑡) |
78 | 31 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)) |
79 | 78 | eqcomd 2765 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄) = 𝐸) |
80 | 79 | fveq1d 6653 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)‘𝑡) = (𝐸‘𝑡)) |
81 | 80 | itgeq2dv 24466 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)(𝐸‘𝑡) d𝑡) |
82 | 77, 81 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑄 d𝑥 = ∫(𝐴(,)𝐵)(𝐸‘𝑡) d𝑡) |
83 | | intlewftc.7 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 = (ℝ D 𝐺)) |
84 | 83 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐸 = (ℝ D 𝐺)) |
85 | 84 | fveq1d 6653 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐸‘𝑡) = ((ℝ D 𝐺)‘𝑡)) |
86 | 85 | itgeq2dv 24466 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐸‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐺)‘𝑡) d𝑡) |
87 | | fss 6505 |
. . . . . . . . . . . . 13
⊢ ((𝐸:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐸:(𝐴(,)𝐵)⟶ℂ) |
88 | 42, 58, 87 | syl2anc 588 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸:(𝐴(,)𝐵)⟶ℂ) |
89 | | cncffvrn 23584 |
. . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ 𝐸
∈ ((𝐴(,)𝐵)–cn→ℝ)) → (𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ 𝐸:(𝐴(,)𝐵)⟶ℂ)) |
90 | 61, 40, 89 | syl2anc 588 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ 𝐸:(𝐴(,)𝐵)⟶ℂ)) |
91 | 88, 90 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
92 | 83 | eleq1d 2835 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ (ℝ D 𝐺) ∈ ((𝐴(,)𝐵)–cn→ℂ))) |
93 | 91, 92 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐺) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
94 | 93, 92 | mpbird 260 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
95 | 94, 92 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐺) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
96 | 83, 30 | eqeltrrd 2852 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐺) ∈
𝐿1) |
97 | | fss 6505 |
. . . . . . . . . 10
⊢ ((𝐺:(𝐴[,]𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
98 | 22, 58, 97 | syl2anc 588 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
99 | | cncffvrn 23584 |
. . . . . . . . . 10
⊢ ((ℂ
⊆ ℂ ∧ 𝐺
∈ ((𝐴[,]𝐵)–cn→ℝ)) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ 𝐺:(𝐴[,]𝐵)⟶ℂ)) |
100 | 61, 20, 99 | syl2anc 588 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ 𝐺:(𝐴[,]𝐵)⟶ℂ)) |
101 | 98, 100 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
102 | 8, 4, 5, 95, 96, 101 | ftc2 24728 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐺)‘𝑡) d𝑡 = ((𝐺‘𝐵) − (𝐺‘𝐴))) |
103 | 86, 102 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐸‘𝑡) d𝑡 = ((𝐺‘𝐵) − (𝐺‘𝐴))) |
104 | 82, 103 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑄 d𝑥 = ((𝐺‘𝐵) − (𝐺‘𝐴))) |
105 | 76, 104 | breq12d 5038 |
. . . 4
⊢ (𝜑 → (∫(𝐴(,)𝐵)𝑃 d𝑥 ≤ ∫(𝐴(,)𝐵)𝑄 d𝑥 ↔ ((𝐹‘𝐵) − (𝐹‘𝐴)) ≤ ((𝐺‘𝐵) − (𝐺‘𝐴)))) |
106 | 47, 105 | mpbid 235 |
. . 3
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ≤ ((𝐺‘𝐵) − (𝐺‘𝐴))) |
107 | | intlewftc.15 |
. . 3
⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐺‘𝐴)) |
108 | 19, 18, 25, 24, 106, 107 | le2addd 11282 |
. 2
⊢ (𝜑 → (((𝐹‘𝐵) − (𝐹‘𝐴)) + (𝐹‘𝐴)) ≤ (((𝐺‘𝐵) − (𝐺‘𝐴)) + (𝐺‘𝐴))) |
109 | 57, 12 | sseldi 3886 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ) |
110 | 57, 18 | sseldi 3886 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) |
111 | 109, 110 | npcand 11024 |
. . 3
⊢ (𝜑 → (((𝐹‘𝐵) − (𝐹‘𝐴)) + (𝐹‘𝐴)) = (𝐹‘𝐵)) |
112 | 57, 23 | sseldi 3886 |
. . . 4
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℂ) |
113 | 57, 24 | sseldi 3886 |
. . . 4
⊢ (𝜑 → (𝐺‘𝐴) ∈ ℂ) |
114 | 112, 113 | npcand 11024 |
. . 3
⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) + (𝐺‘𝐴)) = (𝐺‘𝐵)) |
115 | 111, 114 | breq12d 5038 |
. 2
⊢ (𝜑 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) + (𝐹‘𝐴)) ≤ (((𝐺‘𝐵) − (𝐺‘𝐴)) + (𝐺‘𝐴)) ↔ (𝐹‘𝐵) ≤ (𝐺‘𝐵))) |
116 | 108, 115 | mpbid 235 |
1
⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐺‘𝐵)) |