| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prfi 9363 | . . 3
⊢ {ran
𝑄, ∪ ran 𝐼} ∈ Fin | 
| 2 | 1 | a1i 11 | . 2
⊢ (𝜑 → {ran 𝑄, ∪ ran 𝐼} ∈ Fin) | 
| 3 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) | 
| 4 |  | fourierdlem70.q | . . . . . . . . . . 11
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) | 
| 5 |  | ovex 7464 | . . . . . . . . . . 11
⊢
(0...𝑀) ∈
V | 
| 6 |  | fex 7246 | . . . . . . . . . . 11
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ V) → 𝑄 ∈ V) | 
| 7 | 4, 5, 6 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ V) | 
| 8 |  | rnexg 7924 | . . . . . . . . . 10
⊢ (𝑄 ∈ V → ran 𝑄 ∈ V) | 
| 9 | 7, 8 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ran 𝑄 ∈ V) | 
| 10 |  | fzofi 14015 | . . . . . . . . . . . 12
⊢
(0..^𝑀) ∈
Fin | 
| 11 |  | fourierdlem70.i | . . . . . . . . . . . . 13
⊢ 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) | 
| 12 | 11 | rnmptfi 45176 | . . . . . . . . . . . 12
⊢
((0..^𝑀) ∈ Fin
→ ran 𝐼 ∈
Fin) | 
| 13 | 10, 12 | ax-mp 5 | . . . . . . . . . . 11
⊢ ran 𝐼 ∈ Fin | 
| 14 | 13 | elexi 3503 | . . . . . . . . . 10
⊢ ran 𝐼 ∈ V | 
| 15 | 14 | uniex 7761 | . . . . . . . . 9
⊢ ∪ ran 𝐼 ∈ V | 
| 16 |  | uniprg 4923 | . . . . . . . . 9
⊢ ((ran
𝑄 ∈ V ∧ ∪ ran 𝐼 ∈ V) → ∪ {ran 𝑄, ∪ ran 𝐼} = (ran 𝑄 ∪ ∪ ran
𝐼)) | 
| 17 | 9, 15, 16 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → ∪ {ran 𝑄, ∪ ran 𝐼} = (ran 𝑄 ∪ ∪ ran
𝐼)) | 
| 18 | 17 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → ∪ {ran
𝑄, ∪ ran 𝐼} = (ran 𝑄 ∪ ∪ ran
𝐼)) | 
| 19 | 3, 18 | eleqtrd 2843 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) | 
| 20 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ
↑m (0...𝑦))
∣ (((𝑣‘0) =
𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))}) = (𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑m
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))}) | 
| 21 |  | fourierdlem70.m | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 22 |  | reex 11246 | . . . . . . . . . . . . . . 15
⊢ ℝ
∈ V | 
| 23 | 22, 5 | elmap 8911 | . . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
↔ 𝑄:(0...𝑀)⟶ℝ) | 
| 24 | 4, 23 | sylibr 234 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) | 
| 25 |  | fourierdlem70.q0 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘0) = 𝐴) | 
| 26 |  | fourierdlem70.qm | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) | 
| 27 | 25, 26 | jca 511 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) | 
| 28 |  | fourierdlem70.qlt | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 29 | 28 | ralrimiva 3146 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 30 | 24, 27, 29 | jca32 515 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) | 
| 31 | 20 | fourierdlem2 46124 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ ((𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑m
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))})‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 32 | 21, 31 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∈ ((𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑m
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))})‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 33 | 30, 32 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ((𝑦 ∈ ℕ ↦ {𝑣 ∈ (ℝ ↑m
(0...𝑦)) ∣ (((𝑣‘0) = 𝐴 ∧ (𝑣‘𝑦) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑦)(𝑣‘𝑖) < (𝑣‘(𝑖 + 1)))})‘𝑀)) | 
| 34 | 20, 21, 33 | fourierdlem15 46137 | . . . . . . . . . 10
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) | 
| 35 | 34 | frnd 6744 | . . . . . . . . 9
⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵)) | 
| 36 | 35 | sselda 3983 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 37 | 36 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 38 |  | simpll 767 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝜑) | 
| 39 |  | elunnel1 4154 | . . . . . . . . 9
⊢ ((𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ ∪ ran
𝐼) | 
| 40 | 39 | adantll 714 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ ∪ ran
𝐼) | 
| 41 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝑠 ∈ ∪ ran 𝐼) | 
| 42 | 11 | funmpt2 6605 | . . . . . . . . . . 11
⊢ Fun 𝐼 | 
| 43 |  | elunirn 7271 | . . . . . . . . . . 11
⊢ (Fun
𝐼 → (𝑠 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖))) | 
| 44 | 42, 43 | mp1i 13 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → (𝑠 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖))) | 
| 45 | 41, 44 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → ∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖)) | 
| 46 |  | id 22 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ dom 𝐼) | 
| 47 |  | ovex 7464 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V | 
| 48 | 47, 11 | dmmpti 6712 | . . . . . . . . . . . . . . . . . 18
⊢ dom 𝐼 = (0..^𝑀) | 
| 49 | 46, 48 | eleqtrdi 2851 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ dom 𝐼 → 𝑖 ∈ (0..^𝑀)) | 
| 50 | 11 | fvmpt2 7027 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (0..^𝑀) ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∈ V) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) | 
| 51 | 49, 47, 50 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ dom 𝐼 → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) | 
| 52 | 51 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) | 
| 53 |  | ioossicc 13473 | . . . . . . . . . . . . . . . 16
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) | 
| 54 |  | fourierdlem70.a | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 55 | 54 | rexrd 11311 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝐴 ∈
ℝ*) | 
| 57 |  | fourierdlem70.2 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 58 | 57 | rexrd 11311 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 59 | 58 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝐵 ∈
ℝ*) | 
| 60 | 34 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) | 
| 61 | 49 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → 𝑖 ∈ (0..^𝑀)) | 
| 62 | 56, 59, 60, 61 | fourierdlem8 46130 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵)) | 
| 63 | 53, 62 | sstrid 3995 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵)) | 
| 64 | 52, 63 | eqsstrd 4018 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝐼‘𝑖) ⊆ (𝐴[,]𝐵)) | 
| 65 | 64 | 3adant3 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ (𝐼‘𝑖)) → (𝐼‘𝑖) ⊆ (𝐴[,]𝐵)) | 
| 66 |  | simp3 1139 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ (𝐼‘𝑖)) → 𝑠 ∈ (𝐼‘𝑖)) | 
| 67 | 65, 66 | sseldd 3984 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼 ∧ 𝑠 ∈ (𝐼‘𝑖)) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 68 | 67 | 3exp 1120 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ dom 𝐼 → (𝑠 ∈ (𝐼‘𝑖) → 𝑠 ∈ (𝐴[,]𝐵)))) | 
| 69 | 68 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → (𝑖 ∈ dom 𝐼 → (𝑠 ∈ (𝐼‘𝑖) → 𝑠 ∈ (𝐴[,]𝐵)))) | 
| 70 | 69 | rexlimdv 3153 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → (∃𝑖 ∈ dom 𝐼 𝑠 ∈ (𝐼‘𝑖) → 𝑠 ∈ (𝐴[,]𝐵))) | 
| 71 | 45, 70 | mpd 15 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 72 | 38, 40, 71 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) ∧ ¬ 𝑠 ∈ ran 𝑄) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 73 | 37, 72 | pm2.61dan 813 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 74 | 19, 73 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 75 |  | fourierdlem70.f | . . . . . 6
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) | 
| 76 | 75 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑠) ∈ ℝ) | 
| 77 | 74, 76 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → (𝐹‘𝑠) ∈ ℝ) | 
| 78 | 77 | recnd 11289 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → (𝐹‘𝑠) ∈ ℂ) | 
| 79 | 78 | abscld 15475 | . 2
⊢ ((𝜑 ∧ 𝑠 ∈ ∪ {ran
𝑄, ∪ ran 𝐼}) → (abs‘(𝐹‘𝑠)) ∈ ℝ) | 
| 80 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → 𝑤 = ran 𝑄) | 
| 81 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ) | 
| 82 |  | fzfid 14014 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → (0...𝑀) ∈ Fin) | 
| 83 |  | rnffi 45180 | . . . . . . 7
⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin) | 
| 84 | 81, 82, 83 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → ran 𝑄 ∈ Fin) | 
| 85 | 80, 84 | eqeltrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → 𝑤 ∈ Fin) | 
| 86 | 85 | adantlr 715 | . . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ 𝑤 = ran 𝑄) → 𝑤 ∈ Fin) | 
| 87 | 75 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝐹:(𝐴[,]𝐵)⟶ℝ) | 
| 88 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝜑) | 
| 89 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ 𝑤) | 
| 90 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤) → 𝑤 = ran 𝑄) | 
| 91 | 89, 90 | eleqtrd 2843 | . . . . . . . . . . 11
⊢ ((𝑤 = ran 𝑄 ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ ran 𝑄) | 
| 92 | 91 | adantll 714 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ ran 𝑄) | 
| 93 | 88, 92, 36 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 94 | 87, 93 | ffvelcdmd 7105 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → (𝐹‘𝑠) ∈ ℝ) | 
| 95 | 94 | recnd 11289 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → (𝐹‘𝑠) ∈ ℂ) | 
| 96 | 95 | abscld 15475 | . . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ran 𝑄) ∧ 𝑠 ∈ 𝑤) → (abs‘(𝐹‘𝑠)) ∈ ℝ) | 
| 97 | 96 | ralrimiva 3146 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 = ran 𝑄) → ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ∈ ℝ) | 
| 98 | 97 | adantlr 715 | . . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ 𝑤 = ran 𝑄) → ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ∈ ℝ) | 
| 99 |  | fimaxre3 12214 | . . . 4
⊢ ((𝑤 ∈ Fin ∧ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ∈ ℝ) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) | 
| 100 | 86, 98, 99 | syl2anc 584 | . . 3
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ 𝑤 = ran 𝑄) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) | 
| 101 |  | simpll 767 | . . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ ¬ 𝑤 = ran 𝑄) → 𝜑) | 
| 102 |  | neqne 2948 | . . . . . 6
⊢ (¬
𝑤 = ran 𝑄 → 𝑤 ≠ ran 𝑄) | 
| 103 |  | elprn1 45648 | . . . . . 6
⊢ ((𝑤 ∈ {ran 𝑄, ∪ ran 𝐼} ∧ 𝑤 ≠ ran 𝑄) → 𝑤 = ∪ ran 𝐼) | 
| 104 | 102, 103 | sylan2 593 | . . . . 5
⊢ ((𝑤 ∈ {ran 𝑄, ∪ ran 𝐼} ∧ ¬ 𝑤 = ran 𝑄) → 𝑤 = ∪ ran 𝐼) | 
| 105 | 104 | adantll 714 | . . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ ¬ 𝑤 = ran 𝑄) → 𝑤 = ∪ ran 𝐼) | 
| 106 | 10, 12 | mp1i 13 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ran 𝐼 ∈ Fin) | 
| 107 |  | ax-resscn 11212 | . . . . . . . . . 10
⊢ ℝ
⊆ ℂ | 
| 108 | 107 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 109 | 75, 108 | fssd 6753 | . . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) | 
| 110 | 109 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝐹:(𝐴[,]𝐵)⟶ℂ) | 
| 111 | 71 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → 𝑠 ∈ (𝐴[,]𝐵)) | 
| 112 | 110, 111 | ffvelcdmd 7105 | . . . . . 6
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → (𝐹‘𝑠) ∈ ℂ) | 
| 113 | 112 | abscld 15475 | . . . . 5
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑠 ∈ ∪ ran
𝐼) → (abs‘(𝐹‘𝑠)) ∈ ℝ) | 
| 114 | 47, 11 | fnmpti 6711 | . . . . . . . . . 10
⊢ 𝐼 Fn (0..^𝑀) | 
| 115 |  | fvelrnb 6969 | . . . . . . . . . 10
⊢ (𝐼 Fn (0..^𝑀) → (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡)) | 
| 116 | 114, 115 | ax-mp 5 | . . . . . . . . 9
⊢ (𝑡 ∈ ran 𝐼 ↔ ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) | 
| 117 | 116 | biimpi 216 | . . . . . . . 8
⊢ (𝑡 ∈ ran 𝐼 → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) | 
| 118 | 117 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡) | 
| 119 | 4 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) | 
| 120 |  | elfzofz 13715 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) | 
| 121 | 120 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) | 
| 122 | 119, 121 | ffvelcdmd 7105 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) | 
| 123 |  | fzofzp1 13803 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) | 
| 124 | 123 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) | 
| 125 | 119, 124 | ffvelcdmd 7105 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) | 
| 126 |  | fourierdlem70.fcn | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) | 
| 127 |  | fourierdlem70.l | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) | 
| 128 |  | fourierdlem70.r | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) | 
| 129 | 122, 125,
126, 127, 128 | cncfioobd 45912 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏) | 
| 130 |  | fvres 6925 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠) = (𝐹‘𝑠)) | 
| 131 | 130 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) = (abs‘(𝐹‘𝑠))) | 
| 132 | 131 | breq1d 5153 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑠)) ≤ 𝑏)) | 
| 133 | 132 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ (abs‘(𝐹‘𝑠)) ≤ 𝑏)) | 
| 134 | 133 | ralbidva 3176 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏)) | 
| 135 | 134 | rexbidv 3179 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏)) | 
| 136 | 129, 135 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏) | 
| 137 | 136 | 3adant3 1133 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏) | 
| 138 | 47, 50 | mpan2 691 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (0..^𝑀) → (𝐼‘𝑖) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) | 
| 139 | 138 | eqcomd 2743 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^𝑀) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) | 
| 140 | 139 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (𝐼‘𝑖)) | 
| 141 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (𝐼‘𝑖) = 𝑡) | 
| 142 | 140, 141 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = 𝑡) | 
| 143 | 142 | raleqdv 3326 | . . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) | 
| 144 | 143 | rexbidv 3179 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) | 
| 145 | 144 | 3adant1 1131 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → (∃𝑏 ∈ ℝ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘(𝐹‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) | 
| 146 | 137, 145 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ (𝐼‘𝑖) = 𝑡) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏) | 
| 147 | 146 | 3exp 1120 | . . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏))) | 
| 148 | 147 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (𝑖 ∈ (0..^𝑀) → ((𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏))) | 
| 149 | 148 | rexlimdv 3153 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → (∃𝑖 ∈ (0..^𝑀)(𝐼‘𝑖) = 𝑡 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏)) | 
| 150 | 118, 149 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏) | 
| 151 | 150 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝑤 = ∪ ran 𝐼) ∧ 𝑡 ∈ ran 𝐼) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ 𝑡 (abs‘(𝐹‘𝑠)) ≤ 𝑏) | 
| 152 |  | eqimss 4042 | . . . . . 6
⊢ (𝑤 = ∪
ran 𝐼 → 𝑤 ⊆ ∪ ran 𝐼) | 
| 153 | 152 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → 𝑤 ⊆ ∪ ran
𝐼) | 
| 154 | 106, 113,
151, 153 | ssfiunibd 45321 | . . . 4
⊢ ((𝜑 ∧ 𝑤 = ∪ ran 𝐼) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) | 
| 155 | 101, 105,
154 | syl2anc 584 | . . 3
⊢ (((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) ∧ ¬ 𝑤 = ran 𝑄) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) | 
| 156 | 100, 155 | pm2.61dan 813 | . 2
⊢ ((𝜑 ∧ 𝑤 ∈ {ran 𝑄, ∪ ran 𝐼}) → ∃𝑧 ∈ ℝ ∀𝑠 ∈ 𝑤 (abs‘(𝐹‘𝑠)) ≤ 𝑧) | 
| 157 | 21 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑀 ∈ ℕ) | 
| 158 | 4 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑄:(0...𝑀)⟶ℝ) | 
| 159 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (𝐴[,]𝐵)) | 
| 160 | 25 | eqcomd 2743 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 = (𝑄‘0)) | 
| 161 | 26 | eqcomd 2743 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 = (𝑄‘𝑀)) | 
| 162 | 160, 161 | oveq12d 7449 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀))) | 
| 163 | 162 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀))) | 
| 164 | 159, 163 | eleqtrd 2843 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) | 
| 165 | 164 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) | 
| 166 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ¬ 𝑡 ∈ ran 𝑄) | 
| 167 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → (𝑄‘𝑘) = (𝑄‘𝑗)) | 
| 168 | 167 | breq1d 5153 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → ((𝑄‘𝑘) < 𝑡 ↔ (𝑄‘𝑗) < 𝑡)) | 
| 169 | 168 | cbvrabv 3447 | . . . . . . . . . . . . 13
⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝑡} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑡} | 
| 170 | 169 | supeq1i 9487 | . . . . . . . . . . . 12
⊢
sup({𝑘 ∈
(0..^𝑀) ∣ (𝑄‘𝑘) < 𝑡}, ℝ, < ) = sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) < 𝑡}, ℝ, < ) | 
| 171 | 157, 158,
165, 166, 170 | fourierdlem25 46147 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) | 
| 172 | 138 | eleq2d 2827 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^𝑀) → (𝑡 ∈ (𝐼‘𝑖) ↔ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) | 
| 173 | 172 | rexbiia 3092 | . . . . . . . . . . 11
⊢
(∃𝑖 ∈
(0..^𝑀)𝑡 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ (0..^𝑀)𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) | 
| 174 | 171, 173 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ∃𝑖 ∈ (0..^𝑀)𝑡 ∈ (𝐼‘𝑖)) | 
| 175 | 48 | eqcomi 2746 | . . . . . . . . . . 11
⊢
(0..^𝑀) = dom 𝐼 | 
| 176 | 175 | rexeqi 3325 | . . . . . . . . . 10
⊢
(∃𝑖 ∈
(0..^𝑀)𝑡 ∈ (𝐼‘𝑖) ↔ ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖)) | 
| 177 | 174, 176 | sylib 218 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖)) | 
| 178 |  | elunirn 7271 | . . . . . . . . . 10
⊢ (Fun
𝐼 → (𝑡 ∈ ∪ ran 𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖))) | 
| 179 | 42, 178 | mp1i 13 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → (𝑡 ∈ ∪ ran
𝐼 ↔ ∃𝑖 ∈ dom 𝐼 𝑡 ∈ (𝐼‘𝑖))) | 
| 180 | 177, 179 | mpbird 257 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑡 ∈ ran 𝑄) → 𝑡 ∈ ∪ ran
𝐼) | 
| 181 | 180 | ex 412 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (¬ 𝑡 ∈ ran 𝑄 → 𝑡 ∈ ∪ ran
𝐼)) | 
| 182 | 181 | orrd 864 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ ran 𝑄 ∨ 𝑡 ∈ ∪ ran
𝐼)) | 
| 183 |  | elun 4153 | . . . . . 6
⊢ (𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼) ↔ (𝑡 ∈ ran 𝑄 ∨ 𝑡 ∈ ∪ ran
𝐼)) | 
| 184 | 182, 183 | sylibr 234 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) | 
| 185 | 184 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑡 ∈ (𝐴[,]𝐵)𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) | 
| 186 |  | dfss3 3972 | . . . 4
⊢ ((𝐴[,]𝐵) ⊆ (ran 𝑄 ∪ ∪ ran
𝐼) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)𝑡 ∈ (ran 𝑄 ∪ ∪ ran
𝐼)) | 
| 187 | 185, 186 | sylibr 234 | . . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (ran 𝑄 ∪ ∪ ran
𝐼)) | 
| 188 | 187, 17 | sseqtrrd 4021 | . 2
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ {ran
𝑄, ∪ ran 𝐼}) | 
| 189 | 2, 79, 156, 188 | ssfiunibd 45321 | 1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑠 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑠)) ≤ 𝑥) |