| Step | Hyp | Ref
| Expression |
| 1 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇))) |
| 2 | 1 | rexbidv 3179 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
| 3 | 2 | elrab 3692 |
. . . . 5
⊢ (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
| 4 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
| 5 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑧𝜑 |
| 6 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑧 𝑥 ∈ ℂ |
| 7 | | nfre1 3285 |
. . . . . . . . 9
⊢
Ⅎ𝑧∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) |
| 8 | 6, 7 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝑥 ∈ ℂ ∧
∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
| 9 | 5, 8 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑧(𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) |
| 10 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑧 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) |
| 11 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 = (𝑧 + 𝑇)) |
| 12 | | iccshift.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 13 | | iccshift.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 14 | 12, 13 | iccssred 13474 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 15 | 14 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ ℝ) |
| 16 | | iccshift.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ) |
| 18 | 15, 17 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ∈ ℝ) |
| 19 | 12 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ) |
| 20 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ (𝐴[,]𝐵)) |
| 21 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
| 22 | | elicc2 13452 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
| 23 | 19, 21, 22 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))) |
| 24 | 20, 23 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)) |
| 25 | 24 | simp2d 1144 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑧) |
| 26 | 19, 15, 17, 25 | leadd1dd 11877 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑧 + 𝑇)) |
| 27 | 24 | simp3d 1145 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ≤ 𝐵) |
| 28 | 15, 21, 17, 27 | leadd1dd 11877 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)) |
| 29 | 18, 26, 28 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))) |
| 30 | 29 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))) |
| 31 | 12, 16 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 + 𝑇) ∈ ℝ) |
| 32 | 31 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐴 + 𝑇) ∈ ℝ) |
| 33 | 13, 16 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 + 𝑇) ∈ ℝ) |
| 34 | 33 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐵 + 𝑇) ∈ ℝ) |
| 35 | | elicc2 13452 |
. . . . . . . . . . . 12
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))) |
| 36 | 32, 34, 35 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))) |
| 37 | 30, 36 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 38 | 11, 37 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 39 | 38 | 3exp 1120 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))) |
| 40 | 39 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))) |
| 41 | 9, 10, 40 | rexlimd 3266 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
| 42 | 4, 41 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 43 | 3, 42 | sylan2b 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 44 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ) |
| 45 | 33 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ) |
| 46 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 47 | | eliccre 45518 |
. . . . . . 7
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
| 48 | 44, 45, 46, 47 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ) |
| 49 | 48 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ) |
| 50 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ) |
| 51 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ) |
| 52 | 16 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℝ) |
| 53 | 48, 52 | resubcld 11691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ) |
| 54 | 12 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 55 | 16 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℂ) |
| 56 | 54, 55 | pncand 11621 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴) |
| 57 | 56 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
| 58 | 57 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇)) |
| 59 | | elicc2 13452 |
. . . . . . . . . . . 12
⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
| 60 | 44, 45, 59 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))) |
| 61 | 46, 60 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))) |
| 62 | 61 | simp2d 1144 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥) |
| 63 | 44, 48, 52, 62 | lesub1dd 11879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) ≤ (𝑥 − 𝑇)) |
| 64 | 58, 63 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 − 𝑇)) |
| 65 | 61 | simp3d 1145 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇)) |
| 66 | 48, 45, 52, 65 | lesub1dd 11879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ ((𝐵 + 𝑇) − 𝑇)) |
| 67 | 13 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 68 | 67, 55 | pncand 11621 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
| 69 | 68 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵) |
| 70 | 66, 69 | breqtrd 5169 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ 𝐵) |
| 71 | 50, 51, 53, 64, 70 | eliccd 45517 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) |
| 72 | 55 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ) |
| 73 | 49, 72 | npcand 11624 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 − 𝑇) + 𝑇) = 𝑥) |
| 74 | 73 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 = ((𝑥 − 𝑇) + 𝑇)) |
| 75 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑧 = (𝑥 − 𝑇) → (𝑧 + 𝑇) = ((𝑥 − 𝑇) + 𝑇)) |
| 76 | 75 | rspceeqv 3645 |
. . . . . 6
⊢ (((𝑥 − 𝑇) ∈ (𝐴[,]𝐵) ∧ 𝑥 = ((𝑥 − 𝑇) + 𝑇)) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
| 77 | 71, 74, 76 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)) |
| 78 | 49, 77, 3 | sylanbrc 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) |
| 79 | 43, 78 | impbida 801 |
. . 3
⊢ (𝜑 → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))) |
| 80 | 79 | eqrdv 2735 |
. 2
⊢ (𝜑 → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) |
| 81 | 80 | eqcomd 2743 |
1
⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) |