| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem15.3 | . . . . . 6
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) | 
| 2 |  | fourierdlem15.2 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 3 |  | fourierdlem15.1 | . . . . . . . 8
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) | 
| 4 | 3 | fourierdlem2 46124 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 5 | 2, 4 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) | 
| 6 | 1, 5 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) | 
| 7 | 6 | simpld 494 | . . . 4
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) | 
| 8 |  | reex 11246 | . . . . . 6
⊢ ℝ
∈ V | 
| 9 | 8 | a1i 11 | . . . . 5
⊢ (𝜑 → ℝ ∈
V) | 
| 10 |  | ovex 7464 | . . . . . 6
⊢
(0...𝑀) ∈
V | 
| 11 | 10 | a1i 11 | . . . . 5
⊢ (𝜑 → (0...𝑀) ∈ V) | 
| 12 | 9, 11 | elmapd 8880 | . . . 4
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ)) | 
| 13 | 7, 12 | mpbid 232 | . . 3
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) | 
| 14 |  | ffn 6736 | . . 3
⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀)) | 
| 15 | 13, 14 | syl 17 | . 2
⊢ (𝜑 → 𝑄 Fn (0...𝑀)) | 
| 16 | 6 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) | 
| 17 | 16 | simpld 494 | . . . . . . . 8
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) | 
| 18 | 17 | simpld 494 | . . . . . . 7
⊢ (𝜑 → (𝑄‘0) = 𝐴) | 
| 19 |  | nnnn0 12533 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) | 
| 20 |  | nn0uz 12920 | . . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) | 
| 21 | 19, 20 | eleqtrdi 2851 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
(ℤ≥‘0)) | 
| 22 | 2, 21 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) | 
| 23 |  | eluzfz1 13571 | . . . . . . . . 9
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) | 
| 24 | 22, 23 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 0 ∈ (0...𝑀)) | 
| 25 | 13, 24 | ffvelcdmd 7105 | . . . . . . 7
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) | 
| 26 | 18, 25 | eqeltrrd 2842 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 27 | 26 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ∈ ℝ) | 
| 28 | 17 | simprd 495 | . . . . . . 7
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) | 
| 29 |  | eluzfz2 13572 | . . . . . . . . 9
⊢ (𝑀 ∈
(ℤ≥‘0) → 𝑀 ∈ (0...𝑀)) | 
| 30 | 22, 29 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) | 
| 31 | 13, 30 | ffvelcdmd 7105 | . . . . . . 7
⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ) | 
| 32 | 28, 31 | eqeltrrd 2842 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 33 | 32 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐵 ∈ ℝ) | 
| 34 | 13 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ) | 
| 35 | 18 | eqcomd 2743 | . . . . . . 7
⊢ (𝜑 → 𝐴 = (𝑄‘0)) | 
| 36 | 35 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 = (𝑄‘0)) | 
| 37 |  | elfzuz 13560 | . . . . . . . 8
⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈
(ℤ≥‘0)) | 
| 38 | 37 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈
(ℤ≥‘0)) | 
| 39 | 13 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑄:(0...𝑀)⟶ℝ) | 
| 40 |  | 0zd 12625 | . . . . . . . . . 10
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ∈ ℤ) | 
| 41 |  | elfzel2 13562 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ) | 
| 42 | 41 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℤ) | 
| 43 |  | elfzelz 13564 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℤ) | 
| 44 | 43 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℤ) | 
| 45 |  | elfzle1 13567 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0...𝑖) → 0 ≤ 𝑗) | 
| 46 | 45 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 0 ≤ 𝑗) | 
| 47 | 43 | zred 12722 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ∈ ℝ) | 
| 48 | 47 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ ℝ) | 
| 49 |  | elfzelz 13564 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ) | 
| 50 | 49 | zred 12722 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ) | 
| 51 | 50 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ∈ ℝ) | 
| 52 | 41 | zred 12722 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑀 ∈ ℝ) | 
| 54 |  | elfzle2 13568 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑖) → 𝑗 ≤ 𝑖) | 
| 55 | 54 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑖) | 
| 56 |  | elfzle2 13568 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀) | 
| 57 | 56 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑖 ≤ 𝑀) | 
| 58 | 48, 51, 53, 55, 57 | letrd 11418 | . . . . . . . . . 10
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ≤ 𝑀) | 
| 59 | 40, 42, 44, 46, 58 | elfzd 13555 | . . . . . . . . 9
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀)) | 
| 60 | 59 | adantll 714 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → 𝑗 ∈ (0...𝑀)) | 
| 61 | 39, 60 | ffvelcdmd 7105 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...𝑖)) → (𝑄‘𝑗) ∈ ℝ) | 
| 62 |  | simpll 767 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝜑) | 
| 63 |  | elfzle1 13567 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 0 ≤ 𝑗) | 
| 64 | 63 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ≤ 𝑗) | 
| 65 |  | elfzelz 13564 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℤ) | 
| 66 | 65 | zred 12722 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ∈ ℝ) | 
| 67 | 66 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℝ) | 
| 68 | 50 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ∈ ℝ) | 
| 69 | 52 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℝ) | 
| 70 |  | peano2rem 11576 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℝ → (𝑖 − 1) ∈
ℝ) | 
| 71 | 68, 70 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ) | 
| 72 |  | elfzle2 13568 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1)) | 
| 73 | 72 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1)) | 
| 74 | 68 | ltm1d 12200 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑖 − 1) < 𝑖) | 
| 75 | 67, 71, 68, 73, 74 | lelttrd 11419 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑖) | 
| 76 | 56 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑖 ≤ 𝑀) | 
| 77 | 67, 68, 69, 75, 76 | ltletrd 11421 | . . . . . . . . . 10
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 < 𝑀) | 
| 78 | 65 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ ℤ) | 
| 79 |  | 0zd 12625 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 0 ∈
ℤ) | 
| 80 | 41 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑀 ∈ ℤ) | 
| 81 |  | elfzo 13701 | . . . . . . . . . . 11
⊢ ((𝑗 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑀 ∈
ℤ) → (𝑗 ∈
(0..^𝑀) ↔ (0 ≤
𝑗 ∧ 𝑗 < 𝑀))) | 
| 82 | 78, 79, 80, 81 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀))) | 
| 83 | 64, 77, 82 | mpbir2and 713 | . . . . . . . . 9
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀)) | 
| 84 | 83 | adantll 714 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → 𝑗 ∈ (0..^𝑀)) | 
| 85 | 13 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) | 
| 86 |  | elfzofz 13715 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ (0...𝑀)) | 
| 87 | 86 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀)) | 
| 88 | 85, 87 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ) | 
| 89 |  | fzofzp1 13803 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀)) | 
| 90 | 89 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀)) | 
| 91 | 85, 90 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘(𝑗 + 1)) ∈ ℝ) | 
| 92 |  | eleq1w 2824 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0..^𝑀) ↔ 𝑗 ∈ (0..^𝑀))) | 
| 93 | 92 | anbi2d 630 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0..^𝑀)))) | 
| 94 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗)) | 
| 95 |  | oveq1 7438 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1)) | 
| 96 | 95 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑗 + 1))) | 
| 97 | 94, 96 | breq12d 5156 | . . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑗) < (𝑄‘(𝑗 + 1)))) | 
| 98 | 93, 97 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))))) | 
| 99 | 16 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 100 | 99 | r19.21bi 3251 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) | 
| 101 | 98, 100 | chvarvv 1998 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))) | 
| 102 | 88, 91, 101 | ltled 11409 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1))) | 
| 103 | 62, 84, 102 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...(𝑖 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1))) | 
| 104 | 38, 61, 103 | monoord 14073 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖)) | 
| 105 | 36, 104 | eqbrtrd 5165 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ≤ (𝑄‘𝑖)) | 
| 106 |  | elfzuz3 13561 | . . . . . . . 8
⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ (ℤ≥‘𝑖)) | 
| 107 | 106 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (ℤ≥‘𝑖)) | 
| 108 | 13 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑄:(0...𝑀)⟶ℝ) | 
| 109 |  | fz0fzelfz0 13674 | . . . . . . . . 9
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀)) | 
| 110 | 109 | adantll 714 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → 𝑗 ∈ (0...𝑀)) | 
| 111 | 108, 110 | ffvelcdmd 7105 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...𝑀)) → (𝑄‘𝑗) ∈ ℝ) | 
| 112 | 13 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑄:(0...𝑀)⟶ℝ) | 
| 113 |  | 0zd 12625 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈
ℤ) | 
| 114 | 41 | ad2antlr 727 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℤ) | 
| 115 |  | elfzelz 13564 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℤ) | 
| 116 | 115 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℤ) | 
| 117 |  | 0red 11264 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ∈
ℝ) | 
| 118 | 50 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ∈ ℝ) | 
| 119 | 115 | zred 12722 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ∈ ℝ) | 
| 120 | 119 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ) | 
| 121 |  | elfzle1 13567 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑖) | 
| 123 |  | elfzle1 13567 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑖 ≤ 𝑗) | 
| 124 | 123 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑖 ≤ 𝑗) | 
| 125 | 117, 118,
120, 122, 124 | letrd 11418 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗) | 
| 126 | 125 | adantll 714 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ 𝑗) | 
| 127 | 119 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ) | 
| 128 | 2 | nnred 12281 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 129 | 128 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℝ) | 
| 130 |  | 1red 11262 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈
ℝ) | 
| 131 | 129, 130 | resubcld 11691 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) ∈ ℝ) | 
| 132 |  | elfzle2 13568 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (𝑖...(𝑀 − 1)) → 𝑗 ≤ (𝑀 − 1)) | 
| 133 | 132 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ (𝑀 − 1)) | 
| 134 | 129 | ltm1d 12200 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑀 − 1) < 𝑀) | 
| 135 | 127, 131,
129, 133, 134 | lelttrd 11419 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀) | 
| 136 | 127, 129,
135 | ltled 11409 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀) | 
| 137 | 136 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ≤ 𝑀) | 
| 138 | 113, 114,
116, 126, 137 | elfzd 13555 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0...𝑀)) | 
| 139 | 112, 138 | ffvelcdmd 7105 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ∈ ℝ) | 
| 140 | 116 | peano2zd 12725 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ ℤ) | 
| 141 | 119 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ ℝ) | 
| 142 |  | 1red 11262 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈
ℝ) | 
| 143 |  | 0le1 11786 | . . . . . . . . . . . 12
⊢ 0 ≤
1 | 
| 144 | 143 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤
1) | 
| 145 | 141, 142,
126, 144 | addge0d 11839 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 0 ≤ (𝑗 + 1)) | 
| 146 | 127, 131,
130, 133 | leadd1dd 11877 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ ((𝑀 − 1) + 1)) | 
| 147 | 2 | nncnd 12282 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 148 | 147 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑀 ∈ ℂ) | 
| 149 |  | 1cnd 11256 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 1 ∈
ℂ) | 
| 150 | 148, 149 | npcand 11624 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀) | 
| 151 | 146, 150 | breqtrd 5169 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀) | 
| 152 | 151 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ≤ 𝑀) | 
| 153 | 113, 114,
140, 145, 152 | elfzd 13555 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 + 1) ∈ (0...𝑀)) | 
| 154 | 112, 153 | ffvelcdmd 7105 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘(𝑗 + 1)) ∈ ℝ) | 
| 155 |  | simpll 767 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝜑) | 
| 156 | 135 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 < 𝑀) | 
| 157 | 116, 113,
114, 81 | syl3anc 1373 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑗 ∈ (0..^𝑀) ↔ (0 ≤ 𝑗 ∧ 𝑗 < 𝑀))) | 
| 158 | 126, 156,
157 | mpbir2and 713 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → 𝑗 ∈ (0..^𝑀)) | 
| 159 | 155, 158,
101 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) < (𝑄‘(𝑗 + 1))) | 
| 160 | 139, 154,
159 | ltled 11409 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑗 ∈ (𝑖...(𝑀 − 1))) → (𝑄‘𝑗) ≤ (𝑄‘(𝑗 + 1))) | 
| 161 | 107, 111,
160 | monoord 14073 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀)) | 
| 162 | 28 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑀) = 𝐵) | 
| 163 | 161, 162 | breqtrd 5169 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ 𝐵) | 
| 164 | 27, 33, 34, 105, 163 | eliccd 45517 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (𝐴[,]𝐵)) | 
| 165 | 164 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵)) | 
| 166 |  | fnfvrnss 7141 | . . 3
⊢ ((𝑄 Fn (0...𝑀) ∧ ∀𝑖 ∈ (0...𝑀)(𝑄‘𝑖) ∈ (𝐴[,]𝐵)) → ran 𝑄 ⊆ (𝐴[,]𝐵)) | 
| 167 | 15, 165, 166 | syl2anc 584 | . 2
⊢ (𝜑 → ran 𝑄 ⊆ (𝐴[,]𝐵)) | 
| 168 |  | df-f 6565 | . 2
⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) ↔ (𝑄 Fn (0...𝑀) ∧ ran 𝑄 ⊆ (𝐴[,]𝐵))) | 
| 169 | 15, 167, 168 | sylanbrc 583 | 1
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) |