Metamath Proof Explorer

Theorem ovolicc2lem3

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Hypotheses ovolicc.1 ⊢ φ → A ∈ ℝ
ovolicc.2 ⊢ φ → B ∈ ℝ
ovolicc.3 ⊢ φ → A ≤ B
ovolicc2.4 ⊢ S = seq 1 + abs ∘ − ∘ F
ovolicc2.5 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
ovolicc2.6 ⊢ φ → U ∈ 𝒫 ran ⁡ . ∘ F ∩ Fin
ovolicc2.7 ⊢ φ → A B ⊆ ⋃ U
ovolicc2.8 ⊢ φ → G : U ⟶ ℕ
ovolicc2.9 ⊢ φ ∧ t ∈ U → . ∘ F ⁡ G ⁡ t = t
ovolicc2.10 ⊢ T = u ∈ U | u ∩ A B ≠ ∅
ovolicc2.11 ⊢ φ → H : T ⟶ T
ovolicc2.12 ⊢ φ ∧ t ∈ T → if 2 nd ⁡ F ⁡ G ⁡ t ≤ B 2 nd ⁡ F ⁡ G ⁡ t B ∈ H ⁡ t
ovolicc2.13 ⊢ φ → A ∈ C
ovolicc2.14 ⊢ φ → C ∈ T
ovolicc2.15 ⊢ K = seq 1 H ∘ 1 st ℕ × C
ovolicc2.16 ⊢ W = n ∈ ℕ | B ∈ K ⁡ n
Assertion ovolicc2lem3 ⊢ φ ∧ N ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m ∧ P ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → N = P ↔ 2 nd ⁡ F ⁡ G ⁡ K ⁡ N = 2 nd ⁡ F ⁡ G ⁡ K ⁡ P

Proof

