| Step | Hyp | Ref
| Expression |
| 1 | | intlewftc.4 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
| 2 | | cncff 24919 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
| 4 | | intlewftc.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 5 | | intlewftc.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 6 | 4 | leidd 11829 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≤ 𝐵) |
| 7 | 4, 5, 6 | 3jca 1129 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵)) |
| 8 | | intlewftc.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 9 | | elicc2 13452 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵))) |
| 10 | 8, 4, 9 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵))) |
| 11 | 7, 10 | mpbird 257 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
| 12 | 3, 11 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) |
| 13 | 8 | leidd 11829 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐴) |
| 14 | 8, 13, 5 | 3jca 1129 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) |
| 15 | | elicc2 13452 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) |
| 16 | 8, 4, 15 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) |
| 17 | 14, 16 | mpbird 257 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
| 18 | 3, 17 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
| 19 | 12, 18 | resubcld 11691 |
. . 3
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ) |
| 20 | | intlewftc.5 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
| 21 | | cncff 24919 |
. . . . . 6
⊢ (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐺:(𝐴[,]𝐵)⟶ℝ) |
| 22 | 20, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℝ) |
| 23 | 22, 11 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℝ) |
| 24 | 22, 17 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝐺‘𝐴) ∈ ℝ) |
| 25 | 23, 24 | resubcld 11691 |
. . 3
⊢ (𝜑 → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ) |
| 26 | | intlewftc.10 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
𝐿1) |
| 27 | | intlewftc.12 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)) |
| 28 | 27 | eleq1d 2826 |
. . . . . 6
⊢ (𝜑 → (𝐷 ∈ 𝐿1 ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃) ∈
𝐿1)) |
| 29 | 26, 28 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃) ∈
𝐿1) |
| 30 | | intlewftc.11 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
𝐿1) |
| 31 | | intlewftc.13 |
. . . . . . 7
⊢ (𝜑 → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)) |
| 32 | 31 | eleq1d 2826 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∈ 𝐿1 ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄) ∈
𝐿1)) |
| 33 | 30, 32 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄) ∈
𝐿1) |
| 34 | | intlewftc.8 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 35 | | cncff 24919 |
. . . . . . . 8
⊢ (𝐷 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐷:(𝐴(,)𝐵)⟶ℝ) |
| 36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐷:(𝐴(,)𝐵)⟶ℝ) |
| 37 | 27 | feq1d 6720 |
. . . . . . 7
⊢ (𝜑 → (𝐷:(𝐴(,)𝐵)⟶ℝ ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃):(𝐴(,)𝐵)⟶ℝ)) |
| 38 | 36, 37 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃):(𝐴(,)𝐵)⟶ℝ) |
| 39 | 38 | fvmptelcdm 7133 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ∈ ℝ) |
| 40 | | intlewftc.9 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 41 | | cncff 24919 |
. . . . . . . 8
⊢ (𝐸 ∈ ((𝐴(,)𝐵)–cn→ℝ) → 𝐸:(𝐴(,)𝐵)⟶ℝ) |
| 42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐸:(𝐴(,)𝐵)⟶ℝ) |
| 43 | 31 | feq1d 6720 |
. . . . . . 7
⊢ (𝜑 → (𝐸:(𝐴(,)𝐵)⟶ℝ ↔ (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄):(𝐴(,)𝐵)⟶ℝ)) |
| 44 | 42, 43 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄):(𝐴(,)𝐵)⟶ℝ) |
| 45 | 44 | fvmptelcdm 7133 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑄 ∈ ℝ) |
| 46 | | intlewftc.14 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑃 ≤ 𝑄) |
| 47 | 29, 33, 39, 45, 46 | itgle 25845 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑃 d𝑥 ≤ ∫(𝐴(,)𝐵)𝑄 d𝑥) |
| 48 | 39 | itgmpt 25818 |
. . . . . 6
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑃 d𝑥 = ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡) d𝑡) |
| 49 | 27 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷‘𝑡) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡)) |
| 50 | 49 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐷‘𝑡) = ((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡)) |
| 51 | 50 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡) = (𝐷‘𝑡)) |
| 52 | 51 | itgeq2dv 25817 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)(𝐷‘𝑡) d𝑡) |
| 53 | | intlewftc.6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 = (ℝ D 𝐹)) |
| 54 | 53 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐷 = (ℝ D 𝐹)) |
| 55 | 54 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐷‘𝑡) = ((ℝ D 𝐹)‘𝑡)) |
| 56 | 55 | itgeq2dv 25817 |
. . . . . . . 8
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐷‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
| 57 | | ax-resscn 11212 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
| 58 | 57 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 59 | | fss 6752 |
. . . . . . . . . . . 12
⊢ ((𝐷:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐷:(𝐴(,)𝐵)⟶ℂ) |
| 60 | 36, 58, 59 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷:(𝐴(,)𝐵)⟶ℂ) |
| 61 | | ssidd 4007 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 62 | | cncfcdm 24924 |
. . . . . . . . . . . 12
⊢ ((ℂ
⊆ ℂ ∧ 𝐷
∈ ((𝐴(,)𝐵)–cn→ℝ)) → (𝐷 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ 𝐷:(𝐴(,)𝐵)⟶ℂ)) |
| 63 | 61, 34, 62 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ 𝐷:(𝐴(,)𝐵)⟶ℂ)) |
| 64 | 60, 63 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 65 | 53 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))) |
| 66 | 64, 65 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 67 | 53, 26 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) ∈
𝐿1) |
| 68 | | fss 6752 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴[,]𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
| 69 | 3, 58, 68 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
| 70 | | cncfcdm 24924 |
. . . . . . . . . . 11
⊢ ((ℂ
⊆ ℂ ∧ 𝐹
∈ ((𝐴[,]𝐵)–cn→ℝ)) → (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ 𝐹:(𝐴[,]𝐵)⟶ℂ)) |
| 71 | 61, 1, 70 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ 𝐹:(𝐴[,]𝐵)⟶ℂ)) |
| 72 | 69, 71 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 73 | 8, 4, 5, 66, 67, 72 | ftc2 26085 |
. . . . . . . 8
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
| 74 | 56, 73 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐷‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
| 75 | 52, 74 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑃)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
| 76 | 48, 75 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑃 d𝑥 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
| 77 | 45 | itgmpt 25818 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑄 d𝑥 = ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)‘𝑡) d𝑡) |
| 78 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐸 = (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)) |
| 79 | 78 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄) = 𝐸) |
| 80 | 79 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)‘𝑡) = (𝐸‘𝑡)) |
| 81 | 80 | itgeq2dv 25817 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑄)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)(𝐸‘𝑡) d𝑡) |
| 82 | 77, 81 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑄 d𝑥 = ∫(𝐴(,)𝐵)(𝐸‘𝑡) d𝑡) |
| 83 | | intlewftc.7 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 = (ℝ D 𝐺)) |
| 84 | 83 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → 𝐸 = (ℝ D 𝐺)) |
| 85 | 84 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐸‘𝑡) = ((ℝ D 𝐺)‘𝑡)) |
| 86 | 85 | itgeq2dv 25817 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐸‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐺)‘𝑡) d𝑡) |
| 87 | | fss 6752 |
. . . . . . . . . . . . 13
⊢ ((𝐸:(𝐴(,)𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐸:(𝐴(,)𝐵)⟶ℂ) |
| 88 | 42, 58, 87 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸:(𝐴(,)𝐵)⟶ℂ) |
| 89 | | cncfcdm 24924 |
. . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ 𝐸
∈ ((𝐴(,)𝐵)–cn→ℝ)) → (𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ 𝐸:(𝐴(,)𝐵)⟶ℂ)) |
| 90 | 61, 40, 89 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ 𝐸:(𝐴(,)𝐵)⟶ℂ)) |
| 91 | 88, 90 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 92 | 83 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ) ↔ (ℝ D 𝐺) ∈ ((𝐴(,)𝐵)–cn→ℂ))) |
| 93 | 91, 92 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐺) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 94 | 93, 92 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 95 | 94, 92 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐺) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 96 | 83, 30 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐺) ∈
𝐿1) |
| 97 | | fss 6752 |
. . . . . . . . . 10
⊢ ((𝐺:(𝐴[,]𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
| 98 | 22, 58, 97 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
| 99 | | cncfcdm 24924 |
. . . . . . . . . 10
⊢ ((ℂ
⊆ ℂ ∧ 𝐺
∈ ((𝐴[,]𝐵)–cn→ℝ)) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ 𝐺:(𝐴[,]𝐵)⟶ℂ)) |
| 100 | 61, 20, 99 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ 𝐺:(𝐴[,]𝐵)⟶ℂ)) |
| 101 | 98, 100 | mpbird 257 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 102 | 8, 4, 5, 95, 96, 101 | ftc2 26085 |
. . . . . . 7
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐺)‘𝑡) d𝑡 = ((𝐺‘𝐵) − (𝐺‘𝐴))) |
| 103 | 86, 102 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐸‘𝑡) d𝑡 = ((𝐺‘𝐵) − (𝐺‘𝐴))) |
| 104 | 82, 103 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝑄 d𝑥 = ((𝐺‘𝐵) − (𝐺‘𝐴))) |
| 105 | 76, 104 | breq12d 5156 |
. . . 4
⊢ (𝜑 → (∫(𝐴(,)𝐵)𝑃 d𝑥 ≤ ∫(𝐴(,)𝐵)𝑄 d𝑥 ↔ ((𝐹‘𝐵) − (𝐹‘𝐴)) ≤ ((𝐺‘𝐵) − (𝐺‘𝐴)))) |
| 106 | 47, 105 | mpbid 232 |
. . 3
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ≤ ((𝐺‘𝐵) − (𝐺‘𝐴))) |
| 107 | | intlewftc.15 |
. . 3
⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐺‘𝐴)) |
| 108 | 19, 18, 25, 24, 106, 107 | le2addd 11882 |
. 2
⊢ (𝜑 → (((𝐹‘𝐵) − (𝐹‘𝐴)) + (𝐹‘𝐴)) ≤ (((𝐺‘𝐵) − (𝐺‘𝐴)) + (𝐺‘𝐴))) |
| 109 | 57, 12 | sselid 3981 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ) |
| 110 | 57, 18 | sselid 3981 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) |
| 111 | 109, 110 | npcand 11624 |
. . 3
⊢ (𝜑 → (((𝐹‘𝐵) − (𝐹‘𝐴)) + (𝐹‘𝐴)) = (𝐹‘𝐵)) |
| 112 | 57, 23 | sselid 3981 |
. . . 4
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℂ) |
| 113 | 57, 24 | sselid 3981 |
. . . 4
⊢ (𝜑 → (𝐺‘𝐴) ∈ ℂ) |
| 114 | 112, 113 | npcand 11624 |
. . 3
⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) + (𝐺‘𝐴)) = (𝐺‘𝐵)) |
| 115 | 111, 114 | breq12d 5156 |
. 2
⊢ (𝜑 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) + (𝐹‘𝐴)) ≤ (((𝐺‘𝐵) − (𝐺‘𝐴)) + (𝐺‘𝐴)) ↔ (𝐹‘𝐵) ≤ (𝐺‘𝐵))) |
| 116 | 108, 115 | mpbid 232 |
1
⊢ (𝜑 → (𝐹‘𝐵) ≤ (𝐺‘𝐵)) |