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

Theorem mbfi1fseqlem5 25107
Description: Lemma for mbfi1fseq 25109. 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 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ 𝐹:β„βŸΆ(0[,)+∞))
32ffvelcdmda 7039 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ (0[,)+∞))
4 elrege0 13380 . . . . . . . . . . . . 13 ((πΉβ€˜π‘₯) ∈ (0[,)+∞) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)))
53, 4sylib 217 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)))
65simpld 496 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
7 2nn 12234 . . . . . . . . . . . . . 14 2 ∈ β„•
8 nnnn0 12428 . . . . . . . . . . . . . 14 (𝐴 ∈ β„• β†’ 𝐴 ∈ β„•0)
9 nnexpcl 13989 . . . . . . . . . . . . . 14 ((2 ∈ β„• ∧ 𝐴 ∈ β„•0) β†’ (2↑𝐴) ∈ β„•)
107, 8, 9sylancr 588 . . . . . . . . . . . . 13 (𝐴 ∈ β„• β†’ (2↑𝐴) ∈ β„•)
1110ad2antlr 726 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) ∈ β„•)
1211nnred 12176 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) ∈ ℝ)
136, 12remulcld 11193 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) Β· (2↑𝐴)) ∈ ℝ)
1411nnnn0d 12481 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) ∈ β„•0)
1514nn0ge0d 12484 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (2↑𝐴))
16 mulge0 11681 . . . . . . . . . . 11 ((((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 ≀ (2↑𝐴))) β†’ 0 ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
175, 12, 15, 16syl12anc 836 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
18 flge0nn0 13734 . . . . . . . . . 10 ((((πΉβ€˜π‘₯) Β· (2↑𝐴)) ∈ ℝ ∧ 0 ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴))) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„•0)
1913, 17, 18syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„•0)
2019nn0red 12482 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ ℝ)
2119nn0ge0d 12484 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))))
2211nngt0d 12210 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 < (2↑𝐴))
23 divge0 12032 . . . . . . . 8 ((((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ ℝ ∧ 0 ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴)))) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 < (2↑𝐴))) β†’ 0 ≀ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
2420, 21, 12, 22, 23syl22anc 838 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
25 simpr 486 . . . . . . . . . . . . 13 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ 𝑦 = π‘₯)
2625fveq2d 6850 . . . . . . . . . . . 12 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘₯))
27 simpl 484 . . . . . . . . . . . . 13 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ π‘š = 𝐴)
2827oveq2d 7377 . . . . . . . . . . . 12 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ (2β†‘π‘š) = (2↑𝐴))
2926, 28oveq12d 7379 . . . . . . . . . . 11 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ ((πΉβ€˜π‘¦) Β· (2β†‘π‘š)) = ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
3029fveq2d 6850 . . . . . . . . . 10 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ (βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) = (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))))
3130, 28oveq12d 7379 . . . . . . . . 9 ((π‘š = 𝐴 ∧ 𝑦 = π‘₯) β†’ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
32 mbfi1fseq.3 . . . . . . . . 9 𝐽 = (π‘š ∈ β„•, 𝑦 ∈ ℝ ↦ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)))
33 ovex 7394 . . . . . . . . 9 ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ∈ V
3431, 32, 33ovmpoa 7514 . . . . . . . 8 ((𝐴 ∈ β„• ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
3534adantll 713 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)))
3624, 35breqtrrd 5137 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (𝐴𝐽π‘₯))
378nn0ge0d 12484 . . . . . . 7 (𝐴 ∈ β„• β†’ 0 ≀ 𝐴)
3837ad2antlr 726 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ 𝐴)
39 breq2 5113 . . . . . . 7 ((𝐴𝐽π‘₯) = if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) β†’ (0 ≀ (𝐴𝐽π‘₯) ↔ 0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴)))
40 breq2 5113 . . . . . . 7 (𝐴 = if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) β†’ (0 ≀ 𝐴 ↔ 0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴)))
4139, 40ifboth 4529 . . . . . 6 ((0 ≀ (𝐴𝐽π‘₯) ∧ 0 ≀ 𝐴) β†’ 0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴))
4236, 38, 41syl2anc 585 . . . . 5 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴))
43 0le0 12262 . . . . 5 0 ≀ 0
44 breq2 5113 . . . . . 6 (if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) β†’ (0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ↔ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)))
45 breq2 5113 . . . . . 6 (0 = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) β†’ (0 ≀ 0 ↔ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)))
4644, 45ifboth 4529 . . . . 5 ((0 ≀ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ∧ 0 ≀ 0) β†’ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
4742, 43, 46sylancl 587 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
4847ralrimiva 3140 . . 3 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ βˆ€π‘₯ ∈ ℝ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
49 0re 11165 . . . . . . 7 0 ∈ ℝ
50 fnconstg 6734 . . . . . . 7 (0 ∈ ℝ β†’ (β„‚ Γ— {0}) Fn β„‚)
5149, 50ax-mp 5 . . . . . 6 (β„‚ Γ— {0}) Fn β„‚
52 df-0p 25057 . . . . . . 7 0𝑝 = (β„‚ Γ— {0})
5352fneq1i 6603 . . . . . 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 25106 . . . . . 6 (πœ‘ β†’ 𝐺:β„•βŸΆdom ∫1)
5958ffvelcdmda 7039 . . . . 5 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜π΄) ∈ dom ∫1)
60 i1ff 25063 . . . . 5 ((πΊβ€˜π΄) ∈ dom ∫1 β†’ (πΊβ€˜π΄):β„βŸΆβ„)
61 ffn 6672 . . . . 5 ((πΊβ€˜π΄):β„βŸΆβ„ β†’ (πΊβ€˜π΄) Fn ℝ)
6259, 60, 613syl 18 . . . 4 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜π΄) Fn ℝ)
63 cnex 11140 . . . . 5 β„‚ ∈ V
6463a1i 11 . . . 4 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ β„‚ ∈ V)
65 reex 11150 . . . . 5 ℝ ∈ V
6665a1i 11 . . . 4 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ ℝ ∈ V)
67 ax-resscn 11116 . . . . 5 ℝ βŠ† β„‚
68 sseqin2 4179 . . . . 5 (ℝ βŠ† β„‚ ↔ (β„‚ ∩ ℝ) = ℝ)
6967, 68mpbi 229 . . . 4 (β„‚ ∩ ℝ) = ℝ
70 0pval 25058 . . . . 5 (π‘₯ ∈ β„‚ β†’ (0π‘β€˜π‘₯) = 0)
7170adantl 483 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ β„‚) β†’ (0π‘β€˜π‘₯) = 0)
7256, 1, 32, 57mbfi1fseqlem2 25104 . . . . . . 7 (𝐴 ∈ β„• β†’ (πΊβ€˜π΄) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)))
7372fveq1d 6848 . . . . . 6 (𝐴 ∈ β„• β†’ ((πΊβ€˜π΄)β€˜π‘₯) = ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))β€˜π‘₯))
7473ad2antlr 726 . . . . 5 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΊβ€˜π΄)β€˜π‘₯) = ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))β€˜π‘₯))
75 simpr 486 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ π‘₯ ∈ ℝ)
76 rge0ssre 13382 . . . . . . . . . . . . . . . 16 (0[,)+∞) βŠ† ℝ
77 simpr 486 . . . . . . . . . . . . . . . . 17 ((π‘š ∈ β„• ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ)
78 ffvelcdm 7036 . . . . . . . . . . . . . . . . 17 ((𝐹:β„βŸΆ(0[,)+∞) ∧ 𝑦 ∈ ℝ) β†’ (πΉβ€˜π‘¦) ∈ (0[,)+∞))
791, 77, 78syl2an 597 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (πΉβ€˜π‘¦) ∈ (0[,)+∞))
8076, 79sselid 3946 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (πΉβ€˜π‘¦) ∈ ℝ)
81 nnnn0 12428 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„• β†’ π‘š ∈ β„•0)
82 nnexpcl 13989 . . . . . . . . . . . . . . . . . 18 ((2 ∈ β„• ∧ π‘š ∈ β„•0) β†’ (2β†‘π‘š) ∈ β„•)
837, 81, 82sylancr 588 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„• β†’ (2β†‘π‘š) ∈ β„•)
8483ad2antrl 727 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (2β†‘π‘š) ∈ β„•)
8584nnred 12176 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (2β†‘π‘š) ∈ ℝ)
8680, 85remulcld 11193 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ ((πΉβ€˜π‘¦) Β· (2β†‘π‘š)) ∈ ℝ)
87 reflcl 13710 . . . . . . . . . . . . . 14 (((πΉβ€˜π‘¦) Β· (2β†‘π‘š)) ∈ ℝ β†’ (βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) ∈ ℝ)
8886, 87syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ (βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) ∈ ℝ)
8988, 84nndivred 12215 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘š ∈ β„• ∧ 𝑦 ∈ ℝ)) β†’ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) ∈ ℝ)
9089ralrimivva 3194 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘š ∈ β„• βˆ€π‘¦ ∈ ℝ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) ∈ ℝ)
9132fmpo 8004 . . . . . . . . . . 11 (βˆ€π‘š ∈ β„• βˆ€π‘¦ ∈ ℝ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) ∈ ℝ ↔ 𝐽:(β„• Γ— ℝ)βŸΆβ„)
9290, 91sylib 217 . . . . . . . . . 10 (πœ‘ β†’ 𝐽:(β„• Γ— ℝ)βŸΆβ„)
93 fovcdm 7528 . . . . . . . . . 10 ((𝐽:(β„• Γ— ℝ)βŸΆβ„ ∧ 𝐴 ∈ β„• ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) ∈ ℝ)
9492, 93syl3an1 1164 . . . . . . . . 9 ((πœ‘ ∧ 𝐴 ∈ β„• ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) ∈ ℝ)
95943expa 1119 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) ∈ ℝ)
96 nnre 12168 . . . . . . . . 9 (𝐴 ∈ β„• β†’ 𝐴 ∈ ℝ)
9796ad2antlr 726 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 𝐴 ∈ ℝ)
9895, 97ifcld 4536 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ∈ ℝ)
99 ifcl 4535 . . . . . . 7 ((if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ∈ ℝ)
10098, 49, 99sylancl 587 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ∈ ℝ)
101 eqid 2733 . . . . . . 7 (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
102101fvmpt2 6963 . . . . . 6 ((π‘₯ ∈ ℝ ∧ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ∈ ℝ) β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))β€˜π‘₯) = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
10375, 100, 102syl2anc 585 . . . . 5 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))β€˜π‘₯) = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
10474, 103eqtrd 2773 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΊβ€˜π΄)β€˜π‘₯) = if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0))
10555, 62, 64, 66, 69, 71, 104ofrfval 7631 . . 3 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (0𝑝 ∘r ≀ (πΊβ€˜π΄) ↔ βˆ€π‘₯ ∈ ℝ 0 ≀ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0)))
10648, 105mpbird 257 . 2 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ 0𝑝 ∘r ≀ (πΊβ€˜π΄))
10756, 1, 32mbfi1fseqlem1 25103 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐽:(β„• Γ— ℝ)⟢(0[,)+∞))
108107ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 𝐽:(β„• Γ— ℝ)⟢(0[,)+∞))
109 peano2nn 12173 . . . . . . . . . . . . 13 (𝐴 ∈ β„• β†’ (𝐴 + 1) ∈ β„•)
110109ad2antlr 726 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴 + 1) ∈ β„•)
111108, 110, 75fovcdmd 7530 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((𝐴 + 1)𝐽π‘₯) ∈ (0[,)+∞))
112 elrege0 13380 . . . . . . . . . . 11 (((𝐴 + 1)𝐽π‘₯) ∈ (0[,)+∞) ↔ (((𝐴 + 1)𝐽π‘₯) ∈ ℝ ∧ 0 ≀ ((𝐴 + 1)𝐽π‘₯)))
113111, 112sylib 217 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((𝐴 + 1)𝐽π‘₯) ∈ ℝ ∧ 0 ≀ ((𝐴 + 1)𝐽π‘₯)))
114113simpld 496 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((𝐴 + 1)𝐽π‘₯) ∈ ℝ)
115 min1 13117 . . . . . . . . . 10 (((𝐴𝐽π‘₯) ∈ ℝ ∧ 𝐴 ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴𝐽π‘₯))
11695, 97, 115syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴𝐽π‘₯))
117 2cn 12236 . . . . . . . . . . . . . . 15 2 ∈ β„‚
1188ad2antlr 726 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 𝐴 ∈ β„•0)
119 expp1 13983 . . . . . . . . . . . . . . 15 ((2 ∈ β„‚ ∧ 𝐴 ∈ β„•0) β†’ (2↑(𝐴 + 1)) = ((2↑𝐴) Β· 2))
120117, 118, 119sylancr 588 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑(𝐴 + 1)) = ((2↑𝐴) Β· 2))
121120oveq2d 7377 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑(𝐴 + 1))) = (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· ((2↑𝐴) Β· 2)))
12235, 95eqeltrrd 2835 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ∈ ℝ)
123122recnd 11191 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) ∈ β„‚)
12412recnd 11191 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) ∈ β„‚)
125 2cnd 12239 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 2 ∈ β„‚)
126123, 124, 125mulassd 11186 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑𝐴)) Β· 2) = (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· ((2↑𝐴) Β· 2)))
12720recnd 11191 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„‚)
12811nnne0d 12211 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑𝐴) β‰  0)
129127, 124, 128divcan1d 11940 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑𝐴)) = (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))))
130129oveq1d 7376 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑𝐴)) Β· 2) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2))
131121, 126, 1303eqtr2d 2779 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑(𝐴 + 1))) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2))
132 flle 13713 . . . . . . . . . . . . . . . 16 (((πΉβ€˜π‘₯) Β· (2↑𝐴)) ∈ ℝ β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
13313, 132syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)))
134 2re 12235 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
135 2pos 12264 . . . . . . . . . . . . . . . . . 18 0 < 2
136134, 135pm3.2i 472 . . . . . . . . . . . . . . . . 17 (2 ∈ ℝ ∧ 0 < 2)
137136a1i 11 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2 ∈ ℝ ∧ 0 < 2))
138 lemul1 12015 . . . . . . . . . . . . . . . 16 (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ ℝ ∧ ((πΉβ€˜π‘₯) Β· (2↑𝐴)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2)))
13920, 13, 137, 138syl3anc 1372 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ≀ ((πΉβ€˜π‘₯) Β· (2↑𝐴)) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2)))
140133, 139mpbid 231 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2))
141120oveq2d 7377 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) = ((πΉβ€˜π‘₯) Β· ((2↑𝐴) Β· 2)))
1426recnd 11191 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
143142, 124, 125mulassd 11186 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2) = ((πΉβ€˜π‘₯) Β· ((2↑𝐴) Β· 2)))
144141, 143eqtr4d 2776 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) = (((πΉβ€˜π‘₯) Β· (2↑𝐴)) Β· 2))
145140, 144breqtrrd 5137 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))))
146110nnnn0d 12481 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴 + 1) ∈ β„•0)
147 nnexpcl 13989 . . . . . . . . . . . . . . . . 17 ((2 ∈ β„• ∧ (𝐴 + 1) ∈ β„•0) β†’ (2↑(𝐴 + 1)) ∈ β„•)
1487, 146, 147sylancr 588 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑(𝐴 + 1)) ∈ β„•)
149148nnred 12176 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (2↑(𝐴 + 1)) ∈ ℝ)
1506, 149remulcld 11193 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ∈ ℝ)
15113flcld 13712 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„€)
152 2z 12543 . . . . . . . . . . . . . . 15 2 ∈ β„€
153 zmulcl 12560 . . . . . . . . . . . . . . 15 (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) ∈ β„€ ∧ 2 ∈ β„€) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ∈ β„€)
154151, 152, 153sylancl 587 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ∈ β„€)
155 flge 13719 . . . . . . . . . . . . . 14 ((((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ∈ ℝ ∧ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ∈ β„€) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))))))
156150, 154, 155syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ↔ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))))))
157145, 156mpbid 231 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) Β· 2) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))))
158131, 157eqbrtrd 5131 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑𝐴))) / (2↑𝐴)) Β· (2↑(𝐴 + 1))) ≀ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))))
159 reflcl 13710 . . . . . . . . . . . . 13 (((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))) ∈ ℝ β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) ∈ ℝ)
160150, 159syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) ∈ ℝ)
161148nngt0d 12210 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 < (2↑(𝐴 + 1)))
162 lemuldiv 12043 . . . . . . . . . . . 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 1375 . . . . . . . . . . 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 486 . . . . . . . . . . . . . . . 16 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ 𝑦 = π‘₯)
166165fveq2d 6850 . . . . . . . . . . . . . . 15 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘₯))
167 simpl 484 . . . . . . . . . . . . . . . 16 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ π‘š = (𝐴 + 1))
168167oveq2d 7377 . . . . . . . . . . . . . . 15 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ (2β†‘π‘š) = (2↑(𝐴 + 1)))
169166, 168oveq12d 7379 . . . . . . . . . . . . . 14 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ ((πΉβ€˜π‘¦) Β· (2β†‘π‘š)) = ((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1))))
170169fveq2d 6850 . . . . . . . . . . . . 13 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ (βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) = (βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))))
171170, 168oveq12d 7379 . . . . . . . . . . . 12 ((π‘š = (𝐴 + 1) ∧ 𝑦 = π‘₯) β†’ ((βŒŠβ€˜((πΉβ€˜π‘¦) Β· (2β†‘π‘š))) / (2β†‘π‘š)) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
172 ovex 7394 . . . . . . . . . . . 12 ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))) ∈ V
173171, 32, 172ovmpoa 7514 . . . . . . . . . . 11 (((𝐴 + 1) ∈ β„• ∧ π‘₯ ∈ ℝ) β†’ ((𝐴 + 1)𝐽π‘₯) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
174110, 75, 173syl2anc 585 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((𝐴 + 1)𝐽π‘₯) = ((βŒŠβ€˜((πΉβ€˜π‘₯) Β· (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
175164, 35, 1743brtr4d 5141 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴𝐽π‘₯) ≀ ((𝐴 + 1)𝐽π‘₯))
17698, 95, 114, 116, 175letrd 11320 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ ((𝐴 + 1)𝐽π‘₯))
177110nnred 12176 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴 + 1) ∈ ℝ)
178 min2 13118 . . . . . . . . . 10 (((𝐴𝐽π‘₯) ∈ ℝ ∧ 𝐴 ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ 𝐴)
17995, 97, 178syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ 𝐴)
18097lep1d 12094 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 𝐴 ≀ (𝐴 + 1))
18198, 97, 177, 179, 180letrd 11320 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴 + 1))
182 breq2 5113 . . . . . . . . 9 (((𝐴 + 1)𝐽π‘₯) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) β†’ (if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ ((𝐴 + 1)𝐽π‘₯) ↔ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1))))
183 breq2 5113 . . . . . . . . 9 ((𝐴 + 1) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) β†’ (if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴 + 1) ↔ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1))))
184182, 183ifboth 4529 . . . . . . . 8 ((if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ ((𝐴 + 1)𝐽π‘₯) ∧ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ (𝐴 + 1)) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
185176, 181, 184syl2anc 585 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
186185adantr 482 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴) ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
187 iftrue 4496 . . . . . . 7 (π‘₯ ∈ (-𝐴[,]𝐴) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) = if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴))
188187adantl 483 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) = if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴))
189177renegcld 11590 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ -(𝐴 + 1) ∈ ℝ)
19097, 177lenegd 11742 . . . . . . . . . 10 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (𝐴 ≀ (𝐴 + 1) ↔ -(𝐴 + 1) ≀ -𝐴))
191180, 190mpbid 231 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ -(𝐴 + 1) ≀ -𝐴)
192 iccss 13341 . . . . . . . . 9 (((-(𝐴 + 1) ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ) ∧ (-(𝐴 + 1) ≀ -𝐴 ∧ 𝐴 ≀ (𝐴 + 1))) β†’ (-𝐴[,]𝐴) βŠ† (-(𝐴 + 1)[,](𝐴 + 1)))
193189, 177, 191, 180, 192syl22anc 838 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (-𝐴[,]𝐴) βŠ† (-(𝐴 + 1)[,](𝐴 + 1)))
194193sselda 3948 . . . . . . 7 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)))
195194iftrued 4498 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
196186, 188, 1953brtr4d 5141 . . . . 5 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
197 iffalse 4499 . . . . . . 7 (Β¬ π‘₯ ∈ (-𝐴[,]𝐴) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) = 0)
198197adantl 483 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) = 0)
199113simprd 497 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ ((𝐴 + 1)𝐽π‘₯))
200146nn0ge0d 12484 . . . . . . . . 9 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (𝐴 + 1))
201 breq2 5113 . . . . . . . . . 10 (((𝐴 + 1)𝐽π‘₯) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) β†’ (0 ≀ ((𝐴 + 1)𝐽π‘₯) ↔ 0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1))))
202 breq2 5113 . . . . . . . . . 10 ((𝐴 + 1) = if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) β†’ (0 ≀ (𝐴 + 1) ↔ 0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1))))
203201, 202ifboth 4529 . . . . . . . . 9 ((0 ≀ ((𝐴 + 1)𝐽π‘₯) ∧ 0 ≀ (𝐴 + 1)) β†’ 0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
204199, 200, 203syl2anc 585 . . . . . . . 8 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)))
205 breq2 5113 . . . . . . . . 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 5113 . . . . . . . . 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 4529 . . . . . . . 8 ((0 ≀ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) ∧ 0 ≀ 0) β†’ 0 ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
208204, 43, 207sylancl 587 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
209208adantr 482 . . . . . 6 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ 0 ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
210198, 209eqbrtrd 5131 . . . . 5 ((((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (-𝐴[,]𝐴)) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
211196, 210pm2.61dan 812 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
212211ralrimiva 3140 . . 3 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
213 ffvelcdm 7036 . . . . . 6 ((𝐺:β„•βŸΆdom ∫1 ∧ (𝐴 + 1) ∈ β„•) β†’ (πΊβ€˜(𝐴 + 1)) ∈ dom ∫1)
21458, 109, 213syl2an 597 . . . . 5 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜(𝐴 + 1)) ∈ dom ∫1)
215 i1ff 25063 . . . . 5 ((πΊβ€˜(𝐴 + 1)) ∈ dom ∫1 β†’ (πΊβ€˜(𝐴 + 1)):β„βŸΆβ„)
216 ffn 6672 . . . . 5 ((πΊβ€˜(𝐴 + 1)):β„βŸΆβ„ β†’ (πΊβ€˜(𝐴 + 1)) Fn ℝ)
217214, 215, 2163syl 18 . . . 4 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜(𝐴 + 1)) Fn ℝ)
218 inidm 4182 . . . 4 (ℝ ∩ ℝ) = ℝ
21956, 1, 32, 57mbfi1fseqlem2 25104 . . . . . . 7 ((𝐴 + 1) ∈ β„• β†’ (πΊβ€˜(𝐴 + 1)) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0)))
220219fveq1d 6848 . . . . . 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 4536 . . . . . . 7 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) ∈ ℝ)
223 ifcl 4535 . . . . . . 7 ((if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0) ∈ ℝ)
224222, 49, 223sylancl 587 . . . . . 6 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0) ∈ ℝ)
225 eqid 2733 . . . . . . 7 (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0)) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
226225fvmpt2 6963 . . . . . 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 585 . . . . 5 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))β€˜π‘₯) = if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
228221, 227eqtrd 2773 . . . 4 (((πœ‘ ∧ 𝐴 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ ((πΊβ€˜(𝐴 + 1))β€˜π‘₯) = if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0))
22962, 217, 66, 66, 218, 104, 228ofrfval 7631 . . 3 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ ((πΊβ€˜π΄) ∘r ≀ (πΊβ€˜(𝐴 + 1)) ↔ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (-𝐴[,]𝐴), if((𝐴𝐽π‘₯) ≀ 𝐴, (𝐴𝐽π‘₯), 𝐴), 0) ≀ if(π‘₯ ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽π‘₯) ≀ (𝐴 + 1), ((𝐴 + 1)𝐽π‘₯), (𝐴 + 1)), 0)))
230212, 229mpbird 257 . 2 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (πΊβ€˜π΄) ∘r ≀ (πΊβ€˜(𝐴 + 1)))
231106, 230jca 513 1 ((πœ‘ ∧ 𝐴 ∈ β„•) β†’ (0𝑝 ∘r ≀ (πΊβ€˜π΄) ∧ (πΊβ€˜π΄) ∘r ≀ (πΊβ€˜(𝐴 + 1))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  Vcvv 3447   ∩ cin 3913   βŠ† wss 3914  ifcif 4490  {csn 4590   class class class wbr 5109   ↦ cmpt 5192   Γ— cxp 5635  dom cdm 5637   Fn wfn 6495  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361   ∈ cmpo 7363   ∘r cofr 7620  β„‚cc 11057  β„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   Β· cmul 11064  +∞cpnf 11194   < clt 11197   ≀ cle 11198  -cneg 11394   / cdiv 11820  β„•cn 12161  2c2 12216  β„•0cn0 12421  β„€cz 12507  [,)cico 13275  [,]cicc 13276  βŒŠcfl 13704  β†‘cexp 13976  MblFncmbf 25001  βˆ«1citg1 25002  0𝑝c0p 25056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7621  df-ofr 7622  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-er 8654  df-map 8773  df-pm 8774  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fi 9355  df-sup 9386  df-inf 9387  df-oi 9454  df-dju 9845  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-n0 12422  df-z 12508  df-uz 12772  df-q 12882  df-rp 12924  df-xneg 13041  df-xadd 13042  df-xmul 13043  df-ioo 13277  df-ico 13279  df-icc 13280  df-fz 13434  df-fzo 13577  df-fl 13706  df-seq 13916  df-exp 13977  df-hash 14240  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-clim 15379  df-rlim 15380  df-sum 15580  df-rest 17312  df-topgen 17333  df-psmet 20811  df-xmet 20812  df-met 20813  df-bl 20814  df-mopn 20815  df-top 22266  df-topon 22283  df-bases 22319  df-cmp 22761  df-ovol 24851  df-vol 24852  df-mbf 25006  df-itg1 25007  df-0p 25057
This theorem is referenced by:  mbfi1fseqlem6  25108
  Copyright terms: Public domain W3C validator