MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfi1fseqlem5 Structured version   Visualization version   GIF version

Theorem mbfi1fseqlem5 25244
Description: Lemma for mbfi1fseq 25246. Verify that 𝐺 describes an increasing sequence of positive functions. (Contributed by Mario Carneiro, 16-Aug-2014.)
Hypotheses
Ref Expression
mbfi1fseq.1 (πœ‘ β†’ 𝐹 ∈ MblFn)
mbfi1fseq.2 (πœ‘ β†’ 𝐹:β„βŸΆ(0[,)+∞))
mbfi1fseq.3 𝐽 = (π‘š ∈ β„•, 𝑦 ∈ ℝ ↦ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)))
mbfi1fseq.4 𝐺 = (π‘š ∈ β„• ↦ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-π‘š[,]π‘š), if((π‘šπ½π‘₯) ≀ π‘š, (π‘šπ½π‘₯), π‘š), 0)))
Assertion
Ref Expression
mbfi1fseqlem5 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (0𝑝 ∘r ≀ (πΊβ€˜π΄) ∧ (πΊβ€˜π΄) ∘r ≀ (πΊβ€˜(𝐴 + 1))))
Distinct variable groups:   π‘₯,π‘š,𝑦,𝐹   π‘₯,𝐺   π‘š,𝐽   πœ‘,π‘š,π‘₯,𝑦   𝐴,π‘š,π‘₯,𝑦
Allowed substitution hints:   𝐺(𝑦,π‘š)   𝐽(π‘₯,𝑦)

