Proof of Theorem mbfi1fseqlem5
| Step | Hyp | Ref
| Expression |
| 1 | | mbfi1fseq.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
| 2 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞)) |
| 3 | 2 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
| 4 | | elrege0 13494 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 5 | 3, 4 | sylib 218 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
| 6 | 5 | simpld 494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
| 7 | | 2nn 12339 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
| 8 | | nnnn0 12533 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
| 9 | | nnexpcl 14115 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝐴
∈ ℕ0) → (2↑𝐴) ∈ ℕ) |
| 10 | 7, 8, 9 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ →
(2↑𝐴) ∈
ℕ) |
| 11 | 10 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈
ℕ) |
| 12 | 11 | nnred 12281 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈
ℝ) |
| 13 | 6, 12 | remulcld 11291 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ) |
| 14 | 11 | nnnn0d 12587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈
ℕ0) |
| 15 | 14 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (2↑𝐴)) |
| 16 | | mulge0 11781 |
. . . . . . . . . . 11
⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 ≤ (2↑𝐴))) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) |
| 17 | 5, 12, 15, 16 | syl12anc 837 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) |
| 18 | | flge0nn0 13860 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈
ℕ0) |
| 19 | 13, 17, 18 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈
ℕ0) |
| 20 | 19 | nn0red 12588 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ) |
| 21 | 19 | nn0ge0d 12590 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤
(⌊‘((𝐹‘𝑥) · (2↑𝐴)))) |
| 22 | 11 | nngt0d 12315 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝐴)) |
| 23 | | divge0 12137 |
. . . . . . . 8
⊢
((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ ∧ 0 ≤
(⌊‘((𝐹‘𝑥) · (2↑𝐴)))) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 < (2↑𝐴))) → 0 ≤
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴))) |
| 24 | 20, 21, 12, 22, 23 | syl22anc 839 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴))) |
| 25 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
| 26 | 25 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥)) |
| 27 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑚 = 𝐴) |
| 28 | 27 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝐴)) |
| 29 | 26, 28 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝐴))) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝐴)))) |
| 31 | 30, 28 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴))) |
| 32 | | mbfi1fseq.3 |
. . . . . . . . 9
⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦
((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) |
| 33 | | ovex 7464 |
. . . . . . . . 9
⊢
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ V |
| 34 | 31, 32, 33 | ovmpoa 7588 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴))) |
| 35 | 34 | adantll 714 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴))) |
| 36 | 24, 35 | breqtrrd 5171 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴𝐽𝑥)) |
| 37 | 8 | nn0ge0d 12590 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → 0 ≤
𝐴) |
| 38 | 37 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝐴) |
| 39 | | breq2 5147 |
. . . . . . 7
⊢ ((𝐴𝐽𝑥) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) → (0 ≤ (𝐴𝐽𝑥) ↔ 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))) |
| 40 | | breq2 5147 |
. . . . . . 7
⊢ (𝐴 = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) → (0 ≤ 𝐴 ↔ 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))) |
| 41 | 39, 40 | ifboth 4565 |
. . . . . 6
⊢ ((0 ≤
(𝐴𝐽𝑥) ∧ 0 ≤ 𝐴) → 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)) |
| 42 | 36, 38, 41 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)) |
| 43 | | 0le0 12367 |
. . . . 5
⊢ 0 ≤
0 |
| 44 | | breq2 5147 |
. . . . . 6
⊢
(if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) → (0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ↔ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))) |
| 45 | | breq2 5147 |
. . . . . 6
⊢ (0 =
if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) → (0 ≤ 0 ↔ 0 ≤
if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))) |
| 46 | 44, 45 | ifboth 4565 |
. . . . 5
⊢ ((0 ≤
if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) |
| 47 | 42, 43, 46 | sylancl 586 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) |
| 48 | 47 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) |
| 49 | | 0re 11263 |
. . . . . . 7
⊢ 0 ∈
ℝ |
| 50 | | fnconstg 6796 |
. . . . . . 7
⊢ (0 ∈
ℝ → (ℂ × {0}) Fn ℂ) |
| 51 | 49, 50 | ax-mp 5 |
. . . . . 6
⊢ (ℂ
× {0}) Fn ℂ |
| 52 | | df-0p 25705 |
. . . . . . 7
⊢
0𝑝 = (ℂ × {0}) |
| 53 | 52 | fneq1i 6665 |
. . . . . 6
⊢
(0𝑝 Fn ℂ ↔ (ℂ × {0}) Fn
ℂ) |
| 54 | 51, 53 | mpbir 231 |
. . . . 5
⊢
0𝑝 Fn ℂ |
| 55 | 54 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) →
0𝑝 Fn ℂ) |
| 56 | | mbfi1fseq.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ MblFn) |
| 57 | | mbfi1fseq.4 |
. . . . . . 7
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) |
| 58 | 56, 1, 32, 57 | mbfi1fseqlem4 25753 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℕ⟶dom
∫1) |
| 59 | 58 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) ∈ dom
∫1) |
| 60 | | i1ff 25711 |
. . . . 5
⊢ ((𝐺‘𝐴) ∈ dom ∫1 → (𝐺‘𝐴):ℝ⟶ℝ) |
| 61 | | ffn 6736 |
. . . . 5
⊢ ((𝐺‘𝐴):ℝ⟶ℝ → (𝐺‘𝐴) Fn ℝ) |
| 62 | 59, 60, 61 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) Fn ℝ) |
| 63 | | cnex 11236 |
. . . . 5
⊢ ℂ
∈ V |
| 64 | 63 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℂ ∈
V) |
| 65 | | reex 11246 |
. . . . 5
⊢ ℝ
∈ V |
| 66 | 65 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℝ ∈
V) |
| 67 | | ax-resscn 11212 |
. . . . 5
⊢ ℝ
⊆ ℂ |
| 68 | | sseqin2 4223 |
. . . . 5
⊢ (ℝ
⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ) |
| 69 | 67, 68 | mpbi 230 |
. . . 4
⊢ (ℂ
∩ ℝ) = ℝ |
| 70 | | 0pval 25706 |
. . . . 5
⊢ (𝑥 ∈ ℂ →
(0𝑝‘𝑥) = 0) |
| 71 | 70 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℂ) →
(0𝑝‘𝑥) = 0) |
| 72 | 56, 1, 32, 57 | mbfi1fseqlem2 25751 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))) |
| 73 | 72 | fveq1d 6908 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥)) |
| 74 | 73 | ad2antlr 727 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥)) |
| 75 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
| 76 | | rge0ssre 13496 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℝ |
| 77 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℝ) |
| 78 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:ℝ⟶(0[,)+∞)
∧ 𝑦 ∈ ℝ)
→ (𝐹‘𝑦) ∈
(0[,)+∞)) |
| 79 | 1, 77, 78 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞)) |
| 80 | 76, 79 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ) |
| 81 | | nnnn0 12533 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ0) |
| 82 | | nnexpcl 14115 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℕ ∧ 𝑚
∈ ℕ0) → (2↑𝑚) ∈ ℕ) |
| 83 | 7, 81, 82 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ →
(2↑𝑚) ∈
ℕ) |
| 84 | 83 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈
ℕ) |
| 85 | 84 | nnred 12281 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈
ℝ) |
| 86 | 80, 85 | remulcld 11291 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ) |
| 87 | | reflcl 13836 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ →
(⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ) |
| 88 | 86, 87 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) →
(⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ) |
| 89 | 88, 84 | nndivred 12320 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) →
((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ) |
| 90 | 89 | ralrimivva 3202 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ) |
| 91 | 32 | fmpo 8093 |
. . . . . . . . . . 11
⊢
(∀𝑚 ∈
ℕ ∀𝑦 ∈
ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ ×
ℝ)⟶ℝ) |
| 92 | 90, 91 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽:(ℕ ×
ℝ)⟶ℝ) |
| 93 | | fovcdm 7603 |
. . . . . . . . . 10
⊢ ((𝐽:(ℕ ×
ℝ)⟶ℝ ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ) |
| 94 | 92, 93 | syl3an1 1164 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ) |
| 95 | 94 | 3expa 1119 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ) |
| 96 | | nnre 12273 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
| 97 | 96 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ) |
| 98 | 95, 97 | ifcld 4572 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ℝ) |
| 99 | | ifcl 4571 |
. . . . . . 7
⊢
((if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ) |
| 100 | 98, 49, 99 | sylancl 586 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ) |
| 101 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) |
| 102 | 101 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) |
| 103 | 75, 100, 102 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) |
| 104 | 74, 103 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝐴)‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) |
| 105 | 55, 62, 64, 66, 69, 71, 104 | ofrfval 7707 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) →
(0𝑝 ∘r ≤ (𝐺‘𝐴) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))) |
| 106 | 48, 105 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) →
0𝑝 ∘r ≤ (𝐺‘𝐴)) |
| 107 | 56, 1, 32 | mbfi1fseqlem1 25750 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽:(ℕ ×
ℝ)⟶(0[,)+∞)) |
| 108 | 107 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐽:(ℕ ×
ℝ)⟶(0[,)+∞)) |
| 109 | | peano2nn 12278 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈
ℕ) |
| 110 | 109 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℕ) |
| 111 | 108, 110,
75 | fovcdmd 7605 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞)) |
| 112 | | elrege0 13494 |
. . . . . . . . . . 11
⊢ (((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞) ↔ (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥))) |
| 113 | 111, 112 | sylib 218 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥))) |
| 114 | 113 | simpld 494 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ ℝ) |
| 115 | | min1 13231 |
. . . . . . . . . 10
⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥)) |
| 116 | 95, 97, 115 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥)) |
| 117 | | 2cn 12341 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
| 118 | 8 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈
ℕ0) |
| 119 | | expp1 14109 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℕ0) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2)) |
| 120 | 117, 118,
119 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2)) |
| 121 | 120 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2))) |
| 122 | 35, 95 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℝ) |
| 123 | 122 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℂ) |
| 124 | 12 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈
ℂ) |
| 125 | | 2cnd 12344 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 2 ∈
ℂ) |
| 126 | 123, 124,
125 | mulassd 11284 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2))) |
| 127 | 20 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℂ) |
| 128 | 11 | nnne0d 12316 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ≠ 0) |
| 129 | 127, 124,
128 | divcan1d 12044 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) = (⌊‘((𝐹‘𝑥) · (2↑𝐴)))) |
| 130 | 129 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2)) |
| 131 | 121, 126,
130 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2)) |
| 132 | | flle 13839 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ →
(⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴))) |
| 133 | 13, 132 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴))) |
| 134 | | 2re 12340 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
| 135 | | 2pos 12369 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
2 |
| 136 | 134, 135 | pm3.2i 470 |
. . . . . . . . . . . . . . . . 17
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 137 | 136 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2 ∈ ℝ
∧ 0 < 2)) |
| 138 | | lemul1 12119 |
. . . . . . . . . . . . . . . 16
⊢
(((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ ∧ ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2))) |
| 139 | 20, 13, 137, 138 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2))) |
| 140 | 133, 139 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2)) |
| 141 | 120 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = ((𝐹‘𝑥) · ((2↑𝐴) · 2))) |
| 142 | 6 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ) |
| 143 | 142, 124,
125 | mulassd 11284 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (2↑𝐴)) · 2) = ((𝐹‘𝑥) · ((2↑𝐴) · 2))) |
| 144 | 141, 143 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = (((𝐹‘𝑥) · (2↑𝐴)) · 2)) |
| 145 | 140, 144 | breqtrrd 5171 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1)))) |
| 146 | 110 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈
ℕ0) |
| 147 | | nnexpcl 14115 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℕ ∧ (𝐴 +
1) ∈ ℕ0) → (2↑(𝐴 + 1)) ∈ ℕ) |
| 148 | 7, 146, 147 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈
ℕ) |
| 149 | 148 | nnred 12281 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈
ℝ) |
| 150 | 6, 149 | remulcld 11291 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ) |
| 151 | 13 | flcld 13838 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ) |
| 152 | | 2z 12649 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
| 153 | | zmulcl 12666 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ ∧ 2 ∈ ℤ)
→ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈
ℤ) |
| 154 | 151, 152,
153 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈
ℤ) |
| 155 | | flge 13845 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ ∧
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ) →
(((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))) |
| 156 | 150, 154,
155 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))) |
| 157 | 145, 156 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1))))) |
| 158 | 131, 157 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1))))) |
| 159 | | reflcl 13836 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ →
(⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ) |
| 160 | 150, 159 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ) |
| 161 | 148 | nngt0d 12315 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑(𝐴 + 1))) |
| 162 | | lemuldiv 12148 |
. . . . . . . . . . . 12
⊢
((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℝ ∧
(⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ ∧
((2↑(𝐴 + 1)) ∈
ℝ ∧ 0 < (2↑(𝐴 + 1)))) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))) |
| 163 | 122, 160,
149, 161, 162 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))) |
| 164 | 158, 163 | mpbid 232 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))) |
| 165 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
| 166 | 165 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥)) |
| 167 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → 𝑚 = (𝐴 + 1)) |
| 168 | 167 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑(𝐴 + 1))) |
| 169 | 166, 168 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑(𝐴 + 1)))) |
| 170 | 169 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1))))) |
| 171 | 170, 168 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))) |
| 172 | | ovex 7464 |
. . . . . . . . . . . 12
⊢
((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))) ∈ V |
| 173 | 171, 32, 172 | ovmpoa 7588 |
. . . . . . . . . . 11
⊢ (((𝐴 + 1) ∈ ℕ ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))) |
| 174 | 110, 75, 173 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))) |
| 175 | 164, 35, 174 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ≤ ((𝐴 + 1)𝐽𝑥)) |
| 176 | 98, 95, 114, 116, 175 | letrd 11418 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥)) |
| 177 | 110 | nnred 12281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℝ) |
| 178 | | min2 13232 |
. . . . . . . . . 10
⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴) |
| 179 | 95, 97, 178 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴) |
| 180 | 97 | lep1d 12199 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ≤ (𝐴 + 1)) |
| 181 | 98, 97, 177, 179, 180 | letrd 11418 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1)) |
| 182 | | breq2 5147 |
. . . . . . . . 9
⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥) ↔ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))) |
| 183 | | breq2 5147 |
. . . . . . . . 9
⊢ ((𝐴 + 1) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1) ↔ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))) |
| 184 | 182, 183 | ifboth 4565 |
. . . . . . . 8
⊢
((if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥) ∧ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1)) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))) |
| 185 | 176, 181,
184 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))) |
| 186 | 185 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))) |
| 187 | | iftrue 4531 |
. . . . . . 7
⊢ (𝑥 ∈ (-𝐴[,]𝐴) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)) |
| 188 | 187 | adantl 481 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)) |
| 189 | 177 | renegcld 11690 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ∈ ℝ) |
| 190 | 97, 177 | lenegd 11842 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 ≤ (𝐴 + 1) ↔ -(𝐴 + 1) ≤ -𝐴)) |
| 191 | 180, 190 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ≤ -𝐴) |
| 192 | | iccss 13455 |
. . . . . . . . 9
⊢
(((-(𝐴 + 1) ∈
ℝ ∧ (𝐴 + 1)
∈ ℝ) ∧ (-(𝐴
+ 1) ≤ -𝐴 ∧ 𝐴 ≤ (𝐴 + 1))) → (-𝐴[,]𝐴) ⊆ (-(𝐴 + 1)[,](𝐴 + 1))) |
| 193 | 189, 177,
191, 180, 192 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (-𝐴[,]𝐴) ⊆ (-(𝐴 + 1)[,](𝐴 + 1))) |
| 194 | 193 | sselda 3983 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → 𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1))) |
| 195 | 194 | iftrued 4533 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))) |
| 196 | 186, 188,
195 | 3brtr4d 5175 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 197 | | iffalse 4534 |
. . . . . . 7
⊢ (¬
𝑥 ∈ (-𝐴[,]𝐴) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = 0) |
| 198 | 197 | adantl 481 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = 0) |
| 199 | 113 | simprd 495 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐴 + 1)𝐽𝑥)) |
| 200 | 146 | nn0ge0d 12590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴 + 1)) |
| 201 | | breq2 5147 |
. . . . . . . . . 10
⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (0 ≤ ((𝐴 + 1)𝐽𝑥) ↔ 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))) |
| 202 | | breq2 5147 |
. . . . . . . . . 10
⊢ ((𝐴 + 1) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (0 ≤ (𝐴 + 1) ↔ 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))) |
| 203 | 201, 202 | ifboth 4565 |
. . . . . . . . 9
⊢ ((0 ≤
((𝐴 + 1)𝐽𝑥) ∧ 0 ≤ (𝐴 + 1)) → 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))) |
| 204 | 199, 200,
203 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))) |
| 205 | | breq2 5147 |
. . . . . . . . 9
⊢
(if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) → (0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ↔ 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))) |
| 206 | | breq2 5147 |
. . . . . . . . 9
⊢ (0 =
if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) → (0 ≤ 0 ↔ 0 ≤
if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))) |
| 207 | 205, 206 | ifboth 4565 |
. . . . . . . 8
⊢ ((0 ≤
if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∧ 0 ≤ 0) → 0 ≤
if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 208 | 204, 43, 207 | sylancl 586 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 209 | 208 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 210 | 198, 209 | eqbrtrd 5165 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 211 | 196, 210 | pm2.61dan 813 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 212 | 211 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 213 | | ffvelcdm 7101 |
. . . . . 6
⊢ ((𝐺:ℕ⟶dom
∫1 ∧ (𝐴
+ 1) ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom
∫1) |
| 214 | 58, 109, 213 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom
∫1) |
| 215 | | i1ff 25711 |
. . . . 5
⊢ ((𝐺‘(𝐴 + 1)) ∈ dom ∫1 →
(𝐺‘(𝐴 +
1)):ℝ⟶ℝ) |
| 216 | | ffn 6736 |
. . . . 5
⊢ ((𝐺‘(𝐴 + 1)):ℝ⟶ℝ → (𝐺‘(𝐴 + 1)) Fn ℝ) |
| 217 | 214, 215,
216 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) Fn ℝ) |
| 218 | | inidm 4227 |
. . . 4
⊢ (ℝ
∩ ℝ) = ℝ |
| 219 | 56, 1, 32, 57 | mbfi1fseqlem2 25751 |
. . . . . . 7
⊢ ((𝐴 + 1) ∈ ℕ →
(𝐺‘(𝐴 + 1)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))) |
| 220 | 219 | fveq1d 6908 |
. . . . . 6
⊢ ((𝐴 + 1) ∈ ℕ →
((𝐺‘(𝐴 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥)) |
| 221 | 110, 220 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘(𝐴 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥)) |
| 222 | 114, 177 | ifcld 4572 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∈ ℝ) |
| 223 | | ifcl 4571 |
. . . . . . 7
⊢
((if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∈ ℝ ∧ 0 ∈
ℝ) → if(𝑥 ∈
(-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ) |
| 224 | 222, 49, 223 | sylancl 586 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ) |
| 225 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 226 | 225 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 227 | 75, 224, 226 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 228 | 221, 227 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘(𝐴 + 1))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) |
| 229 | 62, 217, 66, 66, 218, 104, 228 | ofrfval 7707 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ((𝐺‘𝐴) ∘r ≤ (𝐺‘(𝐴 + 1)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))) |
| 230 | 212, 229 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) ∘r ≤ (𝐺‘(𝐴 + 1))) |
| 231 | 106, 230 | jca 511 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) →
(0𝑝 ∘r ≤ (𝐺‘𝐴) ∧ (𝐺‘𝐴) ∘r ≤ (𝐺‘(𝐴 + 1)))) |