Proof of Theorem itgsplitioo
| Step | Hyp | Ref
| Expression |
| 1 | | itgsplitioo.3 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶)) |
| 2 | | itgsplitioo.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 3 | | itgsplitioo.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 4 | | elicc2 13452 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ∈ (𝐴[,]𝐶) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶))) |
| 5 | 2, 3, 4 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∈ (𝐴[,]𝐶) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶))) |
| 6 | 1, 5 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) |
| 7 | 6 | simp2d 1144 |
. . . . 5
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 8 | 6 | simp1d 1143 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 9 | 2, 8 | leloed 11404 |
. . . . 5
⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) |
| 10 | 7, 9 | mpbid 232 |
. . . 4
⊢ (𝜑 → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)) |
| 11 | 10 | ord 865 |
. . 3
⊢ (𝜑 → (¬ 𝐴 < 𝐵 → 𝐴 = 𝐵)) |
| 12 | 2 | rexrd 11311 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 13 | | iooss1 13422 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) |
| 14 | 12, 7, 13 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) |
| 15 | 14 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐴(,)𝐶)) |
| 16 | | itgsplitioo.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐶)) → 𝐷 ∈ ℂ) |
| 17 | 15, 16 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝐷 ∈ ℂ) |
| 18 | | itgsplitioo.6 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐵(,)𝐶) ↦ 𝐷) ∈
𝐿1) |
| 19 | 17, 18 | itgcl 25819 |
. . . . . 6
⊢ (𝜑 → ∫(𝐵(,)𝐶)𝐷 d𝑥 ∈ ℂ) |
| 20 | 19 | addlidd 11462 |
. . . . 5
⊢ (𝜑 → (0 + ∫(𝐵(,)𝐶)𝐷 d𝑥) = ∫(𝐵(,)𝐶)𝐷 d𝑥) |
| 21 | 20 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → ∫(𝐵(,)𝐶)𝐷 d𝑥 = (0 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) |
| 22 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐴(,)𝐶) = (𝐵(,)𝐶)) |
| 23 | | itgeq1 25808 |
. . . . . 6
⊢ ((𝐴(,)𝐶) = (𝐵(,)𝐶) → ∫(𝐴(,)𝐶)𝐷 d𝑥 = ∫(𝐵(,)𝐶)𝐷 d𝑥) |
| 24 | 22, 23 | syl 17 |
. . . . 5
⊢ (𝐴 = 𝐵 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = ∫(𝐵(,)𝐶)𝐷 d𝑥) |
| 25 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → (𝐴(,)𝐵) = (𝐵(,)𝐵)) |
| 26 | | iooid 13415 |
. . . . . . . . 9
⊢ (𝐵(,)𝐵) = ∅ |
| 27 | 25, 26 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → (𝐴(,)𝐵) = ∅) |
| 28 | | itgeq1 25808 |
. . . . . . . 8
⊢ ((𝐴(,)𝐵) = ∅ → ∫(𝐴(,)𝐵)𝐷 d𝑥 = ∫∅𝐷 d𝑥) |
| 29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → ∫(𝐴(,)𝐵)𝐷 d𝑥 = ∫∅𝐷 d𝑥) |
| 30 | | itg0 25815 |
. . . . . . 7
⊢
∫∅𝐷 d𝑥 = 0 |
| 31 | 29, 30 | eqtrdi 2793 |
. . . . . 6
⊢ (𝐴 = 𝐵 → ∫(𝐴(,)𝐵)𝐷 d𝑥 = 0) |
| 32 | 31 | oveq1d 7446 |
. . . . 5
⊢ (𝐴 = 𝐵 → (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥) = (0 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) |
| 33 | 24, 32 | eqeq12d 2753 |
. . . 4
⊢ (𝐴 = 𝐵 → (∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥) ↔ ∫(𝐵(,)𝐶)𝐷 d𝑥 = (0 + ∫(𝐵(,)𝐶)𝐷 d𝑥))) |
| 34 | 21, 33 | syl5ibrcom 247 |
. . 3
⊢ (𝜑 → (𝐴 = 𝐵 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥))) |
| 35 | 11, 34 | syld 47 |
. 2
⊢ (𝜑 → (¬ 𝐴 < 𝐵 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥))) |
| 36 | 6 | simp3d 1145 |
. . . . 5
⊢ (𝜑 → 𝐵 ≤ 𝐶) |
| 37 | 8, 3 | leloed 11404 |
. . . . 5
⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
| 38 | 36, 37 | mpbid 232 |
. . . 4
⊢ (𝜑 → (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)) |
| 39 | 38 | ord 865 |
. . 3
⊢ (𝜑 → (¬ 𝐵 < 𝐶 → 𝐵 = 𝐶)) |
| 40 | 3 | rexrd 11311 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
| 41 | | iooss2 13423 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ*
∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) |
| 42 | 40, 36, 41 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) |
| 43 | 42 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐶)) |
| 44 | 43, 16 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐷 ∈ ℂ) |
| 45 | | itgsplitioo.5 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈
𝐿1) |
| 46 | 44, 45 | itgcl 25819 |
. . . . . 6
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝐷 d𝑥 ∈ ℂ) |
| 47 | 46 | addridd 11461 |
. . . . 5
⊢ (𝜑 → (∫(𝐴(,)𝐵)𝐷 d𝑥 + 0) = ∫(𝐴(,)𝐵)𝐷 d𝑥) |
| 48 | 47 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → ∫(𝐴(,)𝐵)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + 0)) |
| 49 | | oveq2 7439 |
. . . . . 6
⊢ (𝐵 = 𝐶 → (𝐴(,)𝐵) = (𝐴(,)𝐶)) |
| 50 | | itgeq1 25808 |
. . . . . 6
⊢ ((𝐴(,)𝐵) = (𝐴(,)𝐶) → ∫(𝐴(,)𝐵)𝐷 d𝑥 = ∫(𝐴(,)𝐶)𝐷 d𝑥) |
| 51 | 49, 50 | syl 17 |
. . . . 5
⊢ (𝐵 = 𝐶 → ∫(𝐴(,)𝐵)𝐷 d𝑥 = ∫(𝐴(,)𝐶)𝐷 d𝑥) |
| 52 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝐵 = 𝐶 → (𝐵(,)𝐵) = (𝐵(,)𝐶)) |
| 53 | 26, 52 | eqtr3id 2791 |
. . . . . . . 8
⊢ (𝐵 = 𝐶 → ∅ = (𝐵(,)𝐶)) |
| 54 | | itgeq1 25808 |
. . . . . . . 8
⊢ (∅
= (𝐵(,)𝐶) → ∫∅𝐷 d𝑥 = ∫(𝐵(,)𝐶)𝐷 d𝑥) |
| 55 | 53, 54 | syl 17 |
. . . . . . 7
⊢ (𝐵 = 𝐶 → ∫∅𝐷 d𝑥 = ∫(𝐵(,)𝐶)𝐷 d𝑥) |
| 56 | 30, 55 | eqtr3id 2791 |
. . . . . 6
⊢ (𝐵 = 𝐶 → 0 = ∫(𝐵(,)𝐶)𝐷 d𝑥) |
| 57 | 56 | oveq2d 7447 |
. . . . 5
⊢ (𝐵 = 𝐶 → (∫(𝐴(,)𝐵)𝐷 d𝑥 + 0) = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) |
| 58 | 51, 57 | eqeq12d 2753 |
. . . 4
⊢ (𝐵 = 𝐶 → (∫(𝐴(,)𝐵)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + 0) ↔ ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥))) |
| 59 | 48, 58 | syl5ibcom 245 |
. . 3
⊢ (𝜑 → (𝐵 = 𝐶 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥))) |
| 60 | 39, 59 | syld 47 |
. 2
⊢ (𝜑 → (¬ 𝐵 < 𝐶 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥))) |
| 61 | | indir 4286 |
. . . . . . . 8
⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ∩ (𝐵(,)𝐶)) = (((𝐴(,)𝐵) ∩ (𝐵(,)𝐶)) ∪ ({𝐵} ∩ (𝐵(,)𝐶))) |
| 62 | 8 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 63 | 12, 62 | jca 511 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
| 65 | 62, 40 | jca 511 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∈ ℝ* ∧ 𝐶 ∈
ℝ*)) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈
ℝ*)) |
| 67 | 8 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ) |
| 68 | 67 | leidd 11829 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ≤ 𝐵) |
| 69 | | ioodisj 13522 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
∧ 𝐵 ≤ 𝐵) → ((𝐴(,)𝐵) ∩ (𝐵(,)𝐶)) = ∅) |
| 70 | 64, 66, 68, 69 | syl21anc 838 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,)𝐵) ∩ (𝐵(,)𝐶)) = ∅) |
| 71 | | incom 4209 |
. . . . . . . . . . 11
⊢ ({𝐵} ∩ (𝐵(,)𝐶)) = ((𝐵(,)𝐶) ∩ {𝐵}) |
| 72 | 67 | ltnrd 11395 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ¬ 𝐵 < 𝐵) |
| 73 | | eliooord 13446 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐵 ∧ 𝐵 < 𝐶)) |
| 74 | 73 | simpld 494 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (𝐵(,)𝐶) → 𝐵 < 𝐵) |
| 75 | 72, 74 | nsyl 140 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ¬ 𝐵 ∈ (𝐵(,)𝐶)) |
| 76 | | disjsn 4711 |
. . . . . . . . . . . 12
⊢ (((𝐵(,)𝐶) ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ (𝐵(,)𝐶)) |
| 77 | 75, 76 | sylibr 234 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐵(,)𝐶) ∩ {𝐵}) = ∅) |
| 78 | 71, 77 | eqtrid 2789 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ({𝐵} ∩ (𝐵(,)𝐶)) = ∅) |
| 79 | 70, 78 | uneq12d 4169 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝐴(,)𝐵) ∩ (𝐵(,)𝐶)) ∪ ({𝐵} ∩ (𝐵(,)𝐶))) = (∅ ∪
∅)) |
| 80 | | un0 4394 |
. . . . . . . . 9
⊢ (∅
∪ ∅) = ∅ |
| 81 | 79, 80 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝐴(,)𝐵) ∩ (𝐵(,)𝐶)) ∪ ({𝐵} ∩ (𝐵(,)𝐶))) = ∅) |
| 82 | 61, 81 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝐴(,)𝐵) ∪ {𝐵}) ∩ (𝐵(,)𝐶)) = ∅) |
| 83 | 82 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (vol*‘(((𝐴(,)𝐵) ∪ {𝐵}) ∩ (𝐵(,)𝐶))) = (vol*‘∅)) |
| 84 | | ovol0 25528 |
. . . . . 6
⊢
(vol*‘∅) = 0 |
| 85 | 83, 84 | eqtrdi 2793 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (vol*‘(((𝐴(,)𝐵) ∪ {𝐵}) ∩ (𝐵(,)𝐶))) = 0) |
| 86 | 12, 62, 40 | 3jca 1129 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*)) |
| 87 | | ioojoin 13523 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝐴(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)𝐶)) = (𝐴(,)𝐶)) |
| 88 | 86, 87 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝐴(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)𝐶)) = (𝐴(,)𝐶)) |
| 89 | 88 | eqcomd 2743 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝐴(,)𝐶) = (((𝐴(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)𝐶))) |
| 90 | 16 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) ∧ 𝑥 ∈ (𝐴(,)𝐶)) → 𝐷 ∈ ℂ) |
| 91 | 45 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈
𝐿1) |
| 92 | | ssun1 4178 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ {𝐵}) |
| 93 | 92 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ {𝐵})) |
| 94 | | ioossre 13448 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 95 | 94 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝐴(,)𝐵) ⊆ ℝ) |
| 96 | 67 | snssd 4809 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → {𝐵} ⊆ ℝ) |
| 97 | 95, 96 | unssd 4192 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ ℝ) |
| 98 | | uncom 4158 |
. . . . . . . . . . . 12
⊢ ((𝐴(,)𝐵) ∪ {𝐵}) = ({𝐵} ∪ (𝐴(,)𝐵)) |
| 99 | 98 | difeq1i 4122 |
. . . . . . . . . . 11
⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ∖ (𝐴(,)𝐵)) = (({𝐵} ∪ (𝐴(,)𝐵)) ∖ (𝐴(,)𝐵)) |
| 100 | | difun2 4481 |
. . . . . . . . . . 11
⊢ (({𝐵} ∪ (𝐴(,)𝐵)) ∖ (𝐴(,)𝐵)) = ({𝐵} ∖ (𝐴(,)𝐵)) |
| 101 | 99, 100 | eqtri 2765 |
. . . . . . . . . 10
⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ∖ (𝐴(,)𝐵)) = ({𝐵} ∖ (𝐴(,)𝐵)) |
| 102 | | difss 4136 |
. . . . . . . . . 10
⊢ ({𝐵} ∖ (𝐴(,)𝐵)) ⊆ {𝐵} |
| 103 | 101, 102 | eqsstri 4030 |
. . . . . . . . 9
⊢ (((𝐴(,)𝐵) ∪ {𝐵}) ∖ (𝐴(,)𝐵)) ⊆ {𝐵} |
| 104 | | ovolsn 25530 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ →
(vol*‘{𝐵}) =
0) |
| 105 | 67, 104 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (vol*‘{𝐵}) = 0) |
| 106 | | ovolssnul 25522 |
. . . . . . . . 9
⊢
(((((𝐴(,)𝐵) ∪ {𝐵}) ∖ (𝐴(,)𝐵)) ⊆ {𝐵} ∧ {𝐵} ⊆ ℝ ∧ (vol*‘{𝐵}) = 0) →
(vol*‘(((𝐴(,)𝐵) ∪ {𝐵}) ∖ (𝐴(,)𝐵))) = 0) |
| 107 | 103, 96, 105, 106 | mp3an2i 1468 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (vol*‘(((𝐴(,)𝐵) ∪ {𝐵}) ∖ (𝐴(,)𝐵))) = 0) |
| 108 | | ssun1 4178 |
. . . . . . . . . . 11
⊢ ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ (((𝐴(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)𝐶)) |
| 109 | 108, 88 | sseqtrid 4026 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,)𝐵) ∪ {𝐵}) ⊆ (𝐴(,)𝐶)) |
| 110 | 109 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) ∧ 𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐵})) → 𝑥 ∈ (𝐴(,)𝐶)) |
| 111 | 110, 90 | syldan 591 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) ∧ 𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐵})) → 𝐷 ∈ ℂ) |
| 112 | 93, 97, 107, 111 | itgss3 25850 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈ 𝐿1 ↔ (𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐵}) ↦ 𝐷) ∈ 𝐿1) ∧
∫(𝐴(,)𝐵)𝐷 d𝑥 = ∫((𝐴(,)𝐵) ∪ {𝐵})𝐷 d𝑥)) |
| 113 | 112 | simpld 494 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈ 𝐿1 ↔ (𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐵}) ↦ 𝐷) ∈
𝐿1)) |
| 114 | 91, 113 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐵}) ↦ 𝐷) ∈
𝐿1) |
| 115 | 18 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (𝑥 ∈ (𝐵(,)𝐶) ↦ 𝐷) ∈
𝐿1) |
| 116 | 85, 89, 90, 114, 115 | itgsplit 25871 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫((𝐴(,)𝐵) ∪ {𝐵})𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) |
| 117 | 112 | simprd 495 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ∫(𝐴(,)𝐵)𝐷 d𝑥 = ∫((𝐴(,)𝐵) ∪ {𝐵})𝐷 d𝑥) |
| 118 | 117 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥) = (∫((𝐴(,)𝐵) ∪ {𝐵})𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) |
| 119 | 116, 118 | eqtr4d 2780 |
. . 3
⊢ ((𝜑 ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) |
| 120 | 119 | ex 412 |
. 2
⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥))) |
| 121 | 35, 60, 120 | ecased 1036 |
1
⊢ (𝜑 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥)) |