Proof of Theorem mbfi1fseqlem5
StepHypRef Expression
1 mbfi1fseq.2 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:β„βŸΆ(0[,)+∞))
21adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ 𝐹:β„βŸΆ(0[,)+∞))
32ffvelcdmda 7086 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ (0[,)+∞))
4 elrege0 13433 . . . . . . . . . . . . 13 ((πΉβ€˜π‘₯) ∈ (0[,)+∞) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)))
53, 4sylib 217 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)))
65simpld 495 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
7 2nn 12287 . . . . . . . . . . . . . 14 2 ∈ β„•
8 nnnn0 12481 . . . . . . . . . . . . . 14 (𝐴 ∈ β„• β†’ 𝐴 ∈ β„•0)
9 nnexpcl 14042 . . . . . . . . . . . . . 14 ((2 ∈ β„• ∧ 𝐴 ∈ β„•0) β†’ (2↑𝐴) ∈ β„•)
107, 8, 9sylancr 587 . . . . . . . . . . . . 13 (𝐴 ∈ β„• β†’ (2↑𝐴) ∈ β„•)
1110ad2antlr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) ∈ β„•)
1211nnred 12229 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) ∈ ℝ)
136, 12remulcld 11246 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) Β· (2↑𝐴)) ∈ ℝ)
1411nnnn0d 12534 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) ∈ β„•0)
1514nn0ge0d 12537 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (2↑𝐴))
16 mulge0 11734 . . . . . . . . . . 11 ((((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 ≀ (2↑𝐴))) β†’ 0 ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
175, 12, 15, 16syl12anc 835 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
18 flge0nn0 13787 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) Β· (2↑𝐴)) ∈ ℝ ∧ 0 ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴))) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„•0)
1913, 17, 18syl2anc 584 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„•0)
2019nn0red 12535 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ ℝ)
2119nn0ge0d 12537 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))))
2211nngt0d 12263 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 < (2↑𝐴))
23 divge0 12085 . . . . . . . 8 ((((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ ℝ ∧ 0 ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴)))) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 < (2↑𝐴))) β†’ 0 ≀ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
2420, 21, 12, 22, 23syl22anc 837 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
25 simpr 485 . . . . . . . . . . . . 13 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ 𝑦 = π‘₯)
2625fveq2d 6895 . . . . . . . . . . . 12 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘₯))
27 simpl 483 . . . . . . . . . . . . 13 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ π‘š = 𝐴)
2827oveq2d 7427 . . . . . . . . . . . 12 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ (2β†‘π‘š) = (2↑𝐴))
2926, 28oveq12d 7429 . . . . . . . . . . 11 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ ((πΉβ€˜π‘¦) Β· (2β†‘π‘š)) = ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
3029fveq2d 6895 . . . . . . . . . 10 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ (βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) = (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))))
3130, 28oveq12d 7429 . . . . . . . . 9 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
32 mbfi1fseq.3 . . . . . . . . 9 𝐽 = (π‘š ∈ β„•, 𝑦 ∈ ℝ ↦ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)))
33 ovex 7444 . . . . . . . . 9 ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ∈ V
3431, 32, 33ovmpoa 7565 . . . . . . . 8 ((𝐴 ∈ β„• ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
3534adantll 712 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
3624, 35breqtrrd 5176 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (𝐴𝐽π‘₯))
378nn0ge0d 12537 . . . . . . 7 (𝐴 ∈ β„• β†’ 0 ≀ 𝐴)
3837ad2antlr 725 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ 𝐴)
39 breq2 5152 . . . . . . 7 ((𝐴𝐽π‘₯) = if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) β†’ (0 ≀ (𝐴𝐽π‘₯) ↔ 0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴)))
40 breq2 5152 . . . . . . 7 (𝐴 = if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) β†’ (0 ≀ 𝐴 ↔ 0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴)))
4139, 40ifboth 4567 . . . . . 6 ((0 ≀ (𝐴𝐽π‘₯) ∧ 0 ≀ 𝐴) β†’ 0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴))
4236, 38, 41syl2anc 584 . . . . 5 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴))
43 0le0 12315 . . . . 5 0 ≀ 0
44 breq2 5152 . . . . . 6 (if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) β†’ (0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ↔ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)))
45 breq2 5152 . . . . . 6 (0 = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) β†’ (0 ≀ 0 ↔ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)))
4644, 45ifboth 4567 . . . . 5 ((0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ∧ 0 ≀ 0) β†’ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
4742, 43, 46sylancl 586 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
4847ralrimiva 3146 . . 3 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ βˆ€π‘₯ ∈ ℝ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
49 0re 11218 . . . . . . 7 0 ∈ ℝ
50 fnconstg 6779 . . . . . . 7 (0 ∈ ℝ β†’ (β„‚ Γ— {0}) Fn β„‚)
5149, 50ax-mp 5 . . . . . 6 (β„‚ Γ— {0}) Fn β„‚
52 df-0p 25194 . . . . . . 7 0𝑝 = (β„‚ Γ— {0})
5352fneq1i 6646 . . . . . 6 (0𝑝 Fn β„‚ ↔ (β„‚ Γ— {0}) Fn β„‚)
5451, 53mpbir 230 . . . . 5 0𝑝 Fn β„‚
5554a1i 11 . . . 4 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ 0𝑝 Fn β„‚)
56 mbfi1fseq.1 . . . . . . 7 (πœ‘ β†’ 𝐹 ∈ MblFn)
57 mbfi1fseq.4 . . . . . . 7 𝐺 = (π‘š ∈ β„• ↦ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-π‘š[,]π‘š), if((π‘šπ½π‘₯) ≀ π‘š, (π‘šπ½π‘₯), π‘š), 0)))
5856, 1, 32, 57mbfi1fseqlem4 25243 . . . . . 6 (πœ‘ β†’ 𝐺:β„•βŸΆdom ∫1)
5958ffvelcdmda 7086 . . . . 5 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜π΄) ∈ dom ∫1)
60 i1ff 25200 . . . . 5 ((πΊβ€˜π΄) ∈ dom ∫1 β†’ (πΊβ€˜π΄):β„βŸΆβ„)
61 ffn 6717 . . . . 5 ((πΊβ€˜π΄):β„βŸΆβ„ β†’ (πΊβ€˜π΄) Fn ℝ)
6259, 60, 613syl 18 . . . 4 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜π΄) Fn ℝ)
63 cnex 11193 . . . . 5 β„‚ ∈ V
6463a1i 11 . . . 4 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ β„‚ ∈ V)
65 reex 11203 . . . . 5 ℝ ∈ V
6665a1i 11 . . . 4 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ ℝ ∈ V)
67 ax-resscn 11169 . . . . 5 ℝ βŠ† β„‚
68 sseqin2 4215 . . . . 5 (ℝ βŠ† β„‚ ↔ (β„‚ ∩ ℝ) = ℝ)
6967, 68mpbi 229 . . . 4 (β„‚ ∩ ℝ) = ℝ
70 0pval 25195 . . . . 5 (π‘₯ ∈ β„‚ β†’ (0π‘β€˜π‘₯) = 0)
7170adantl 482 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ β„‚) β†’ (0π‘β€˜π‘₯) = 0)
7256, 1, 32, 57mbfi1fseqlem2 25241 . . . . . . 7 (𝐴 ∈ β„• β†’ (πΊβ€˜π΄) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)))
7372fveq1d 6893 . . . . . 6 (𝐴 ∈ β„• β†’ ((πΊβ€˜π΄)β€˜π‘₯) = ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))β€˜π‘₯))
7473ad2antlr 725 . . . . 5 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΊβ€˜π΄)β€˜π‘₯) = ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))β€˜π‘₯))
75 simpr 485 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ π‘₯ ∈ ℝ)
76 rge0ssre 13435 . . . . . . . . . . . . . . . 16 (0[,)+∞) βŠ† ℝ
77 simpr 485 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ β„• ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ)
78 ffvelcdm 7083 . . . . . . . . . . . . . . . . 17 ((𝐹:β„βŸΆ(0[,)+∞) ∧ 𝑦 ∈ ℝ) β†’ (πΉβ€˜π‘¦) ∈ (0[,)+∞))
791, 77, 78syl2an 596 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (πΉβ€˜π‘¦) ∈ (0[,)+∞))
8076, 79sselid 3980 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (πΉβ€˜π‘¦) ∈ ℝ)
81 nnnn0 12481 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„• β†’ π‘š ∈ β„•0)
82 nnexpcl 14042 . . . . . . . . . . . . . . . . . 18 ((2 ∈ β„• ∧ π‘š ∈ β„•0) β†’ (2β†‘π‘š) ∈ β„•)
837, 81, 82sylancr 587 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• β†’ (2β†‘π‘š) ∈ β„•)
8483ad2antrl 726 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (2β†‘π‘š) ∈ β„•)
8584nnred 12229 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (2β†‘π‘š) ∈ ℝ)
8680, 85remulcld 11246 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ ((πΉβ€˜π‘¦) Β· (2β†‘π‘š)) ∈ ℝ)
87 reflcl 13763 . . . . . . . . . . . . . 14 (((πΉβ€˜π‘¦) Β· (2β†‘π‘š)) ∈ ℝ β†’ (βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) ∈ ℝ)
8886, 87syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) ∈ ℝ)
8988, 84nndivred 12268 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) ∈ ℝ)
9089ralrimivva 3200 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘š ∈ β„• βˆ€π‘¦ ∈ ℝ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) ∈ ℝ)
9132fmpo 8056 . . . . . . . . . . 11 (βˆ€π‘š ∈ β„• βˆ€π‘¦ ∈ ℝ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) ∈ ℝ ↔ 𝐽:(β„• Γ— ℝ)βŸΆβ„)
9290, 91sylib 217 . . . . . . . . . 10 (πœ‘ β†’ 𝐽:(β„• Γ— ℝ)βŸΆβ„)
93 fovcdm 7579 . . . . . . . . . 10 ((𝐽:(β„• Γ— ℝ)βŸΆβ„ ∧ 𝐴 ∈ β„• ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) ∈ ℝ)
9492, 93syl3an1 1163 . . . . . . . . 9 ((πœ‘ ∧ 𝐴 ∈ β„• ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) ∈ ℝ)
95943expa 1118 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) ∈ ℝ)
96 nnre 12221 . . . . . . . . 9 (𝐴 ∈ β„• β†’ 𝐴 ∈ ℝ)
9796ad2antlr 725 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 𝐴 ∈ ℝ)
9895, 97ifcld 4574 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ∈ ℝ)
99 ifcl 4573 . . . . . . 7 ((if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ∈ ℝ)
10098, 49, 99sylancl 586 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ∈ ℝ)
101 eqid 2732 . . . . . . 7 (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
102101fvmpt2 7009 . . . . . 6 ((π‘₯ ∈ ℝ ∧ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ∈ ℝ) β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))β€˜π‘₯) = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
10375, 100, 102syl2anc 584 . . . . 5 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))β€˜π‘₯) = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
10474, 103eqtrd 2772 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΊβ€˜π΄)β€˜π‘₯) = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
10555, 62, 64, 66, 69, 71, 104ofrfval 7682 . . 3 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (0𝑝 ∘r ≀ (πΊβ€˜π΄) ↔ βˆ€π‘₯ ∈ ℝ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)))
10648, 105mpbird 256 . 2 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ 0𝑝 ∘r ≀ (πΊβ€˜π΄))
10756, 1, 32mbfi1fseqlem1 25240 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐽:(β„• Γ— ℝ)⟢(0[,)+∞))
108107ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 𝐽:(β„• Γ— ℝ)⟢(0[,)+∞))
109 peano2nn 12226 . . . . . . . . . . . . 13 (𝐴 ∈ β„• β†’ (𝐴 + 1) ∈ β„•)
110109ad2antlr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴 + 1) ∈ β„•)
111108, 110, 75fovcdmd 7581 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((𝐴 + 1)𝐽π‘₯) ∈ (0[,)+∞))
112 elrege0 13433 . . . . . . . . . . 11 (((𝐴 + 1)𝐽π‘₯) ∈ (0[,)+∞) ↔ (((𝐴 + 1)𝐽π‘₯) ∈ ℝ ∧ 0 ≀ ((𝐴 + 1)𝐽π‘₯)))
113111, 112sylib 217 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((𝐴 + 1)𝐽π‘₯) ∈ ℝ ∧ 0 ≀ ((𝐴 + 1)𝐽π‘₯)))
114113simpld 495 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((𝐴 + 1)𝐽π‘₯) ∈ ℝ)
115 min1 13170 . . . . . . . . . 10 (((𝐴𝐽π‘₯) ∈ ℝ ∧ 𝐴 ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴𝐽π‘₯))
11695, 97, 115syl2anc 584 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴𝐽π‘₯))
117 2cn 12289 . . . . . . . . . . . . . . 15 2 ∈ β„‚
1188ad2antlr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 𝐴 ∈ β„•0)
119 expp1 14036 . . . . . . . . . . . . . . 15 ((2 ∈ β„‚ ∧ 𝐴 ∈ β„•0) β†’ (2↑(𝐴 + 1)) = ((2↑𝐴) Β· 2))
120117, 118, 119sylancr 587 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑(𝐴 + 1)) = ((2↑𝐴) Β· 2))
121120oveq2d 7427 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑(𝐴 + 1))) = (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· ((2↑𝐴) Β· 2)))
12235, 95eqeltrrd 2834 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ∈ ℝ)
123122recnd 11244 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ∈ β„‚)
12412recnd 11244 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) ∈ β„‚)
125 2cnd 12292 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 2 ∈ β„‚)
126123, 124, 125mulassd 11239 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑𝐴)) Β· 2) = (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· ((2↑𝐴) Β· 2)))
12720recnd 11244 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„‚)
12811nnne0d 12264 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) β‰  0)
129127, 124, 128divcan1d 11993 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑𝐴)) = (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))))
130129oveq1d 7426 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑𝐴)) Β· 2) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2))
131121, 126, 1303eqtr2d 2778 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑(𝐴 + 1))) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2))
132 flle 13766 . . . . . . . . . . . . . . . 16 (((πΉβ€˜π‘₯) Β· (2↑𝐴)) ∈ ℝ β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
13313, 132syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
134 2re 12288 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
135 2pos 12317 . . . . . . . . . . . . . . . . . 18 0 < 2
136134, 135pm3.2i 471 . . . . . . . . . . . . . . . . 17 (2 ∈ ℝ ∧ 0 < 2)
137136a1i 11 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2 ∈ ℝ ∧ 0 < 2))
138 lemul1 12068 . . . . . . . . . . . . . . . 16 (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ ℝ ∧ ((πΉβ€˜π‘₯) Β· (2↑𝐴)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2)))
13920, 13, 137, 138syl3anc 1371 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2)))
140133, 139mpbid 231 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2))
141120oveq2d 7427 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) = ((πΉβ€˜π‘₯) Β· ((2↑𝐴) Β· 2)))
1426recnd 11244 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
143142, 124, 125mulassd 11239 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2) = ((πΉβ€˜π‘₯) Β· ((2↑𝐴) Β· 2)))
144141, 143eqtr4d 2775 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) = (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2))
145140, 144breqtrrd 5176 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))))
146110nnnn0d 12534 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴 + 1) ∈ β„•0)
147 nnexpcl 14042 . . . . . . . . . . . . . . . . 17 ((2 ∈ β„• ∧ (𝐴 + 1) ∈ β„•0) β†’ (2↑(𝐴 + 1)) ∈ β„•)
1487, 146, 147sylancr 587 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑(𝐴 + 1)) ∈ β„•)
149148nnred 12229 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑(𝐴 + 1)) ∈ ℝ)
1506, 149remulcld 11246 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ∈ ℝ)
15113flcld 13765 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„€)
152 2z 12596 . . . . . . . . . . . . . . 15 2 ∈ β„€
153 zmulcl 12613 . . . . . . . . . . . . . . 15 (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„€ ∧ 2 ∈ β„€) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ∈ β„€)
154151, 152, 153sylancl 586 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ∈ β„€)
155 flge 13772 . . . . . . . . . . . . . 14 ((((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ∈ ℝ ∧ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ∈ β„€) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))))))
156150, 154, 155syl2anc 584 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))))))
157145, 156mpbid 231 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))))
158131, 157eqbrtrd 5170 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑(𝐴 + 1))) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))))
159 reflcl 13763 . . . . . . . . . . . . 13 (((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ∈ ℝ β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) ∈ ℝ)
160150, 159syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) ∈ ℝ)
161148nngt0d 12263 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 < (2↑(𝐴 + 1)))
162 lemuldiv 12096 . . . . . . . . . . . 12 ((((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ∈ ℝ ∧ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) ∈ ℝ ∧ ((2↑(𝐴 + 1)) ∈ ℝ ∧ 0 < (2↑(𝐴 + 1)))) β†’ ((((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑(𝐴 + 1))) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ≀ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))))
163122, 160, 149, 161, 162syl112anc 1374 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑(𝐴 + 1))) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ≀ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))))
164158, 163mpbid 231 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ≀ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
165 simpr 485 . . . . . . . . . . . . . . . 16 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ 𝑦 = π‘₯)
166165fveq2d 6895 . . . . . . . . . . . . . . 15 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘₯))
167 simpl 483 . . . . . . . . . . . . . . . 16 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ π‘š = (𝐴 + 1))
168167oveq2d 7427 . . . . . . . . . . . . . . 15 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ (2β†‘π‘š) = (2↑(𝐴 + 1)))
169166, 168oveq12d 7429 . . . . . . . . . . . . . 14 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ ((πΉβ€˜π‘¦) Β· (2β†‘π‘š)) = ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))))
170169fveq2d 6895 . . . . . . . . . . . . 13 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ (βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) = (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))))
171170, 168oveq12d 7429 . . . . . . . . . . . 12 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
172 ovex 7444 . . . . . . . . . . . 12 ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))) ∈ V
173171, 32, 172ovmpoa 7565 . . . . . . . . . . 11 (((𝐴 + 1) ∈ β„• ∧ π‘₯ ∈ ℝ) β†’ ((𝐴 + 1)𝐽π‘₯) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
174110, 75, 173syl2anc 584 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((𝐴 + 1)𝐽π‘₯) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
175164, 35, 1743brtr4d 5180 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) ≀ ((𝐴 + 1)𝐽π‘₯))
17698, 95, 114, 116, 175letrd 11373 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ ((𝐴 + 1)𝐽π‘₯))
177110nnred 12229 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴 + 1) ∈ ℝ)
178 min2 13171 . . . . . . . . . 10 (((𝐴𝐽π‘₯) ∈ ℝ ∧ 𝐴 ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ 𝐴)
17995, 97, 178syl2anc 584 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ 𝐴)
18097lep1d 12147 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 𝐴 ≀ (𝐴 + 1))
18198, 97, 177, 179, 180letrd 11373 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴 + 1))
182 breq2 5152 . . . . . . . . 9 (((𝐴 + 1)𝐽π‘₯) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) β†’ (if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ ((𝐴 + 1)𝐽π‘₯) ↔ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1))))
183 breq2 5152 . . . . . . . . 9 ((𝐴 + 1) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) β†’ (if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴 + 1) ↔ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1))))
184182, 183ifboth 4567 . . . . . . . 8 ((if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ ((𝐴 + 1)𝐽π‘₯) ∧ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴 + 1)) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
185176, 181, 184syl2anc 584 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
186185adantr 481 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
187 iftrue 4534 . . . . . . 7 (π‘₯ ∈ (-𝐴[,]𝐴) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) = if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴))
188187adantl 482 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) = if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴))
189177renegcld 11643 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ -(𝐴 + 1) ∈ ℝ)
19097, 177lenegd 11795 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴 ≀ (𝐴 + 1) ↔ -(𝐴 + 1) ≀ -𝐴))
191180, 190mpbid 231 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ -(𝐴 + 1) ≀ -𝐴)
192 iccss 13394 . . . . . . . . 9 (((-(𝐴 + 1) ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ) ∧ (-(𝐴 + 1) ≀ -𝐴 ∧ 𝐴 ≀ (𝐴 + 1))) β†’ (-𝐴[,]𝐴) βŠ† (-(𝐴 + 1)[,](𝐴 + 1)))
193189, 177, 191, 180, 192syl22anc 837 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (-𝐴[,]𝐴) βŠ† (-(𝐴 + 1)[,](𝐴 + 1)))
194193sselda 3982 . . . . . . 7 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)))
195194iftrued 4536 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
196186, 188, 1953brtr4d 5180 . . . . 5 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
197 iffalse 4537 . . . . . . 7 (Β¬ π‘₯ ∈ (-𝐴[,]𝐴) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) = 0)
198197adantl 482 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) = 0)
199113simprd 496 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ ((𝐴 + 1)𝐽π‘₯))
200146nn0ge0d 12537 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (𝐴 + 1))
201 breq2 5152 . . . . . . . . . 10 (((𝐴 + 1)𝐽π‘₯) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) β†’ (0 ≀ ((𝐴 + 1)𝐽π‘₯) ↔ 0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1))))
202 breq2 5152 . . . . . . . . . 10 ((𝐴 + 1) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) β†’ (0 ≀ (𝐴 + 1) ↔ 0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1))))
203201, 202ifboth 4567 . . . . . . . . 9 ((0 ≀ ((𝐴 + 1)𝐽π‘₯) ∧ 0 ≀ (𝐴 + 1)) β†’ 0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
204199, 200, 203syl2anc 584 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
205 breq2 5152 . . . . . . . . 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 5152 . . . . . . . . 9 (0 = if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0) β†’ (0 ≀ 0 ↔ 0 ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0)))
207205, 206ifboth 4567 . . . . . . . 8 ((0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) ∧ 0 ≀ 0) β†’ 0 ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
208204, 43, 207sylancl 586 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
209208adantr 481 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ 0 ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
210198, 209eqbrtrd 5170 . . . . 5 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
211196, 210pm2.61dan 811 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
212211ralrimiva 3146 . . 3 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
213 ffvelcdm 7083 . . . . . 6 ((𝐺:β„•βŸΆdom ∫1 ∧ (𝐴 + 1) ∈ β„•) β†’ (πΊβ€˜(𝐴 + 1)) ∈ dom ∫1)
21458, 109, 213syl2an 596 . . . . 5 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜(𝐴 + 1)) ∈ dom ∫1)
215 i1ff 25200 . . . . 5 ((πΊβ€˜(𝐴 + 1)) ∈ dom ∫1 β†’ (πΊβ€˜(𝐴 + 1)):β„βŸΆβ„)
216 ffn 6717 . . . . 5 ((πΊβ€˜(𝐴 + 1)):β„βŸΆβ„ β†’ (πΊβ€˜(𝐴 + 1)) Fn ℝ)
217214, 215, 2163syl 18 . . . 4 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜(𝐴 + 1)) Fn ℝ)
218 inidm 4218 . . . 4 (ℝ ∩ ℝ) = ℝ
21956, 1, 32, 57mbfi1fseqlem2 25241 . . . . . . 7 ((𝐴 + 1) ∈ β„• β†’ (πΊβ€˜(𝐴 + 1)) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0)))
220219fveq1d 6893 . . . . . 6 ((𝐴 + 1) ∈ β„• β†’ ((πΊβ€˜(𝐴 + 1))β€˜π‘₯) = ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))β€˜π‘₯))
221110, 220syl 17 . . . . 5 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΊβ€˜(𝐴 + 1))β€˜π‘₯) = ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))β€˜π‘₯))
222114, 177ifcld 4574 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) ∈ ℝ)
223 ifcl 4573 . . . . . . 7 ((if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0) ∈ ℝ)
224222, 49, 223sylancl 586 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0) ∈ ℝ)
225 eqid 2732 . . . . . . 7 (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0)) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
226225fvmpt2 7009 . . . . . 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))
22775, 224, 226syl2anc 584 . . . . 5 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))β€˜π‘₯) = if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
228221, 227eqtrd 2772 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΊβ€˜(𝐴 + 1))β€˜π‘₯) = if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
22962, 217, 66, 66, 218, 104, 228ofrfval 7682 . . 3 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ ((πΊβ€˜π΄) ∘r ≀ (πΊβ€˜(𝐴 + 1)) ↔ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0)))
230212, 229mpbird 256 . 2 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜π΄) ∘r ≀ (πΊβ€˜(𝐴 + 1)))
231106, 230jca 512 1 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (0𝑝 ∘r ≀ (πΊβ€˜π΄) ∧ (πΊβ€˜π΄) ∘r ≀ (πΊβ€˜(𝐴 + 1))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  Vcvv 3474   ∩ cin 3947   βŠ† wss 3948  ifcif 4528  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413   ∘r cofr 7671  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  +∞cpnf 11247   < clt 11250   ≀ cle 11251  -cneg 11447   / cdiv 11873  β„•cn 12214  2c2 12269  β„•0cn0 12474  β„€cz 12560  [,)cico 13328  [,]cicc 13329  βŒŠcfl 13757  β†‘cexp 14029  MblFncmbf 25138  βˆ«1citg1 25139  0𝑝c0p 25193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-ofr 7673  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-q 12935  df-rp 12977  df-xneg 13094  df-xadd 13095  df-xmul 13096  df-ioo 13330  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-fl 13759  df-seq 13969  df-exp 14030  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-clim 15434  df-rlim 15435  df-sum 15635  df-rest 17370  df-topgen 17391  df-psmet 20942  df-xmet 20943  df-met 20944  df-bl 20945  df-mopn 20946  df-top 22403  df-topon 22420  df-bases 22456  df-cmp 22898  df-ovol 24988  df-vol 24989  df-mbf 25143  df-itg1 25144  df-0p 25194
This theorem is referenced by:  mbfi1fseqlem6  25245
  Copyright terms: Public domain W3C validator