Step Hyp Ref Expression
1 ovolicc.1 ⊢ φ → A ∈ ℝ
2 ovolicc.2 ⊢ φ → B ∈ ℝ
3 ovolicc.3 ⊢ φ → A ≤ B
4 ovolicc2.4 ⊢ S = seq 1 + abs ∘ − ∘ F
5 ovolicc2.5 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
6 ovolicc2.6 ⊢ φ → U ∈ 𝒫 ran ⁡ . ∘ F ∩ Fin
7 ovolicc2.7 ⊢ φ → A B ⊆ ⋃ U
8 ovolicc2.8 ⊢ φ → G : U ⟶ ℕ
9 ovolicc2.9 ⊢ φ ∧ t ∈ U → . ∘ F ⁡ G ⁡ t = t
10 ovolicc2.10 ⊢ T = u ∈ U | u ∩ A B ≠ ∅
11 ovolicc2.11 ⊢ φ → H : T ⟶ T
12 ovolicc2.12 ⊢ φ ∧ t ∈ T → if 2 nd ⁡ F ⁡ G ⁡ t ≤ B 2 nd ⁡ F ⁡ G ⁡ t B ∈ H ⁡ t
13 ovolicc2.13 ⊢ φ → A ∈ C
14 ovolicc2.14 ⊢ φ → C ∈ T
15 ovolicc2.15 ⊢ K = seq 1 H ∘ 1 st ℕ × C
16 ovolicc2.16 ⊢ W = n ∈ ℕ | B ∈ K ⁡ n
17 2fveq3 ⊢ y = k → G ⁡ K ⁡ y = G ⁡ K ⁡ k
18 17 fveq2d ⊢ y = k → F ⁡ G ⁡ K ⁡ y = F ⁡ G ⁡ K ⁡ k
19 18 fveq2d ⊢ y = k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y = 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
20 2fveq3 ⊢ y = N → G ⁡ K ⁡ y = G ⁡ K ⁡ N
21 20 fveq2d ⊢ y = N → F ⁡ G ⁡ K ⁡ y = F ⁡ G ⁡ K ⁡ N
22 21 fveq2d ⊢ y = N → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y = 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
23 2fveq3 ⊢ y = P → G ⁡ K ⁡ y = G ⁡ K ⁡ P
24 23 fveq2d ⊢ y = P → F ⁡ G ⁡ K ⁡ y = F ⁡ G ⁡ K ⁡ P
25 24 fveq2d ⊢ y = P → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y = 2 nd ⁡ F ⁡ G ⁡ K ⁡ P
26 ssrab2 ⊢ n ∈ ℕ | ∀ m ∈ W n ≤ m ⊆ ℕ
27 nnssre ⊢ ℕ ⊆ ℝ
28 26 27 sstri ⊢ n ∈ ℕ | ∀ m ∈ W n ≤ m ⊆ ℝ
29 26 sseli ⊢ y ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → y ∈ ℕ
30 inss2 ⊢ ≤ ∩ ℝ 2 ⊆ ℝ 2
31 fss ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ ≤ ∩ ℝ 2 ⊆ ℝ 2 → F : ℕ ⟶ ℝ 2
32 5 30 31 sylancl ⊢ φ → F : ℕ ⟶ ℝ 2
33 32 adantr ⊢ φ ∧ y ∈ ℕ → F : ℕ ⟶ ℝ 2
34 8 adantr ⊢ φ ∧ y ∈ ℕ → G : U ⟶ ℕ
35 nnuz ⊢ ℕ = ℤ ≥ 1
36 1zzd ⊢ φ → 1 ∈ ℤ
37 35 15 36 14 11 algrf ⊢ φ → K : ℕ ⟶ T
38 37 adantr ⊢ φ ∧ y ∈ ℕ → K : ℕ ⟶ T
39 10 ssrab3 ⊢ T ⊆ U
40 fss ⊢ K : ℕ ⟶ T ∧ T ⊆ U → K : ℕ ⟶ U
41 38 39 40 sylancl ⊢ φ ∧ y ∈ ℕ → K : ℕ ⟶ U
42 ffvelrn ⊢ K : ℕ ⟶ U ∧ y ∈ ℕ → K ⁡ y ∈ U
43 41 42 sylancom ⊢ φ ∧ y ∈ ℕ → K ⁡ y ∈ U
44 34 43 ffvelrnd ⊢ φ ∧ y ∈ ℕ → G ⁡ K ⁡ y ∈ ℕ
45 33 44 ffvelrnd ⊢ φ ∧ y ∈ ℕ → F ⁡ G ⁡ K ⁡ y ∈ ℝ 2
46 xp2nd ⊢ F ⁡ G ⁡ K ⁡ y ∈ ℝ 2 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y ∈ ℝ
47 45 46 syl ⊢ φ ∧ y ∈ ℕ → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y ∈ ℝ
48 29 47 sylan2 ⊢ φ ∧ y ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y ∈ ℝ
49 26 sseli ⊢ k ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → k ∈ ℕ
50 49 ad2antll ⊢ φ ∧ y ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m ∧ k ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → k ∈ ℕ
51 29 anim2i ⊢ φ ∧ y ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → φ ∧ y ∈ ℕ
52 51 adantrr ⊢ φ ∧ y ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m ∧ k ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → φ ∧ y ∈ ℕ
53 breq1 ⊢ n = k → n ≤ m ↔ k ≤ m
54 53 ralbidv ⊢ n = k → ∀ m ∈ W n ≤ m ↔ ∀ m ∈ W k ≤ m
55 54 elrab ⊢ k ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m ↔ k ∈ ℕ ∧ ∀ m ∈ W k ≤ m
56 55 simprbi ⊢ k ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → ∀ m ∈ W k ≤ m
57 56 ad2antll ⊢ φ ∧ y ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m ∧ k ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → ∀ m ∈ W k ≤ m
58 breq1 ⊢ x = 1 → x ≤ m ↔ 1 ≤ m
59 58 ralbidv ⊢ x = 1 → ∀ m ∈ W x ≤ m ↔ ∀ m ∈ W 1 ≤ m
60 breq2 ⊢ x = 1 → y < x ↔ y < 1
61 2fveq3 ⊢ x = 1 → G ⁡ K ⁡ x = G ⁡ K ⁡ 1
62 61 fveq2d ⊢ x = 1 → F ⁡ G ⁡ K ⁡ x = F ⁡ G ⁡ K ⁡ 1
63 62 fveq2d ⊢ x = 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ x = 2 nd ⁡ F ⁡ G ⁡ K ⁡ 1
64 63 breq2d ⊢ x = 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ 1
65 60 64 imbi12d ⊢ x = 1 → y < x → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ y < 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ 1
66 59 65 imbi12d ⊢ x = 1 → ∀ m ∈ W x ≤ m → y < x → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ ∀ m ∈ W 1 ≤ m → y < 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ 1
67 66 imbi2d ⊢ x = 1 → φ ∧ y ∈ ℕ → ∀ m ∈ W x ≤ m → y < x → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ φ ∧ y ∈ ℕ → ∀ m ∈ W 1 ≤ m → y < 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ 1
68 breq1 ⊢ x = k → x ≤ m ↔ k ≤ m
69 68 ralbidv ⊢ x = k → ∀ m ∈ W x ≤ m ↔ ∀ m ∈ W k ≤ m
70 breq2 ⊢ x = k → y < x ↔ y < k
71 2fveq3 ⊢ x = k → G ⁡ K ⁡ x = G ⁡ K ⁡ k
72 71 fveq2d ⊢ x = k → F ⁡ G ⁡ K ⁡ x = F ⁡ G ⁡ K ⁡ k
73 72 fveq2d ⊢ x = k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ x = 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
74 73 breq2d ⊢ x = k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
75 70 74 imbi12d ⊢ x = k → y < x → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
76 69 75 imbi12d ⊢ x = k → ∀ m ∈ W x ≤ m → y < x → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ ∀ m ∈ W k ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
77 76 imbi2d ⊢ x = k → φ ∧ y ∈ ℕ → ∀ m ∈ W x ≤ m → y < x → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ φ ∧ y ∈ ℕ → ∀ m ∈ W k ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
78 breq1 ⊢ x = k + 1 → x ≤ m ↔ k + 1 ≤ m
79 78 ralbidv ⊢ x = k + 1 → ∀ m ∈ W x ≤ m ↔ ∀ m ∈ W k + 1 ≤ m
80 breq2 ⊢ x = k + 1 → y < x ↔ y < k + 1
81 2fveq3 ⊢ x = k + 1 → G ⁡ K ⁡ x = G ⁡ K ⁡ k + 1
82 81 fveq2d ⊢ x = k + 1 → F ⁡ G ⁡ K ⁡ x = F ⁡ G ⁡ K ⁡ k + 1
83 82 fveq2d ⊢ x = k + 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ x = 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
84 83 breq2d ⊢ x = k + 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
85 80 84 imbi12d ⊢ x = k + 1 → y < x → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ y < k + 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
86 79 85 imbi12d ⊢ x = k + 1 → ∀ m ∈ W x ≤ m → y < x → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ ∀ m ∈ W k + 1 ≤ m → y < k + 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
87 86 imbi2d ⊢ x = k + 1 → φ ∧ y ∈ ℕ → ∀ m ∈ W x ≤ m → y < x → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ x ↔ φ ∧ y ∈ ℕ → ∀ m ∈ W k + 1 ≤ m → y < k + 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
88 nnnlt1 ⊢ y ∈ ℕ → ¬ y < 1
89 88 adantl ⊢ φ ∧ y ∈ ℕ → ¬ y < 1
90 89 pm2.21d ⊢ φ ∧ y ∈ ℕ → y < 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ 1
91 90 a1d ⊢ φ ∧ y ∈ ℕ → ∀ m ∈ W 1 ≤ m → y < 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ 1
92 nnre ⊢ k ∈ ℕ → k ∈ ℝ
93 92 adantr ⊢ k ∈ ℕ ∧ m ∈ W → k ∈ ℝ
94 93 lep1d ⊢ k ∈ ℕ ∧ m ∈ W → k ≤ k + 1
95 peano2re ⊢ k ∈ ℝ → k + 1 ∈ ℝ
96 93 95 syl ⊢ k ∈ ℕ ∧ m ∈ W → k + 1 ∈ ℝ
97 16 ssrab3 ⊢ W ⊆ ℕ
98 97 27 sstri ⊢ W ⊆ ℝ
99 98 sseli ⊢ m ∈ W → m ∈ ℝ
100 99 adantl ⊢ k ∈ ℕ ∧ m ∈ W → m ∈ ℝ
101 letr ⊢ k ∈ ℝ ∧ k + 1 ∈ ℝ ∧ m ∈ ℝ → k ≤ k + 1 ∧ k + 1 ≤ m → k ≤ m
102 93 96 100 101 syl3anc ⊢ k ∈ ℕ ∧ m ∈ W → k ≤ k + 1 ∧ k + 1 ≤ m → k ≤ m
103 94 102 mpand ⊢ k ∈ ℕ ∧ m ∈ W → k + 1 ≤ m → k ≤ m
104 103 ralimdva ⊢ k ∈ ℕ → ∀ m ∈ W k + 1 ≤ m → ∀ m ∈ W k ≤ m
105 104 imim1d ⊢ k ∈ ℕ → ∀ m ∈ W k ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → ∀ m ∈ W k + 1 ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
106 105 adantl ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ → ∀ m ∈ W k ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → ∀ m ∈ W k + 1 ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
107 simplr ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y ∈ ℕ
108 simprl ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → k ∈ ℕ
109 nnleltp1 ⊢ y ∈ ℕ ∧ k ∈ ℕ → y ≤ k ↔ y < k + 1
110 107 108 109 syl2anc ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y ≤ k ↔ y < k + 1
111 107 nnred ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y ∈ ℝ
112 108 nnred ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → k ∈ ℝ
113 111 112 leloed ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y ≤ k ↔ y < k ∨ y = k
114 110 113 bitr3d ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y < k + 1 ↔ y < k ∨ y = k
115 simpll ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → φ
116 ltp1 ⊢ k ∈ ℝ → k < k + 1
117 ltnle ⊢ k ∈ ℝ ∧ k + 1 ∈ ℝ → k < k + 1 ↔ ¬ k + 1 ≤ k
118 95 117 mpdan ⊢ k ∈ ℝ → k < k + 1 ↔ ¬ k + 1 ≤ k
119 116 118 mpbid ⊢ k ∈ ℝ → ¬ k + 1 ≤ k
120 112 119 syl ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → ¬ k + 1 ≤ k
121 breq2 ⊢ m = k → k + 1 ≤ m ↔ k + 1 ≤ k
122 121 rspccv ⊢ ∀ m ∈ W k + 1 ≤ m → k ∈ W → k + 1 ≤ k
123 122 ad2antll ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → k ∈ W → k + 1 ≤ k
124 120 123 mtod ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → ¬ k ∈ W
125 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 ovolicc2lem2 ⊢ φ ∧ k ∈ ℕ ∧ ¬ k ∈ W → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ≤ B
126 115 108 124 125 syl12anc ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ≤ B
127 126 iftrued ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → if 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ≤ B 2 nd ⁡ F ⁡ G ⁡ K ⁡ k B = 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
128 2fveq3 ⊢ t = K ⁡ k → F ⁡ G ⁡ t = F ⁡ G ⁡ K ⁡ k
129 128 fveq2d ⊢ t = K ⁡ k → 2 nd ⁡ F ⁡ G ⁡ t = 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
130 129 breq1d ⊢ t = K ⁡ k → 2 nd ⁡ F ⁡ G ⁡ t ≤ B ↔ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ≤ B
131 130 129 ifbieq1d ⊢ t = K ⁡ k → if 2 nd ⁡ F ⁡ G ⁡ t ≤ B 2 nd ⁡ F ⁡ G ⁡ t B = if 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ≤ B 2 nd ⁡ F ⁡ G ⁡ K ⁡ k B
132 fveq2 ⊢ t = K ⁡ k → H ⁡ t = H ⁡ K ⁡ k
133 131 132 eleq12d ⊢ t = K ⁡ k → if 2 nd ⁡ F ⁡ G ⁡ t ≤ B 2 nd ⁡ F ⁡ G ⁡ t B ∈ H ⁡ t ↔ if 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ≤ B 2 nd ⁡ F ⁡ G ⁡ K ⁡ k B ∈ H ⁡ K ⁡ k
134 12 ralrimiva ⊢ φ → ∀ t ∈ T if 2 nd ⁡ F ⁡ G ⁡ t ≤ B 2 nd ⁡ F ⁡ G ⁡ t B ∈ H ⁡ t
135 134 ad2antrr ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → ∀ t ∈ T if 2 nd ⁡ F ⁡ G ⁡ t ≤ B 2 nd ⁡ F ⁡ G ⁡ t B ∈ H ⁡ t
136 37 ad2antrr ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → K : ℕ ⟶ T
137 136 108 ffvelrnd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → K ⁡ k ∈ T
138 133 135 137 rspcdva ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → if 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ≤ B 2 nd ⁡ F ⁡ G ⁡ K ⁡ k B ∈ H ⁡ K ⁡ k
139 127 138 eqeltrrd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ H ⁡ K ⁡ k
140 35 15 36 14 11 algrp1 ⊢ φ ∧ k ∈ ℕ → K ⁡ k + 1 = H ⁡ K ⁡ k
141 140 ad2ant2r ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → K ⁡ k + 1 = H ⁡ K ⁡ k
142 139 141 eleqtrrd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ K ⁡ k + 1
143 136 39 40 sylancl ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → K : ℕ ⟶ U
144 108 peano2nnd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → k + 1 ∈ ℕ
145 143 144 ffvelrnd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → K ⁡ k + 1 ∈ U
146 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢ φ ∧ K ⁡ k + 1 ∈ U → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ K ⁡ k + 1 ↔ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ k + 1 < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∧ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
147 115 145 146 syl2anc ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ K ⁡ k + 1 ↔ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ k + 1 < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∧ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
148 142 147 mpbid ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ k + 1 < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∧ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
149 148 simp3d ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
150 47 adantr ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y ∈ ℝ
151 32 ad2antrr ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → F : ℕ ⟶ ℝ 2
152 8 ad2antrr ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → G : U ⟶ ℕ
153 143 108 ffvelrnd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → K ⁡ k ∈ U
154 152 153 ffvelrnd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → G ⁡ K ⁡ k ∈ ℕ
155 151 154 ffvelrnd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → F ⁡ G ⁡ K ⁡ k ∈ ℝ 2
156 xp2nd ⊢ F ⁡ G ⁡ K ⁡ k ∈ ℝ 2 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ ℝ
157 155 156 syl ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ ℝ
158 152 145 ffvelrnd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → G ⁡ K ⁡ k + 1 ∈ ℕ
159 151 158 ffvelrnd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → F ⁡ G ⁡ K ⁡ k + 1 ∈ ℝ 2
160 xp2nd ⊢ F ⁡ G ⁡ K ⁡ k + 1 ∈ ℝ 2 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1 ∈ ℝ
161 159 160 syl ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1 ∈ ℝ
162 lttr ⊢ 2 nd ⁡ F ⁡ G ⁡ K ⁡ y ∈ ℝ ∧ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∈ ℝ ∧ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1 ∈ ℝ → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∧ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
163 150 157 161 162 syl3anc ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k ∧ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
164 149 163 mpan2d ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
165 164 imim2d ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
166 165 com23 ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y < k → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
167 19 breq1d ⊢ y = k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1 ↔ 2 nd ⁡ F ⁡ G ⁡ K ⁡ k < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
168 149 167 syl5ibrcom ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y = k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
169 168 a1dd ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y = k → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
170 166 169 jaod ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y < k ∨ y = k → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
171 114 170 sylbid ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y < k + 1 → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
172 171 com23 ⊢ φ ∧ y ∈ ℕ ∧ k ∈ ℕ ∧ ∀ m ∈ W k + 1 ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → y < k + 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
173 106 172 animpimp2impd ⊢ k ∈ ℕ → φ ∧ y ∈ ℕ → ∀ m ∈ W k ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k → φ ∧ y ∈ ℕ → ∀ m ∈ W k + 1 ≤ m → y < k + 1 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k + 1
174 67 77 87 77 91 173 nnind ⊢ k ∈ ℕ → φ ∧ y ∈ ℕ → ∀ m ∈ W k ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
175 50 52 57 174 syl3c ⊢ φ ∧ y ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m ∧ k ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → y < k → 2 nd ⁡ F ⁡ G ⁡ K ⁡ y < 2 nd ⁡ F ⁡ G ⁡ K ⁡ k
176 19 22 25 28 48 175 eqord1 ⊢ φ ∧ N ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m ∧ P ∈ n ∈ ℕ | ∀ m ∈ W n ≤ m → N = P ↔ 2 nd ⁡ F ⁡ G ⁡ K ⁡ N = 2 nd ⁡ F ⁡ G ⁡ K ⁡ P